sine and cosine and pi

Stream: kbb

[Chris Hughes]

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]

Do you have complex exp or only real?

[Chris Hughes]

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

[Patrick Massot]

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

[Johan Commelin]

You're such a mathematician.

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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]

Rights, so we need continuity of exp.

[Johan Commelin]

For either definition.

[Patrick Massot]

I both cases yes

[Johan Commelin]

What is the best way to do this continuity proof?

[Johan Commelin]

Generalise to arbitrary power series?

[Patrick Massot]

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]

I like your second definition.

[Johan Commelin]

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

[Reid Barton]

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

[Johan Commelin]

Ok, sounds good.

[Reid Barton]

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

[Patrick Massot]

indeed we must exclude that the kernel is trivial

[Reid Barton]

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

[Patrick Massot]

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

[Reid Barton]

Okay--if $\cos t$ was positive everywhere then $\sin t$ would be increasing, and then $\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]

This all looks super tedious

[Patrick Massot]

Let's do perfectoid spaces

[Johan Commelin]

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

[Johan Commelin]

But how do I put this into Lean?

[Patrick Massot]

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

[Johan Commelin]

Aah thanks, that indeed looks useful.

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

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

[Chris Hughes]

We do know exp \ne 0

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

there is

[Johan Commelin]

Ooh, my VScode didn't find it.

[Johan Commelin]

Let me try again

[Johan Commelin]

Aah, it only has squeeze in its docstring

[Johannes Hölzl]

grep for sandwich in mathlib

[Patrick Massot]

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

[Patrick Massot]

grep for squeeze also works

[Patrick Massot]

but grep for gendarme doesn't work

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

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

[Johan Commelin]

So, should we create power_series.lean on cocalc?

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

I'm quite addicted to that experience.

[Patrick Massot]

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]

I will take a look

[Johannes Hölzl]

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]

The lemma termdiffs assumes that various power series converge.

[Johan Commelin]

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]

Is that right?

[Johan Commelin]

I mean, there won't change that much

[Johannes Hölzl]

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

[Johan Commelin]

Ok, and this is purely algebraic stuff, right?

[Johan Commelin]

Or do you also mean the analytic derivative?

[Johannes Hölzl]

I guess we need to analytic derivative to prove continuity

[Johan Commelin]

Hmmm, ok

[Johan Commelin]

And we really need all of this to define pi?

[Johan Commelin]

Well, we will need this stuff anyway

[Johan Commelin]

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

[Johannes Hölzl]

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]

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

[Johannes Hölzl]

of course

[Johannes Hölzl]

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

[Johannes Hölzl]

it uses IVT

[Johan Commelin]

Right, so we need continuity

[Johannes Hölzl]

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

[Johan Commelin]

Ok

[Chris Hughes]

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]

@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]

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]

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]

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]

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]

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

[Mario Carneiro]

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

[Chris Hughes]

How do I state continuous at a point?

[Mario Carneiro]

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

[Chris Hughes]

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

[Chris Hughes]

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

[Patrick Massot]

I think I already answered that earlier today

[Chris Hughes]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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]

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

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

[Mario Carneiro]

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

[Patrick Massot]

The name is bad, but the statement is ok

[Patrick Massot]

assuming you know exp 0

[Mario Carneiro]

that's true, it should say tendsto_exp_zero or something

[Patrick Massot]

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

[Chris Hughes]

And this only works for real.exp right?

[Patrick Massot]

Why?

[Patrick Massot]

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

[Chris Hughes]

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]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Patrick Massot]

but he seems to have a new idea

[Mario Carneiro]

this bound works on complexes too

[Mario Carneiro]

it is a special case of the tail bound on exp

[Mario Carneiro]

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

[Mario Carneiro]

when abs x <= 1

[Patrick Massot]

I need to go, sorry

[Chris Hughes]

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]

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]

you should go revise M1P1 :P

[Chris Hughes]

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

[Mario Carneiro]

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

[Mario Carneiro]

here x is a complex number

[Chris Hughes]

I could probably manage that.

[Chris Hughes]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

maybe, but I'd prefer to defer it

[Patrick Massot]

@Chris Hughes are you currently working on exp?

[Chris Hughes]

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

[Chris Hughes]

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, hδ⟩ := 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 hδ (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 (hδ $ 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 _)
                    (@hδ 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]

Well done!

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

So maybe you should just leave this like it is.

[Chris Hughes]

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

[Johan Commelin]

Yes, agreed.

[Chris Hughes]

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

[Kenny Lau]

@Chris Hughes how much topology do you know?

[Chris Hughes]

More or less none.

[Kenny Lau]

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]

