[Merged by Bors] - feat(data/real/pi): Leibniz's series for pi

docs/100.yaml

@@ -84,7 +84,9 @@
   decl   : function.embedding.schroeder_bernstein
   author : Mario Carneiro
 26:
-  title  : Leibnitz’s Series for Pi
+  title  : Leibniz’s Series for Pi
+  decl   : real.leibniz
+  author : Benjamin Davidson
 27:
   title  : Sum of the Angles of a Triangle
   decl   : euclidean_geometry.angle_add_angle_add_angle_eq_pi

src/analysis/special_functions/exp_log.lean

@@ -416,12 +416,16 @@ begin
   exact tendsto_at_top_mono' at_top B A
 end
 
-/-- The real exponential function tends to 0 at -infinity or, equivalently, `exp(-x)` tends to `0`
-at +infinity -/
+/-- The real exponential function tends to `0` at `-∞` or, equivalently, `exp(-x)` tends to `0`
+at `+∞` -/
 lemma tendsto_exp_neg_at_top_nhds_0 : tendsto (λx, exp (-x)) at_top (𝓝 0) :=
 (tendsto_inv_at_top_zero.comp (tendsto_exp_at_top)).congr (λx, (exp_neg x).symm)
 
-/-- The function `exp(x)/x^n` tends to +infinity at +infinity, for any natural number `n` -/
+/-- The real exponential function tends to `1` at `0` -/
+lemma tendsto_exp_nhds_0_nhds_1 : tendsto exp (𝓝 0) (𝓝 1) :=
+by { convert continuous_exp.tendsto 0, simp }
+
+/-- The function `exp(x)/x^n` tends to `+∞` at `+∞`, for any natural number `n` -/
 lemma tendsto_exp_div_pow_at_top (n : ℕ) : tendsto (λx, exp x / x^n) at_top at_top :=
 begin
   have n_pos : (0 : ℝ) < n + 1 := nat.cast_add_one_pos n,

src/analysis/special_functions/pow.lean

@@ -312,6 +312,12 @@ end
 lemma div_rpow (hx : 0 ≤ x) (hy : 0 ≤ y) (z : ℝ) : (x / y) ^ z = x^z / y^z :=
 by simp only [div_eq_mul_inv, mul_rpow hx (inv_nonneg.2 hy), inv_rpow hy]
 
+lemma log_rpow {x : ℝ} (hx : 0 < x) (y : ℝ) : log (x^y) = y * (log x) :=
+begin
+  apply exp_injective,
+  rw [exp_log (rpow_pos_of_pos hx y), ← exp_log hx, mul_comm, rpow_def_of_pos (exp_pos (log x)) y],
+end
+
 lemma rpow_lt_rpow (hx : 0 ≤ x) (hxy : x < y) (hz : 0 < z) : x^z < y^z :=
 begin
   rw le_iff_eq_or_lt at hx, cases hx,
