Zulip Chat Archive

Stream: kbb

Topic: sine and cosine and pi


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?

Patrick Massot (Sep 15 2018 at 11:56):

Do you have complex exp or only real?

Chris Hughes (Sep 15 2018 at 12:15):

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

Patrick Massot (Sep 15 2018 at 13:06):

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

Johan Commelin (Sep 15 2018 at 13:06):

You're such a mathematician.

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.

Johan Commelin (Sep 15 2018 at 13:08):

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

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)

Johan Commelin (Sep 15 2018 at 13:09):

Rights, so we need continuity of exp.

Johan Commelin (Sep 15 2018 at 13:09):

For either definition.

Patrick Massot (Sep 15 2018 at 13:09):

I both cases yes

Johan Commelin (Sep 15 2018 at 13:10):

What is the best way to do this continuity proof?

Johan Commelin (Sep 15 2018 at 13:10):

Generalise to arbitrary power series?

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

Johan Commelin (Sep 15 2018 at 13:11):

I like your second definition.

Johan Commelin (Sep 15 2018 at 13:11):

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

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.

Johan Commelin (Sep 15 2018 at 13:13):

Ok, sounds good.

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?

Patrick Massot (Sep 15 2018 at 13:16):

indeed we must exclude that the kernel is trivial

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.

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

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.

Patrick Massot (Sep 15 2018 at 13:29):

This all looks super tedious

Patrick Massot (Sep 15 2018 at 13:29):

Let's do perfectoid spaces

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.

Johan Commelin (Sep 15 2018 at 13:40):

But how do I put this into Lean?

Patrick Massot (Sep 15 2018 at 13:43):

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

Johan Commelin (Sep 15 2018 at 13:46):

Aah thanks, that indeed looks useful.

Johan Commelin (Sep 15 2018 at 13:47):

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

Patrick Massot (Sep 15 2018 at 13:47):

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

Johan Commelin (Sep 15 2018 at 13:47):

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

Chris Hughes (Sep 15 2018 at 13:49):

We do know exp \ne 0

Johan Commelin (Sep 15 2018 at 14:07):

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

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?

Patrick Massot (Sep 15 2018 at 14:07):

there is

Johan Commelin (Sep 15 2018 at 14:07):

Ooh, my VScode didn't find it.

Johan Commelin (Sep 15 2018 at 14:08):

Let me try again

Johan Commelin (Sep 15 2018 at 14:08):

Aah, it only has squeeze in its docstring

Johannes Hölzl (Sep 15 2018 at 14:08):

grep for sandwich in mathlib

Patrick Massot (Sep 15 2018 at 14:08):

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

Patrick Massot (Sep 15 2018 at 14:09):

grep for squeeze also works

Patrick Massot (Sep 15 2018 at 14:09):

but grep for gendarme doesn't work

Johan Commelin (Sep 15 2018 at 14:14):

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

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

Johan Commelin (Sep 15 2018 at 14:18):

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

Johan Commelin (Sep 15 2018 at 14:18):

So, should we create power_series.lean on cocalc?

Johan Commelin (Sep 15 2018 at 14:19):

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

Johan Commelin (Sep 15 2018 at 14:21):

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

Johan Commelin (Sep 15 2018 at 14:21):

I'm quite addicted to that experience.

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)

Johannes Hölzl (Sep 15 2018 at 14:35):

I will take a look

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

Johannes Hölzl (Sep 15 2018 at 14:50):

The lemma termdiffs assumes that various power series converge.

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.

Johan Commelin (Sep 15 2018 at 14:53):

Is that right?

Johan Commelin (Sep 15 2018 at 14:53):

I mean, there won't change that much

Johannes Hölzl (Sep 15 2018 at 14:57):

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

Johan Commelin (Sep 15 2018 at 14:58):

Ok, and this is purely algebraic stuff, right?

Johan Commelin (Sep 15 2018 at 14:58):

Or do you also mean the analytic derivative?

Johannes Hölzl (Sep 15 2018 at 14:59):

I guess we need to analytic derivative to prove continuity

Johan Commelin (Sep 15 2018 at 15:00):

Hmmm, ok

Johan Commelin (Sep 15 2018 at 15:00):

And we really need all of this to define pi?

Johan Commelin (Sep 15 2018 at 15:01):

Well, we will need this stuff anyway

Johan Commelin (Sep 15 2018 at 15:03):

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

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

Johan Commelin (Sep 15 2018 at 15:06):

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