Do we know that intervals are connected?

[Johan Commelin]

Does Lean even know what an interval is?

[Reid Barton]

I don't think we have connectedness yet

[Reid Barton]

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

[Reid Barton]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Chris Hughes]

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, hδ⟩ := 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 hδ (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 (hδ $ 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 _)
                    (@hδ 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]

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

[Johan Commelin]

Right, you need the closed interval.

[Mario Carneiro]

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]

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

[Chris Hughes]

Is it weaker or stronger than my assumption?

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Chris Hughes]

I see.

[Johan Commelin]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

that's weird, how did you prove it?

[Mario Carneiro]

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

[Chris Hughes]

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]

Oh, you really did the case n=1 directly

[Mario Carneiro]

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

[Mario Carneiro]

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

[Chris Hughes]

Not sure what the general case is.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Chris Hughes]

That makes way more sense.

[Reid Barton]

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]

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]

How do you get the bounds on cosine?

[Chris Hughes]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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]

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

[Kenny Lau]

and you want to prove continuity at 0 first

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

so set delta = epsilon/exp(x)

[Mario Carneiro]

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]

the RHS looks right

[Kenny Lau]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

Wonderful! Can you get pi before tomorrow then?

[Chris Hughes]

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]

Did you push everything?

[Patrick Massot]

Doesn't seem so

[Chris Hughes]

Not yet

[Patrick Massot]

It would be easier to see what inequalities you have

[Chris Hughes]

Just pushing now

[Reid Barton]

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

[Reid Barton]

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]

or maybe even squeeze_zero

[Mario Carneiro]

There should be a theorem about continuity on metric spaces

[Mario Carneiro]

continuous_of_metric

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Chris Hughes]

How do I get continuity?

[Kenny Lau]

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

[Mario Carneiro]

do we know that C is a topological ring?

[Chris Hughes]

@Mario Carneiro yes

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Chris Hughes]

What lemmas are you applying Kenny?

[Mario Carneiro]

Ah, found it: continuous_mul is what you want

[Mario Carneiro]

to deduce the first of Kenny's statements

[Mario Carneiro]

wait no, tendsto_mul

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

would not recommend epsilon-delta to deduce 1

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

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]

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]

use exact

[Mario Carneiro]

apply will go crazy unfolding pis because of a bug

[Chris Hughes]

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]

I see the problem.

[Chris Hughes]

Silly me

[Mario Carneiro]

is that sarcasm? because I don't

[Chris Hughes]

x_1 instead of x on first line

[Mario Carneiro]

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

[Chris Hughes]

What's the lemma I use for composing with sub

[Chris Hughes]

tends.comp d'oh

[Chris Hughes]

This must be easy surely

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

yes

[Mario Carneiro]

that's the easiest way, at least

[Chris Hughes]

exp is continuous is now a fact.

[Kenny Lau]

how much time do we still have?

[Patrick Massot]

Here it's 9:27pm

[Patrick Massot]

So 8:27pm in London

[Patrick Massot]

So we have 12 hours

[Patrick Massot]

roughly

[Patrick Massot]

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

[Chris Hughes]

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

[Mario Carneiro]

continuity of real part

[Mario Carneiro]

and continuity of real injection

[Mario Carneiro]

How did you define real.sin?

[Patrick Massot]

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

[Chris Hughes]

(complex.sin x).re

[Patrick Massot]

So continuity should indeed follow as Mario wrote

[Chris Hughes]

I couldn't find continuous_re

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

abs_re_le_abs

[Chris Hughes]

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

[Patrick Massot]

How far are you from pi then?

[Chris Hughes]

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

[Patrick Massot]

So, who's writing to Kevin tomorrow?

[Chris Hughes]

def pi : ℝ := 2 * classical.some exists_cos_eq_zero

[Kenny Lau]

then pi can be 3*3.14...?

[Mario Carneiro]

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

[Chris Hughes]

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

[Kenny Lau]

fair enough

[Mario Carneiro]

also sin (pi/2) = 1

[Mario Carneiro]

the rest should be easy

[Kenny Lau]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Chris Hughes]

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

[Mario Carneiro]

yes, it's mostly smooth sailing at this point

[Chris Hughes]

I pushed.

[Kenny Lau]

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

[Kenny Lau]

although I will wake up 4 hours later

[Mario Carneiro]

ooh, you are 12 hours away from me

[Kevin Buzzard]

I've been 50 for about 10 minutes

[Chris Hughes]

Happy Birthday!

[Kevin Buzzard]

Holey Moley we have pi!

[Kevin Buzzard]

I am so happy!

[Kevin Buzzard]

I need to go to bed!