Email Gateway (Aug 19 2022 at 17:19): Email Gateway (Aug 19 2022 at 17:19):From: Aadish Kumar <aadish.k@gmail.com>
Thank you Larry.
I had hoped that this would provide the insight to the following problem:
lemma
fixes f g :: "real ⇒ real"
assumes
"open S"
"∀w∈S. ∀h. (w+h)∈S --> h * (f w) ≤ g (w+h) - g w"
"∀w∈S. ∀h. (w+h)∈S --> g (w+h) - g w ≤ h * f (w+h)"
shows "∀w∈S. eventually (λh. f w ≤ (g (w + h) - g w)/h) (at 0)"
using assms unfolding eventually_at
apply (simp add: divide_simps mult_ac)
where I have two conditions to prove. However letting "S=UNIV", I am left
with only one condition to prove. Initially, I thought that defining S as
open would help but not in this case. Do you have any suggestions?
I appreciate the help.
Regards,
Aadish
Email Gateway (Aug 19 2022 at 17:21):From: Aadish Kumar <aadish.k@gmail.com>
Dear List,
With some help I was able to make some progress on the problem. When h ≥ 0
or h ≤ 0, (g (w + h) - g w)/h) is bounded by the same variables, therefore
taking the limits as h approaches 0 should yield the same result in both
cases. How can I combine both results to show that the result is true for
any h? Any help would be appreciated.
lemma fixes f g :: "real ⇒ real"
assumes "open S"
"∀a b. a < b <-> f a < f b"
"∀a. f a > 0"
"S={a..b}"
"continuous_on S f"
"∀w∈S. (λh. f (w+h)) -- 0 --> f w"
"∀w∈S. (λh. f w) -- 0 --> f w"
"∀w∈S. eventually (λh. (h ≥ 0 --> f (w+h) ≥ (g (w + h) - g w)/h) ∧ (h ≥ 0
--> f w ≤ (g (w + h) - g w)/h)) (at 0)"
"∀w∈S. eventually (λh. (h ≤ 0 --> f (w+h) ≤ (g (w + h) - g w)/h) ∧ (h ≤ 0
--> f w ≥ (g (w + h) - g w)/h)) (at 0)"
shows "∀w∈S. ((λh. (g (w+h) - g w)/h) ---> f w) (at 0)"
Regards,
Aadish
Email Gateway (Aug 19 2022 at 17:26):From: Aadish Kumar <aadish.k@gmail.com>
Dear List,
I'm having trouble with a particular problem in Isabelle which I believe it
due to my lack of knowledge regarding Isabelle notation.
I want to prove
lemma fixes f g :: "real ⇒ real"
assumes "∀w∈S. ∀h. (w+h)∈S --> h * (f w) ≤ g (w+h) - g w" "continuous_on S
g" "continuous_on S f"
shows "∀w∈S. eventually (λh. f w ≤ (g (w + h) - g w)/h) (at_right 0)"
which is simply true because we are just dividing by h, and (w+h)∈S.
I can solve this if I assume the set S is open:
lemma fixes f g :: "real ⇒ real"
assumes "∀w∈S. ∀h. (w+h)∈S --> h * (f w) ≤ g (w+h) - g w" "open S"
"continuous_on UNIV g" "continuous_on UNIV f"
shows "∀w∈S. eventually (λh. f w ≤ (g (w + h) - g w)/h) (at_right 0)"
unfolding eventually_at at_right_eq
using assms always_eventually open_real_def
apply (simp add: divide_simps mult_ac)
by (metis add.commute diff_0_right diff_add_cancel diff_diff_eq2 dist_norm
real_norm_def)
However mathematically, since (w+h)∈S, and open S is not needed. Is there a
way I can include that (w+h)∈S in the my "shows" statement, so I can prove
the result without assuming an open S?
Regards,
Aadish
Email Gateway (Aug 19 2022 at 17:26):From: Wenda Li <wl302@cam.ac.uk>
Dear Aadish,
I suspect "open S" should be a necessary condition in your case:
lemma
fixes f g :: "real ⇒ real"
assumes "∀w∈S. ∀h. (w+h)∈S --> h * (f w) ≤ g (w+h) - g w"
shows "∀w∈S. eventually (λh. f w ≤ (g (w + h) - g w)/h) (at_right 0)"
unfolding eventually_at
proof
fix w assume "w∈S"
obtain d::real where "d>0" (* need more *) by (metis zero_less_one)
thus "∃d>0. ∀h∈{0<..}. h ≠ 0 ∧ dist h 0 < d ⟶ f w ≤ (g (w + h) - g w)
/ h"
proof (rule_tac x=d in exI,auto simp add:dist_norm)
fix h assume "0 < h" "h < d"
have "w+h∈S" sorry (* without "open S" we cannot obtain a suitable
"d" to show this*)
hence "h * (f w) ≤ g (w+h) - g w" using assms w∈S by auto
thus "f w ≤ (g (w + h) - g w) / h" using h>0 by (simp
add:field_simps)
qed
qed
In order to utilise the assumption (i.e. to have "h * (f w) ≤ g (w+h) -
g w" ), we have to show "w+h∈S", which should be impossible without
assuming "open S".
Cheers,
Wenda
Email Gateway (Aug 19 2022 at 17:26):From: Aadish Kumar <aadish.k@gmail.com>
Thanks for your reply Wenda,
I initially have the condition "∀w∈S. ∀v∈S. g v - g w ≥ (v-w)*(f w)" and
I'm just substituting v=w+h, therefore it is true that (w+h)∈S.
lemma fixes f g :: "real ⇒ real"
assumes "∀w∈S. ∀v∈S. g v - g w ≥ (v-w)*(f w)"
shows "∀w∈S. ∀h. w + h ∈ S ⟶ h * f w ≤ g (w + h) - g w" using assms by
fastforce
Would this make a difference? Will I be able to utilise this in any way?
Regards,
Aadish
Email Gateway (Aug 19 2022 at 17:26):From: Wenda Li <wl302@cam.ac.uk>
Hi Aadish,
The problem is not about the assumptions. It is about how we can utilise
the assumption when proving conclusions:
lemma
fixes f g :: "real ⇒ real"
assumes "∀w∈S. ∀v∈S. g v - g w ≥ (v-w)*(f w)"
shows "∀w∈S. ∀h. w + h ∈ S ⟶ h * f w ≤ g (w + h) - g w"
proof clarify
fix w h assume "w ∈ S" "w + h ∈ S"
note assms[rule_format, OF this] hence "(w + h - w) * f w ≤ g (w + h)
"∀w∈S. ∀v∈S. g v - g w ≥ (v-w)*(f w)" is actually equivalent to "?w ∈ S
==> ?v ∈ S ==> (?v - ?w) * f ?w ≤ g ?v - g ?w" and the conclusion "∀w∈S.
∀h. w + h ∈ S ⟶ h * f w ≤ g (w + h) - g w" can be transformed to "⋀w h.
w ∈ S ==> w + h ∈ S ==> h * f w ≤ g (w + h) - g w", which can be then
proved by fixing w h, assuming "w ∈ S" "w + h ∈ S" and showing "h * f w
≤ g (w + h) - g w". With "w ∈ S" and "w + h ∈ S", we can satisfy the
preconditions of the assumption (i.e. "?w ∈ S" and "?v ∈ S"), and have
"(w + h - w) * f w ≤ g (w + h) - g w" (i.e. utilising the assumption).
However, if the conclusion is like "∀w∈S. eventually (λh. f w ≤ (g (w +
h) - g w)/h) (at_right 0)" which is equivalent to " ∀x. x ∈ S --> (∃d>0.
∀h>0. h < d --> f x ≤ (g (x + h) - g x) / h)", we have to pick a "d"
such that "d>0" and "!h. h>0 --> h<d --> w+h∈S" in order to utilise the
assumption.
Overall, the difference between "∀w∈S. ∀v∈S. g v - g w ≥ (v-w)*(f w)"
and "∀w∈S. ∀h. (w+h)∈S --> h * (f w) ≤ g (w+h) - g w" is little, though
I haven't checked if they are actually equivalent propositions, but the
difference between "∀w∈S. ∀h. w + h ∈ S ⟶ h * f w ≤ g (w + h) - g w" and
"∀w∈S. eventually (λh. f w ≤ (g (w + h) - g w)/h) (at_right 0)" is huge.
Cheers,
Wenda
Email Gateway (Aug 19 2022 at 17:26):From: Aadish Kumar <aadish.k@gmail.com>
Dear Wenda,
Thank you for the insightful code and explanation, I understand now.
Much appreciated,
Aadish
Email Gateway (Aug 22 2022 at 09:01):From: Aadish Kumar <aadish.k@gmail.com>
Dear Isabelle users,
I'm relatively new to Isabelle and I'm having trouble proving a step in a
published proof. The proof starts with the following two inequalities:
Rearranging forms the follow inequality:
Now taking the limit as dv --> 0, we have
using the sandwich theorem and limit definition of derivative.
I can prove this if I explicity assume that dv > 0 or dv < 0. The proof
when dv > 0 is attached. If dv < 0, the inequalities just change sign when
dividing, and after taking the limit, we reach the same result. However, I
understand that when you take a limit, you just look at the behavior of the
expression as it approaches the limiting value. The actual value of the
expression at the limiting value is irrelevant for a limit.
When I attempt to prove this in Isabelle, I have to assume that dv ≠ 0
before I can divide by it, even though I intend to take limits. My question
is how I can prove the final result without having to assume this?
Regards,
Aadish
problem1.thy
Email Gateway (Aug 22 2022 at 09:02):From: Larry Paulson <lp15@cam.ac.uk>
I’m afraid you haven’t formulated your problem correctly:
lemma lm1:
assumes "∀h w. h * win_prob w ≤ util (w+h) - util w"
"∀h w. util (w+h) - util w ≤ h*win_prob (w+h)"
and "∀h. (h::real) > 0"
shows "∀w. (λh. (util (w+h) - util w)/h) -- 0 --> win_prob w"
You are assuming ∀h. (h::real) > 0, which is false of course, because 0 is a real number.
Larry Paulson
Email Gateway (Aug 22 2022 at 09:02):From: Aadish Kumar <aadish.k@gmail.com>
Sorry, I've fixed in my most recent work, and made some progress.
You'll see that I want to show: "∀w. (λh. (util (w+h) - util w)/h) -- 0 --> win_prob w" from the assumptions:
"∀h w. h * win_prob i w ≤ util i (w+h) - util i w"
"∀h w. util i (w+h) - util i w ≤ h*win_prob i (w+h)"
"continuous_on UNIV (win_prob i)"
"continuous_on UNIV (util i)"
If I change the definitions of the functions to:
definition win_prob :: "nat => real => real"
where "win_prob i v = v"
definition util :: "nat => real => real"
where "util i v = v"
I am able to find a solution by using sledgehammer. However if I have the functions in the form:
definition win_prob :: "nat => real => real"
where "win_prob i = real"
definition util :: "nat => real => real"
where "util i = (win_prob i v)*v"
I don't get any suggestions. I've added the continuous_on assumption, however I've still been unable to prove this.
Email Gateway (Aug 22 2022 at 09:02):From: Johannes Hölzl <hoelzl@in.tum.de>
Well the proof is more complicated as it seams to be:
notepad
begin
fix util win_prob :: "real ⇒ real"
assume *:
"∀h w. h * win_prob w ≤ util (w+h) - util w"
"∀h w. util (w+h) - util w ≤ h * win_prob (w+h)"
"continuous_on UNIV win_prob"
"continuous_on UNIV util"
have "∀w. (λh. (util (w+h) - util w)/h) -- 0 --> win_prob w"
proof (rule allI tendsto_sandwich)+
fix w
show "eventually (λh. win_prob w ≤ (util (w + h) - util w) / h) (at
0)"
using *(1) unfolding eventually_at
apply (auto simp: divide_simps mult_ac)
Now we when h is positive everything is fine, divide_simps will rewrite
_ <= _ / h to _ * h <= _
but what happens when h is negative? Then your rules *(1,2) do not fit
anymore!
Email Gateway (Aug 22 2022 at 09:03):From: Aadish Kumar <aadish.k@gmail.com>
Thank you Johannes, that's given me some insight. I'm following a paper
proof where all the assumptions are not clearly explicit so it can be
confusing at times. After testing out a few functions and values, I can
also see that the inequalities don't hold in certain cases. However, if
win_prob is defined as a strictly increasing function, and always positive
then assms(1) and (2) should hold, even if h is negative. I've added these
assumptions however I'm still struggling to find a proof.
I've changed the definition of util to: "real=>real" where "util v =
v*(win_prob v) - c(v)
cost(v) is defined as "real => real" where "cost = real"
h being negative will not effect the result once the win_prob is defined as
strictly increasing and positive. Dividing by h will reverse the
inequalities but after taking limits the result will be the same. However
I'm still struggling to proceed with the proof.
I appreciate your help.
Regards,
Aadish
revan3.thy
Email Gateway (Aug 22 2022 at 09:05):From: Christian Sternagel <c.sternagel@gmail.com>
bounced back to isabelle-users
Dear Kumar,
as far as I can tell, your question is directly related to your earlier
question on the isabelle-users mailing list (which I'm subscribed to, as
a cursory glance at the archives would reveal):
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-March/msg00059.html
If I had something to say about this topic, I would do so through
isabelle-users.
After asking something on a public mailing list, sending private emails
(without reference to the corresponding mail thread on the mailing list)
around is only multiplying the effort for others (since several people
might work on answering your question in parallel without even knowing
it) and should be frowned upon.
Please try to be patient and wait for answers on the mailing list or try
http://stackoverflow.com/questions/tagged/isabelle
in the meanwhile. But if you do, also say so on isabelle-users since you
asked your question there first.
cheers
chris
PS: I've never even used "Deriv" myself and hence might not be the right
person to answer your question.
Email Gateway (Aug 22 2022 at 09:05):From: Aadish Kumar <aadish.k@gmail.com>
In regards to my earlier question, I have made some progress in proving the
lemma using the approach that Johannes Hölzl recommended. I have a further
question on the same issue. You'll see that I am able to prove
"∀w. (λh. (util i (w+h) - util i w)/h) -- 0 --> win_prob i w" using the
assumptions "∀w. ∀h. h * (win_prob i w) ≤ util i (w+h) - util i w"
"∀w. ∀h. util i (w+h) - util i w ≤ h * win_prob i (w+h)"
"∀a b. (win_prob i a) < (win_prob i b) <--> a < b"
"∀a. (win_prob i a)∈{0..1}
"continuous_on UNIV (win_prob i)"
however, if I change the assumptions and goal to:
shows:
"V={a..b}"
"∀w∈V. ∀h. h * (win_prob i w) ≤ util i (w+h) - util i w"
"∀w∈V. ∀h. util i (w+h) - util i w ≤ h * win_prob i (w+h)"
"∀a∈V. ∀b∈V. (win_prob i a) < (win_prob i b) ⟷ a < b"
"∀a∈V. (win_prob i a)∈{0..1}"
"continuous_on V (win_prob i)"
shows "∀w∈V. (λh. (util i (w+h) - util i w)/h) -- 0 --> win_prob i w"
The same method does not go through. All I have changed is that now it
states∀w∈V rather than ∀w. Can anyone provide further support?
I would greatly appreciate it.
Regards,
Aadish Kumar
revan3.thy
Email Gateway (Aug 22 2022 at 09:07):From: Aadish Kumar <aadish.k@gmail.com>
In regards to my previous reply, I've been working on isolating the problem
and I think it all comes down to the following case.
I can prove:
lemma fixes f :: "real ⇒ real"
assumes "continuous_on UNIV f"
shows "∀x. (λh. f (x+h)) -- 0 --> f x"
using assms win_prob_def
by (metis LIM_offset_zero_iff UNIV_I continuous_on_def)
however if I use an interval S, rather than UNIV, sledgehammer yields so
suggestions. Specifically:
lemma fixes f :: "real ⇒ real"
assumes "continuous_on S f"
shows "∀x∈S. (λh. f (x+h)) -- 0 --> f x"
Even adding assumptions such as "S≠{}" and "S⊂UNIV" make no difference. How
would I be able to prove the second lemma? Is there some extra which I am
missing?
I would really appreciate any help or guidance.
Regards,
Aadish
Email Gateway (Aug 22 2022 at 09:07):From: Larry Paulson <lp15@cam.ac.uk>
S needs to be an open set:
lemma fixes f :: "real ⇒ real"
assumes "continuous_on S f" "open S"
shows "∀x∈S. (λh. f (x+h)) -- 0 --> f x"
using assms
by (metis Lim_at_zero at_within_open continuous_on)
Larry Paulson
Last updated: Apr 19 2024 at 20:15 UTC