Bounds on alternating convergent series

Stream: Is there code for X?

[Jeremy Tan]

#9847 proves John Machin's 1706 formula for π, but that's just the formula. What he then did was exploit the Taylor series of the arctangent (Taylor was Machin's contemporary) to compute π to 100 decimal places.

Suppose we reproduced his calculation in mathlib. At some point we would be using the following well-known three-part theorem:

1. Any alternating series where the term magnitude strictly decreases is convergent.
2. Every partial sum ending at a negative term is a lower bound on the limiting value.
3. Every partial sum ending at a positive term is an upper bound on the limiting value.

Do we have any of these three parts in mathlib, for general alternating series?

[Mario Carneiro]

we have the leibniz formula for pi, which should contain all the same components

[Yury G. Kudryashov]

I remember that there was a PR about alternating series. I don't remember if it landed.

[Yury G. Kudryashov]

We have docs#Monotone.cauchySeq_alternating_series_of_tendsto_zero and the next few lemmas for the first item.

[Yury G. Kudryashov]

AFAICS, we don't have the other two.

[Yury G. Kudryashov]

Though it's probably hidden inside the proof.

[Joseph Myers]

The Taylor series for arctan is hidden inside the proof; we don't have it as a separate theorem. (I've previously suggested that the Leibniz formula for pi should be deduced by combining the Taylor series for arctan with Abel's theorem, neither of which we currently have as a separate theorem in mathlib.)

[Jeremy Tan]

In any case I wrote #9889 which defines the complex arctangent and shows its Taylor series expansion

[Jeremy Tan]

@Joseph Myers is this a correct statement of Abel's theorem?

import Mathlib

open Filter Set

open scoped Classical BigOperators Topology Real

theorem abels_theorem (f : ℕ → ℝ) (g : ℝ → ℝ)
    (hf : ∃ l, Tendsto (fun n ↦ ∑ i in Finset.range n, f n) atTop (𝓝 l))
    (h : ∀ x : ℝ, |x| < 1 → Tendsto (fun n ↦ ∑ i in Finset.range n, f n * x ^ n) atTop (𝓝 (g x)))
    (l : ℝ) (hg : Tendsto g (𝓝[<] 1) (𝓝 l)) :
    Tendsto (fun n ↦ ∑ i in Finset.range n, f n) atTop (𝓝 l) := by
  sorry

[Michael Stoll]

There is also a version for functions on the complex unit disk; see Wikipedia. The convergence within the "Stolz sector" can be conveniently expressed via a nhdsWithin filter, I think.

[Jeremy Tan]

import Mathlib

open Filter Set

open scoped Classical BigOperators Topology Real Complex

def stolzSector (M : ℝ) : Filter ℂ :=
  nhdsWithin 1 {z | ‖1 - z‖ < M * (1 - ‖z‖)}

theorem abels_theorem {f : ℕ → ℂ} {g : ℂ → ℂ}
    (h : ∀ z, ‖z‖ < 1 → Tendsto (fun n ↦ ∑ i in Finset.range n, f n * z ^ n) atTop (𝓝 (g z)))
    (hf : ∃ l, Tendsto (fun n ↦ ∑ i in Finset.range n, f n) atTop (𝓝 l))
    {l : ℂ} {M : ℝ} (hg : Tendsto g (stolzSector M) (𝓝 l)) (hM : 1 < M) :
    Tendsto (fun n ↦ ∑ i in Finset.range n, f n) atTop (𝓝 l) := by
  sorry

[Michael Stoll]

I think this does not exactly capture the assumptions. I would perhaps write it as

import Mathlib

open Filter Set

open scoped Classical BigOperators Topology Real Complex

def stolzSector (M : ℝ) : Filter ℂ :=
  nhdsWithin 1 {z | ‖1 - z‖ < M * (1 - ‖z‖)}

theorem abels_theorem {f : ℕ → ℂ} (M : ℝ) {l : ℂ} (h : Tendsto (fun n ↦ ∑ i in Finset.range n, f n) atTop (𝓝 l)) :
    Tendsto (fun z ↦ tsum (fun n ↦ f n * z ^ n)) (stolzSector M) (𝓝 l) := by
  sorry

The assumption is that the power series converges at z = 1 (which implies that it converges absolutely on the open unit disk), and the statement is that one can swap the two limits involved.

[Jeremy Tan]

Your formulation is begging the question with regards to replacing the ad-hoc proof in Data.Real.Pi.Leibniz. The central theorem there is precisely your hypothesis h

[Jeremy Tan]

Abel's theorem is intended to give you l, not ask l from you at the start

[Jeremy Tan]

Perhaps you swapped the hypothesis and statement?

[Michael Stoll]

I think what I wrote is a faithful translation of the statement as given on the Wikipedia page.
To use it, you only need the existence of l (I don't think we have an analogue of Summable (yet?) in this context; otherwise one could write the hypothesis in terms of that). You can then define g as the value of the power series (on the open unit disk), and then the theorem tells you that its limit (within a Stolz sector) is the same as the value of the power series at 1 (which was l). I.e., with the right notions, we could write

theorem abels_theorem {f : ℕ → ℂ} (M : ℝ) (h : Summable' f) :
    Tendsto (fun z ↦ tsum (fun n ↦ f n * z ^ n)) (stolzSector M) (𝓝 (tsum' f))

where Summable' says that the series with terms f n converges (conditionally) and tsum' f is the value of the series.

[Michael Stoll]

And so, if you know that Tendsto g (stolzSector M) (𝓝 l), you can conclude that tsum' f = l.

[Michael Stoll]

(Note that a hypothesis (h : ∃ x : T, P x) is completely equivalent to (x : T) (h : P x), and g can be eliminated from your statement, since it can be defined in terms of f.)

[Jeremy Tan]

Michael Stoll said:

I.e., with the right notions, we could write

theorem abels_theorem {f : ℕ → ℂ} (M : ℝ) (h : Summable' f) :
    Tendsto (fun z ↦ tsum (fun n ↦ f n * z ^ n)) (stolzSector M) (𝓝 (tsum' f))

where Summable' says that the series with terms f n converges (conditionally) and tsum' f is the value of the series.

theorem abels_theorem {f : ℕ → ℂ} (h : CauchySeq fun n => ∑ i in range n, f i) (M : ℝ) :
    Tendsto (fun z ↦ ∑' n, f n * z ^ n) (stolzSector M)
      (𝓝 (cauchySeq_tendsto_of_complete h).choose) := by
  sorry

[Jeremy Tan]

Since ℂ is complete, the CauchySeq hypothesis is equivalent to conditional convergence

[Jeremy Tan]

Apparently I need to show this theorem first

import Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

open Filter Finset Complex
open scoped BigOperators Topology

lemma yyz {f : ℕ → ℂ} {l : ℂ} (h : Tendsto (fun n ↦ ∑ i in range n, f n) atTop (𝓝 l))
    {z : ℂ} (hz : ‖z‖ < 1) : Summable (fun n ↦ f n * z ^ n) := by
  sorry

[Michael Stoll]

I think the way to get that is to first show that f is bounded (from h) and then use comparison with the geometric series.

[Yury G. Kudryashov]

You can use docs#Filter.Tendsto.isBigO_one, multiply it by docs#Asymptotics.isBigO_refl, then use docs#summable_of_isBigO_nat

[Yury G. Kudryashov]

You may want to add IsBigO.smul_summable to the library.

[Jeremy Tan]

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecificLimits.Normed

-- https://planetmath.org/proofofabelslimittheorem

open Filter Finset Complex
open scoped BigOperators Topology

def stolzSector (M : ℝ) : Filter ℂ :=
  nhdsWithin 1 {z | ‖1 - z‖ ≤ M * (1 - ‖z‖)}

variable {f : ℕ → ℂ} {l : ℂ} (h : Tendsto (fun n ↦ ∑ i in range n, f i) atTop (𝓝 l))

/-- The term norms of any convergent series are bounded by some universal constant. -/
lemma norm_bounded_of_tendsto : ∃ C, ∀ n, ‖f n‖ ≤ C := by
  obtain ⟨b, ⟨_, key, _⟩⟩ := cauchySeq_iff_le_tendsto_0.mp h.cauchySeq
  refine' ⟨b 0, fun n ↦ _⟩
  replace key := key n (n + 1) 0 (zero_le _) (zero_le _)
  rwa [dist_partial_sum'] at key

/-- The power series associated with any convergent series is _absolutely_ convergent
in the open unit disc. -/
lemma summable_mul_geometric_of_tendsto {z : ℂ} (hz : ‖z‖ < 1) :
    Summable (fun n ↦ f n * z ^ n) := by
  obtain ⟨C, hC⟩ := norm_bounded_of_tendsto h
  refine' Summable.of_norm_bounded (fun n ↦ C * ‖z‖ ^ n)
    ((summable_geometric_of_abs_lt_1 (by simpa)).mul_left C) (fun n ↦ _)
  simp_rw [norm_mul, norm_pow]
  gcongr
  exact hC n

[Michael Stoll]

It would be nice to also have the version for general radius of convergence (which can either be reduced to your special case or proved directly). I.e., convergence of the power series at some w implies absolute convergence at all z such that ‖z‖ < ‖w‖.

[Jeremy Tan]

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecificLimits.Normed

open Finset Complex
open scoped BigOperators

/-- The power series associated with any convergent series is _absolutely_ convergent
in the open unit disc. -/
lemma summable_power_of_cauchy_series {f : ℕ → ℂ}
    (h : CauchySeq fun n ↦ ∑ k in range n, f k) {z : ℂ} (hz : ‖z‖ < 1) :
    Summable fun n ↦ f n * z ^ n := by
  obtain ⟨C, hC⟩ := norm_bounded_of_cauchy_series h
  rw [summable_iff_cauchySeq_finset]
  refine' cauchySeq_finset_of_geometric_bound (C := C) hz (fun n ↦ _)
  simp_rw [norm_mul, norm_pow]
  gcongr
  exact hC n

/-- If a power series converges at `w`, it converges _absolutely_ for all `z` of lesser norm. -/
lemma summable_power_of_norm_lt {f : ℕ → ℂ} {w : ℂ}
    (h : CauchySeq fun n ↦ ∑ i in range n, f i * w ^ i) {z : ℂ} (hz : ‖z‖ < ‖w‖) :
    Summable fun n ↦ f n * z ^ n := by
  cases' (norm_nonneg w).eq_or_gt with hw hw
  · exact absurd ((norm_nonneg z).trans_lt (hw ▸ hz)) (lt_irrefl 0)
  have := @summable_power_of_cauchy_series _ h (z / w) (by rwa [norm_div, div_lt_one hw])
  rw [norm_eq_abs, AbsoluteValue.pos_iff] at hw
  simp_rw [mul_assoc, ← mul_pow, mul_div_cancel' _ hw] at this
  exact this

[Jeremy Tan]

The above two lemmas are now at #9955

[Michael Stoll]

This looks good to me. Maybe someone better versed in the naming conventions can have a look at the lemma names? There is docs#cauchy_series_of_le_geometric, so I would think the "cauchy_series" part is OK. We have docs#PowerSeries, so I would think that "powerSeries" instead of just "power" would be more appropriate in the names (even though the lemmas do not talk about terms of type PowerSeries).

Do we have the radius of convergence of a (univariate) power series and API for it?
@loogle PowerSeries, HasSum

[loogle]

:shrug: nothing found

[Michael Stoll]

@loogle PowerSeries, Summable

[loogle]

:shrug: nothing found

[Michael Stoll]

Maybe not :frown:

[Jeremy Tan]

I should have proven Abel's limit theorem as you stated it at branch#abellimit

[Jeremy Tan]

(haven't made a PR for it because I want that to be #10000)

[Michael Stoll]

I wonder whether there might not be a more elegant proof using filters instead of epsilons...

[Jeremy Tan]

Probably not @Michael Stoll. Anyway, #10000 it is

[Jeremy Tan]

I've extended #10000 to cover the real case

[Jeremy Tan]

But surely there's a simpler way to prove this sub-theorem?

have m : (𝓝 l).map ((↑) : ℝ → ℂ) ≤ (𝓝 ↑l) := by
    intro s hs
    rw [Filter.mem_map']
    rw [Metric.mem_nhds_iff] at hs ⊢
    obtain ⟨ε, ⟨εpos, hε⟩⟩ := hs
    use ε, εpos
    intro x hx
    rw [Set.subset_def] at hε
    replace hε := hε x
    rw [Metric.mem_ball, dist_eq_norm] at hε hx
    norm_cast at hε
    rw [Complex.norm_real] at hε
    simp [hε hx]

[Michael Stoll]

Combine docs#Complex.ofRealCLM, docs#ContinuousLinearMap.continuous and docs#Continuous.tendsto ? (This does not give exactly what you want, but is maybe close to what you actually need).
(I have some other commitments now and cannot think about that in more detail.)

[Jeremy Tan]

Well now that you mentioned the CLM, it's a two-liner

have m := ofRealCLM.continuous.tendsto l
  rw [show ⇑ofRealCLM = ofReal' by rfl, tendsto_iff_comap, ← map_le_iff_le_comap] at m

[Jeremy Tan]

There's still https://github.com/leanprover-community/mathlib4/pull/10000/files#diff-35646e039986d92194e3a69478b379c60384711e9bb937bee97d74e1dcb73439R73 though

[Michael Stoll]

I've suggested a shorter proof of nhdsWithin_lt_le_nhdsWithin_stolzSet.

[Yury G. Kudryashov]

Jeremy Tan said:

Well now that you mentioned the CLM, it's a two-liner

have m := ofRealCLM.continuous.tendsto l
  rw [show ⇑ofRealCLM = ofReal' by rfl, tendsto_iff_comap, ← map_le_iff_le_comap] at m

In fact, Tendsto is defeq to map _ ≤ _, so it's just ofRealCLM.continuous.tendsto

[Jeremy Tan]

I finally proved the thing I originally wanted to prove at #10120

[Jeremy Tan]

@Michael Stoll I have absolutely no idea how to address @Sébastien Gouëzel's comment on #10000, regarding turning the Stolz set filter into a cone filter. Please help

[Jeremy Tan]

Apparently I have to import Euclidean geometry in order to show that every cone filter lies below some Stolz set filter

[Jeremy Tan]

(which would be importing too much)

[Michael Stoll]

@Jeremy Tan I'm at a conference until Friday and won't have much time before the weekend, but I'll try to have a look then.

[Jeremy Tan]

Well I actually did prove the cone version... using a ton of Euclidean geometry

[Jeremy Tan]

@Michael Stoll ummm...

[Michael Stoll]

Here is an alternative approach:

import Mathlib.Analysis.Complex.Basic

section StolzSet

-- This (or a more general version with real exponent `0 ≤ r ≤ 1`) seems to be missing in Mathlib.
lemma Real.sqrt_one_add_le {x : ℝ} (hx : -1 ≤ x) : sqrt (1 + x) ≤ 1 + x / 2 := by
  refine sqrt_le_iff.mpr ⟨by linarith, ?_⟩
  calc 1 + x
    _ ≤ 1 + x + (x / 2) ^ 2 := le_add_of_nonneg_right <| sq_nonneg _
    _ = (1 + x / 2) ^ 2 := by ring

-- An ugly technical lemma
open Real in
private lemma Complex.stolzCone'_subset_StolzSet_aux (s : ℝ) :
    ∃ M ε, 0 < M ∧ 0 < ε ∧ ∀ x y, 0 < x → x < ε → |y| < s * x →
      sqrt (x ^ 2 + y ^ 2) < M * (1 - sqrt ((1 - x) ^ 2 + y ^ 2)) := by
  refine ⟨2 * sqrt (1 + s ^ 2) + 1, 1 / (1 + s ^ 2), by positivity, by positivity,
    fun x y hx₀ hx₁ hy ↦ ?_⟩
  have H : sqrt ((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
  · calc sqrt ((1 - x) ^ 2 + y ^ 2)
      _ ≤ sqrt ((1 - x) ^ 2 + (s * x) ^ 2) := sqrt_le_sqrt <| by rw [← _root_.sq_abs y]; gcongr
      _ = sqrt (1 - 2 * x + (1 + s ^ 2) * x * x) := by congr 1; ring
      _ ≤ sqrt (1 - 2 * x + (1 + s ^ 2) * (1 / (1 + s ^ 2)) * x) := sqrt_le_sqrt <| by gcongr
      _ = sqrt (1 - x) := by congr 1; field_simp; ring
      _ ≤ 1 - x / 2 := by
        simp_rw [sub_eq_add_neg, ← neg_div]
        refine sqrt_one_add_le <| neg_le_neg_iff.mpr (hx₁.trans_le ?_).le
        rw [div_le_one (by positivity)]
        exact le_add_of_nonneg_right <| sq_nonneg s
  calc sqrt (x ^ 2 + y ^ 2)
    _ ≤ sqrt (x ^ 2 + (s * x) ^ 2) := sqrt_le_sqrt <| by rw [← _root_.sq_abs y]; gcongr
    _ = sqrt ((1 + s ^ 2) * x ^ 2) := by congr; ring
    _ = sqrt (1 + s ^ 2) * x := by rw [sqrt_mul' _ (sq_nonneg x), sqrt_sq hx₀.le]
    _ = 2 * sqrt (1 + s ^ 2) * (x / 2) := by ring
    _ < (2 * sqrt (1 + s ^ 2) + 1) * (x / 2) := by gcongr; exact lt_add_one _
    _ ≤ _ := by gcongr; exact le_sub_comm.mpr H

namespace Complex

-- This seems to be missing in Mathlib.
lemma abs_eq_sqrt_sq_add_sq (z : ℂ) : abs z = Real.sqrt (z.re ^ 2 + z.im ^ 2) := by
  rw [abs_apply, normSq_apply, sq, sq]

/-- The Stolz set for a given `M`, roughly teardrop-shaped with the tip at 1 but tending to the
open unit disc as `M` tends to infinity. -/
def stolzSet (M : ℝ) : Set ℂ := {z | ‖z‖ < 1 ∧ ‖1 - z‖ < M * (1 - ‖z‖)}

-- /-- The cone around 1 with angle `2θ`. -/
-- def stolzCone (θ : ℝ) : Set ℂ := {z | ‖1 - z‖ ≠ 0 ∧ |arg (1 - z)| < θ}

/-- The cone to the left of `1` with angle `2 θ` such that `tan θ = s`. -/
def stolzCone' (s : ℝ) : Set ℂ := {z | |z.im| < s * (1 - z.re)}

lemma stolzCone'_subset_StolzSet_aux' {s : ℝ} (hs : 0 < s) :
    ∃ M ε, 0 < M ∧ 0 < ε ∧ {z : ℂ | 1 - ε < z.re} ∩ stolzCone' s ⊆ stolzSet M := by
  peel stolzCone'_subset_StolzSet_aux s with M ε hM hε H
  rintro z ⟨hzl, hzr⟩
  rw [Set.mem_setOf_eq, sub_lt_comm, ← one_re, ← sub_re] at hzl
  rw [stolzCone', Set.mem_setOf_eq, ← one_re, ← sub_re] at hzr
  replace H :=
    H (1 - z).re z.im ((mul_pos_iff_of_pos_left hs).mp <| (abs_nonneg z.im).trans_lt hzr) hzl hzr
  have h : z.im ^ 2 = (1 - z).im ^ 2
  · simp only [sub_im, one_im, zero_sub, even_two, neg_sq]
  rw [h, ← abs_eq_sqrt_sq_add_sq, ← norm_eq_abs, ← h, sub_re, one_re, sub_sub_cancel,
    ← abs_eq_sqrt_sq_add_sq, ← norm_eq_abs] at H
  exact ⟨sub_pos.mp <| (mul_pos_iff_of_pos_left hM).mp <| (norm_nonneg _).trans_lt H, H⟩

open Topology

lemma  nhdsWithin_stolzCone'_le_nhdsWithin_stolzSet {s : ℝ} (hs : 0 < s) :
    ∃ M, 𝓝[stolzCone' s] 1 ≤ 𝓝[stolzSet M] 1 := by
  obtain ⟨M, ε, _, hε, H⟩ := stolzCone'_subset_StolzSet_aux' hs
  use M
  rw [nhdsWithin_le_iff, mem_nhdsWithin]
  refine ⟨{w | 1 - ε < w.re}, isOpen_lt continuous_const continuous_re, ?_, H⟩
  simp only [Set.mem_setOf_eq, one_re, sub_lt_self_iff, hε]

[Michael Stoll]

@Jeremy Tan :up:

[Jeremy Tan]

@Michael Stoll done!

[Jeremy Tan]

Is there anyone else available to review #10000?

[Jeremy Tan]

Joseph Myers said:

The Taylor series for arctan is hidden inside the proof; we don't have it as a separate theorem. (I've previously suggested that the Leibniz formula for pi should be deduced by combining the Taylor series for arctan with Abel's theorem, neither of which we currently have as a separate theorem in mathlib.)

#11098

[Jeremy Tan]

And #11098 is merged. I have now merged everything I initially wanted to merge