Source indexedlemma · leanprover/lean4:v4.32.0

Complex.log_norm_weierstrassFactor_ge_log_norm_one_sub_nat_mul_max_one_norm_pow

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/WeierstrassFactor.lean:311 to 320

Mathematical statement

Exact Lean statement

lemma log_norm_weierstrassFactor_ge_log_norm_one_sub_nat_mul_max_one_norm_pow
    (m : ℕ) (z : ℂ) :
    Real.log ‖1 - z‖ - (m : ℝ) * max 1 (‖z‖ ^ m) ≤ Real.log ‖weierstrassFactor m z‖

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma log_norm_weierstrassFactor_ge_log_norm_one_sub_nat_mul_max_one_norm_pow    (m : ℕ) (z : ℂ) :    Real.log ‖1 - z‖ - (m : ℝ) * max 1 (‖z‖ ^ m) ≤ Real.log ‖weierstrassFactor m z‖ := by  calc    Real.log ‖1 - z‖ - (m : ℝ) * max 1 (‖z‖ ^ m)        ≤ Real.log ‖1 - z‖ - ‖partialLogSum m z‖ := by          gcongr          exact norm_partialLogSum_le_nat_mul_max_one_norm_pow m z    _ ≤ Real.log ‖weierstrassFactor m z‖ :=      log_norm_weierstrassFactor_ge_log_norm_one_sub_sub m z