Zulip Chat Archive

Stream: kbb

Topic: sine and cosine and pi


view this post on Zulip Chris Hughes (Sep 15 2018 at 11:34):

I've started working on sine and cosine. I have cleaned the proofs up until exp (x + y) and I'm currently working on things like sin (x + y). I have no idea how to define pi however. @Mario Carneiro what's the best way to do this?

view this post on Zulip Patrick Massot (Sep 15 2018 at 11:56):

Do you have complex exp or only real?

view this post on Zulip Chris Hughes (Sep 15 2018 at 12:15):

complex. I'll define real.exp in terms of complex.exp

view this post on Zulip Patrick Massot (Sep 15 2018 at 13:06):

Ok, so sin (x + y) and friends follow immediately from exp(x+y).

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:06):

You're such a mathematician.

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:07):

Remember that you get a /2 in those expressions. You need to convince Lean that you aren't dividing by zero.

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:08):

But Chris is pushing progress to the exp branch on community mathlib

view this post on Zulip Patrick Massot (Sep 15 2018 at 13:08):

For pi you can prove that cos vanishes somewhere between 0 and 2 using the intermediate value theorem, and define pi as twice the first zero of cos. This is cheap but I guess proving other properties from that is painful. A better solution is probably to prove the classification of subgroups of (R, +), and define 2pi as the positive generator of ker(t mapsto exp(i*t)) (this kernel cannot be dense because exp is continuous and non-constant)

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:09):

Rights, so we need continuity of exp.

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:09):

For either definition.

view this post on Zulip Patrick Massot (Sep 15 2018 at 13:09):

I both cases yes

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:10):

What is the best way to do this continuity proof?

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:10):

Generalise to arbitrary power series?

view this post on Zulip Patrick Massot (Sep 15 2018 at 13:10):

We could also cheat and define pi using a random series, but then the link with exp and cos would be harder to establish

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:11):

I like your second definition.

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:11):

We should probably just check what Coq/Mizar/Isabelle do

view this post on Zulip Reid Barton (Sep 15 2018 at 13:11):

If you have ex+y=exeye^{x+y} = e^x e^y then it suffices to show that exe^x is continuous at 0, and for this you can use a crude bound on the power series.

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:13):

Ok, sounds good.

view this post on Zulip Reid Barton (Sep 15 2018 at 13:14):

Patrick, you still have to prove that eit=1e^{it} = 1 for some nonzero real tt first, right?

view this post on Zulip Patrick Massot (Sep 15 2018 at 13:16):

indeed we must exclude that the kernel is trivial

view this post on Zulip Reid Barton (Sep 15 2018 at 13:22):

Does the definition of pi really rely on some explicit estimate like cos2<0\cos 2 < 0?
I guess if you have differential calculus at your disposal, you could show that sint\sin t is bounded, and then conclude that cost\cos t cannot be positive everywhere... wait no, I don't even see how to make this work.

view this post on Zulip Patrick Massot (Sep 15 2018 at 13:23):

https://isabelle.in.tum.de/dist/library/HOL/HOL/Transcendental.html seems to use my first method

view this post on Zulip Reid Barton (Sep 15 2018 at 13:25):

Okay--if cost\cos t was positive everywhere then sint\sin t would be increasing, and then cost\cos t would have to lie below some line of negative slope, a contradiction.
Not sure if one can extract an "elementary" (no differential calculus) proof along these lines.

view this post on Zulip Patrick Massot (Sep 15 2018 at 13:29):

This all looks super tedious

view this post on Zulip Patrick Massot (Sep 15 2018 at 13:29):

Let's do perfectoid spaces

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:40):

Hmmm, @Reid Barton I can easily follow your maths proof that exp is continuous if it is ctu at 0.

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:40):

But how do I put this into Lean?

view this post on Zulip Patrick Massot (Sep 15 2018 at 13:43):

https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/topological_structures.lean#L289 may help

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:46):

Aah thanks, that indeed looks useful.

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:47):

Do we know that (exp x) \ne 0?

view this post on Zulip Patrick Massot (Sep 15 2018 at 13:47):

It's not yet merged in mathlib, but doesn't depend on much

view this post on Zulip Johan Commelin (Sep 15 2018 at 13:47):

Because then we know that exp is a group hom, which might also help.

view this post on Zulip Chris Hughes (Sep 15 2018 at 13:49):

We do know exp \ne 0

view this post on Zulip Johan Commelin (Sep 15 2018 at 14:07):

Hmmm, I'm horrible with these continuity proofs...

view this post on Zulip Johan Commelin (Sep 15 2018 at 14:07):

So there is squeeze_zero, but I don't think there is a generic squeeze lemma, right?

view this post on Zulip Patrick Massot (Sep 15 2018 at 14:07):

there is

view this post on Zulip Johan Commelin (Sep 15 2018 at 14:07):

Ooh, my VScode didn't find it.

view this post on Zulip Johan Commelin (Sep 15 2018 at 14:08):

Let me try again

view this post on Zulip Johan Commelin (Sep 15 2018 at 14:08):

Aah, it only has squeeze in its docstring

view this post on Zulip Johannes Hölzl (Sep 15 2018 at 14:08):

grep for sandwich in mathlib

view this post on Zulip Patrick Massot (Sep 15 2018 at 14:08):

https://github.com/leanprover/mathlib/blob/5613d2ecc92ce8fae9555745bd94756dec61a323/analysis/topology/topological_structures.lean#L438

view this post on Zulip Patrick Massot (Sep 15 2018 at 14:09):

grep for squeeze also works

view this post on Zulip Patrick Massot (Sep 15 2018 at 14:09):

but grep for gendarme doesn't work

view this post on Zulip Johan Commelin (Sep 15 2018 at 14:14):

Hmm snap, of course that doesn't help for continuity of the complex version.

view this post on Zulip Patrick Massot (Sep 15 2018 at 14:16):

Anyway, the long term reasoning is clear: we don't want a trick, we want general results on power series

view this post on Zulip Johan Commelin (Sep 15 2018 at 14:18):

Right. And I think I'dd rather work on the long term

view this post on Zulip Johan Commelin (Sep 15 2018 at 14:18):

So, should we create power_series.lean on cocalc?

view this post on Zulip Johan Commelin (Sep 15 2018 at 14:19):

Maybe Kevin will see it. I think I don't care

view this post on Zulip Johan Commelin (Sep 15 2018 at 14:21):

Is that ok with others? Then we could multiplayer power series into existence.

view this post on Zulip Johan Commelin (Sep 15 2018 at 14:21):

I'm quite addicted to that experience.

view this post on Zulip Patrick Massot (Sep 15 2018 at 14:22):

I would wait until @Johannes Hölzl tells us about how this is done in Isabelle (they have a lot of analysis there)

view this post on Zulip Johannes Hölzl (Sep 15 2018 at 14:35):

I will take a look

view this post on Zulip Johannes Hölzl (Sep 15 2018 at 14:48):

