From 1cd2bf58b81e95012e85affd182e7fa37747224c Mon Sep 17 00:00:00 2001
From: Moritz Firsching <moritz.firsching@gmail.com>
Date: Mon, 27 Jun 2022 19:03:59 +0000
Subject: [PATCH] feat(analysis/special_functions/log/deriv): more power series
 for log (#14881)

This adds a power series expansion for `log ((a + 1) / a)`, and two lemmas that are needed for it. It's planned to be used in the proof of the Stirling formula.

Co-authored-by: nick-kuhn <46423253+nick-kuhn@users.noreply.github.com>



Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: nick-kuhn <46423253+nick-kuhn@users.noreply.github.com>
---
 src/analysis/special_functions/log/deriv.lean | 49 +++++++++++++++++--
 1 file changed, 46 insertions(+), 3 deletions(-)

diff --git a/src/analysis/special_functions/log/deriv.lean b/src/analysis/special_functions/log/deriv.lean
index b21469339a541..0e0cb2362cb1b 100644
--- a/src/analysis/special_functions/log/deriv.lean
+++ b/src/analysis/special_functions/log/deriv.lean
@@ -15,7 +15,7 @@ that the series `∑' n : ℕ, x ^ (n + 1) / (n + 1)` converges to `(-real.log (
 
 ## Tags
 
-logarighm, derivative
+logarithm, derivative
 -/
 
 open filter finset set
@@ -253,12 +253,12 @@ begin
   show summable (λ (n : ℕ), x ^ (n + 1) / (n + 1)),
   { refine summable_of_norm_bounded _ (summable_geometric_of_lt_1 (abs_nonneg _) h) (λ i, _),
     calc ∥x ^ (i + 1) / (i + 1)∥
-    = |x| ^ (i+1) / (i+1) :
+    = |x| ^ (i + 1) / (i + 1) :
       begin
         have : (0 : ℝ) ≤ i + 1 := le_of_lt (nat.cast_add_one_pos i),
         rw [norm_eq_abs, abs_div, ← pow_abs, abs_of_nonneg this],
       end
-    ... ≤ |x| ^ (i+1) / (0 + 1) :
+    ... ≤ |x| ^ (i + 1) / (0 + 1) :
       begin
         apply_rules [div_le_div_of_le_left, pow_nonneg, abs_nonneg, add_le_add_right,
           i.cast_nonneg],
@@ -268,4 +268,47 @@ begin
       by simpa [pow_succ'] using mul_le_of_le_one_right (pow_nonneg (abs_nonneg x) i) (le_of_lt h) }
 end
 
+/-- Power series expansion of `log(1 + x) - log(1 - x)` for `|x| < 1`. -/
+lemma has_sum_log_sub_log_of_abs_lt_1 {x : ℝ} (h : |x| < 1) :
+  has_sum (λ k : ℕ, (2 : ℝ) * (1 / (2 * k + 1)) * x ^ (2 * k + 1)) (log (1 + x) - log(1 - x)) :=
+begin
+  let term := λ n : ℕ, (-1) * ((-x) ^ (n + 1) / ((n : ℝ) + 1)) + x ^ (n + 1) / (n + 1),
+  have h_term_eq_goal : term ∘ (*) 2 = λ k : ℕ, 2 * (1 / (2 * k + 1)) * x ^ (2 * k + 1),
+  { ext n,
+    dsimp [term],
+    rw [odd.neg_pow (⟨n, rfl⟩ : odd (2 * n + 1)) x],
+    push_cast,
+    ring_nf, },
+  rw [← h_term_eq_goal, (nat.mul_right_injective two_pos).has_sum_iff],
+  { have h₁ := (has_sum_pow_div_log_of_abs_lt_1 (eq.trans_lt (abs_neg x) h)).mul_left (-1),
+    convert h₁.add (has_sum_pow_div_log_of_abs_lt_1 h),
+    ring_nf },
+  { intros m hm,
+    rw [range_two_mul, set.mem_set_of_eq] at hm,
+    dsimp [term],
+    rw [even.neg_pow (nat.even_succ.mpr hm), nat.succ_eq_add_one, neg_one_mul, neg_add_self] },
+end
+
+/-- Expansion of `log (1 + a⁻¹)` as a series in powers of `1 / (2 * a + 1)`. -/
+theorem has_sum_log_one_add_inv {a : ℝ} (h : 0 < a) :
+  has_sum (λ k : ℕ, (2 : ℝ) * (1 / (2 * k + 1)) * (1 / (2 * a + 1)) ^ (2 * k + 1))
+  (log (1 + a⁻¹)) :=
+begin
+  have h₁ : |1 / (2 * a + 1)| < 1,
+  { rw [abs_of_pos, div_lt_one],
+    { linarith, },
+    { linarith, },
+    { exact div_pos one_pos (by linarith), }, },
+  convert has_sum_log_sub_log_of_abs_lt_1 h₁,
+  have h₂ : (2 : ℝ) * a + 1 ≠ 0 := by linarith,
+  have h₃ := h.ne',
+  rw ← log_div,
+  { congr,
+    field_simp,
+    linarith, },
+  { field_simp,
+    linarith } ,
+  { field_simp },
+end
+
 end real