[isabelle] Rearranging equations before taking limits

[Larry Paulson]

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

Dear Isabelle users,
I'm relatively new to Isabelle and I'm having trouble proving a step in a
1. S(v) ≥ S(v+dv) + (-dv)*P(v+dv)
2. S(v+dv) ≥ S(v) + (dv)*P(v)
3. P(v+dv) ≥ (S(v+dv) - S(v)) / dv ≥ P(v)
Now taking the limit as dv --> 0, we have
4. dS/dv = P(v)
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>

[Aadish Kumar]

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.

On Wed, Mar 4, 2015 at 8:09 PM, Larry Paulson <***@cam.ac.uk <mailto:***@cam.ac.uk>> wrote:
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

Dear Isabelle users,
I'm relatively new to Isabelle and I'm having trouble proving a step in a
1. S(v) ≥ S(v+dv) + (-dv)*P(v+dv)
2. S(v+dv) ≥ S(v) + (dv)*P(v)
3. P(v+dv) ≥ (S(v+dv) - S(v)) / dv ≥ P(v)
Now taking the limit as dv --> 0, we have
4. dS/dv = P(v)
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>

[Johannes Hölzl]

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!

- Johannes

Post by Aadish Kumar
Sorry, I've fixed in my most recent work, and made some progress.
"∀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)"
definition win_prob :: "nat => real => real"
where "win_prob i v = v"
definition util :: "nat => real => real"
where "util i v = v"
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.
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

Dear Isabelle users,
I'm relatively new to Isabelle and I'm having trouble proving a step in a
1. S(v) ≥ S(v+dv) + (-dv)*P(v+dv)
2. S(v+dv) ≥ S(v) + (dv)*P(v)
3. P(v+dv) ≥ (S(v+dv) - S(v)) / dv ≥ P(v)
Now taking the limit as dv --> 0, we have
4. dS/dv = P(v)
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>

[Christian Sternagel]

*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.

Dear Christian Sternagel,
I am currently a student at the University of Birmingham and I'm working
on a project in Isabelle. I was hoping you could help me as I am the
only undergraduate student working with Isabelle and the support is very
limited.
You'll see that in the attached .thy file, I have lm1, which proves a
result "∀w. ∀h." however if I change it to "∀w∈V. ∀h." as in lm2, I am
struggling to prove the same result. Could you guide me on how I could
solve this problem? Do you think there is an assumption missing?
I would very much appreciate your help.
Thank you very much.
Regards,
Aadish Kumar

[Aadish Kumar]

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

[Larry Paulson]

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

Post by Aadish Kumar
if I use an interval S, rather than UNIV, sledgehammer yields so
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?

[Aadish Kumar]

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

Post by Aadish Kumar
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

Post by Aadish Kumar
if I use an interval S, rather than UNIV, sledgehammer yields so
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

Post by Aadish Kumar
would I be able to prove the second lemma? Is there some extra which I am
missing?

[Aadish Kumar]

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

[Aadish Kumar]

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

[Wenda Li]

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

Post by Aadish Kumar
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.
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

[Aadish Kumar]

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

Post by Wenda Li
Dear Aadish,
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

Post by Aadish Kumar
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.
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

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

[Wenda Li]

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)
- g w" . (* here is
how we utilise the assumption*)
thus "h * f w ≤ g (w + h) - g w" by simp
qed

"∀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

Post by Aadish Kumar
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

Post by Wenda Li
Dear Aadish,
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

Post by Aadish Kumar
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.
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

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

[Aadish Kumar]

Dear Wenda,
Thank you for the insightful code and explanation, I understand now.

Much appreciated,
Aadish

Post by Wenda Li
Hi Aadish,
The problem is not about the assumptions. It is about how we can utilise
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) -
g w" . (* here is
how we utilise the assumption*)
thus "h * f w ≤ g (w + h) - g w" by simp
qed
"∀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

Post by Aadish Kumar
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
Dear Aadish,

Post by Aadish Kumar
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
Dear List,

Post by Aadish Kumar
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.
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

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge