From f7b82ea8816c854dd332e1d1a86c904b6eb4165b Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Sat, 2 Mar 2024 15:23:26 +0800 Subject: [PATCH 1/7] =?UTF-8?q?feat:=20prove=20Leibniz=20=CF=80=20series?= =?UTF-8?q?=20with=20Abel's=20limit=20theorem?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/Analysis/SpecificLimits/Normed.lean | 20 ++- Mathlib/Data/Real/Pi/Leibniz.lean | 171 ++++++-------------- 2 files changed, 65 insertions(+), 126 deletions(-) diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean index b6c4153a2ec26..79d78dc45e384 100644 --- a/Mathlib/Analysis/SpecificLimits/Normed.lean +++ b/Mathlib/Analysis/SpecificLimits/Normed.lean @@ -631,7 +631,15 @@ variable {b : ℝ} {f : ℕ → ℝ} {z : ℕ → E} /-- **Dirichlet's Test** for monotone sequences. -/ theorem Monotone.cauchySeq_series_mul_of_tendsto_zero_of_bounded (hfa : Monotone f) (hf0 : Tendsto f atTop (𝓝 0)) (hgb : ∀ n, ‖∑ i in range n, z i‖ ≤ b) : - CauchySeq fun n ↦ ∑ i in range (n + 1), f i • z i := by + CauchySeq fun n ↦ ∑ i in range n, f i • z i := by + suffices CauchySeq fun n ↦ ∑ i in range (n + 1), f i • z i by + rw [Metric.cauchySeq_iff] at this ⊢ + intro ε hε + replace this := this ε hε + obtain ⟨N, this⟩ := this + use N + 1 + intro m hm n hn + convert this (m - 1) (by omega) (n - 1) (by omega) <;> omega simp_rw [Finset.sum_range_by_parts _ _ (Nat.succ _), sub_eq_add_neg, Nat.succ_sub_succ_eq_sub, tsub_zero] apply (NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded hf0 @@ -650,7 +658,7 @@ theorem Monotone.cauchySeq_series_mul_of_tendsto_zero_of_bounded (hfa : Monotone /-- **Dirichlet's test** for antitone sequences. -/ theorem Antitone.cauchySeq_series_mul_of_tendsto_zero_of_bounded (hfa : Antitone f) (hf0 : Tendsto f atTop (𝓝 0)) (hzb : ∀ n, ‖∑ i in range n, z i‖ ≤ b) : - CauchySeq fun n ↦ ∑ i in range (n + 1), f i • z i := by + CauchySeq fun n ↦ ∑ i in range n, f i • z i := by have hfa' : Monotone fun n ↦ -f n := fun _ _ hab ↦ neg_le_neg <| hfa hab have hf0' : Tendsto (fun n ↦ -f n) atTop (𝓝 0) := by convert hf0.neg @@ -668,7 +676,7 @@ theorem norm_sum_neg_one_pow_le (n : ℕ) : ‖∑ i in range n, (-1 : ℝ) ^ i /-- The **alternating series test** for monotone sequences. See also `Monotone.tendsto_alternating_series_of_tendsto_zero`. -/ theorem Monotone.cauchySeq_alternating_series_of_tendsto_zero (hfa : Monotone f) - (hf0 : Tendsto f atTop (𝓝 0)) : CauchySeq fun n ↦ ∑ i in range (n + 1), (-1) ^ i * f i := by + (hf0 : Tendsto f atTop (𝓝 0)) : CauchySeq fun n ↦ ∑ i in range n, (-1) ^ i * f i := by simp_rw [mul_comm] exact hfa.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0 norm_sum_neg_one_pow_le #align monotone.cauchy_seq_alternating_series_of_tendsto_zero Monotone.cauchySeq_alternating_series_of_tendsto_zero @@ -676,14 +684,14 @@ theorem Monotone.cauchySeq_alternating_series_of_tendsto_zero (hfa : Monotone f) /-- The **alternating series test** for monotone sequences. -/ theorem Monotone.tendsto_alternating_series_of_tendsto_zero (hfa : Monotone f) (hf0 : Tendsto f atTop (𝓝 0)) : - ∃ l, Tendsto (fun n ↦ ∑ i in range (n + 1), (-1) ^ i * f i) atTop (𝓝 l) := + ∃ l, Tendsto (fun n ↦ ∑ i in range n, (-1) ^ i * f i) atTop (𝓝 l) := cauchySeq_tendsto_of_complete <| hfa.cauchySeq_alternating_series_of_tendsto_zero hf0 #align monotone.tendsto_alternating_series_of_tendsto_zero Monotone.tendsto_alternating_series_of_tendsto_zero /-- The **alternating series test** for antitone sequences. See also `Antitone.tendsto_alternating_series_of_tendsto_zero`. -/ theorem Antitone.cauchySeq_alternating_series_of_tendsto_zero (hfa : Antitone f) - (hf0 : Tendsto f atTop (𝓝 0)) : CauchySeq fun n ↦ ∑ i in range (n + 1), (-1) ^ i * f i := by + (hf0 : Tendsto f atTop (𝓝 0)) : CauchySeq fun n ↦ ∑ i in range n, (-1) ^ i * f i := by simp_rw [mul_comm] exact hfa.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0 norm_sum_neg_one_pow_le #align antitone.cauchy_seq_alternating_series_of_tendsto_zero Antitone.cauchySeq_alternating_series_of_tendsto_zero @@ -691,7 +699,7 @@ theorem Antitone.cauchySeq_alternating_series_of_tendsto_zero (hfa : Antitone f) /-- The **alternating series test** for antitone sequences. -/ theorem Antitone.tendsto_alternating_series_of_tendsto_zero (hfa : Antitone f) (hf0 : Tendsto f atTop (𝓝 0)) : - ∃ l, Tendsto (fun n ↦ ∑ i in range (n + 1), (-1) ^ i * f i) atTop (𝓝 l) := + ∃ l, Tendsto (fun n ↦ ∑ i in range n, (-1) ^ i * f i) atTop (𝓝 l) := cauchySeq_tendsto_of_complete <| hfa.cauchySeq_alternating_series_of_tendsto_zero hf0 #align antitone.tendsto_alternating_series_of_tendsto_zero Antitone.tendsto_alternating_series_of_tendsto_zero diff --git a/Mathlib/Data/Real/Pi/Leibniz.lean b/Mathlib/Data/Real/Pi/Leibniz.lean index a34ecb9d4aa72..49aef75d7c83b 100644 --- a/Mathlib/Data/Real/Pi/Leibniz.lean +++ b/Mathlib/Data/Real/Pi/Leibniz.lean @@ -3,136 +3,67 @@ Copyright (c) 2020 Benjamin Davidson. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Benjamin Davidson -/ -import Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv -import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics +import Mathlib.Analysis.Complex.AbelLimit +import Mathlib.Analysis.SpecialFunctions.Complex.Arctan #align_import data.real.pi.leibniz from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982" -/-! ### Leibniz's Series for Pi -/ - +/-! ### Leibniz's series for `π` -/ namespace Real -open Filter Set - -open scoped Classical BigOperators Topology Real - -/-- This theorem establishes **Leibniz's series for `π`**: The alternating sum of the reciprocals - of the odd numbers is `π/4`. Note that this is a conditionally rather than absolutely convergent - series. The main tool that this proof uses is the Mean Value Theorem (specifically avoiding the - Fundamental Theorem of Calculus). +open Filter Finset - Intuitively, the theorem holds because Leibniz's series is the Taylor series of `arctan x` - centered about `0` and evaluated at the value `x = 1`. Therefore, much of this proof consists of - reasoning about a function - `f := arctan x - ∑ i in Finset.range k, (-(1:ℝ))^i * x^(2*i+1) / (2*i+1)`, - the difference between `arctan` and the `k`-th partial sum of its Taylor series. Some ingenuity is - required due to the fact that the Taylor series is not absolutely convergent at `x = 1`. +open scoped BigOperators Topology - This proof requires a bound on `f 1`, the key idea being that `f 1` can be split as the sum of - `f 1 - f u` and `f u`, where `u` is a sequence of values in [0,1], carefully chosen such that - each of these two terms can be controlled (in different ways). +/-- **Leibniz's series for `π`**. The alternating sum of odd number reciprocals is `π / 4`. - We begin the proof by (1) introducing that sequence `u` and then proving that another sequence - constructed from `u` tends to `0` at `+∞`. After (2) converting the limit in our goal to an - inequality, we (3) introduce the auxiliary function `f` defined above. Next, we (4) compute the - derivative of `f`, denoted by `f'`, first generally and then on each of two subintervals of [0,1]. - We then (5) prove a bound for `f'`, again both generally as well as on each of the two - subintervals. Finally, we (6) apply the Mean Value Theorem twice, obtaining bounds on `f 1 - f u` - and `f u - f 0` from the bounds on `f'` (note that `f 0 = 0`). -/ +Note that this is a conditionally rather than absolutely convergent series. The main tool that +this proof uses is Abel's limit theorem, which allows us to extend the Maclaurin series of +`arctan x`, which has radius of convergence 1, to `x = 1`. -/ theorem tendsto_sum_pi_div_four : - Tendsto (fun k => ∑ i in Finset.range k, (-(1 : ℝ)) ^ i / (2 * i + 1)) atTop (𝓝 (π / 4)) := by - rw [tendsto_iff_norm_sub_tendsto_zero, ← tendsto_zero_iff_norm_tendsto_zero] - -- (1) We introduce a useful sequence `u` of values in [0,1], then prove that another sequence - -- constructed from `u` tends to `0` at `+∞` - let u := fun k : ℕ => (k : NNReal) ^ (-1 / (2 * (k : ℝ) + 1)) - have H : Tendsto (fun k : ℕ => (1 : ℝ) - u k + u k ^ (2 * (k : ℝ) + 1)) atTop (𝓝 0) := by - convert (((tendsto_rpow_div_mul_add (-1) 2 1 two_ne_zero.symm).neg.const_add 1).add - tendsto_inv_atTop_zero).comp tendsto_nat_cast_atTop_atTop using 1 - · ext k - simp only [u, NNReal.coe_nat_cast, Function.comp_apply, NNReal.coe_rpow] - rw [← rpow_mul (Nat.cast_nonneg k) (-1 / (2 * (k : ℝ) + 1)) (2 * (k : ℝ) + 1), - @div_mul_cancel _ _ (2 * (k : ℝ) + 1) _ - (by norm_cast; simp only [Nat.succ_ne_zero, not_false_iff]), - rpow_neg_one k, sub_eq_add_neg] - · simp only [add_zero, add_right_neg] - -- (2) We convert the limit in our goal to an inequality - refine' squeeze_zero_norm _ H - intro k - -- Since `k` is now fixed, we henceforth denote `u k` as `U` - let U := u k - -- (3) We introduce an auxiliary function `f` - let b (i : ℕ) x := (-(1 : ℝ)) ^ i * x ^ (2 * i + 1) / (2 * i + 1) - let f x := arctan x - ∑ i in Finset.range k, b i x - suffices f_bound : |f 1 - f 0| ≤ (1 : ℝ) - U + U ^ (2 * (k : ℝ) + 1) by - rw [← norm_neg] - convert f_bound using 1 - simp [b, f] - -- We show that `U` is indeed in [0,1] - have hU1 : (U : ℝ) ≤ 1 := by - by_cases hk : k = 0 - · simp [U, u, hk] - · exact rpow_le_one_of_one_le_of_nonpos - (by norm_cast; exact Nat.succ_le_iff.mpr (Nat.pos_of_ne_zero hk)) (le_of_lt - (@div_neg_of_neg_of_pos _ _ (-(1 : ℝ)) (2 * k + 1) (neg_neg_iff_pos.mpr zero_lt_one) - (by norm_cast; exact Nat.succ_pos'))) - have hU2 := NNReal.coe_nonneg U - -- (4) We compute the derivative of `f`, denoted by `f'` - let f' := fun x : ℝ => (-x ^ 2) ^ k / (1 + x ^ 2) - have has_deriv_at_f : ∀ x, HasDerivAt f (f' x) x := by - intro x - have has_deriv_at_b : ∀ i ∈ Finset.range k, HasDerivAt (b i) ((-x ^ 2) ^ i) x := by - intro i _ - convert HasDerivAt.const_mul ((-1 : ℝ) ^ i / (2 * i + 1)) - (HasDerivAt.pow (2 * i + 1) (hasDerivAt_id x)) using 1 - · ext y - simp only [id.def] - ring - · simp - rw [← mul_assoc, @div_mul_cancel _ _ (2 * (i : ℝ) + 1) _ (by norm_cast; omega), - pow_mul x 2 i, ← mul_pow (-1 : ℝ) (x ^ 2) i] - ring_nf - convert (hasDerivAt_arctan x).sub (HasDerivAt.sum has_deriv_at_b) using 1 - have g_sum := - @geom_sum_eq _ _ (-x ^ 2) ((neg_nonpos.mpr (sq_nonneg x)).trans_lt zero_lt_one).ne k - simp only at g_sum ⊢ - rw [g_sum, ← neg_add' (x ^ 2) 1, add_comm (x ^ 2) 1, sub_eq_add_neg, neg_div', neg_div_neg_eq] - ring - have hderiv1 : ∀ x ∈ Icc (U : ℝ) 1, HasDerivWithinAt f (f' x) (Icc (U : ℝ) 1) x := fun x _ => - (has_deriv_at_f x).hasDerivWithinAt - have hderiv2 : ∀ x ∈ Icc 0 (U : ℝ), HasDerivWithinAt f (f' x) (Icc 0 (U : ℝ)) x := fun x _ => - (has_deriv_at_f x).hasDerivWithinAt - -- (5) We prove a general bound for `f'` and then more precise bounds on each of two subintervals - have f'_bound : ∀ x ∈ Icc (-1 : ℝ) 1, |f' x| ≤ |x| ^ (2 * k) := by - intro x _ - rw [abs_div, IsAbsoluteValue.abv_pow abs (-x ^ 2) k, abs_neg, IsAbsoluteValue.abv_pow abs x 2, - ← pow_mul] - refine' div_le_of_nonneg_of_le_mul (abs_nonneg _) (pow_nonneg (abs_nonneg _) _) _ - refine' le_mul_of_one_le_right (pow_nonneg (abs_nonneg _) _) _ - rw_mod_cast [abs_of_nonneg (add_nonneg zero_le_one (sq_nonneg x) : (0 : ℝ) ≤ _)] - exact (le_add_of_nonneg_right (sq_nonneg x) : (1 : ℝ) ≤ _) - have hbound1 : ∀ x ∈ Ico (U : ℝ) 1, |f' x| ≤ 1 := by - rintro x ⟨hx_left, hx_right⟩ - have hincr := pow_le_pow_left (le_trans hU2 hx_left) (le_of_lt hx_right) (2 * k) - rw [one_pow (2 * k), ← abs_of_nonneg (le_trans hU2 hx_left)] at hincr - rw [← abs_of_nonneg (le_trans hU2 hx_left)] at hx_right - linarith [f'_bound x (mem_Icc.mpr (abs_le.mp (le_of_lt hx_right)))] - have hbound2 : ∀ x ∈ Ico 0 (U : ℝ), |f' x| ≤ U ^ (2 * k) := by - rintro x ⟨hx_left, hx_right⟩ - have hincr := pow_le_pow_left hx_left (le_of_lt hx_right) (2 * k) - rw [← abs_of_nonneg hx_left] at hincr hx_right - rw [← abs_of_nonneg hU2] at hU1 hx_right - exact (f'_bound x (mem_Icc.mpr (abs_le.mp (le_trans (le_of_lt hx_right) hU1)))).trans hincr - -- (6) We twice apply the Mean Value Theorem to obtain bounds on `f` from the bounds on `f'` - have mvt1 := norm_image_sub_le_of_norm_deriv_le_segment' hderiv1 hbound1 _ (right_mem_Icc.mpr hU1) - have mvt2 := norm_image_sub_le_of_norm_deriv_le_segment' hderiv2 hbound2 _ (right_mem_Icc.mpr hU2) - -- The following algebra is enough to complete the proof - calc - |f 1 - f 0| = |f 1 - f U + (f U - f 0)| := by simp - _ ≤ 1 * (1 - U) + U ^ (2 * k) * (U - 0) := - (le_trans (abs_add (f 1 - f U) (f U - f 0)) (add_le_add mvt1 mvt2)) - _ = 1 - U + (U : ℝ) ^ (2 * k) * U := by simp - _ = 1 - u k + u k ^ (2 * (k : ℝ) + 1) := by rw [← pow_succ' (U : ℝ) (2 * k)]; norm_cast + Tendsto (fun k => ∑ i in range k, (-1 : ℝ) ^ i / (2 * i + 1)) atTop (𝓝 (π / 4)) := by + -- The series is alternating with terms of decreasing magnitude, so it converges to _some_ limit + obtain ⟨l, h⟩ : + ∃ l, Tendsto (fun n ↦ ∑ i in range n, (-1 : ℝ) ^ i / (2 * i + 1)) atTop (𝓝 l) := by + apply (antitone_iff_forall_lt.mpr + (fun _ _ _ ↦ by dsimp; gcongr)).tendsto_alternating_series_of_tendsto_zero + (Tendsto.inv_tendsto_atTop (tendsto_atTop_add_const_right _ _ _)) + exact tendsto_nat_cast_atTop_atTop.const_mul_atTop zero_lt_two + -- Abel's limit theorem states that the corresponding power series has the same limit as `x → 1⁻` + have abel := tendsto_tsum_powerSeries_nhdsWithin_lt h + -- Massage the expression to get `x ^ (2 * n + 1)` in the tsum rather than `x ^ n`... + have q : Tendsto (fun x : ℝ ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1) := by + simp_rw [Metric.tendsto_nhdsWithin_nhdsWithin, Set.mem_Iio, sq_lt_one_iff_abs_lt_one] + intro ε hε + use min 1 (ε / 2), by positivity + intro x lb dx + rw [dist_eq, lt_min_iff, abs_sub_lt_iff] at dx + obtain ⟨⟨_, ub⟩, t⟩ := dx + replace ub : 0 < x := by linarith only [ub] + have a : |x| < 1 := by rw [abs_lt]; constructor <;> linarith + refine' ⟨a, _⟩ + rw [dist_eq, show x ^ 2 - 1 = (x + 1) * (x - 1) by ring, abs_mul, show ε = 2 * (ε / 2) by ring] + gcongr + exact (abs_add_le x 1).trans_lt (by rw [← one_add_one_eq_two, abs_one]; gcongr) + have m : 𝓝[<] (1 : ℝ) ≤ 𝓝 1 := tendsto_nhdsWithin_of_tendsto_nhds fun _ a ↦ a + replace abel := (abel.comp q).mul m + rw [mul_one] at abel + -- ...so that we can replace the tsum with the real arctangent function + replace abel : Tendsto arctan (𝓝[<] 1) (𝓝 l) := by + apply abel.congr' + rw [eventuallyEq_nhdsWithin_iff, Metric.eventually_nhds_iff] + use 2, zero_lt_two + intro y hy1 hy2 + rw [dist_eq, abs_sub_lt_iff] at hy1 + rw [Set.mem_Iio] at hy2 + have ny : ‖y‖ < 1 := by rw [norm_eq_abs, abs_lt]; constructor <;> linarith + rw [← (hasSum_arctan ny).tsum_eq, Function.comp_apply, ← tsum_mul_right] + congr with n + rw [mul_assoc, ← pow_mul, ← pow_succ', div_mul_eq_mul_div] + norm_cast + -- But `arctan` is continuous everywhere, so the limit is `arctan 1 = π / 4` + rwa [tendsto_nhds_unique abel ((continuous_arctan.tendsto 1).mono_left m), arctan_one] at h #align real.tendsto_sum_pi_div_four Real.tendsto_sum_pi_div_four end Real From bfa3642e61898c4d31afeddf053bb8a6c9668303 Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Sat, 2 Mar 2024 17:58:58 +0800 Subject: [PATCH 2/7] golf one have --- Mathlib/Analysis/SpecificLimits/Normed.lean | 2 +- Mathlib/Data/Real/Pi/Leibniz.lean | 23 ++++++++------------- 2 files changed, 10 insertions(+), 15 deletions(-) diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean index 79d78dc45e384..cd189209ea5ac 100644 --- a/Mathlib/Analysis/SpecificLimits/Normed.lean +++ b/Mathlib/Analysis/SpecificLimits/Normed.lean @@ -628,7 +628,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] variable {b : ℝ} {f : ℕ → ℝ} {z : ℕ → E} -/-- **Dirichlet's Test** for monotone sequences. -/ +/-- **Dirichlet's test** for monotone sequences. -/ theorem Monotone.cauchySeq_series_mul_of_tendsto_zero_of_bounded (hfa : Monotone f) (hf0 : Tendsto f atTop (𝓝 0)) (hgb : ∀ n, ‖∑ i in range n, z i‖ ≤ b) : CauchySeq fun n ↦ ∑ i in range n, f i • z i := by diff --git a/Mathlib/Data/Real/Pi/Leibniz.lean b/Mathlib/Data/Real/Pi/Leibniz.lean index 49aef75d7c83b..b49be2e888925 100644 --- a/Mathlib/Data/Real/Pi/Leibniz.lean +++ b/Mathlib/Data/Real/Pi/Leibniz.lean @@ -33,27 +33,22 @@ theorem tendsto_sum_pi_div_four : -- Abel's limit theorem states that the corresponding power series has the same limit as `x → 1⁻` have abel := tendsto_tsum_powerSeries_nhdsWithin_lt h -- Massage the expression to get `x ^ (2 * n + 1)` in the tsum rather than `x ^ n`... - have q : Tendsto (fun x : ℝ ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1) := by - simp_rw [Metric.tendsto_nhdsWithin_nhdsWithin, Set.mem_Iio, sq_lt_one_iff_abs_lt_one] - intro ε hε - use min 1 (ε / 2), by positivity - intro x lb dx - rw [dist_eq, lt_min_iff, abs_sub_lt_iff] at dx - obtain ⟨⟨_, ub⟩, t⟩ := dx - replace ub : 0 < x := by linarith only [ub] - have a : |x| < 1 := by rw [abs_lt]; constructor <;> linarith - refine' ⟨a, _⟩ - rw [dist_eq, show x ^ 2 - 1 = (x + 1) * (x - 1) by ring, abs_mul, show ε = 2 * (ε / 2) by ring] - gcongr - exact (abs_add_le x 1).trans_lt (by rw [← one_add_one_eq_two, abs_one]; gcongr) have m : 𝓝[<] (1 : ℝ) ≤ 𝓝 1 := tendsto_nhdsWithin_of_tendsto_nhds fun _ a ↦ a + have q : Tendsto (fun x : ℝ ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1) := by + apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within + · nth_rw 3 [← one_pow 2] + exact Tendsto.pow ‹_› _ + · rw [eventually_iff_exists_mem] + use Set.Ioo (-1) 1 + exact ⟨(by rw [mem_nhdsWithin_Iio_iff_exists_Ioo_subset]; use -1, by simp), + fun _ _ ↦ by rwa [Set.mem_Iio, sq_lt_one_iff_abs_lt_one, abs_lt, ← Set.mem_Ioo]⟩ replace abel := (abel.comp q).mul m rw [mul_one] at abel -- ...so that we can replace the tsum with the real arctangent function replace abel : Tendsto arctan (𝓝[<] 1) (𝓝 l) := by apply abel.congr' rw [eventuallyEq_nhdsWithin_iff, Metric.eventually_nhds_iff] - use 2, zero_lt_two + use 1, zero_lt_one intro y hy1 hy2 rw [dist_eq, abs_sub_lt_iff] at hy1 rw [Set.mem_Iio] at hy2 From df7485f5a9119195c09e1c6b53d37e48400dfb5a Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Sat, 2 Mar 2024 18:26:54 +0800 Subject: [PATCH 3/7] Untangle the obtain --- Mathlib/Data/Real/Pi/Leibniz.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/Data/Real/Pi/Leibniz.lean b/Mathlib/Data/Real/Pi/Leibniz.lean index b49be2e888925..7e8f05c662871 100644 --- a/Mathlib/Data/Real/Pi/Leibniz.lean +++ b/Mathlib/Data/Real/Pi/Leibniz.lean @@ -23,13 +23,13 @@ this proof uses is Abel's limit theorem, which allows us to extend the Maclaurin `arctan x`, which has radius of convergence 1, to `x = 1`. -/ theorem tendsto_sum_pi_div_four : Tendsto (fun k => ∑ i in range k, (-1 : ℝ) ^ i / (2 * i + 1)) atTop (𝓝 (π / 4)) := by - -- The series is alternating with terms of decreasing magnitude, so it converges to _some_ limit + -- The series is alternating with terms of decreasing magnitude, so it converges to some limit obtain ⟨l, h⟩ : ∃ l, Tendsto (fun n ↦ ∑ i in range n, (-1 : ℝ) ^ i / (2 * i + 1)) atTop (𝓝 l) := by - apply (antitone_iff_forall_lt.mpr - (fun _ _ _ ↦ by dsimp; gcongr)).tendsto_alternating_series_of_tendsto_zero - (Tendsto.inv_tendsto_atTop (tendsto_atTop_add_const_right _ _ _)) - exact tendsto_nat_cast_atTop_atTop.const_mul_atTop zero_lt_two + apply Antitone.tendsto_alternating_series_of_tendsto_zero + · exact antitone_iff_forall_lt.mpr fun _ _ _ ↦ by gcongr + · apply Tendsto.inv_tendsto_atTop; apply tendsto_atTop_add_const_right + exact tendsto_nat_cast_atTop_atTop.const_mul_atTop zero_lt_two -- Abel's limit theorem states that the corresponding power series has the same limit as `x → 1⁻` have abel := tendsto_tsum_powerSeries_nhdsWithin_lt h -- Massage the expression to get `x ^ (2 * n + 1)` in the tsum rather than `x ^ n`... From 334bcd8f52f61aeddc5bdb64539f525b7cf7e8d6 Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Sun, 3 Mar 2024 14:02:31 +0800 Subject: [PATCH 4/7] `cauchySeq_shift` --- Mathlib/Analysis/SpecificLimits/Normed.lean | 9 +-------- Mathlib/Topology/UniformSpace/Cauchy.lean | 11 +++++++++++ 2 files changed, 12 insertions(+), 8 deletions(-) diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean index cd189209ea5ac..8b0e46ca49990 100644 --- a/Mathlib/Analysis/SpecificLimits/Normed.lean +++ b/Mathlib/Analysis/SpecificLimits/Normed.lean @@ -632,14 +632,7 @@ variable {b : ℝ} {f : ℕ → ℝ} {z : ℕ → E} theorem Monotone.cauchySeq_series_mul_of_tendsto_zero_of_bounded (hfa : Monotone f) (hf0 : Tendsto f atTop (𝓝 0)) (hgb : ∀ n, ‖∑ i in range n, z i‖ ≤ b) : CauchySeq fun n ↦ ∑ i in range n, f i • z i := by - suffices CauchySeq fun n ↦ ∑ i in range (n + 1), f i • z i by - rw [Metric.cauchySeq_iff] at this ⊢ - intro ε hε - replace this := this ε hε - obtain ⟨N, this⟩ := this - use N + 1 - intro m hm n hn - convert this (m - 1) (by omega) (n - 1) (by omega) <;> omega + rw [cauchySeq_shift 1] simp_rw [Finset.sum_range_by_parts _ _ (Nat.succ _), sub_eq_add_neg, Nat.succ_sub_succ_eq_sub, tsub_zero] apply (NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded hf0 diff --git a/Mathlib/Topology/UniformSpace/Cauchy.lean b/Mathlib/Topology/UniformSpace/Cauchy.lean index 83a9e5e98d6f2..a7c46f36128a5 100644 --- a/Mathlib/Topology/UniformSpace/Cauchy.lean +++ b/Mathlib/Topology/UniformSpace/Cauchy.lean @@ -310,6 +310,17 @@ theorem tendsto_nhds_of_cauchySeq_of_subseq [Preorder β] {u : β → α} (hu : le_nhds_of_cauchy_adhp hu (mapClusterPt_of_comp hf ha) #align tendsto_nhds_of_cauchy_seq_of_subseq tendsto_nhds_of_cauchySeq_of_subseq +/-- Any shift of a Cauchy sequence is also a Cauchy sequence. -/ +theorem cauchySeq_shift {u : ℕ → α} (k : ℕ) : CauchySeq u ↔ CauchySeq fun n ↦ u (n + k) := by + constructor <;> intro h + · exact h.comp_tendsto (tendsto_add_atTop_nat k) + · rw [cauchySeq_iff] at h ⊢ + intro V mV + obtain ⟨N, h⟩ := h V mV + use N + k + intro a _ b _ + convert h (a - k) (by omega) (b - k) (by omega) <;> omega + theorem Filter.HasBasis.cauchySeq_iff {γ} [Nonempty β] [SemilatticeSup β] {u : β → α} {p : γ → Prop} {s : γ → Set (α × α)} (h : (𝓤 α).HasBasis p s) : CauchySeq u ↔ ∀ i, p i → ∃ N, ∀ m, N ≤ m → ∀ n, N ≤ n → (u m, u n) ∈ s i := by From bbd56ac84598f25179ac10615b8c021da4cf5a6e Mon Sep 17 00:00:00 2001 From: Jeremy Tan Jie Rui Date: Sun, 3 Mar 2024 16:56:38 +0800 Subject: [PATCH 5/7] Update Mathlib/Topology/UniformSpace/Cauchy.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/Topology/UniformSpace/Cauchy.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Topology/UniformSpace/Cauchy.lean b/Mathlib/Topology/UniformSpace/Cauchy.lean index a7c46f36128a5..3a94a8eac2f75 100644 --- a/Mathlib/Topology/UniformSpace/Cauchy.lean +++ b/Mathlib/Topology/UniformSpace/Cauchy.lean @@ -318,8 +318,8 @@ theorem cauchySeq_shift {u : ℕ → α} (k : ℕ) : CauchySeq u ↔ CauchySeq f intro V mV obtain ⟨N, h⟩ := h V mV use N + k - intro a _ b _ - convert h (a - k) (by omega) (b - k) (by omega) <;> omega + intro a ha b hb + convert h (a - k) (Nat.le_sub_of_add_le ha) (b - k) (Nat.le_sub_of_add_le hb) <;> omega theorem Filter.HasBasis.cauchySeq_iff {γ} [Nonempty β] [SemilatticeSup β] {u : β → α} {p : γ → Prop} {s : γ → Set (α × α)} (h : (𝓤 α).HasBasis p s) : From 0d0e40b1effa187bb366416a5cda653ed364cd2a Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Sun, 3 Mar 2024 17:43:43 +0800 Subject: [PATCH 6/7] get rid of `congr` --- Mathlib/Data/Real/Pi/Leibniz.lean | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/Mathlib/Data/Real/Pi/Leibniz.lean b/Mathlib/Data/Real/Pi/Leibniz.lean index 7e8f05c662871..d53fd53c14572 100644 --- a/Mathlib/Data/Real/Pi/Leibniz.lean +++ b/Mathlib/Data/Real/Pi/Leibniz.lean @@ -16,11 +16,8 @@ open Filter Finset open scoped BigOperators Topology -/-- **Leibniz's series for `π`**. The alternating sum of odd number reciprocals is `π / 4`. - -Note that this is a conditionally rather than absolutely convergent series. The main tool that -this proof uses is Abel's limit theorem, which allows us to extend the Maclaurin series of -`arctan x`, which has radius of convergence 1, to `x = 1`. -/ +/-- **Leibniz's series for `π`**. The alternating sum of odd number reciprocals is `π / 4`, +proved by using Abel's limit theorem to extend the Maclaurin series of `arctan` to 1. -/ theorem tendsto_sum_pi_div_four : Tendsto (fun k => ∑ i in range k, (-1 : ℝ) ^ i / (2 * i + 1)) atTop (𝓝 (π / 4)) := by -- The series is alternating with terms of decreasing magnitude, so it converges to some limit @@ -54,8 +51,7 @@ theorem tendsto_sum_pi_div_four : rw [Set.mem_Iio] at hy2 have ny : ‖y‖ < 1 := by rw [norm_eq_abs, abs_lt]; constructor <;> linarith rw [← (hasSum_arctan ny).tsum_eq, Function.comp_apply, ← tsum_mul_right] - congr with n - rw [mul_assoc, ← pow_mul, ← pow_succ', div_mul_eq_mul_div] + simp_rw [mul_assoc, ← pow_mul, ← pow_succ', div_mul_eq_mul_div] norm_cast -- But `arctan` is continuous everywhere, so the limit is `arctan 1 = π / 4` rwa [tendsto_nhds_unique abel ((continuous_arctan.tendsto 1).mono_left m), arctan_one] at h From 12ca68346605abadcac534757f80646daf0a727a Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Sun, 3 Mar 2024 21:55:44 +0800 Subject: [PATCH 7/7] swap --- Mathlib/Analysis/SpecificLimits/Normed.lean | 2 +- Mathlib/Topology/UniformSpace/Cauchy.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean index 8b0e46ca49990..4748a2a05eb11 100644 --- a/Mathlib/Analysis/SpecificLimits/Normed.lean +++ b/Mathlib/Analysis/SpecificLimits/Normed.lean @@ -632,7 +632,7 @@ variable {b : ℝ} {f : ℕ → ℝ} {z : ℕ → E} theorem Monotone.cauchySeq_series_mul_of_tendsto_zero_of_bounded (hfa : Monotone f) (hf0 : Tendsto f atTop (𝓝 0)) (hgb : ∀ n, ‖∑ i in range n, z i‖ ≤ b) : CauchySeq fun n ↦ ∑ i in range n, f i • z i := by - rw [cauchySeq_shift 1] + rw [← cauchySeq_shift 1] simp_rw [Finset.sum_range_by_parts _ _ (Nat.succ _), sub_eq_add_neg, Nat.succ_sub_succ_eq_sub, tsub_zero] apply (NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded hf0 diff --git a/Mathlib/Topology/UniformSpace/Cauchy.lean b/Mathlib/Topology/UniformSpace/Cauchy.lean index 3a94a8eac2f75..91544bd20a10d 100644 --- a/Mathlib/Topology/UniformSpace/Cauchy.lean +++ b/Mathlib/Topology/UniformSpace/Cauchy.lean @@ -311,15 +311,15 @@ theorem tendsto_nhds_of_cauchySeq_of_subseq [Preorder β] {u : β → α} (hu : #align tendsto_nhds_of_cauchy_seq_of_subseq tendsto_nhds_of_cauchySeq_of_subseq /-- Any shift of a Cauchy sequence is also a Cauchy sequence. -/ -theorem cauchySeq_shift {u : ℕ → α} (k : ℕ) : CauchySeq u ↔ CauchySeq fun n ↦ u (n + k) := by +theorem cauchySeq_shift {u : ℕ → α} (k : ℕ) : CauchySeq (fun n ↦ u (n + k)) ↔ CauchySeq u := by constructor <;> intro h - · exact h.comp_tendsto (tendsto_add_atTop_nat k) · rw [cauchySeq_iff] at h ⊢ intro V mV obtain ⟨N, h⟩ := h V mV use N + k intro a ha b hb convert h (a - k) (Nat.le_sub_of_add_le ha) (b - k) (Nat.le_sub_of_add_le hb) <;> omega + · exact h.comp_tendsto (tendsto_add_atTop_nat k) theorem Filter.HasBasis.cauchySeq_iff {γ} [Nonempty β] [SemilatticeSup β] {u : β → α} {p : γ → Prop} {s : γ → Set (α × α)} (h : (𝓤 α).HasBasis p s) :