@@ -731,6 +737,71 @@ lemma deriv_within_sqrt (hf : differentiable_within_at ℝ f s x) (hx : f x ≠
 
 end differentiability
 
+section limits
+open real filter
+
+/-- The function `x^y` tends to `+∞` at `+∞` for any real number `1 ≤ y` -/
+lemma tendsto_rpow_at_top {y : ℝ} (hy : 1 ≤ y) : tendsto (λ (x:ℝ), (x^y)) at_top at_top :=
+begin
+  rw tendsto_at_top_at_top,
+  intro b, use max b 1, intros x hx,
+  exact le_trans (le_of_max_le_left (by rwa rpow_one x))
+          (rpow_le_rpow_of_exponent_le (le_of_max_le_right hx) hy),
+end
+
+/-- The function `x^(-y)` tends to `0` at `+∞` for any real number `1 ≤ y` -/
+lemma tendsto_rpow_of_neg_at_top_zero {y : ℝ} (hy : 1 ≤ y) : tendsto (λ (x:ℝ), x^(-y)) at_top (𝓝 0) :=
+tendsto.congr' (eventually_eq_of_mem (Ioi_mem_at_top 0) (λ x hx, (rpow_neg (le_of_lt hx) y).symm))
+  (tendsto.inv_tendsto_at_top (tendsto_rpow_at_top hy))
+
+/-- The function `(b * exp(x) + c) / (x^n)` tends to `+∞` at `+∞`, for any natural number `1 ≤ n`
+and any real numbers `b` and `c` such that `b` is positive -/
+lemma tendsto_mul_exp_plus_div_pow_at_top (b c : ℝ) (n : ℕ) (hb : 0 < b) (hn : 1 ≤ (n:ℝ)) :
+  tendsto (λ (x:ℝ), (b * (exp x) + c) / (x^n)) at_top at_top :=
+begin
+  refine tendsto.congr' (eventually_eq_of_mem (Ioi_mem_at_top 0) _)
+    (tendsto_at_top_add_tendsto_right (tendsto_at_top_mul_left hb (tendsto_exp_div_pow_at_top n))
+      ((tendsto_rpow_of_neg_at_top_zero hn).mul (@tendsto_const_nhds _ _ _ c _))),
+  intros x hx,
+  simp only [rpow_neg (le_of_lt hx) n, rpow_nat_cast],
+  ring,
+end
+
+/-- The function `((x^n) / b * exp(x) + c) ` tends to `0` at `+∞`, for any natural number `1 ≤ n`
+and any real numbers `b` and `c` such that `b` is positive -/
+lemma tendsto_div_pow_mul_exp_plus_at_top_nhds_0 (b c : ℝ) (n : ℕ) (hb : 0 < b) (hn : 1 ≤ (n:ℝ)) :
+  tendsto (λ (x:ℝ), x^n / (b * (exp x) + c)) at_top (𝓝 0) :=
+begin
+  convert tendsto.inv_tendsto_at_top (tendsto_mul_exp_plus_div_pow_at_top b c n hb hn),
+  ext x,
+  simpa only [pi.inv_apply] using inv_div.symm,
+end
+
+/-- The function `x ^ (a / (b * x + c))` tends to `1` at `+∞`, for any real numbers `a`, `b`, and `c`
+such that `b` is positive. -/
+lemma tendsto_rpow_of_div_mul_add (a b c : ℝ) (hb : 0 < b) : tendsto (λ (x:ℝ), x ^ (a / (b*x+c))) at_top (𝓝 1) :=
+begin
+  refine tendsto.congr' _ ((tendsto_exp_nhds_0_nhds_1.comp
+    (by simpa only [mul_zero, pow_one] using ((@tendsto_const_nhds _ _ _ a _).mul
+      (tendsto_div_pow_mul_exp_plus_at_top_nhds_0 b c 1 hb (by norm_num))))).comp
+        (tendsto_log_at_top)),
+  apply eventually_eq_of_mem (Ioi_mem_at_top (0:ℝ)),
+  intros x hx,
+  simp only [set.mem_Ioi, function.comp_app] at hx ⊢,
+  rw [exp_log hx, ← exp_log (rpow_pos_of_pos hx (a / (b * x + c))), log_rpow hx (a / (b * x + c))],
+  field_simp,
+end
+
+/-- Special case of `tendsto_rpow_of_div_mul_add` with `a = 1`, `b = 1`, and `c = 0` -/
+lemma tendsto_rpow_of_div : tendsto (λ (x:ℝ), x ^ ((1:ℝ) / x)) at_top (𝓝 1) :=
+by { convert tendsto_rpow_of_div_mul_add (1:ℝ) _ (0:ℝ) zero_lt_one, ring }
+
+/-- Special case of `tendsto_rpow_of_div_mul_add` with `a = -1`, `b = 1`, and `c = 0` -/
+lemma tendsto_rpow_of_neg_div : tendsto (λ (x:ℝ), x ^ (-(1:ℝ) / x)) at_top (𝓝 1) :=
+by { convert tendsto_rpow_of_div_mul_add (-(1:ℝ)) _ (0:ℝ) zero_lt_one, ring }
+
+end limits
+
 namespace nnreal
 
 /-- The nonnegative real power function `x^y`, defined for `x : ℝ≥0` and `y : ℝ ` as the

src/data/real/pi.lean

@@ -1,9 +1,9 @@
 /-
 Copyright (c) 2019 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn
+Authors: Floris van Doorn, Benjamin Davidson
 -/
-import analysis.special_functions.trigonometric
+import analysis.special_functions.pow
 
 namespace real
 
@@ -142,4 +142,109 @@ lemma pi_lt_3141593 : pi < 3.141593 := by pi_upper_bound [
   27720/19601, 56935/30813, 49359/25163, 258754/130003, 113599/56868, 1101994/551163,
   8671537/4336095, 3877807/1938940, 52483813/26242030, 56946167/28473117, 23798415/11899211]
 