Johannes Hölzl (Sep 15 2018 at 15:06):

of course

Johannes Hölzl (Sep 15 2018 at 15:06):

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

Johannes Hölzl (Sep 15 2018 at 15:07):

it uses IVT

Johan Commelin (Sep 15 2018 at 15:07):

Right, so we need continuity

Johannes Hölzl (Sep 15 2018 at 15:08):

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

Johan Commelin (Sep 15 2018 at 15:09):

Ok

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.

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.

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.

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

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)

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}

Chris Hughes (Sep 15 2018 at 19:39):

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

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

Chris Hughes (Sep 15 2018 at 19:49):

How do I state continuous at a point?

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))

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?

Chris Hughes (Sep 15 2018 at 19:59):

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

Patrick Massot (Sep 15 2018 at 20:02):

I think I already answered that earlier today

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.

Patrick Massot (Sep 15 2018 at 20:02):

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

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))

Mario Carneiro (Sep 15 2018 at 20:04):

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

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

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)

Mario Carneiro (Sep 15 2018 at 20:06):

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

Patrick Massot (Sep 15 2018 at 20:06):

The name is bad, but the statement is ok

Patrick Massot (Sep 15 2018 at 20:07):

assuming you know exp 0

Mario Carneiro (Sep 15 2018 at 20:07):

that's true, it should say tendsto_exp_zero or something

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)

Chris Hughes (Sep 15 2018 at 20:12):

And this only works for real.exp right?

Patrick Massot (Sep 15 2018 at 20:12):

Why?

Patrick Massot (Sep 15 2018 at 20:12):

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

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.

Patrick Massot (Sep 15 2018 at 20:15):

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

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

Patrick Massot (Sep 15 2018 at 20:15):

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

Patrick Massot (Sep 15 2018 at 20:15):

but he seems to have a new idea

Mario Carneiro (Sep 15 2018 at 20:15):

this bound works on complexes too

Mario Carneiro (Sep 15 2018 at 20:16):

it is a special case of the tail bound on exp

Mario Carneiro (Sep 15 2018 at 20:17):

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

Mario Carneiro (Sep 15 2018 at 20:18):

when abs x <= 1

Patrick Massot (Sep 15 2018 at 20:19):

I need to go, sorry

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.

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.

Kenny Lau (Sep 15 2018 at 20:26):

you should go revise M1P1 :P

Chris Hughes (Sep 15 2018 at 20:26):

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

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

Mario Carneiro (Sep 15 2018 at 20:28):

here x is a complex number

Chris Hughes (Sep 15 2018 at 20:28):

I could probably manage that.

Chris Hughes (Sep 15 2018 at 20:29):

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

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

Kenny Lau (Sep 15 2018 at 20:30):

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

Mario Carneiro (Sep 15 2018 at 20:30):

maybe, but I'd prefer to defer it

Patrick Massot (Sep 17 2018 at 08:50):

@Chris Hughes are you currently working on exp?

Chris Hughes (Sep 17 2018 at 08:52):

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

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)

Johan Commelin (Sep 17 2018 at 18:13):

Well done!

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?

Johan Commelin (Sep 17 2018 at 18:15):

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

Johan Commelin (Sep 17 2018 at 18:15):

So maybe you should just leave this like it is.

Chris Hughes (Sep 17 2018 at 18:22):

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

Johan Commelin (Sep 17 2018 at 18:22):

Yes, agreed.

Chris Hughes (Sep 17 2018 at 18:22):

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

Kenny Lau (Sep 17 2018 at 18:26):

@Chris Hughes how much topology do you know?

Chris Hughes (Sep 17 2018 at 18:27):

More or less none.

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

Johan Commelin (Sep 17 2018 at 18:32):

Do we know that intervals are connected?

Johan Commelin (Sep 17 2018 at 18:32):

Does Lean even know what an interval is?

Reid Barton (Sep 17 2018 at 18:32):

I don't think we have connectedness yet

Reid Barton (Sep 17 2018 at 18:33):

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

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

Kenny Lau (Sep 17 2018 at 18:36):

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

Mario Carneiro (Sep 17 2018 at 18:42):

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

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))

Mario Carneiro (Sep 17 2018 at 18:46):

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

Mario Carneiro (Sep 17 2018 at 18:46):

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

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)

Chris Hughes (Sep 17 2018 at 19:10):

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

Johan Commelin (Sep 17 2018 at 19:12):