So, continuity of exp is proved using derivability. There is a section "Term-by-Term Differentiability of Power Series" in http://isabelle.in.tum.de/dist/library/HOL/HOL/Transcendental.html where most of it is proved. The central part is termdiffs which states: DERIV (λx. ∑n. c n * x^n) x :> (∑n. (diffs c) n * x^n). Where diffs c := (λn. of_nat (Suc n) * c (Suc n)) (Suc is nat.succ and of_nat is the coercion nat to a real_algebra).

view this post on Zulip Johannes Hölzl (Sep 15 2018 at 14:50):

The lemma termdiffs assumes that various power series converge.

view this post on Zulip Johan Commelin (Sep 15 2018 at 14:53):

So it would make sense to define power series, and then we need to change the definition of exp to use those power series.

view this post on Zulip Johan Commelin (Sep 15 2018 at 14:53):

Is that right?

view this post on Zulip Johan Commelin (Sep 15 2018 at 14:53):

I mean, there won't change that much

view this post on Zulip Johannes Hölzl (Sep 15 2018 at 14:57):

Yes, I think it would make sense to define power series. Also derivatives...

view this post on Zulip Johan Commelin (Sep 15 2018 at 14:58):

Ok, and this is purely algebraic stuff, right?

view this post on Zulip Johan Commelin (Sep 15 2018 at 14:58):

Or do you also mean the analytic derivative?

view this post on Zulip Johannes Hölzl (Sep 15 2018 at 14:59):

I guess we need to analytic derivative to prove continuity

view this post on Zulip Johan Commelin (Sep 15 2018 at 15:00):

Hmmm, ok

view this post on Zulip Johan Commelin (Sep 15 2018 at 15:00):

And we really need all of this to define pi?

view this post on Zulip Johan Commelin (Sep 15 2018 at 15:01):

Well, we will need this stuff anyway

view this post on Zulip Johan Commelin (Sep 15 2018 at 15:03):

I'm going to create a power_series.lean on CoCalc

view this post on Zulip Johannes Hölzl (Sep 15 2018 at 15:05):

In Isabelle:
pi = 2 * (THE x. 0 ≤ x ∧ x ≤ 2 ∧ cos x = 0)
and then even more algebric facts about cos and sin

view this post on Zulip Johan Commelin (Sep 15 2018 at 15:06):

Right, but I guess there is a hidden proof that such x exists, not?

view this post on Zulip Johannes Hölzl (Sep 15 2018 at 15:06):

of course

view this post on Zulip Johannes Hölzl (Sep 15 2018 at 15:06):

cos_is_zero: "∃!x::real. 0 ≤ x ∧ x ≤ 2 ∧ cos x = 0"

view this post on Zulip Johannes Hölzl (Sep 15 2018 at 15:07):

it uses IVT

view this post on Zulip Johan Commelin (Sep 15 2018 at 15:07):

Right, so we need continuity

view this post on Zulip Johannes Hölzl (Sep 15 2018 at 15:08):

it also uses derivative of cos and that sin 2 > 0

view this post on Zulip Johan Commelin (Sep 15 2018 at 15:09):

Ok

view this post on Zulip Chris Hughes (Sep 15 2018 at 18:19):

I just pushed a load of stuff to the exp branch of community mathlib. It's about as far as I can go without continuity of exp and I'm not sure what the best approach for that is.

view this post on Zulip Mario Carneiro (Sep 15 2018 at 19:17):

@Chris Hughes In metamath we used a very low brow approach to exp (it comes before analysis), which I think worked quite well.

  • I assume you already have things like the addition formula and other algebraic stuff on sin and cos.
  • exp is continuous iff it is continuous at each point. By facts about multiplying functions continuous at a point, you can show that it suffices to prove exp is continuous at zero.
  • 1 + x <= exp x for positive x by taking away the rest of the summands; exp x <= 1/(1-x) by comparing the infinite series of these two. Thus exp is continuous and even differentiable at zero by the sandwich lemma.
  • It follows from basic topological ring action that sin is continuous.
  • pi is the infimum of the positive zeros of the sin function. We need to show this is well defined and a zero of the sin function.
  • Suppose a is a zero of sin in the range (2,4), and b is a positive zero of sin. Show that if pi < a then (pi + a) / 2 <= b, because 2*a - b is also a zero of sin.
  • By the intermediate value theorem applied to sin, and sin 2 > 0 and sin 4 < 0, there is a zero a in this range, and pi exists. if pi < a, then (pi + a) / 2 <= pi by the above lemma, since pi is the infimum of all positive roots of sin. Thus a <= pi and thus pi is the unique zero of sin in this range.

view this post on Zulip Chris Hughes (Sep 15 2018 at 19:27):

Can you point me to the sandwich lemma, and the facts about multiplying functions continuous at points? I've never touched anything in the analysis folder before now.

view this post on Zulip Mario Carneiro (Sep 15 2018 at 19:28):

For the bounds:

  • sin 4 = 2 * sin 2 * cos 2 is negative because sin 2 is positive and cos 2 is negative
  • -7/9 < cos 2 < -1/9 because cos 2 = 2 * (cos 1)^2 - 1 and 1/3 < cos 1 < 2/3
  • sin (2*x) is positive for all 0<x<=1 because sin x and cos x are
  • x - x^3/3 < sin x < x and 1 - 2/3 * x^2 < cos x < 1 - x^2/3 on (0, 1] by infinite series bounds

view this post on Zulip Mario Carneiro (Sep 15 2018 at 19:30):

I'm not sure we have it, but it should be easy to show over the reals (or whatever generalization best encompasses the reals)

view this post on Zulip Mario Carneiro (Sep 15 2018 at 19:33):

By the way, metamath used to have a direct proof before analysis was developed, but now continuity of exp follows from differentiability, and continuity uses various topological notions and proofs. I think the definition of exp can be in data.{real,complex}.basic, but pi and other facts that depend on continuity should go in the topological part, at analysis.{real,complex}

view this post on Zulip Chris Hughes (Sep 15 2018 at 19:39):

Where are the relevant theorems in the lean library? Do we have IVT?

view this post on Zulip Mario Carneiro (Sep 15 2018 at 19:42):

I don't think we do. I would want to just prove it over the reals for now

view this post on Zulip Chris Hughes (Sep 15 2018 at 19:49):

How do I state continuous at a point?

view this post on Zulip Mario Carneiro (Sep 15 2018 at 19:52):

In topology, f : X -> Y is continuous at x if tendsto f (nhds x) (nhds (f x))

view this post on Zulip Chris Hughes (Sep 15 2018 at 19:57):

And what are the lemmas that let me prove that it's continuous everywhere if it's continuous at 0?

view this post on Zulip Chris Hughes (Sep 15 2018 at 19:59):

I'm not even sure why that's true.

view this post on Zulip Patrick Massot (Sep 15 2018 at 20:02):

I think I already answered that earlier today

view this post on Zulip Chris Hughes (Sep 15 2018 at 20:02):

I think I've worked out vaguely why it's true in maths, but not in lean.

view this post on Zulip Patrick Massot (Sep 15 2018 at 20:02):

https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/topological_structures.lean#L289

view this post on Zulip Patrick Massot (Sep 15 2018 at 20:04):