+
+/-! ### Leibniz's Series for Pi -/
+
+noncomputable theory
+open real filter set
+open_locale classical big_operators topological_space
+local notation `|`x`|` := abs x
+local notation `π` := real.pi
+
+/-- This lemma 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. -/
+lemma leibniz : tendsto (λ k, ∑ i in finset.range k, ((-(1:ℝ))^i / (2*i+1))) at_top (𝓝 (π/4)) :=
+begin
+  rw [tendsto_iff_norm_tendsto_zero, ← tendsto_zero_iff_norm_tendsto_zero],
+  -- 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 := λ (k:ℕ), (k:nnreal) ^ (-1 / (2 * (k:ℝ) + 1)),
+  have H : tendsto (λ (k:ℕ), (1:ℝ) - (u k) + (u k) ^ (2 * (k:ℝ) + 1)) at_top (𝓝 0),
+    { convert (tendsto.const_add (1:ℝ) (((tendsto_rpow_of_div_mul_add (-1) 2 1 (by norm_num)).neg).add
+        tendsto_inv_at_top_zero)).comp tendsto_coe_nat_real_at_top_at_top,
+    { ext k,
+      simp only [nnreal.coe_nat_cast, function.comp_app, 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, linarith }), rpow_neg_one k],
+      ring },
+    { simp } },
+  -- 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,
+  -- We introduce 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),
+  { rw ← norm_neg,
+    convert f_bound,
+    simp only [f], simp [b] }, -- SHOULD BE ABLE TO COMBINE?
+  -- We show that `U` is indeed in [0,1]
+  have hU1 : (U:ℝ) ≤ 1,
+  { by_cases hk : k = 0,
+    { simpa only [U, hk] using zero_rpow_le_one _ },
+    { 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)
+          (by norm_num) (by { norm_cast, linarith } ))) } },
+  have hU2 := nnreal.coe_nonneg U,
+  -- We compute the derivative of `f`, denoted by `f'`
+  let f' := λ (x:ℝ), (-x^2) ^ k / (1 + x^2),
+  have has_deriv_at_f : ∀ (x:ℝ), has_deriv_at f (f' x) x,
+  { intro x,
+    have has_deriv_at_b : ∀ i ∈ finset.range k, (has_deriv_at (b i) ((-x^2)^i) x),
+    { intros i hi,
+      convert has_deriv_at.const_mul ((-1:ℝ)^i / (2*i+1)) (@has_deriv_at.pow _ _ _ _ _ (2*i+1)
+        (has_deriv_at_id x)),
+      { ext y,
+        simp only [b, id.def],
+        ring },
+      { simp only [nat.add_succ_sub_one, add_zero, mul_one, id.def, nat.cast_bit0, nat.cast_add,
+                  nat.cast_one, nat.cast_mul],
+        rw [← mul_assoc, @div_mul_cancel _ _ _ (2*(i:ℝ)+1) (by { norm_cast, linarith }),
+            pow_mul x 2 i, ← mul_pow (-1) (x^2) i],
+        ring } },
+    convert (has_deriv_at_arctan x).sub (has_deriv_at.sum has_deriv_at_b),
+    have g_sum := @geom_sum _ _ (-x^2) (by linarith [neg_nonpos.mpr (pow_two_nonneg x)]) k,
+    simp only [geom_series, f'] 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 f_deriv1 : ∀ x ∈ Icc (U:ℝ) 1, has_deriv_within_at f (f' x) (Icc (U:ℝ) 1) x :=
+    λ x hx, (has_deriv_at_f x).has_deriv_within_at,
+  have f_deriv2 : ∀ x ∈ Icc 0 (U:ℝ), has_deriv_within_at f (f' x) (Icc 0 (U:ℝ)) x :=
+    λ x hx, (has_deriv_at_f x).has_deriv_within_at,
+  -- 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),
+  { intros x hx,
+    rw [abs_div, is_monoid_hom.map_pow abs (-x^2) k, abs_neg, is_monoid_hom.map_pow abs x 2,
+        tactic.ring_exp.pow_e_pf_exp rfl rfl, @abs_of_pos _ _ (1+x^2) (by nlinarith)],
+    convert @div_le_div_of_le_left _ _ _ (1+x^2) 1 (pow_nonneg (abs_nonneg x) (2*k)) (by norm_num)
+      (by nlinarith),
+    simp },
+  have hbound1 : ∀ x ∈ Ico (U:ℝ) 1, |f' x| ≤ 1,
+  { intros x hx,
+    cases hx,
+    have hincr := pow_le_pow_of_le_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),
+  { intros x hx,
+    cases hx,
+    have hincr := pow_le_pow_of_le_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,
+    linarith [f'_bound x (mem_Icc.mpr (abs_le.mp (le_trans (le_of_lt hx_right) hU1)))] },
+  -- Finally, 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' f_deriv1 hbound1 _ (right_mem_Icc.mpr hU1),
+  have mvt2 := norm_image_sub_le_of_norm_deriv_le_segment' f_deriv2 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 ring
+               ... ≤ 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 ring
+               ... = 1 - (u k) + (u k)^(2*(k:ℝ)+1) : by { rw [← pow_succ' (U:ℝ) (2*k)], norm_cast },
+end
+
 end real

src/topology/algebra/monoid.lean

@@ -67,6 +67,16 @@ lemma filter.tendsto.mul {f : β → α} {g : β → α} {x : filter β} {a b :
   tendsto (λx, f x * g x) x (𝓝 (a * b)) :=
 tendsto_mul.comp (hf.prod_mk_nhds hg)
 
+@[to_additive]
+lemma tendsto.const_mul (b : α) {c : α} {f : β → α} {l : filter β}
+  (h : tendsto (λ (k:β), f k) l (𝓝 c)) : tendsto (λ (k:β), b * f k) l (𝓝 (b * c)) :=
+tendsto_const_nhds.mul h
+
+@[to_additive]
+lemma tendsto.mul_const (b : α) {c : α} {f : β → α} {l : filter β}
+  (h : tendsto (λ (k:β), f k) l (𝓝 c)) : tendsto (λ (k:β), f k * b) l (𝓝 (c * b)) :=
+h.mul tendsto_const_nhds
+
 @[to_additive]
 lemma continuous_at.mul [topological_space β] {f : β → α} {g : β → α} {x : β}
   (hf : continuous_at f x) (hg : continuous_at g x) :