Complex.log_norm_weierstrassFactor_ge_log_norm_one_sub_sub

For ‖z‖ ≤ 1 / 2, ‖E_m(z) - 1‖ ≤ 4‖z‖^(m+1). -/ theorem weierstrassFactor_sub_one_pow_bound {m : ℕ} {z : ℂ} (hz : ‖z‖ ≤ 1 / 2) : ‖weierstrassFactor m z - 1‖ ≤ 4 * ‖z‖ ^ (m + 1) := by by_cases hm : m = 0 · subst hm have hmain : ‖(1 - z) - 1‖ ≤ 4 * ‖z‖ ^ 1 := by have h : (1 - z) - 1 = -z := by ring calc ‖(1 - z) - 1‖ = ‖-z‖ := by simp [h] _ = ‖z‖ := norm_neg z _ = ‖z‖ ^ 1 := by simp _ ≤ 4 * ‖z‖ ^ 1 := by nlinarith [pow_nonneg (norm_nonneg z) 1] simpa [weierstrassFactor] using hmain · have hz_lt : ‖z‖ < 1 := lt_of_le_of_lt hz (by norm_num) by_cases hz1 : z = 1 · exfalso; rw [hz1] at hz; norm_num at hz have h_eq : weierstrassFactor m z = exp (-logTail m z) := weierstrassFactor_eq_exp_neg_tail m hz_lt hz1 rw [h_eq] have h_tail_bound := norm_logTail_le_two_mul_norm_pow hz_lt hz m have hw_le_one : ‖-logTail m z‖ ≤ 1 := by simp only [norm_neg] have : ‖logTail m z‖ ≤ 1 := by have hm_pos : 0 < m := Nat.pos_of_ne_zero hm have h2 : 2 ≤ m + 1 := by exact Nat.succ_le_succ (Nat.succ_le_iff.2 hm_pos) have hpow : (‖z‖ ^ (m + 1)) ≤ (‖z‖ ^ 2) := by have hz1' : ‖z‖ ≤ 1 := by nlinarith [hz] have hz0' : 0 ≤ ‖z‖ := norm_nonneg z exact pow_le_pow_of_le_one hz0' hz1' h2 have hmul : 2 * ‖z‖ ^ (m + 1) ≤ 2 * ‖z‖ ^ 2 := by gcongr have hsq : 2 * ‖z‖ ^ 2 ≤ 1 := by have hz0 : 0 ≤ ‖z‖ := norm_nonneg z have hz_sq : ‖z‖ ^ 2 ≤ (1 / 2 : ℝ) ^ 2 := pow_le_pow_left₀ hz0 hz 2 nlinarith exact (h_tail_bound.trans hmul).trans hsq linarith have h_exp_sub_one : ‖exp (-logTail m z) - 1‖ ≤ 2 * ‖-logTail m z‖ := Complex.norm_exp_sub_one_le hw_le_one simp only [norm_neg] at h_exp_sub_one calc ‖exp (-logTail m z) - 1‖ ≤ 2 * ‖logTail m z‖ := h_exp_sub_one _ ≤ 2 * (2 * ‖z‖ ^ (m + 1)) := by gcongr _ = 4 * ‖z‖ ^ (m + 1) := by ring

/-!

Lower bounds on Real.log ‖weierstrassFactor m z‖

Auxiliary inequalities for minimum-modulus / Cartan-type arguments in Hadamard factorization.