Right, you need the closed interval.

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))

Chris Hughes (Sep 17 2018 at 19:17):

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

Chris Hughes (Sep 17 2018 at 19:22):

Is it weaker or stronger than my assumption?

Johan Commelin (Sep 17 2018 at 19:24):

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

Mario Carneiro (Sep 17 2018 at 19:25):

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

Mario Carneiro (Sep 17 2018 at 19:25):

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

Chris Hughes (Sep 17 2018 at 19:26):

I see.

Johan Commelin (Sep 17 2018 at 19:26):

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

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

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

Chris Hughes (Sep 19 2018 at 17:27):

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

Mario Carneiro (Sep 19 2018 at 17:35):

that's weird, how did you prove it?

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

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

Mario Carneiro (Sep 19 2018 at 17:40):

Oh, you really did the case n=1 directly

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

Mario Carneiro (Sep 19 2018 at 17:41):

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

Chris Hughes (Sep 19 2018 at 17:41):

Not sure what the general case is.

Mario Carneiro (Sep 19 2018 at 17:42):

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

Mario Carneiro (Sep 19 2018 at 17:42):

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

Chris Hughes (Sep 19 2018 at 17:42):

That makes way more sense.

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?

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}

Chris Hughes (Sep 19 2018 at 19:40):

How do you get the bounds on cosine?

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

Chris Hughes (Sep 19 2018 at 19:42):

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

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.

Mario Carneiro (Sep 19 2018 at 20:04):

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

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

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

Kenny Lau (Sep 20 2018 at 13:19):

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

Kenny Lau (Sep 20 2018 at 13:19):

and you want to prove continuity at 0 first

Kenny Lau (Sep 20 2018 at 13:20):

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

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

Kenny Lau (Sep 20 2018 at 13:20):

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

Kenny Lau (Sep 20 2018 at 13:21):

so set delta = epsilon/exp(x)

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))

Mario Carneiro (Sep 20 2018 at 13:23):

the RHS looks right

Kenny Lau (Sep 20 2018 at 13:25):

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

Mario Carneiro (Sep 20 2018 at 13:29):

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

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

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

Patrick Massot (Sep 20 2018 at 14:28):

Wonderful! Can you get pi before tomorrow then?

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.

Patrick Massot (Sep 20 2018 at 14:30):

Did you push everything?

Patrick Massot (Sep 20 2018 at 14:31):

Doesn't seem so

Chris Hughes (Sep 20 2018 at 14:31):

Not yet

Patrick Massot (Sep 20 2018 at 14:31):

It would be easier to see what inequalities you have

Chris Hughes (Sep 20 2018 at 14:35):

Just pushing now

Reid Barton (Sep 20 2018 at 14:35):

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

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

Reid Barton (Sep 20 2018 at 14:43):

or maybe even squeeze_zero

Mario Carneiro (Sep 20 2018 at 14:44):

There should be a theorem about continuity on metric spaces

Mario Carneiro (Sep 20 2018 at 14:44):

continuous_of_metric

Mario Carneiro (Sep 20 2018 at 14:45):

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

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

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

Chris Hughes (Sep 20 2018 at 18:26):

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

Chris Hughes (Sep 20 2018 at 18:26):

How do I get continuity?

Kenny Lau (Sep 20 2018 at 18:27):

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

Mario Carneiro (Sep 20 2018 at 18:27):

do we know that C is a topological ring?

Chris Hughes (Sep 20 2018 at 18:28):

@Mario Carneiro yes

Kenny Lau (Sep 20 2018 at 18:29):

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

Kenny Lau (Sep 20 2018 at 18:29):

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

Kenny Lau (Sep 20 2018 at 18:29):

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

Chris Hughes (Sep 20 2018 at 18:30):

What lemmas are you applying Kenny?

Mario Carneiro (Sep 20 2018 at 18:30):

Ah, found it: continuous_mul is what you want

Mario Carneiro (Sep 20 2018 at 18:31):

to deduce the first of Kenny's statements

Mario Carneiro (Sep 20 2018 at 18:31):

wait no, tendsto_mul

Mario Carneiro (Sep 20 2018 at 18:32):

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

Mario Carneiro (Sep 20 2018 at 18:35):

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

Kenny Lau (Sep 20 2018 at 18:36):

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

Kenny Lau (Sep 20 2018 at 18:36):

would not recommend epsilon-delta to deduce 1

Mario Carneiro (Sep 20 2018 at 18:36):

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

