Zulip Chat Archive

Stream: new members

Topic: IVT

adriana (Apr 28 2020 at 17:12):

can anyone help me prove this lemma for the IVT? I'm very new and don't yet understand much.

def continuous2 (f:ℝ → ℝ ) :=
∀ x : ℝ, ∀ ε >0, ∃ δ > 0, ∀ y, abs (x-y) <δ → abs (f x - f y) < ε

lemma continuous_implies {f : ℝ → ℝ} (Hf : continuous2 f)
{a b : ℝ} (Hab : a < b) (K := {x : ℝ | x>a ∧ x<b ∧ f x < 0})
(c:= Sup K):
f c = 0
:=
by_contradiction

Johan Commelin (Apr 28 2020 at 17:17):

Tip, to get syntax highlighting, post your code like this

```
code goes here
```

Johan Commelin (Apr 28 2020 at 17:17):

It seems that you have too many := in the lemma

Johan Commelin (Apr 28 2020 at 17:18):

Or is this some syntax that I do not know???

Patrick Massot (Apr 28 2020 at 17:18):

This is syntactically correct but not what adriana meant

Kevin Buzzard (Apr 28 2020 at 17:19):

K : opt_param (set ℝ) {x : ℝ | x > a ∧ x < b ∧ f x < 0},

Patrick Massot (Apr 28 2020 at 17:19):

Yes, this is declaring a default value for K

Kevin Buzzard (Apr 28 2020 at 17:19):

Yeah, the first thing to do is to get the lemma stated correctly.

Kevin Buzzard (Apr 28 2020 at 17:21):

lemma continuous_implies {f : ℝ → ℝ} (Hf : continuous2 f)
{a b : ℝ} (Hab : a < b) :
let K := {x : ℝ | x>a ∧ x<b ∧ f x < 0} in
let c := Sup K in
f c = 0
:=
begin
  sorry
end

This compiles but it's horrible

Kevin Buzzard (Apr 28 2020 at 17:21):

oh -- and it's also not provable

Patrick Massot (Apr 28 2020 at 17:21):

Also, this lemma seems non-obvious to prove if you are so new to Lean that you can't state it.

Kevin Buzzard (Apr 28 2020 at 17:21):

because f could be the constant function 1

Kevin Buzzard (Apr 28 2020 at 17:22):

Yes this will be very hard to prove if you do not know enough Lean to state the lemma.

Patrick Massot (Apr 28 2020 at 17:22):

Oh, I didn't even read everything

Kevin Buzzard (Apr 28 2020 at 17:22):

that's because we're mathematicians

Kevin Buzzard (Apr 28 2020 at 17:22):

we have inbuilt autocorrect

Patrick Massot (Apr 28 2020 at 17:22):

You missed the assumptions f(a) < 0 and f(b) > 0 presumably

Kevin Buzzard (Apr 28 2020 at 17:23):

not like those CS people always fussing about details

Patrick Massot (Apr 28 2020 at 17:23):

Especially when the topic is called IVT and this is clearly part of a proof we know...

Patrick Massot (Apr 28 2020 at 17:24):

Ok, so

lemma continuous_implies {f : ℝ → ℝ} (Hf : continuous2 f)
{a b : ℝ} (Ha : f a < 0) (Hb : 0 < f b) (Hab : a < b) :
f (Sup {x | a < x ∧ x < b ∧ f x < 0}) = 0 :=
begin
  sorry
end

is more promising

Patrick Massot (Apr 28 2020 at 17:24):

but still probably much too hard for a complete beginner.

Kevin Buzzard (Apr 28 2020 at 17:26):

Using let in the theorem statement makes the goal awful. But it sounds very natural mathematically -- "Let $f:\mathbb{R}\to\mathbb{R}$ be a continuous function, and say $a<b$ and $f(a)<0<f(b).$ If $K=\{x\in(a,b)\,\mid\,f(x)<0\}$ and $c=Sup(K)$ then $f(c)=0$ ." That sounds like a nice maths theorem -- is there a nice way of formalising that in Lean?

Kevin Buzzard (Apr 28 2020 at 17:27):

So Patrick has avoided introducing $K$ and $c$ completely.

Patrick Massot (Apr 28 2020 at 17:27):

This is still very much an internal details of the proof. You could have stated the lemma using exists

Kevin Buzzard (Apr 28 2020 at 17:27):

Right -- but it is what people might write on the blackboard

Kevin Buzzard (Apr 28 2020 at 17:28):

It's like we give away some of our secrets in the theorem statement, rather than just claiming that there exists $c$ with $f(c)=0$ and then packaging away the secret in the proof

Kenny Lau (Apr 28 2020 at 17:28):

now you're thinking like Lean -- in mathematics the existence remembers the data

Patrick Massot (Apr 28 2020 at 17:30):

Kevin, you can still use let in the statement. The proof state will be ok after intro

Patrick Massot (Apr 28 2020 at 17:31):

You can even intros K c, dsimp [K, c] if you want to be exactly proving my goal.

Kevin Buzzard (Apr 28 2020 at 17:34):

Oh I didn't know dsimp would substitute in those let variables

Reid Barton (Apr 28 2020 at 17:34):

You can also literally introduce variables K, c together with equality hypotheses hK, hc, which looks clumsy, but actually works reasonably well.