Importing that and apply it to reals prove that tendsto f (nhds x) (nhds (f x)) iff tendsto (lambda h, f (x+h)) (nhds 0) (nhds (f x))

view this post on Zulip Mario Carneiro (Sep 15 2018 at 20:04):

this is a consequence of (\lam x, x + h) being a homeo

view this post on Zulip Patrick Massot (Sep 15 2018 at 20:04):

In case of exp you can rewrite f (x+h) as exp(x)*exp(h), use exp(x) converges (it's constant) and the result at zero

view this post on Zulip Chris Hughes (Sep 15 2018 at 20:06):

Is this the correct statement of exp is continuous at x = 0

lemma continuous_exp : tendsto exp (nhds 0) (nhds 1)

view this post on Zulip Mario Carneiro (Sep 15 2018 at 20:06):

yes, hopefully you know exp 0 = 1 already by algebraic stuff

view this post on Zulip Patrick Massot (Sep 15 2018 at 20:06):

The name is bad, but the statement is ok

view this post on Zulip Patrick Massot (Sep 15 2018 at 20:07):

assuming you know exp 0

view this post on Zulip Mario Carneiro (Sep 15 2018 at 20:07):

that's true, it should say tendsto_exp_zero or something

view this post on Zulip Patrick Massot (Sep 15 2018 at 20:09):

We should probably prove the lemma for general homomorphisms between topological group (continuity at zero implies continuity)

view this post on Zulip Chris Hughes (Sep 15 2018 at 20:12):

And this only works for real.exp right?

view this post on Zulip Patrick Massot (Sep 15 2018 at 20:12):

Why?

view this post on Zulip Patrick Massot (Sep 15 2018 at 20:12):

Didn't you prove the addition formula for complex numbers?

view this post on Zulip Chris Hughes (Sep 15 2018 at 20:14):

Yes, but tendsto_of_tendsto_of_tendsto_of_le_of_le requires a partial order on complexes, unless I'm doing something wrong.

view this post on Zulip Patrick Massot (Sep 15 2018 at 20:15):

Oh, I meant that continuity at zero in C implies continuity everywhere

view this post on Zulip Mario Carneiro (Sep 15 2018 at 20:15):

The metamath comment says that the key step is abs (exp x - x - 1) <= (abs x) ^ 2 * 3/4

view this post on Zulip Patrick Massot (Sep 15 2018 at 20:15):

But Mario's idea to prove continuity at zero works in R

view this post on Zulip Patrick Massot (Sep 15 2018 at 20:15):

but he seems to have a new idea

view this post on Zulip Mario Carneiro (Sep 15 2018 at 20:15):

this bound works on complexes too

view this post on Zulip Mario Carneiro (Sep 15 2018 at 20:16):

it is a special case of the tail bound on exp

view this post on Zulip Mario Carneiro (Sep 15 2018 at 20:17):

abs (sum k = m,...,infty (x ^ n / n!)) <= (abs a)^m * ((m + 1) / (m! * m))

view this post on Zulip Mario Carneiro (Sep 15 2018 at 20:18):

when abs x <= 1

view this post on Zulip Patrick Massot (Sep 15 2018 at 20:19):

I need to go, sorry

view this post on Zulip Chris Hughes (Sep 15 2018 at 20:19):

How does the bound work on the complexes when they don't have linear order? What's the correct statement? abs ∘ exp is continuous doesn't seem like enough to prove exp is continuous. Bear in mind I know very little about analysis.

view this post on Zulip Chris Hughes (Sep 15 2018 at 20:22):

If I manage to turn my goal into something in terms of functions I recognize, I;m sure I'll be fine, but I just need to work out how to get from nhds to something I recognize.

view this post on Zulip Kenny Lau (Sep 15 2018 at 20:26):

you should go revise M1P1 :P

view this post on Zulip Chris Hughes (Sep 15 2018 at 20:26):

That doesn't mention anything to do with complex numbers.

view this post on Zulip Mario Carneiro (Sep 15 2018 at 20:28):

The statement abs (exp x - x - 1) <= (abs x) ^ 2 * 3/4 is enough to prove that exp is differentiable at 0

view this post on Zulip Mario Carneiro (Sep 15 2018 at 20:28):

here x is a complex number

view this post on Zulip Chris Hughes (Sep 15 2018 at 20:28):

I could probably manage that.

view this post on Zulip Chris Hughes (Sep 15 2018 at 20:29):

You'll have to help me turn that into anything about continuity.

view this post on Zulip Mario Carneiro (Sep 15 2018 at 20:29):

For continuity you could probably just do the zeroth order tail bound, which is abs (exp x - 1) <= (abs x) * 2

view this post on Zulip Kenny Lau (Sep 15 2018 at 20:30):

is it realistic to develop a general theory of complex power series?

view this post on Zulip Mario Carneiro (Sep 15 2018 at 20:30):

maybe, but I'd prefer to defer it

view this post on Zulip Patrick Massot (Sep 17 2018 at 08:50):

@Chris Hughes are you currently working on exp?

view this post on Zulip Chris Hughes (Sep 17 2018 at 08:52):

No, and I am doing other things today. I might work on it tomorrow.

view this post on Zulip Chris Hughes (Sep 17 2018 at 18:12):

I made some progress. I proved IVT, though I'm not sure if there is some clever simple proof.

lemma IVT {f :   } (hf : continuous f) {x y : } (hx : f x  0) (hy : 0  f y)
  (hxy : x  y) :  z : , x  z  z  y  f z = 0 :=
let z := Sup {a | f a  0  x  a  a  y} in
have hz₁ :  a,  g  {a :  | f a  0  x  a  a  y}, g  a := y, λ _ h, h.2.2,
have hz₂ :  a, a  {a :  | f a  0  x  a  a  y} := x, hx, le_refl _, hxy,
z, le_Sup _ hz₁ hx, le_refl _, hxy,
  (Sup_le {a | f a  0  x  a  a  y} hz₂ hz₁).2 (λ _ h, h.2.2),
  eq_of_forall_dist_le $ λ ε ε0,
    let δ, hδ0,  := tendsto_nhds_of_metric.1 (continuous_iff_tendsto.1 hf z) ε ε0 in
    (le_total 0 (f z)).elim
      (λ h, le_of_not_gt $ λ hfε, begin
        rw [dist_0_eq_abs, abs_of_nonneg h] at hfε,
        refine mt (Sup_le {a | f a  0  x  a  a  y} hz₂ hz₁).2
          (not_le_of_gt (sub_lt_self z (half_pos hδ0)))
          (λ g hg, le_of_not_gt
            (λ hgδ, not_lt_of_ge hg.1
              (lt_trans (sub_pos_of_lt hfε) (sub_lt_of_sub_lt
                (lt_of_le_of_lt (le_abs_self _) _))))),
        rw abs_sub,
        exact  (abs_sub_lt_iff.2 lt_of_le_of_lt (sub_nonpos.2 (le_Sup _ hz₁ hg)) hδ0,
          by simp only [z] at *; linarith)
        end)
      (λ h, le_of_not_gt $ λ hfε, begin
        rw [dist_0_eq_abs, abs_of_nonpos h] at hfε,
        refine mt (le_Sup {a | f a  0  x  a  a  y})
          (λ h :  k, k  {a | f a  0  x  a  a  y}  k  z,
            not_le_of_gt ((lt_add_iff_pos_left z).2 (half_pos hδ0))
              (h _ le_trans (le_sub_iff_add_le.2 (le_trans (le_abs_self _)
                    (le_of_lt ( $ by rw [dist_eq, add_sub_cancel, abs_of_nonneg (le_of_lt (half_pos hδ0))];
                      exact half_lt_self hδ0))))
                  (le_of_lt (sub_neg_of_lt hfε)),
                le_trans (le_Sup _ hz₁ hx, le_refl _, hxy) (le_of_lt ((lt_add_iff_pos_left _).2 (half_pos hδ0))),
                le_of_not_gt (λ hδy, not_lt_of_ge hy (lt_of_le_of_lt (show f y  f y - f z - ε, by linarith)
                  (sub_neg_of_lt (lt_of_le_of_lt (le_abs_self _)
                    (@ y (abs_sub_lt_iff.2 by simp only [z] at *; linarith,
                      sub_lt_iff_lt_add.2 (by rw add_comm; exact lt_add_of_le_of_pos
                        ((Sup_le _ hz₂ hz₁).2 (λ _ h, h.2.2)) hδ0))))))))) hz₁
        end)

view this post on Zulip Johan Commelin (Sep 17 2018 at 18:13):

Well done!

view this post on Zulip Johan Commelin (Sep 17 2018 at 18:14):

@Chris Hughes I guess you could quite easily change the 0s in the statement into a parameter, right?

view this post on Zulip Johan Commelin (Sep 17 2018 at 18:15):

Hmm, but you are use half_pos and things like that.

view this post on Zulip Johan Commelin (Sep 17 2018 at 18:15):

So maybe you should just leave this like it is.

view this post on Zulip Chris Hughes (Sep 17 2018 at 18:22):

I can deduce the general statement from this quite easily I imagine.

view this post on Zulip Johan Commelin (Sep 17 2018 at 18:22):

Yes, agreed.

view this post on Zulip Chris Hughes (Sep 17 2018 at 18:22):

The more important generalisation is that it only needs to be continuous on the interval.

view this post on Zulip Kenny Lau (Sep 17 2018 at 18:26):

@Chris Hughes how much topology do you know?

view this post on Zulip Chris Hughes (Sep 17 2018 at 18:27):

More or less none.

view this post on Zulip Kenny Lau (Sep 17 2018 at 18:28):

if x<y and f(x)<0 and f(y)>0, then {t | f(t) < 0} and {t | f(t) > 0} are two disjoint open subsets of [x,y]. Since [x,y] is connected, the union of those two sets can't be the entirety of [x,y], so there must be something not belonging to those two sets, i.e. t such that f(t) = 0

view this post on Zulip Johan Commelin (Sep 17 2018 at 18:32):

Do we know that intervals are connected?

view this post on Zulip Johan Commelin (Sep 17 2018 at 18:32):

Does Lean even know what an interval is?

view this post on Zulip Reid Barton (Sep 17 2018 at 18:32):

I don't think we have connectedness yet

view this post on Zulip Reid Barton (Sep 17 2018 at 18:33):

We do have intervals though and Lean knows closed ones are compact

view this post on Zulip Reid Barton (Sep 17 2018 at 18:34):

Basically it's a similar proof to the one above I think, except the set {a | f a <= 0 ...} is now called U

view this post on Zulip Kenny Lau (Sep 17 2018 at 18:36):

right, we know they're compact but not that they're connected...?

view this post on Zulip Mario Carneiro (Sep 17 2018 at 18:42):

right, the meat of this proof is showing that R is connected

view this post on Zulip Mario Carneiro (Sep 17 2018 at 18:44):

I think you can pretty trivially generalize the assumption to ∀ x, a < x → x < b → tendsto f (nhds x) (nhds (f x))

view this post on Zulip Mario Carneiro (Sep 17 2018 at 18:46):

If you prefer, you can prove the version assuming continuous f as a corollary

view this post on Zulip Mario Carneiro (Sep 17 2018 at 18:46):

other than that, I think this is fine for the first cut

view this post on Zulip Chris Hughes (Sep 17 2018 at 19:07):

I almost generalized it to ∀ x, a < x → x < b → tendsto f (nhds x) (nhds (f x)). I have lt instead of le. Generalizing it to lt seems to add quite a bit of complication.

lemma IVT {f :   } {x y : }
  (hf :  a, x  a  a  y  tendsto f (nhds a) (nhds (f a))) (hx : f x  0) (hy : 0  f y)
  (hxy : x  y) :  z : , x  z  z  y  f z = 0 :=
let z := Sup {a | f a  0  x  a  a  y} in
have hz₁ :  a,  g  {a :  | f a  0  x  a  a  y}, g  a := y, λ _ h, h.2.2,
have hz₂ :  a, a  {a :  | f a  0  x  a  a  y} := x, hx, le_refl _, hxy,
have hxz : x  z, from le_Sup _ hz₁ hx, le_refl _, hxy,
have hzy : z  y, from (Sup_le _ hz₂ hz₁).2 (λ _ h, h.2.2),
z, hxz, hzy,
  eq_of_forall_dist_le $ λ ε ε0,
    let δ, hδ0,  := tendsto_nhds_of_metric.1 (hf _ hxz hzy) ε ε0 in
    (le_total 0 (f z)).elim
      (λ h, le_of_not_gt $ λ hfε, begin
        rw [dist_0_eq_abs, abs_of_nonneg h] at hfε,
        refine mt (Sup_le {a | f a  0  x  a  a  y} hz₂ hz₁).2
          (not_le_of_gt (sub_lt_self z (half_pos hδ0)))
          (λ g hg, le_of_not_gt
            (λ hgδ, not_lt_of_ge hg.1
              (lt_trans (sub_pos_of_lt hfε) (sub_lt_of_sub_lt
                (lt_of_le_of_lt (le_abs_self _) _))))),
        rw abs_sub,
        exact  (abs_sub_lt_iff.2 lt_of_le_of_lt (sub_nonpos.2 (le_Sup _ hz₁ hg)) hδ0,
          by simp only [z] at *; linarith)
        end)
      (λ h, le_of_not_gt $ λ hfε, begin
        rw [dist_0_eq_abs, abs_of_nonpos h] at hfε,
        refine mt (le_Sup {a | f a  0  x  a  a  y})
          (λ h :  k, k  {a | f a  0  x  a  a  y}  k  z,
            not_le_of_gt ((lt_add_iff_pos_left z).2 (half_pos hδ0))
              (h _ le_trans (le_sub_iff_add_le.2 (le_trans (le_abs_self _)
                    (le_of_lt ( $ by rw [dist_eq, add_sub_cancel, abs_of_nonneg (le_of_lt (half_pos hδ0))];
                      exact half_lt_self hδ0))))
                  (le_of_lt (sub_neg_of_lt hfε)),
                le_trans hxz (le_of_lt ((lt_add_iff_pos_left _).2 (half_pos hδ0))),
                le_of_not_gt (λ hδy, not_lt_of_ge hy (lt_of_le_of_lt (show f y  f y - f z - ε, by linarith)
                  (sub_neg_of_lt (lt_of_le_of_lt (le_abs_self _)
                    (@ y (abs_sub_lt_iff.2 by simp only [z] at *; linarith,
                      sub_lt_iff_lt_add.2 (by rw add_comm; exact lt_add_of_le_of_pos
                        hzy hδ0))))))))) hz₁
        end)

view this post on Zulip Chris Hughes (Sep 17 2018 at 19:10):

In fact generalizing to lt makes the statement false I think.

view this post on Zulip Johan Commelin (Sep 17 2018 at 19:12):

Right, you need the closed interval.

view this post on Zulip Mario Carneiro (Sep 17 2018 at 19:14):

ah yes, you're right. In order to properly say "continuous on [a, b]" you would need tendsto f (nhds a ⊓ principal (Icc a b)) (nhds (f a))

view this post on Zulip Chris Hughes (Sep 17 2018 at 19:17):

What does that mean, and how is it different from my assumption?

view this post on Zulip Chris Hughes (Sep 17 2018 at 19:22):

Is it weaker or stronger than my assumption?

view this post on Zulip Johan Commelin (Sep 17 2018 at 19:24):

@Chris Hughes you know about left/right-continuity at a point?

view this post on Zulip Mario Carneiro (Sep 17 2018 at 19:25):

My predicate says that f restricted to [a, b] is continuous

view this post on Zulip Mario Carneiro (Sep 17 2018 at 19:25):

so it might have discontinuity at a or b from outside the interval

view this post on Zulip Chris Hughes (Sep 17 2018 at 19:26):

I see.

view this post on Zulip Johan Commelin (Sep 17 2018 at 19:26):

Eg: f x = if x \in [a,b] then 0 else 1

view this post on Zulip Mario Carneiro (Sep 17 2018 at 19:26):

But you should be able to extend any continuous function on [a,b] to one continuous in your sense anyway, so I wouldn't make a big deal about it

view this post on Zulip Chris Hughes (Sep 19 2018 at 17:26):

I managed to prove this today.

lemma exp_continuous_aux {x : } (hx : abs x  1) :
  abs (exp x - x - 1)  abs x ^ 2 * (5 / 6) :=

It's 5 / 6 instead of 3/4, is that going to be a problem? I'm not sure where my extra 1/12 went

view this post on Zulip Chris Hughes (Sep 19 2018 at 17:27):

I suppose it depends on whether I can still prove the cos inequalities

view this post on Zulip Mario Carneiro (Sep 19 2018 at 17:35):

that's weird, how did you prove it?

view this post on Zulip Mario Carneiro (Sep 19 2018 at 17:36):

I don't think we need any particular bound for this part, that's enough for continuity of course

view this post on Zulip Chris Hughes (Sep 19 2018 at 17:39):

This is my proof. I think the lost information is probably in the step
sum (range (j - 3)) (λ m, 1 / (m + 3).fact) ≤ sum (range (j - 3)) (λ m, 1 / 6 * (1 / 2) ^ m)

lemma exp_continuous_aux {x : } (hx : abs x  1) :
  abs (exp x - x - 1)  abs x ^ 2 * (5 / 6) :=
have onesubhalf : (1 : ) - 1 / 2 = 1 / 2, by norm_num,
have abshalf : abs (1 / 2 : ) = 1 / 2 :=
  calc abs (1 / 2 : ) = abs ((1 / 2 : ) : ) : congr_arg abs $ by simp [of_real_div, of_real_bit0, of_real_inv]
  ... = (1 / 2 : ) : by rw [abs_of_nonneg]; norm_num,
begin
  conv in (exp x - x) {congr, skip, rw  lim_const x},
  rw [exp, sub_eq_add_neg, sub_eq_add_neg,  lim_const 1,
     lim_neg,  lim_neg, lim_add, lim_add,  lim_abs],
  refine real.lim_le _ _ (cau_seq.le_of_exists 3, (λ j hj, _)),
  show (abs (sum (range j) (λ m, x ^ m / m.fact) - x - 1)  abs x ^ 2 * (5 / 6)),
  exact calc abs ((sum (range j)) (λ m, x ^ m / m.fact) - x - 1) =
      abs x ^ 2 * abs (sum (range (j - 2)) (λ m, x ^ m / (m + 2).fact)) :
    by conv {to_lhs, rw [ nat.sub_add_cancel (nat.le_of_succ_le hj), sum_range_succ', sum_range_succ']};
      simp [pow_succ, mul_sum.symm, abs_mul, mul_div_assoc, mul_assoc]
  ... = abs x ^ 2 * abs (sum (range (j - 3)) (λ m, x ^ (m + 1) / (m + 3).fact) + 1 / 2) :
    by conv {to_lhs, rw [ nat.succ_sub_succ, nat.succ_sub hj, sum_range_succ'] };
      simp [nat.fact, bit0]
  ...  abs x ^ 2 * (5 / 6) : mul_le_mul_of_nonneg_left
    (calc abs (sum (range (j - 3)) (λ m, x ^ (m + 1) / (m + 3).fact) + 1 / 2)
           abs (sum (range (j - 3)) (λ m, x ^ (m + 1) / (m + 3).fact)) + abs (1 / 2) :
        abs_add _ _
      ... = abs (sum (range (j - 3)) (λ m, x ^ (m + 1) / (m + 3).fact)) + 1 / 2 :
        by rw abshalf
      ...  sum (range (j - 3)) (λ m, abs (x ^ (m + 1) / (m + 3).fact)) + 1 / 2 :
        add_le_add_right (abv_sum_le_sum_abv _ _) _
      ...  sum (range (j - 3)) (λ m, 1 / (m + 3).fact) + 1 / 2 :
        add_le_add_right (sum_le_sum (λ n _,
          by rw [abs_div, is_absolute_value.abv_pow abs,  of_real_nat_cast,
            abs_of_nonneg (nat.cast_nonneg _)];
          refine (div_le_div_right (nat.cast_pos.2 (nat.fact_pos _))).2
            (pow_le_one _ (abs_nonneg _) hx))) _
      ...  sum (range (j - 3)) (λ m, 1 / 6 * (1 / 2) ^ m) + 1 / 2 :
        add_le_add_right (sum_le_sum $ λ n hn, begin
          clear hn,
          induction n with n ih,
          { simp [bit0, bit1, mul_add, add_mul] },
          { rw [nat.fact_succ, pow_succ', one_div_eq_inv, nat.cast_mul, mul_inv',  mul_assoc (1 / 6 : )],
            refine mul_le_mul (by rwa inv_eq_one_div) _
              (inv_nonneg.2 (nat.cast_nonneg _))
              (mul_nonneg (by norm_num) (pow_nonneg (by norm_num) _)),
            rw [one_div_eq_inv],
            refine (inv_le_inv (nat.cast_pos.2 (nat.succ_pos _)) (by norm_num)).2
              (by rw  nat.cast_two; exact nat.cast_le.2 dec_trivial) }
        end) _
      ... = 1 / 6 * ((1 - (1 / 2) ^ (j - 3)) / (1 - 1 / 2)) + 1 / 2 :
        by rw [ mul_sum, geo_series_eq]; norm_num
      ...  1 / 6 * (1 / (1 - 1 / 2)) + 1 / 2 :
        add_le_add_right (mul_le_mul_of_nonneg_left ((div_le_div_right (by norm_num)).2
          (sub_le_self _ (pow_nonneg (by norm_num) _))) (by norm_num)) _
      ... = 5 / 6 : by norm_num)
    (pow_two_nonneg (abs x))
end

view this post on Zulip Mario Carneiro (Sep 19 2018 at 17:40):

Oh, you really did the case n=1 directly

view this post on Zulip Mario Carneiro (Sep 19 2018 at 17:40):

I was thinking you would just prove the general case, there is less stuff floating around that way

view this post on Zulip Mario Carneiro (Sep 19 2018 at 17:41):

well, it's done now, we can revisit later

view this post on Zulip Chris Hughes (Sep 19 2018 at 17:41):

Not sure what the general case is.

view this post on Zulip Mario Carneiro (Sep 19 2018 at 17:42):

abs (sum k = m,...,infty (x ^ n / n!)) <= (abs a)^m * ((m + 1) / (m! * m))

view this post on Zulip Mario Carneiro (Sep 19 2018 at 17:42):

You can also write exp x - finset.sum ... instead of that tail sum if you prefer

view this post on Zulip Chris Hughes (Sep 19 2018 at 17:42):

That makes way more sense.

view this post on Zulip Reid Barton (Sep 19 2018 at 17:50):

By the way, how hard is it to get log once we have exp? Specifically how hard is it to show that every nonzero complex number is in the range of exp?

view this post on Zulip Mario Carneiro (Sep 19 2018 at 18:13):

This comes fairly late in the development.

  • First you do the real log function. exp is easily seen to be increasing so you get an inverse by IVT. I can expand on this
  • sin is a bijection from [-pi/2, pi/2] to [-1, 1]. Again, this has subparts
  • Injectivity of exp: exp x = 1 iff x = 2*pi*i*n for some n
  • The complex square root function exists. You can define it as sqrt z = sqrt (abs z) * ((abs z + z) / abs (abs z + z)) off the negative real axis
  • If D is an interval of length 2pi, and y : D is chosen to be a multiple of 2 pi from 2 * arcsin (im (sqrt z)), then z = exp (I * y), which shows surjectivity of the imaginary part
  • By combining surjectivity on real and imaginary parts and injectivity, you get that exp is bijective in any domain of the form {z | z.im \in D}

view this post on Zulip Chris Hughes (Sep 19 2018 at 19:40):

How do you get the bounds on cosine?

view this post on Zulip Chris Hughes (Sep 19 2018 at 19:41):

specifically 1/3 < cos 1 < 2 / 3 the fact that exp x - x - 1 \le abs x ^ 2 * 3 / 4 is only good enough for 1/4 \le cos 1 \le 7 / 4

view this post on Zulip Chris Hughes (Sep 19 2018 at 19:42):

do you need bounds on sine 1 and use cos^2 + sin^2 = 1

view this post on Zulip Mario Carneiro (Sep 19 2018 at 20:03):

The claim is that abs (cos x - (1 - x^2 / 2)) < x^2 / 6 for x \in (0, 1]. By the m=4 case of the tail bound on exp, cos x - (1 - x^2 / 2) = re (exp4 (I*x)) <= abs (exp4 (I*x)) <= x^4 * ((4 + 1) / (4! * 4)) < x^4 / 6 <= x^2 / 6, where exp4 is the tail of exp starting at 4.

view this post on Zulip Mario Carneiro (Sep 19 2018 at 20:04):

(sorry! looks like you do need more of the tail bound)

view this post on Zulip Mario Carneiro (Sep 19 2018 at 20:05):

in metamath, each inequality there is a sublemma (or instance of a lemma), probably don't pack it all together since it is independently useful

view this post on Zulip Chris Hughes (Sep 20 2018 at 13:17):

Major progress. The following have now been proved. @Mario Carneiro how do I get continuous exp from the first one?

lemma exp_bound {x : } (hx : abs x  1) {n : } (hn : 0 < n) :
  abs (exp x - (range n.succ).sum (λ m, x ^ m / m.fact))  abs x ^ n.succ * (n.fact * n)⁻¹

lemma cos_one_bound : abs' (real.cos 1 - 1 / 2)  1 / 18

view this post on Zulip Kenny Lau (Sep 20 2018 at 13:19):

you might want to specialize the n first if you want to prove continuity

view this post on Zulip Kenny Lau (Sep 20 2018 at 13:19):

and you want to prove continuity at 0 first

view this post on Zulip Kenny Lau (Sep 20 2018 at 13:20):

(since exp(y)-exp(x) = exp(x) [exp(y-x)-1])

view this post on Zulip Mario Carneiro (Sep 20 2018 at 13:20):

As I mentioned, if you take n = 1 then you have abs (exp x - 1) <= abs x

view this post on Zulip Kenny Lau (Sep 20 2018 at 13:20):

so combining our statements, |exp(y)-exp(x)| <= exp(x) |y-x|

view this post on Zulip Kenny Lau (Sep 20 2018 at 13:21):

so set delta = epsilon/exp(x)

view this post on Zulip Mario Carneiro (Sep 20 2018 at 13:22):

wait, isn't the bound off by one? the claim was about sum m=n ... infty (x^m/m!) which should be abs (exp x - (range n).sum (λ m, x ^ m / m.fact))

view this post on Zulip Mario Carneiro (Sep 20 2018 at 13:23):

the RHS looks right

view this post on Zulip Kenny Lau (Sep 20 2018 at 13:25):

well n=1 gives |exp(x)-1-x| <= |x|^2

view this post on Zulip Mario Carneiro (Sep 20 2018 at 13:29):

I guess the order is right, the constant is a bit off

view this post on Zulip Mario Carneiro (Sep 20 2018 at 13:29):

lemma exp_bound {x : ℂ} (hx : abs x ≤ 1) {n : ℕ} (hn : 0 < n) :
  abs (exp x - (range n).sum (λ m, x ^ m / m.fact)) ≤ abs x ^ n * (n.succ / (n.fact * n)) := sorry

view this post on Zulip Chris Hughes (Sep 20 2018 at 14:20):

Does it matter? We have everything we need for pi

lemma cos_one_le : real.cos 1  5 / 9 :=
calc real.cos 1  1 / 2 + 1 / 18 : sub_le_iff_le_add.1 (abs_sub_le_iff.1 cos_one_bound).1
... = 5 / 9 : by norm_num

lemma le_cos_one : 4 / 9  real.cos 1 :=
calc 4 / 9 = 1 / 2 - 1 / 18 : by norm_num
...  real.cos 1 : sub_le_of_sub_le (abs_sub_le_iff.1 cos_one_bound).2

lemma cos_two_le : real.cos 2  -31 / 81 :=
calc real.cos 2 = real.cos (2 * 1) : congr_arg real.cos (by simp [bit0])
... = _ : real.cos_two_mul 1
...  2 * (5 / 9) ^ 2 - 1 :
  sub_le_sub_right (mul_le_mul_of_nonneg_left
  (by rw [pow_two, pow_two]; exact
    mul_self_le_mul_self (le_trans (by norm_num) le_cos_one) _)
  (by norm_num)) _
... = -31 / 81 : by norm_num

view this post on Zulip Patrick Massot (Sep 20 2018 at 14:28):

Wonderful! Can you get pi before tomorrow then?

view this post on Zulip Chris Hughes (Sep 20 2018 at 14:30):

If someone tells me how to turn my inequalities about exp into a proof of continuity. I don't know what the lemma is.

view this post on Zulip Patrick Massot (Sep 20 2018 at 14:30):

Did you push everything?

view this post on Zulip Patrick Massot (Sep 20 2018 at 14:31):

Doesn't seem so

view this post on Zulip Chris Hughes (Sep 20 2018 at 14:31):

Not yet

view this post on Zulip Patrick Massot (Sep 20 2018 at 14:31):

It would be easier to see what inequalities you have

view this post on Zulip Chris Hughes (Sep 20 2018 at 14:35):

Just pushing now

view this post on Zulip Reid Barton (Sep 20 2018 at 14:35):

Do we know that C\mathbb{C} is a normed group?

view this post on Zulip Reid Barton (Sep 20 2018 at 14:42):

I guess it would be quite easy to add. Then you should be able to use tendsto_iff_norm_tendsto_zero and tendsto_of_tendsto_of_tendsto_of_le_of_le somehow

view this post on Zulip Reid Barton (Sep 20 2018 at 14:43):

or maybe even squeeze_zero

view this post on Zulip Mario Carneiro (Sep 20 2018 at 14:44):

There should be a theorem about continuity on metric spaces

view this post on Zulip Mario Carneiro (Sep 20 2018 at 14:44):

continuous_of_metric

view this post on Zulip Mario Carneiro (Sep 20 2018 at 14:45):

oh wait, you just want continuity at zero, that is tendsto_nhds_of_metric

view this post on Zulip Mario Carneiro (Sep 20 2018 at 14:46):

just rewrite dist 0 x to abs x and you should be set with a straight epsilon delta proof

view this post on Zulip Mario Carneiro (Sep 20 2018 at 14:47):

You shouldn't make your constants too precise, it makes the proof harder for norm_num and the gain is not that great. In particular you should weaken the second theorem to cos 2 < 0

view this post on Zulip Chris Hughes (Sep 20 2018 at 18:26):

So I have lemma tendsto_exp_zero_one : tendsto exp (nhds 0) (nhds 1) :=

view this post on Zulip Chris Hughes (Sep 20 2018 at 18:26):

How do I get continuity?

view this post on Zulip Kenny Lau (Sep 20 2018 at 18:27):

note that exp(x+h) = exp(x) exp(h)

view this post on Zulip Mario Carneiro (Sep 20 2018 at 18:27):

do we know that C is a topological ring?

view this post on Zulip Chris Hughes (Sep 20 2018 at 18:28):

@Mario Carneiro yes

view this post on Zulip Kenny Lau (Sep 20 2018 at 18:29):

\forall x, tendsto (\lambda h, exp x * exp h) (nhds 0) (nhds (exp x * 1))

view this post on Zulip Kenny Lau (Sep 20 2018 at 18:29):

\forall x, tendsto (\lambda h, exp (x+h)) (nhds 0) (nhds (exp x))

view this post on Zulip Kenny Lau (Sep 20 2018 at 18:29):

\forall x, tendsto exp (nhds x) (nhds (exp x))

view this post on Zulip Chris Hughes (Sep 20 2018 at 18:30):

What lemmas are you applying Kenny?

view this post on Zulip Mario Carneiro (Sep 20 2018 at 18:30):

Ah, found it: continuous_mul is what you want

view this post on Zulip Mario Carneiro (Sep 20 2018 at 18:31):

to deduce the first of Kenny's statements

view this post on Zulip Mario Carneiro (Sep 20 2018 at 18:31):

wait no, tendsto_mul

view this post on Zulip Mario Carneiro (Sep 20 2018 at 18:32):

the second one is easy/algebraic, and the third is that lemma that Patrick mentioned

view this post on Zulip Mario Carneiro (Sep 20 2018 at 18:35):

Alternatively you could just use continuity of subtraction to avoid mentioning homeos

view this post on Zulip Kenny Lau (Sep 20 2018 at 18:36):

from 2 to 3 can be easily done with epsilon-delta

view this post on Zulip Kenny Lau (Sep 20 2018 at 18:36):

would not recommend epsilon-delta to deduce 1

view this post on Zulip Mario Carneiro (Sep 20 2018 at 18:36):

don't listen to kenny, you are done with epsilons now

view this post on Zulip Kenny Lau (Sep 20 2018 at 18:36):

we're in the post-epsilon stage of maths, right

view this post on Zulip Mario Carneiro (Sep 20 2018 at 18:38):

if you know tendsto (\lambda h, exp (x+h)) (nhds 0) (nhds (exp x)) then if you compose with (\lambda y, y - x) which is continuous then you get tendsto (\lambda y, exp (x+(y - x))) (nhds x) (nhds (exp x))

view this post on Zulip Chris Hughes (Sep 20 2018 at 18:41):

My goal is tendsto (λ (x_1 : ℂ), exp x) (nhds 0) (nhds 1) I try apply tendsto_exp_zero_one, which looks like this tendsto_exp_zero_one : tendsto (λ x : ℂ, exp x) (nhds (0 : ℂ)) (nhds (1 : ℂ)) and it hangs.

view this post on Zulip Mario Carneiro (Sep 20 2018 at 18:42):

use exact

view this post on Zulip Mario Carneiro (Sep 20 2018 at 18:43):

apply will go crazy unfolding pis because of a bug

view this post on Zulip Chris Hughes (Sep 20 2018 at 18:44):

exact this fails

x : complex,
this :
  @filter.tendsto.{0 0} complex complex (λ (x : complex), complex.exp x)
    (@nhds.{0} complex
       (@uniform_space.to_topological_space.{0} complex
          (@metric_space.to_uniform_space'.{0} complex complex.metric_space))
       (@has_zero.zero.{0} complex complex.has_zero))
    (@nhds.{0} complex
       (@uniform_space.to_topological_space.{0} complex
          (@metric_space.to_uniform_space'.{0} complex complex.metric_space))
       (@has_one.one.{0} complex complex.has_one))
 @filter.tendsto.{0 0} complex complex (λ (x_1 : complex), complex.exp x)
    (@nhds.{0} complex
       (@uniform_space.to_topological_space.{0} complex
          (@metric_space.to_uniform_space'.{0} complex complex.metric_space))
       (@has_zero.zero.{0} complex complex.has_zero))
    (@nhds.{0} complex
       (@uniform_space.to_topological_space.{0} complex
          (@metric_space.to_uniform_space'.{0} complex complex.metric_space))
       (@has_one.one.{0} complex complex.has_one))

view this post on Zulip Chris Hughes (Sep 20 2018 at 18:44):

I see the problem.

view this post on Zulip Chris Hughes (Sep 20 2018 at 18:44):

Silly me

view this post on Zulip Mario Carneiro (Sep 20 2018 at 18:45):

is that sarcasm? because I don't

view this post on Zulip Chris Hughes (Sep 20 2018 at 18:46):

x_1 instead of x on first line

view this post on Zulip Mario Carneiro (Sep 20 2018 at 18:49):

by the way, convert is a nice way to diagnose these bugs

view this post on Zulip Chris Hughes (Sep 20 2018 at 18:51):

What's the lemma I use for composing with sub

view this post on Zulip Chris Hughes (Sep 20 2018 at 18:52):

tends.comp d'oh

view this post on Zulip Chris Hughes (Sep 20 2018 at 19:06):

This must be easy surely

tendsto (λ (y : ), y - x) (nhds x) (nhds 0)

view this post on Zulip Mario Carneiro (Sep 20 2018 at 19:07):

by the way I suggest you do all your compositions at the start, getting something like tendsto (\lam y, exp x * exp (y - x)) (nhds x) (nhds (exp x * exp (x - x)))

view this post on Zulip Chris Hughes (Sep 20 2018 at 19:08):

I worked that bit out. Do I have to use tendsto_sub and the identity and constant functions?

view this post on Zulip Mario Carneiro (Sep 20 2018 at 19:08):

yes

view this post on Zulip Mario Carneiro (Sep 20 2018 at 19:09):

that's the easiest way, at least

view this post on Zulip Chris Hughes (Sep 20 2018 at 19:20):

exp is continuous is now a fact.

view this post on Zulip Kenny Lau (Sep 20 2018 at 19:22):

how much time do we still have?

view this post on Zulip Patrick Massot (Sep 20 2018 at 19:27):

Here it's 9:27pm

view this post on Zulip Patrick Massot (Sep 20 2018 at 19:28):

So 8:27pm in London

view this post on Zulip Patrick Massot (Sep 20 2018 at 19:28):

So we have 12 hours

view this post on Zulip Patrick Massot (Sep 20 2018 at 19:28):

roughly

view this post on Zulip Patrick Massot (Sep 20 2018 at 19:29):

Who's going to tell Kevin tomorrow? @Johan Commelin ?

view this post on Zulip Chris Hughes (Sep 20 2018 at 19:43):

How do you prove continuous real.sin from continuous complex.sin?

view this post on Zulip Mario Carneiro (Sep 20 2018 at 19:43):

continuity of real part

view this post on Zulip Mario Carneiro (Sep 20 2018 at 19:43):

and continuity of real injection

view this post on Zulip Mario Carneiro (Sep 20 2018 at 19:44):

How did you define real.sin?

view this post on Zulip Patrick Massot (Sep 20 2018 at 19:52):

https://github.com/leanprover-community/mathlib/blob/4c670fc338c3e6cdff8c1f01e03f1279fd3926bd/data/complex/exponential.lean#L349

view this post on Zulip Chris Hughes (Sep 20 2018 at 19:52):

(complex.sin x).re

view this post on Zulip Patrick Massot (Sep 20 2018 at 19:53):

So continuity should indeed follow as Mario wrote

view this post on Zulip Chris Hughes (Sep 20 2018 at 19:53):

I couldn't find continuous_re

view this post on Zulip Patrick Massot (Sep 20 2018 at 19:54):

Do you want us to prove it, or did you do it already?

view this post on Zulip Mario Carneiro (Sep 20 2018 at 20:03):

I think there is a theorem that re is a contracting map, which is enough to prove continuity

view this post on Zulip Mario Carneiro (Sep 20 2018 at 20:04):

abs_re_le_abs

view this post on Zulip Chris Hughes (Sep 20 2018 at 20:24):

I managed to work it out. I thought there was some simple proof without deltas, but deltas is really short anyway.

view this post on Zulip Patrick Massot (Sep 20 2018 at 20:25):

How far are you from pi then?

view this post on Zulip Chris Hughes (Sep 20 2018 at 20:26):

More or less there. Just have to apply IVT which I have already proved.

view this post on Zulip Patrick Massot (Sep 20 2018 at 20:29):

So, who's writing to Kevin tomorrow?

view this post on Zulip Chris Hughes (Sep 20 2018 at 20:46):

def pi :  := 2 * classical.some exists_cos_eq_zero

view this post on Zulip Kenny Lau (Sep 20 2018 at 20:47):

then pi can be 3*3.14...?

view this post on Zulip Mario Carneiro (Sep 20 2018 at 20:47):

have you proven that cos (pi/2) = 0?

view this post on Zulip Chris Hughes (Sep 20 2018 at 20:49):

lemma exists_cos_eq_zero : ∃ x, 1 ≤ x ∧ x ≤ 2 ∧ cos x = 0 @Kenny Lau

view this post on Zulip Kenny Lau (Sep 20 2018 at 20:49):

fair enough

view this post on Zulip Mario Carneiro (Sep 20 2018 at 20:49):

also sin (pi/2) = 1

view this post on Zulip Mario Carneiro (Sep 20 2018 at 20:49):

the rest should be easy

view this post on Zulip Kenny Lau (Sep 20 2018 at 20:49):

well sin(pi/2)=1 implies cos(pi/2)=0...

view this post on Zulip Mario Carneiro (Sep 20 2018 at 20:50):

but it looks like he proved cos (pi/2) = 0, which only implies sin(pi/2) = +- 1

view this post on Zulip Mario Carneiro (Sep 20 2018 at 20:51):

Metamath uses the lemma that sin x > 0 on (0, 2] by double angle formulas on what you already have

view this post on Zulip Chris Hughes (Sep 20 2018 at 20:52):

I'm sure that's all quite easily doable.

view this post on Zulip Mario Carneiro (Sep 20 2018 at 20:53):

yes, it's mostly smooth sailing at this point

view this post on Zulip Chris Hughes (Sep 20 2018 at 20:53):

I pushed.

view this post on Zulip Kenny Lau (Sep 20 2018 at 21:04):

I'm afraid it's now 05:03 AM in Hong Kong and I must leave now...

view this post on Zulip Kenny Lau (Sep 20 2018 at 21:04):

although I will wake up 4 hours later

view this post on Zulip Mario Carneiro (Sep 20 2018 at 21:04):

ooh, you are 12 hours away from me

view this post on Zulip Kevin Buzzard (Sep 20 2018 at 23:10):

I've been 50 for about 10 minutes

view this post on Zulip Chris Hughes (Sep 20 2018 at 23:11):

Happy Birthday!

view this post on Zulip Kevin Buzzard (Sep 20 2018 at 23:11):

Holey Moley we have pi!

view this post on Zulip Kevin Buzzard (Sep 20 2018 at 23:11):

I am so happy!

view this post on Zulip Kevin Buzzard (Sep 20 2018 at 23:13):

I need to go to bed!


Last updated: May 18 2021 at 11:11 UTC