Kenny Lau (Sep 20 2018 at 18:36):

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

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))

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.

Mario Carneiro (Sep 20 2018 at 18:42):

use exact

Mario Carneiro (Sep 20 2018 at 18:43):

apply will go crazy unfolding pis because of a bug

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))

Chris Hughes (Sep 20 2018 at 18:44):

I see the problem.

Chris Hughes (Sep 20 2018 at 18:44):

Silly me

Mario Carneiro (Sep 20 2018 at 18:45):

is that sarcasm? because I don't

Chris Hughes (Sep 20 2018 at 18:46):

x_1 instead of x on first line

Mario Carneiro (Sep 20 2018 at 18:49):

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

Chris Hughes (Sep 20 2018 at 18:51):

What's the lemma I use for composing with sub

Chris Hughes (Sep 20 2018 at 18:52):

tends.comp d'oh

Chris Hughes (Sep 20 2018 at 19:06):

This must be easy surely

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

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)))

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?

Mario Carneiro (Sep 20 2018 at 19:08):

yes

Mario Carneiro (Sep 20 2018 at 19:09):

that's the easiest way, at least

Chris Hughes (Sep 20 2018 at 19:20):

exp is continuous is now a fact.

Kenny Lau (Sep 20 2018 at 19:22):

how much time do we still have?

Patrick Massot (Sep 20 2018 at 19:27):

Here it's 9:27pm

Patrick Massot (Sep 20 2018 at 19:28):

So 8:27pm in London

Patrick Massot (Sep 20 2018 at 19:28):

So we have 12 hours

Patrick Massot (Sep 20 2018 at 19:28):

roughly

Patrick Massot (Sep 20 2018 at 19:29):

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

Chris Hughes (Sep 20 2018 at 19:43):

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

Mario Carneiro (Sep 20 2018 at 19:43):

continuity of real part

Mario Carneiro (Sep 20 2018 at 19:43):

and continuity of real injection

Mario Carneiro (Sep 20 2018 at 19:44):

How did you define real.sin?

Patrick Massot (Sep 20 2018 at 19:52):

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

Chris Hughes (Sep 20 2018 at 19:52):

(complex.sin x).re

Patrick Massot (Sep 20 2018 at 19:53):

So continuity should indeed follow as Mario wrote

Chris Hughes (Sep 20 2018 at 19:53):

I couldn't find continuous_re

Patrick Massot (Sep 20 2018 at 19:54):

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

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

Mario Carneiro (Sep 20 2018 at 20:04):

abs_re_le_abs

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.

Patrick Massot (Sep 20 2018 at 20:25):

How far are you from pi then?

Chris Hughes (Sep 20 2018 at 20:26):

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

Patrick Massot (Sep 20 2018 at 20:29):

So, who's writing to Kevin tomorrow?

Chris Hughes (Sep 20 2018 at 20:46):

def pi :  := 2 * classical.some exists_cos_eq_zero

Kenny Lau (Sep 20 2018 at 20:47):

then pi can be 3*3.14...?

Mario Carneiro (Sep 20 2018 at 20:47):

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

Chris Hughes (Sep 20 2018 at 20:49):

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

Kenny Lau (Sep 20 2018 at 20:49):

fair enough

Mario Carneiro (Sep 20 2018 at 20:49):

also sin (pi/2) = 1

Mario Carneiro (Sep 20 2018 at 20:49):

the rest should be easy

Kenny Lau (Sep 20 2018 at 20:49):

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

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

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

Chris Hughes (Sep 20 2018 at 20:52):

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

Mario Carneiro (Sep 20 2018 at 20:53):

yes, it's mostly smooth sailing at this point

Chris Hughes (Sep 20 2018 at 20:53):

I pushed.

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

Kenny Lau (Sep 20 2018 at 21:04):

although I will wake up 4 hours later

Mario Carneiro (Sep 20 2018 at 21:04):

ooh, you are 12 hours away from me

Kevin Buzzard (Sep 20 2018 at 23:10):

I've been 50 for about 10 minutes

Chris Hughes (Sep 20 2018 at 23:11):

Happy Birthday!

Kevin Buzzard (Sep 20 2018 at 23:11):

Holey Moley we have pi!

Kevin Buzzard (Sep 20 2018 at 23:11):

I am so happy!

Kevin Buzzard (Sep 20 2018 at 23:13):

I need to go to bed!


Last updated: Dec 20 2023 at 11:08 UTC