Source indexedlemma · leanprover/lean4:v4.32.0

Complex.neg_log_one_sub_eq_partialLogSum_add_logTail

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean:246 to 258

Source documentation

Decompose the logarithm series into its first m terms and the remaining tail.

Exact Lean statement

lemma neg_log_one_sub_eq_partialLogSum_add_logTail {z : ℂ} (hz : ‖z‖ < 1) (m : ℕ) :
    -log (1 - z) = partialLogSum m z + logTail m z

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma neg_log_one_sub_eq_partialLogSum_add_logTail {z : ℂ} (hz : ‖z‖ < 1) (m : ℕ) :    -log (1 - z) = partialLogSum m z + logTail m z := by  let f : ℕ → ℂ := fun k ↦ z ^ (k + 1) / ((k : ℂ) + 1)  have h_summable : Summable f := by    simpa [f, Nat.cast_add, Nat.cast_one, add_assoc, add_comm, add_left_comm] using      (summable_logTail hz 0)  have h_decomp := h_summable.sum_add_tsum_nat_add m  rw [neg_log_one_sub_eq_tsum hz, partialLogSum_eq_sum, ← h_decomp]  congr 1  dsimp only [logTail]  refine tsum_congr fun k ↦ ?_  simp only [f, Nat.cast_add]  ring_nf