Zulip Chat Archive

Stream: maths

Topic: help proving IVT


view this post on Zulip adriana (Apr 01 2020 at 02:55):

hello, I am just getting started using lean and was wondering if anyone could help me out

I am trying to prove the IVT using the basic functions in lean. Right now, I have the following:

theorem intermediate_value {f : ℝ → ℝ} (Hf : continuous f)
{a b : ℝ} (Hab : a < b)
(Hav : f a < 0) (Hbv : f b > 0) :
∃ c, a < c ∧ c < b ∧ f c = 0 :=
begin
let K := {x | a<b ∧ x>a ∧ x<b ∧ f x <= 0},
let c := is_lub K,
--here I would like to use the definition of least upper bound, image of c, and continuity to say that f(c) is within epsilon of 0 but I'm not sure how to use the syntax of lean
end

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 03:01):

is_lub is a predicate; you probably want let c := Sup K.

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 03:03):

BTW, no need to include a < b in the definition of K. You already have it in Hab.

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 03:06):

If you use non-strict inequalities everywhere, then you'll be able to say that K is closed, hence it contains its Sup (see cSup_mem_of_is_closed).

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 03:06):

And you'll need to show that f x < 0 is impossible.

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 03:09):

Or you can do something like (not tested)

rcases lt_trichotomy 0 (f c) with Hc | Hc | Hc,

In two cases you'll get to a contradiction, and in the middle case you'll need to show a < c and c < b.

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 03:10):

It makes sense to prove a ≤ c and c ≤ b before doing rcases.

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 03:10):

Use cSup_le and le_cSup lemmas.

view this post on Zulip adriana (Apr 01 2020 at 03:28):

which import statement do I need in order to use Sup?

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 03:35):

What is your mathlib version? It older versions it is in lattice namespace (was changed a few weeks ago).

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 03:37):

It is defined in order/complete_lattice; lemmas that work for reals are in order/conditionally_complete_lattice, and the latter file is imported by data/real/basic.

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 03:37):

So, if you have real numbers, then you probably have Sup and most of its properties.

view this post on Zulip adriana (Apr 01 2020 at 04:02):

thanks, I had the old version!


Last updated: May 11 2021 at 16:22 UTC