feat(data/real/pi): Wallis product for pi (#6568)

Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>

Author: winston-h-zhang

src/analysis/special_functions/integrals.lean

@@ -11,12 +11,17 @@ import measure_theory.interval_integral
 This file contains proofs of the integrals of various simple functions, including `pow`, `exp`,
 `inv`/`one_div`, `sin`, `cos`, and `λ x, 1 / (1 + x^2)`.
 
+There are also facts about more complicated integrals:
+* `sin x ^ n`: We prove a recursive formula for `sin x ^ (n + 2)` in terms of `sin x ^ n`,
+  along with explicit product formulas for even and odd `n`.
+
 With these lemmas, many simple integrals can be computed by `simp` or `norm_num`.
 
 This file is still being developed.
 -/
 
-open real set interval_integral
+open real set interval_integral filter
+open_locale real big_operators topological_space
 variables {a b : ℝ}
 
 namespace interval_integral
@@ -96,8 +101,6 @@ end
 lemma interval_integrable_inv_one_add_sq : interval_integrable (λ x:ℝ, (1 + x^2)⁻¹) μ a b :=
 by simpa only [one_div] using interval_integrable_one_div_one_add_sq
 
-end interval_integral
-
 @[simp]
 lemma integral_pow (n : ℕ) : ∫ x in a..b, x ^ n = (b^(n+1) - a^(n+1)) / (n + 1) :=
 begin
@@ -151,6 +154,69 @@ by simp only [one_div, integral_inv_of_neg ha hb]
 lemma integral_sin : ∫ x in a..b, sin x = cos a - cos b :=
 by rw integral_deriv_eq_sub' (λ x, -cos x); norm_num [continuous_on_sin]
 
+lemma integral_sin_pow_aux (n : ℕ) : ∫ x in 0..π, sin x ^ (n + 2) =
+  ((n + 1) * ∫ x in 0..π, sin x ^ n) - (n + 1) * ∫ x in 0..π, sin x ^ (n + 2) :=
+begin
+  have hv : ∀ x ∈ interval 0 π, has_deriv_at (-cos) (sin x) x,
+  { intros, convert (has_deriv_at_cos x).neg, rw neg_neg },
+  have hu : ∀ x ∈ interval 0 π, has_deriv_at (λ x, sin x ^ (n + 1)) ((n + 1) * cos x * sin x ^ n) x,
+  { intros,
+    convert (has_deriv_at_pow (n + 1) (sin x)).comp x (has_deriv_at_sin x) using 1,
+    simp [mul_right_comm], },
+  calc ∫ (x : ℝ) in 0..π, sin x ^ (n + 2)
+      = ∫ (x : ℝ) in 0..π, sin x ^ (n + 1) * sin x : by { congr, ext, ring }
+  ... = ∫ (x : ℝ) in 0..π, cos x * (λ (x : ℝ), (↑n + 1) * cos x * sin x ^ n) x : by
+  { simp [integral_mul_deriv_eq_deriv_mul hu hv (by continuity : continuous _).continuous_on
+      (by continuity : continuous _).continuous_on] }
+  ... = (↑n + 1) * ∫ (x : ℝ) in 0..π, cos x ^ 2 * sin x ^ n : by
+  { rw ← integral_const_mul, congr, ext, simp only, ring }
+  ... = (↑n + 1) * ∫ (x : ℝ) in 0..π, sin x ^ n - sin x ^ (n + 2) : by
+  { simp [integral_const_mul, cos_square', sub_mul, ← pow_add, add_comm] }
+  ... = _ - _ : by { rw [integral_sub, mul_sub],
+    { exact ((continuous_pow n).comp continuous_sin).interval_integrable 0 π },
+    { exact ((continuous_pow (n + 2)).comp continuous_sin).interval_integrable 0 π } },
+end
+
+lemma integral_sin_pow_succ_succ (n : ℕ) :
+  ∫ x in 0..π, sin x ^ (n + 2) = (n + 1) / (n + 2) * ∫ x in 0..π, sin x ^ n :=
+begin
+  have : (n:ℝ) + 2 ≠ 0 := by { norm_cast, norm_num },
+  field_simp,
+  convert eq_sub_iff_add_eq.mp (integral_sin_pow_aux n),
+  ring
+end
+
+theorem integral_sin_pow_odd (n : ℕ) :
+  ∫ x in 0..π, sin x ^ (2 * n + 1) = 2 * ∏ i in finset.range n, (2 * i + 2) / (2 * i + 3) :=
+begin
+  induction n with k ih,
+  { norm_num, },
+  rw [finset.prod_range_succ, ← mul_assoc, mul_comm (2:ℝ) ((2 * k + 2) / (2 * k + 3)),
+    mul_assoc, ← ih],
+  have h₁ : 2 * k.succ + 1 = 2 * k + 1 + 2, { ring },
+  have h₂ : (2:ℝ) * k + 1 + 1 = 2 * k + 2, { norm_cast, },
+  have h₃ : (2:ℝ) * k + 1 + 2 = 2 * k + 3, { norm_cast, },
+  simp [h₁, h₂, h₃, integral_sin_pow_succ_succ (2 * k + 1)]
+end
+
+theorem integral_sin_pow_even (n : ℕ) :
+  ∫ x in 0..π, sin x ^ (2 * n) = π * ∏ i in finset.range n, (2 * i + 1) / (2 * i + 2) :=
+begin
+  induction n with k ih,
+  { norm_num, },
+  rw [finset.prod_range_succ, ← mul_assoc, mul_comm π ((2 * k + 1) / (2 * k + 2)), mul_assoc, ← ih],
+  simp [nat.succ_eq_add_one, mul_add, mul_one, integral_sin_pow_succ_succ _],
+end
+
+lemma integral_sin_pow_pos (n : ℕ) : 0 < ∫ x in 0..π, sin x ^ n :=
+begin
+  rcases nat.even_or_odd' n with ⟨k, h, h⟩;
+  simp only [h, integral_sin_pow_even, integral_sin_pow_odd];
+  refine mul_pos (by norm_num [pi_pos]) (finset.prod_pos (λ n hn, div_pos _ _));
+  norm_cast;
+  linarith
+end
+
 @[simp]
 lemma integral_cos : ∫ x in a..b, cos x = sin b - sin a :=
 by rw integral_deriv_eq_sub'; norm_num [continuous_on_cos]
@@ -168,3 +234,5 @@ end
 
 lemma integral_one_div_one_add_sq : ∫ x : ℝ in a..b, 1 / (1 + x^2) = arctan b - arctan a :=
 by simp
+
+end interval_integral

src/data/real/pi.lean

@@ -3,14 +3,15 @@ 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, Benjamin Davidson
 -/
-import analysis.special_functions.pow
+import analysis.special_functions.integrals
 /-!
 # Pi
 
 This file contains lemmas which establish bounds on or approximations of `real.pi`. Notably, these
 include `pi_gt_sqrt_two_add_series` and `pi_lt_sqrt_two_add_series`, which bound `π` using series;
 numerical bounds on `π` such as `pi_gt_314`and `pi_lt_315` (more precise versions are given, too);
-and `tendsto_sum_pi_div_four`, Leibniz's series for `π`.
+and exact (infinite) formulas involving `π`, such as `tendsto_sum_pi_div_four`, Leibniz's
+series for `π`, and `tendsto_prod_pi_div_two`, the Wallis product for `π`.
 -/
 
 open_locale real
@@ -275,4 +276,88 @@ begin
                ... = 1 - (u k) + (u k)^(2*(k:ℝ)+1) : by { rw [← pow_succ' (U:ℝ) (2*k)], norm_cast },
 end
 
+open finset interval_integral
+
+lemma integral_sin_pow_antimono (n : ℕ) :
+  ∫ (x : ℝ) in 0..π, sin x ^ (n + 1) ≤ ∫ (x : ℝ) in 0..π, sin x ^ n :=
+begin
+  refine integral_mono_on _ _ pi_pos.le (λ x hx, _),
+  { exact ((continuous_pow (n + 1)).comp continuous_sin).interval_integrable 0 π },
+  { exact ((continuous_pow n).comp continuous_sin).interval_integrable 0 π },
+  refine pow_le_pow_of_le_one _ (sin_le_one x) (nat.le_add_right n 1),
+  rw interval_of_le pi_pos.le at hx,
+  exact sin_nonneg_of_mem_Icc hx,
+end
+
+lemma integral_sin_pow_div_tendsto_one :
+  tendsto (λ k, (∫ x in 0..π, sin x ^ (2 * k + 1)) / ∫ x in 0..π, sin x ^ (2 * k)) at_top (𝓝 1) :=
+begin
+  have h₃ : ∀ n, (∫ x in 0..π, sin x ^ (2 * n + 1)) / ∫ x in 0..π, sin x ^ (2 * n) ≤ 1 :=
+    λ n, (div_le_one (integral_sin_pow_pos _)).mpr (integral_sin_pow_antimono _),
+  have h₄ :
+    ∀ n, (∫ x in 0..π, sin x ^ (2 * n + 1)) / ∫ x in 0..π, sin x ^ (2 * n) ≥ 2 * n / (2 * n + 1),
+  { intro, cases n,
+    { have : 0 ≤ (1 + 1) / π, exact div_nonneg (by norm_num) pi_pos.le,
+      simp [this] },
+    calc (∫ x in 0..π, sin x ^ (2 * n.succ + 1)) / ∫ x in 0..π, sin x ^ (2 * n.succ) ≥
+      (∫ x in 0..π, sin x ^ (2 * n.succ + 1)) / ∫ x in 0..π, sin x ^ (2 * n + 1) :
+      by { refine div_le_div (integral_sin_pow_pos _).le (le_refl _) (integral_sin_pow_pos _) _,
+        convert integral_sin_pow_antimono (2 * n + 1) using 1 }
+    ... = 2 * ↑(n.succ) / (2 * ↑(n.succ) + 1) :
+      by { symmetry, rw [eq_div_iff, nat.succ_eq_add_one],
+        convert (integral_sin_pow_succ_succ (2 * n + 1)).symm using 3,
+        simp [mul_add], ring, simp [mul_add], ring,
+        exact norm_num.ne_zero_of_pos  _ (integral_sin_pow_pos (2 * n + 1)) } },
+  refine tendsto_of_tendsto_of_tendsto_of_le_of_le _ _ (λ n, (h₄ n).le) (λ n, (h₃ n)),
+  { refine metric.tendsto_at_top.mpr (λ ε hε, ⟨nat_ceil (1 / ε), λ n hn, _⟩),
+    have h : (2:ℝ) * n / (2 * n + 1) - 1 = -1 / (2 * n + 1),
+    { conv_lhs { congr, skip, rw ← @div_self _ _ ((2:ℝ) * n + 1) (by { norm_cast, linarith }), },
+      rw [← sub_div, ← sub_sub, sub_self, zero_sub] },
+    have hpos : (0:ℝ) < 2 * n + 1, { norm_cast, norm_num },
+    rw [real.dist_eq, h, abs_div, abs_neg, abs_one, abs_of_pos hpos, one_div_lt hpos hε],
+    calc 1 / ε ≤ nat_ceil (1 / ε) : le_nat_ceil _
+          ... ≤ n : by exact_mod_cast hn.le
+          ... < 2 * n + 1 : by { norm_cast, linarith } },
+  exact tendsto_const_nhds,
+end
+
+/-- This theorem establishes the Wallis Product for `π`. Our proof is largely about analyzing
+  the behavior of the ratio of the integral of `sin x ^ n` as `n → ∞`.
+  See: https://en.wikipedia.org/wiki/Wallis_product
+
+  The proof can be broken down into two pieces.
+  (Pieces involving general properties of the integral of `sin x ^n` can be found
+  in `analysis.special_functions.integrals`.) First, we use integration by parts to obtain a
+  recursive formula for `∫ x in 0..π, sin x ^ (n + 2)` in terms of `∫ x in 0..π, sin x ^ n`.
+  From this we can obtain closed form products of `∫ x in 0..π, sin x ^ (2 * n)` and
+  `∫ x in 0..π, sin x ^ (2 * n + 1)` via induction. Next, we study the behavior of the ratio
+  `∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)) / ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)` and prove that
+  it converges to one using the squeeze theorem. The final product for `π` is obtained after some
+  algebraic manipulation. -/
+theorem tendsto_prod_pi_div_two :
+  tendsto (λ k, ∏ i in range k,
+    (((2:ℝ) * i + 2) / (2 * i + 1)) * ((2 * i + 2) / (2 * i + 3))) at_top (𝓝 (π/2)) :=
+begin
+  suffices h : tendsto (λ k, 2 / π  * ∏ i in range k,
+    (((2:ℝ) * i + 2) / (2 * i + 1)) * ((2 * i + 2) / (2 * i + 3))) at_top (𝓝 1),
+  { have := tendsto.const_mul (π / 2) h,
+    have h : π / 2 ≠ 0, norm_num [pi_ne_zero],
+    simp only [← mul_assoc, ← @inv_div _ _ π 2, mul_inv_cancel h, one_mul, mul_one] at this,
+    exact this },
+  have h : (λ (k : ℕ), (2:ℝ) / π * ∏ (i : ℕ) in range k,
+    ((2 * i + 2) / (2 * i + 1)) * ((2 * i + 2) / (2 * i + 3))) =
+  λ k, (2 * ∏ i in range k,
+    (2 * i + 2) / (2 * i + 3)) / (π * ∏ (i : ℕ) in range k, (2 * i + 1) / (2 * i + 2)),
+  { funext,
+    have h : ∏ (i : ℕ) in range k, ((2:ℝ) * ↑i + 2) / (2 * ↑i + 1) =
+      1 / (∏ (i : ℕ) in range k, (2 * ↑i + 1) / (2 * ↑i + 2)),
+    { rw [one_div, ← finset.prod_inv_distrib'],
+      refine prod_congr rfl (λ x hx, _),
+      field_simp },
+    rw [prod_mul_distrib, h],
+    field_simp },
+  simp only [h, ← integral_sin_pow_even, ← integral_sin_pow_odd],
+  exact integral_sin_pow_div_tendsto_one,
+end
+
 end real