Source indexedlemma · leanprover/lean4:v4.32.0

Complex.weierstrassFactor_eq_exp_neg_tail

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/WeierstrassFactor.lean:194 to 206

Source documentation

For ‖z‖ < 1 and z ≠ 1, E_m(z) = exp(-logTail_m(z)).

Exact Lean statement

lemma weierstrassFactor_eq_exp_neg_tail (m : ℕ) {z : ℂ} (hz : ‖z‖ < 1) (hz1 : z ≠ 1) :
    weierstrassFactor m z = exp (-logTail m z)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma weierstrassFactor_eq_exp_neg_tail (m : ℕ) {z : ℂ} (hz : ‖z‖ < 1) (hz1 : z ≠ 1) :    weierstrassFactor m z = exp (-logTail m z) := by  unfold weierstrassFactor  have hz_ne_1 : 1 - z ≠ 0 := sub_ne_zero.mpr hz1.symm  rw [← exp_log hz_ne_1, ← Complex.exp_add]  have hsum : log (1 - z) + partialLogSum m z = -logTail m z := by    have hdecomp := neg_log_one_sub_eq_partialLogSum_add_logTail hz m    calc      log (1 - z) + partialLogSum m z          = log (1 - z) + (partialLogSum m z + logTail m z) - logTail m z := by ring      _ = log (1 - z) + (-log (1 - z)) - logTail m z := by rw [hdecomp]      _ = -logTail m z := by ring  simp [hsum]