theorem DRinD1 (R : ℝ) (hR : 0 < R) (hR' : R < 1) : Metric.closedBall 0 R ⊆ Metric.ball 0 1

def zerosetKfR (R : ℝ) (hR : 0 < R) (f : ℂ → ℂ) : Set ℂ

Equations

• zerosetKfR R hR f = {ρ : ℂ | ρ ∈ Metric.closedBall 0 R ∧ f ρ = 0}

theorem lemKinDR (R : ℝ) (hR : 0 < R) (f : ℂ → ℂ) : zerosetKfR R hR f ⊆ Metric.closedBall 0 R

theorem lemKRinK1 (R : ℝ) (hR : 0 < R) (hR' : R < 1) (f : ℂ → ℂ) : zerosetKfR R hR f ⊆ {ρ : ℂ | ρ ∈ Metric.ball 0 1 ∧ f ρ = 0}

theorem lem_bolzano_weierstrass {D : Set ℂ} (hD : IsCompact D) {Z : Set ℂ} (hZ_inf : Z.Infinite) (hZ_sub_D : Z ⊆ D) : ∃ ρ₀ ∈ D, AccPt ρ₀ (Filter.principal Z)

theorem lem_zeros_have_limit_point (R : ℝ) (hR : 0 < R) (f : ℂ → ℂ) (h_Kf_inf : (zerosetKfR R hR f).Infinite) : ∃ ρ₀ ∈ Metric.closedBall 0 R, AccPt ρ₀ (Filter.principal (zerosetKfR R hR f))

theorem lem_identity_theorem (f : ℂ → ℂ) (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 1)) (ρ₀ : ℂ) (hρ₀_in_D1 : ρ₀ ∈ Metric.ball 0 1) (h_acc : AccPt ρ₀ (Filter.principal {ρ : ℂ | ρ ∈ Metric.ball 0 1 ∧ f ρ = 0})) : Set.EqOn f 0 (Metric.ball 0 1)

theorem lem_identity_theoremR (R : ℝ) (hR : 0 < R) (hR' : R < 1) (f : ℂ → ℂ) (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 1)) (ρ₀ : ℂ) (hρ₀_in_DR : ρ₀ ∈ Metric.closedBall 0 R) (h_acc : AccPt ρ₀ (Filter.principal {ρ : ℂ | ρ ∈ Metric.ball 0 1 ∧ f ρ = 0})) : Set.EqOn f 0 (Metric.ball 0 1)

theorem lem_identity_theoremKR (R : ℝ) (hR : 0 < R) (hR' : R < 1) (f : ℂ → ℂ) (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 1)) (h_exists_rho0 : ∃ ρ₀ ∈ Metric.closedBall 0 R, AccPt ρ₀ (Filter.principal (zerosetKfR R hR f))) : Set.EqOn f 0 (Metric.ball 0 1)

theorem lem_identity_infiniteKR (R : ℝ) (hR : 0 < R) (hR' : R < 1) (f : ℂ → ℂ) (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 1)) (h_Kf_inf : (zerosetKfR R hR f).Infinite) : Set.EqOn f 0 (Metric.ball 0 1)

theorem lem_Contra_finiteKR (R : ℝ) (hR : 0 < R) (hR' : R < 1) (f : ℂ → ℂ) (hf : AnalyticOnNhd ℂ f (Metric.closedBall 0 1)) (h_exists_nonzero : ∃ z ∈ Metric.ball 0 1, f z ≠ 0) : (zerosetKfR R hR f).Finite

theorem lem_frho_zero (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (ρ : ℂ) (h_rho_in_KfR1 : ρ ∈ zerosetKfR R1 ⋯ f) : f ρ = 0

theorem lem_m_rho_is_nat (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (hR_lt_1 : R < 1) (ρ : ℂ) (h_rho_in_KfR1 : ρ ∈ zerosetKfR R1 ⋯ f) : analyticOrderAt f ρ ≠ ⊤

theorem analyticOrderAt_ge_one_of_zero (f : ℂ → ℂ) (z : ℂ) (hf : AnalyticAt ℂ f z) (hz : f z = 0) (hfinite : analyticOrderAt f z ≠ ⊤) : analyticOrderAt f z ≥ 1

theorem lem_m_rho_ge_1 (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (hR_lt_1 : R < 1) (ρ : ℂ) (h_rho_in_KfR1 : ρ ∈ zerosetKfR R1 ⋯ f) : analyticOrderAt f ρ ≥ 1

The quotient Cf (no core wrapper)

noncomputable def Cf (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (z : ℂ) : ℂ

The “deflated” quotient: divide f by the product of (z-ρ)^{m_ρ}, and at a zero z=σ use the local factor function h_σ σ in the numerator (so the expression extends analytically).

Equations

• One or more equations did not get rendered due to their size.

Helper lemmas used by the Cf proofs (statements only)

theorem lem_analDiv (R : ℝ) (hR_pos : 0 < R) (hR_lt_1 : R < 1) (w : ℂ) (hw : w ∈ Metric.closedBall 0 R) (h g : ℂ → ℂ) (hh : AnalyticAt ℂ h w) (hg : AnalyticAt ℂ g w) (hg_ne : g w ≠ 0) : AnalyticAt ℂ (fun (z : ℂ) => h z / g z) w

theorem lem_denomAnalAt (S : Finset ℂ) (n : ℂ → ℕ) (hn_pos : ∀ s ∈ S, 0 < n s) (w : ℂ) (hw : w ∉ S) : AnalyticAt ℂ (fun (z : ℂ) => ∏ s ∈ S, (z - s) ^ n s) w ∧ ∏ s ∈ S, (w - s) ^ n s ≠ 0

theorem lem_ratioAnalAt (w : ℂ) (R R1 : ℝ) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (h : ℂ → ℂ) (hh : AnalyticAt ℂ h w) (S : Finset ℂ) (hS : ↑S ⊆ Metric.closedBall 0 R1) (n : ℂ → ℕ) (hn_pos : ∀ s ∈ S, 0 < n s) (hw : w ∈ Metric.closedBall 0 1 \ ↑S) : AnalyticAt ℂ (fun (z : ℂ) => h z / ∏ s ∈ S, (z - s) ^ n s) w

theorem lem_analytic_zero_factor (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (σ : ℂ) (hσ : σ ∈ zerosetKfR R1 ⋯ f) : ∃ (h_σ : ℂ → ℂ), AnalyticAt ℂ h_σ σ ∧ h_σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ z

Cf lemmas (renamed to use Cf directly)

theorem lem_Cf_analytic_off_K {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) (hz : z ∈ Metric.closedBall 0 R \ zerosetKfR R1 ⋯ f) : AnalyticAt ℂ (Cf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ) z

theorem lem_Cf_at_sigma_onK {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (σ : ℂ) (hσ : σ ∈ zerosetKfR R1 ⋯ f) : ∀ᶠ (z : ℂ) in nhds σ, z = σ → Cf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ z = h_σ z z / ∏ ρ ∈ h_finite_zeros.toFinset.erase σ, (z - ρ) ^ (analyticOrderAt f ρ).toNat

theorem lem_K_isolated {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (σ ρ : ℂ) (hσ : σ ∈ zerosetKfR R1 ⋯ f) (hρ : ρ ∈ zerosetKfR R1 ⋯ f) (hne : σ ≠ ρ) : ∀ᶠ (z : ℂ) in nhds σ, z ≠ ρ

theorem lem_Cf_at_sigma_offK0 {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (σ : ℂ) (hσ : σ ∈ zerosetKfR R1 ⋯ f) : ∀ᶠ (z : ℂ) in nhds σ, z ≠ σ → Cf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z / ∏ ρ ∈ h_finite_zeros.toFinset, (z - ρ) ^ (analyticOrderAt f ρ).toNat

theorem lem_prod_no_sigma1 {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (σ : ℂ) (hσ : σ ∈ zerosetKfR R1 ⋯ f) (z : ℂ) : ∏ ρ ∈ h_finite_zeros.toFinset, (z - ρ) ^ (analyticOrderAt f ρ).toNat = (z - σ) ^ (analyticOrderAt f σ).toNat * ∏ ρ ∈ h_finite_zeros.toFinset.erase σ, (z - ρ) ^ (analyticOrderAt f ρ).toNat

theorem lem_prod_no_sigma2 {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (σ : ℂ) (hσ : σ ∈ zerosetKfR R1 ⋯ f) (z : ℂ) (hz : z ∉ zerosetKfR R1 ⋯ f) : (z - σ) ^ (analyticOrderAt f σ).toNat / ∏ ρ ∈ h_finite_zeros.toFinset, (z - ρ) ^ (analyticOrderAt f ρ).toNat = 1 / ∏ ρ ∈ h_finite_zeros.toFinset.erase σ, (z - ρ) ^ (analyticOrderAt f ρ).toNat

theorem lem_Cf_at_sigma_offK {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (σ : ℂ) (hσ : σ ∈ zerosetKfR R1 ⋯ f) : ∀ᶠ (z : ℂ) in nhds σ, z ≠ σ → Cf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ z = h_σ σ z / ∏ ρ ∈ h_finite_zeros.toFinset.erase σ, (z - ρ) ^ (analyticOrderAt f ρ).toNat

theorem lem_Cf_at_sigma {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (σ : ℂ) (hσ : σ ∈ zerosetKfR R1 ⋯ f) : ∀ᶠ (z : ℂ) in nhds σ, Cf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ z = h_σ σ z / ∏ ρ ∈ h_finite_zeros.toFinset.erase σ, (z - ρ) ^ (analyticOrderAt f ρ).toNat

theorem lem_h_ratio_anal {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (σ : ℂ) (hσ : σ ∈ zerosetKfR R1 ⋯ f) (g : ℂ → ℂ) (hg_analytic : AnalyticAt ℂ g σ) : AnalyticAt ℂ (fun (z : ℂ) => g z / ∏ ρ ∈ h_finite_zeros.toFinset.erase σ, (z - ρ) ^ (analyticOrderAt f ρ).toNat) σ

theorem lem_Cf_analytic_at_K {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (σ : ℂ) (hσ : σ ∈ zerosetKfR R1 ⋯ f) : AnalyticAt ℂ (Cf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ) σ

theorem lem_Cf_is_analytic {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) (hz : z ∈ Metric.closedBall 0 R) : AnalyticAt ℂ (Cf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ) z

theorem lem_f_nonzero_off_K {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (z : ℂ) (hz : z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f) : f z ≠ 0

theorem lem_Cf_nonzero_off_K {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) (hz : z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f) : Cf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ z ≠ 0

theorem lem_Cf_nonzero_on_K {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (σ : ℂ) (hσ : σ ∈ zerosetKfR R1 ⋯ f) : Cf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ σ ≠ 0

theorem lem_Cf_never_zero {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) (hz : z ∈ Metric.closedBall 0 R1) : Cf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ z ≠ 0

theorem factor_nonzero_outside_domain (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (ρ : ℂ) (hρ_bound : ‖ρ‖ ≤ R1) (hρ_ne_zero : ρ ≠ 0) (z : ℂ) (hz_in_R1 : ‖z‖ ≤ R1) : ↑R - star ρ * z / ↑R ≠ 0

theorem linear_pow_analytic (a b : ℂ) (n : ℕ) (z : ℂ) : AnalyticAt ℂ (fun (w : ℂ) => (a - b * w) ^ n) z

theorem bl_num_diff {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (z : ℂ) (hz : z ∈ Metric.closedBall 0 R) : DifferentiableAt ℂ (fun (w : ℂ) => ∏ ρ ∈ h_finite_zeros.toFinset, (↑R - star ρ * w / ↑R) ^ (analyticOrderAt f ρ).toNat) z

theorem lem_bl_num_nonzero {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (z : ℂ) (hz : z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f) : ∏ ρ ∈ h_finite_zeros.toFinset, (↑R - star ρ * z / ↑R) ^ (analyticOrderAt f ρ).toNat ≠ 0

noncomputable def Bf (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (z : ℂ) : ℂ

Equations

• One or more equations did not get rendered due to their size.

theorem lem_BfCf {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (z : ℂ) (hz : z ∈ Metric.closedBall 0 R \ zerosetKfR R1 ⋯ f) : Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ z = (f z * ∏ ρ ∈ h_finite_zeros.toFinset, (↑R - star ρ * z / ↑R) ^ (analyticOrderAt f ρ).toNat) / ∏ ρ ∈ h_finite_zeros.toFinset, (z - ρ) ^ (analyticOrderAt f ρ).toNat

theorem lem_Bf_div {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (z : ℂ) (hz : z ∈ Metric.closedBall 0 R \ zerosetKfR R1 ⋯ f) : (∏ ρ ∈ h_finite_zeros.toFinset, (↑R - star ρ * z / ↑R) ^ (analyticOrderAt f ρ).toNat) / ∏ ρ ∈ h_finite_zeros.toFinset, (z - ρ) ^ (analyticOrderAt f ρ).toNat = ∏ ρ ∈ h_finite_zeros.toFinset, (↑R - star ρ * z / ↑R) ^ (analyticOrderAt f ρ).toNat / (z - ρ) ^ (analyticOrderAt f ρ).toNat

theorem lem_Bf_prodpow {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (z : ℂ) (hz : z ∈ Metric.closedBall 0 R \ zerosetKfR R1 ⋯ f) : ∏ ρ ∈ h_finite_zeros.toFinset, (↑R - star ρ * z / ↑R) ^ (analyticOrderAt f ρ).toNat / (z - ρ) ^ (analyticOrderAt f ρ).toNat = ∏ ρ ∈ h_finite_zeros.toFinset, ((↑R - star ρ * z / ↑R) / (z - ρ)) ^ (analyticOrderAt f ρ).toNat

theorem lem_Bf_off_K {R R1 : ℝ} {hR1_pos : 0 < R1} {hR1_lt_R : R1 < R} {hR_lt_1 : R < 1} {f : ℂ → ℂ} {h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z} {h_f_nonzero_at_zero : f 0 ≠ 0} (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (z : ℂ) (hz : z ∈ Metric.closedBall 0 R \ zerosetKfR R1 ⋯ f) : Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ z = f z * ∏ ρ ∈ h_finite_zeros.toFinset, ((↑R - star ρ * z / ↑R) / (z - ρ)) ^ (analyticOrderAt f ρ).toNat

theorem lem_frho_zero_contra (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (ρ : ℂ) : f ρ ≠ 0 → ρ ∉ zerosetKfR R1 ⋯ f

theorem lem_f_is_nonzero (f : ℂ → ℂ) : f 0 ≠ 0 → f ≠ 0

theorem lem_rho_in_disk_R1 (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (f : ℂ → ℂ) (ρ : ℂ) (h_rho_in_KfR1 : ρ ∈ zerosetKfR R1 ⋯ f) : ‖ρ‖ ≤ R1

theorem lem_zero_not_in_Kf (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) : f 0 ≠ 0 → 0 ∉ zerosetKfR R1 ⋯ f

theorem lem_rho_ne_zero (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (ρ : ℂ) : ρ ∈ zerosetKfR R1 ⋯ f → ρ ≠ 0

theorem lem_mod_pos_iff_ne_zero (z : ℂ) : z ≠ 0 → ‖z‖ > 0

theorem lem_mod_rho_pos (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (ρ : ℂ) : ρ ∈ zerosetKfR R1 ⋯ f → ‖ρ‖ > 0

theorem lem_rho_in_disk_R1_repeat (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (f : ℂ → ℂ) (ρ : ℂ) (h_rho_in_KfR1 : ρ ∈ zerosetKfR R1 ⋯ f) : ‖ρ‖ ≤ R1

theorem lem_inv_mono_decr (x y : ℝ) (hx : 0 < x) (hxy : x ≤ y) : 1 / x ≥ 1 / y

theorem lem_inv_mod_rho_ge_inv_R1 (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (ρ : ℂ) (h_rho_in_KfR1 : ρ ∈ zerosetKfR R1 ⋯ f) : 1 / ‖ρ‖ ≥ 1 / R1

theorem lem_mul_pos_preserves_ineq (a b c : ℝ) (hab : a ≤ b) (hc : 0 < c) : a * c ≤ b * c

theorem lem_R_div_mod_rho_ge_R_div_R1 (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (ρ : ℂ) (h_rho_in_KfR1 : ρ ∈ zerosetKfR R1 ⋯ f) : R / ‖ρ‖ ≥ R / R1

theorem lem_R_div_mod_rho_ge_R_over_R1 (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (ρ : ℂ) (h_rho_in_KfR1 : ρ ∈ zerosetKfR R1 ⋯ f) : R / ‖ρ‖ ≥ R / R1

theorem lem_mod_of_prod2 {ι : Type u_1} (K : Finset ι) (w : ι → ℂ) : ‖∏ ρ ∈ K, w ρ‖ = ∏ ρ ∈ K, ‖w ρ‖

theorem lem_mod_Bf_is_prod_mod (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) (hz : z ∉ zerosetKfR R1 ⋯ f) : ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ z‖ = ‖f z‖ * ∏ ρ ∈ h_finite_zeros.toFinset, ‖((↑R - z * star ρ / ↑R) / (z - ρ)) ^ (analyticOrderAt f ρ).toNat‖

theorem lem_abs_pow (w : ℂ) (n : ℕ) : ‖w ^ n‖ = ‖w‖ ^ n

theorem lem_Bmod_pow (R R1 : ℝ) (hR_pos : 0 < R) (hR1 : R1 = 2 * R / 3) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (ρ : ℂ) (h_rho_in_KfR1 : ρ ∈ zerosetKfR R1 ⋯ f) (z : ℂ) : ‖((↑R - z * star ρ / ↑R) / (z - ρ)) ^ (analyticOrderAt f ρ).toNat‖ = ‖(↑R - z * star ρ / ↑R) / (z - ρ)‖ ^ (analyticOrderAt f ρ).toNat

theorem lem_mod_Bf_prod_mod (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) (hz : z ∉ zerosetKfR R1 ⋯ f) : ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ z‖ = ‖f z‖ * ∏ ρ ∈ h_finite_zeros.toFinset, ‖(↑R - z * star ρ / ↑R) / (z - ρ)‖ ^ (analyticOrderAt f ρ).toNat

theorem lem_mod_Bf_at_0 (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) : ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ 0‖ = ‖f 0‖ * ∏ ρ ∈ h_finite_zeros.toFinset, ‖↑R / -ρ‖ ^ (analyticOrderAt f ρ).toNat

theorem lem_mod_div_ (w1 w2 : ℂ) (hw2_ne_zero : w2 ≠ 0) : ‖w1 / w2‖ = ‖w1‖ / ‖w2‖

theorem lem_mod_neg (w : ℂ) : ‖-w‖ = ‖w‖

theorem lem_mod_div_and_neg (R : ℝ) (hR_pos : 0 < R) (ρ : ℂ) (h_rho_ne_zero : ρ ≠ 0) : ‖↑R / -ρ‖ = R / ‖ρ‖

theorem lem_mod_Bf_at_0_eval (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) : ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ 0‖ = ‖f 0‖ * ∏ ρ ∈ h_finite_zeros.toFinset, (R / ‖ρ‖) ^ (analyticOrderAt f ρ).toNat

theorem lem_mod_of_pos_real (x : ℝ) (hx : 0 < x) : |x| = x

theorem lem_mod_Bf_at_0_as_ratio (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) : ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ 0‖ = ‖f 0‖ * ∏ ρ ∈ h_finite_zeros.toFinset, (R / ‖ρ‖) ^ (analyticOrderAt f ρ).toNat

theorem lem_prod_ineq {ι : Type u_1} (K : Finset ι) (a b : ι → ℝ) (h_nonneg : ∀ ρ ∈ K, 0 ≤ a ρ) (h_le : ∀ ρ ∈ K, a ρ ≤ b ρ) : ∏ ρ ∈ K, a ρ ≤ ∏ ρ ∈ K, b ρ

theorem lem_power_ineq (n : ℕ) (c : ℝ) (hc : c > 1) (hn : n ≥ 1) : c ≤ c ^ n

theorem lem_power_ineq_1 (n : ℕ) (c : ℝ) (hc : 1 ≤ c) (hn : 1 ≤ n) : 1 ≤ c ^ n

theorem lem_prod_power_ineq {ι : Type u_1} (K : Finset ι) (c : ι → ℝ) (n : ι → ℕ) (h_c_ge_1 : ∀ ρ ∈ K, 1 ≤ c ρ) (h_n_ge_1 : ∀ ρ ∈ K, 1 ≤ n ρ) : ∏ ρ ∈ K, c ρ ^ n ρ ≥ 1

theorem lem_prod_1 {ι : Type u_1} {M : Type u_2} [CommMonoid M] (K : Finset ι) : ∏ _ρ ∈ K, 1 = 1

theorem lem_prod_power_ineq1 {ι : Type u_1} (K : Finset ι) (c : ι → ℝ) (n : ι → ℕ) (h_c_ge_1 : ∀ ρ ∈ K, 1 ≤ c ρ) (h_n_ge_1 : ∀ ρ ∈ K, 1 ≤ n ρ) : ∏ ρ ∈ K, c ρ ^ n ρ ≥ 1

theorem lem_mod_lower_bound_1 (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (hf0_eq_one : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (hR_lt_1 : R < 1) : ∏ ρ ∈ h_finite_zeros.toFinset, (R / R1) ^ (analyticOrderAt f ρ).toNat ≥ 1

theorem lem_mod_Bf_at_0_ge_1 (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (hf0_eq_one : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) : ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ 0‖ ≥ 1

theorem lem_linear_factor_analytic (R : ℝ) (hR_pos : 0 < R) (ρ z : ℂ) : AnalyticAt ℂ (fun (w : ℂ) => ↑R - star ρ * w / ↑R) z

theorem lem_pow_analyticAt {g : ℂ → ℂ} (n : ℕ) (w : ℂ) : AnalyticAt ℂ g w → AnalyticAt ℂ (fun (z : ℂ) => g z ^ n) w

theorem lem_finset_prod_analyticAt {α : Type u_1} {S : Finset α} {g : α → ℂ → ℂ} (w : ℂ) : (∀ a ∈ S, AnalyticAt ℂ (g a) w) → AnalyticAt ℂ (fun (z : ℂ) => ∏ a ∈ S, g a z) w

theorem analyticOrderAt_top_iff_eventually_zero (f : ℂ → ℂ) (z : ℂ) (hf : AnalyticAt ℂ f z) : analyticOrderAt f z = ⊤ ↔ ∀ᶠ (w : ℂ) in nhds z, f w = 0

theorem isPreconnected_closedBall (x : ℂ) (r : ℝ) : IsPreconnected (Metric.closedBall x r)

theorem Set.infinite_Icc_of_lt {a b : ℝ} (h : a < b) : (Icc a b).Infinite

theorem infinite_closedBall_of_pos (x : ℂ) (r : ℝ) (hr : 0 < r) : (Metric.closedBall x r).Infinite

theorem analyticOrderAt_ne_top_of_finite_zeros_in_ball (f : ℂ → ℂ) (R : ℝ) (hR_pos : 0 < R) (hf_analytic : ∀ z ∈ Metric.closedBall 0 R, AnalyticAt ℂ f z) (ρ : ℂ) (hρ_zero : f ρ = 0) (hρ_in_ball : ρ ∈ Metric.closedBall 0 R) (h_finite_zeros : {z : ℂ | z ∈ Metric.closedBall 0 R ∧ f z = 0}.Finite) : analyticOrderAt f ρ ≠ ⊤

theorem lem_Bf_is_analytic (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) : AnalyticOnNhd ℂ (Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ) (Metric.closedBall 0 R)

theorem complex_mul_star_eq_norm_sq (z : ℂ) : z * star z = ↑‖z‖ ^ 2

theorem lem_mod_Bf_eq_mod_f_on_boundary (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) : ‖z‖ = R → ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ z‖ = ‖f z‖

theorem lem_Bf_bounded_on_boundary (B R R1 : ℝ) (hB : 1 < B) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (hf_le_B : ∀ (z : ℂ), ‖z‖ ≤ R → ‖f z‖ ≤ B) (z : ℂ) : ‖z‖ = R → ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ z‖ ≤ B

theorem norm_eq_radius_of_mem_sphere (w : ℂ) (R : ℝ) (hw : w ∈ Metric.sphere 0 R) : ‖w‖ = R

theorem mem_closedBall_of_norm_le {z : ℂ} {R : ℝ} (hz : ‖z‖ ≤ R) : z ∈ Metric.closedBall 0 R

theorem closure_ball_eq_closedBall_center (R : ℝ) (hR : 0 < R) : closure (Metric.ball 0 R) = Metric.closedBall 0 R

theorem lem_max_mod_principle_for_Bf (B R : ℝ) (hB : 1 < B) (hR_pos : 0 < R) (fB : ℂ → ℂ) (h_analytic : AnalyticOnNhd ℂ fB (Metric.closedBall 0 R)) (h_bd_boundary : ∀ (z : ℂ), ‖z‖ = R → ‖fB z‖ ≤ B) (z : ℂ) : ‖z‖ ≤ R → ‖fB z‖ ≤ B

theorem lem_Bf_bounded_in_disk_from_boundary (B R R1 : ℝ) (hB : 1 < B) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (h_bd_boundary : ∀ (z : ℂ), ‖z‖ = R → ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ z‖ ≤ B) (z : ℂ) : ‖z‖ ≤ R → ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ z‖ ≤ B

theorem lem_Bf_bounded_in_disk_from_f (B R R1 : ℝ) (hB : 1 < B) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (hf_le_B : ∀ (z : ℂ), ‖z‖ ≤ R → ‖f z‖ ≤ B) (z : ℂ) : ‖z‖ ≤ R → ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ z‖ ≤ B

theorem lem_Bf_at_0_le_M (B R R1 : ℝ) (hB : 1 < B) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (hf_le_B : ∀ (z : ℂ), ‖z‖ ≤ R → ‖f z‖ ≤ B) : ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ 0‖ ≤ B

theorem lem_combine_bounds_on_Bf0 (B R R1 : ℝ) (hB : 1 < B) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (hf0_eq_one : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (hBf0 : ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ 0‖ ≤ B) : (R / R1) ^ ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat ≤ B

theorem lem_jensen_inequality_form (B R R1 : ℝ) (hB : 1 < B) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (hf0_eq_one : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (hf_le_B : ∀ (z : ℂ), ‖z‖ ≤ R → ‖f z‖ ≤ B) : (R / R1) ^ ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat ≤ B

theorem lem_log_mono_inc {x y : ℝ} (hx : 0 < x) (hxy : x ≤ y) : Real.log x ≤ Real.log y

theorem lem_three_gt_e : 3 > Real.exp 1

theorem lem_jensen_log_form (B R R1 : ℝ) (hB : 1 < B) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (hf0_eq_one : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (hf_le_B : ∀ (z : ℂ), ‖z‖ ≤ R → ‖f z‖ ≤ B) : (∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat) * Real.log (R / R1) ≤ Real.log B

theorem lem_sum_ineq {ι : Type u_1} (K : Finset ι) (a b : ι → ℝ) (h_le : ∀ i ∈ K, a i ≤ b i) : K.sum a ≤ K.sum b

theorem ENat_coe_ge_one_iff_nat_ge_one (n : ℕ) : ↑n ≥ 1 ↔ 1 ≤ n

theorem nat_one_le_cast_real (n : ℕ) : 1 ≤ n → 1 ≤ ↑n

theorem zerosetKfR_eq_zeros_in_ball (R : ℝ) (hR_pos : 0 < R) (f : ℂ → ℂ) : zerosetKfR R hR_pos f = {z : ℂ | z ∈ Metric.closedBall 0 R ∧ f z = 0}

theorem lem_frho_zero' (R R1 : ℝ) (hR_pos : 0 < R1) (hR1 : R1 < R) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (ρ : ℂ) (h_rho_in_KfR1 : ρ ∈ zerosetKfR R1 ⋯ f) : f ρ = 0

theorem lem_sum_m_rho_1 (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (hR_lt_1 : R < 1) : ↑h_finite_zeros.toFinset.card ≤ ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat

theorem lem_sum_1_is_card {ι : Type u_1} (K : Finset ι) : ∑ x ∈ K, 1 = ↑K.card

theorem lem_sum_m_rho_bound (B R R1 : ℝ) (hB : 1 < B) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (hf0_eq_one : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (hf_le_B : ∀ (z : ℂ), ‖z‖ ≤ R → ‖f z‖ ≤ B) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) : ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat ≤ 1 / Real.log (R / R1) * Real.log B

theorem lem_sum_1_bound (B R R1 : ℝ) (hB : 1 < B) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (hf0_eq_one : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (hf_le_B : ∀ (z : ℂ), ‖z‖ ≤ R → ‖f z‖ ≤ B) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) : ↑h_finite_zeros.toFinset.card ≤ 1 / Real.log (R / R1) * Real.log B

theorem lem_num_zeros_bound (B R R1 : ℝ) (hB : 1 < B) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (hf0_eq_one : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (hf_le_B : ∀ (z : ℂ), ‖z‖ ≤ R → ‖f z‖ ≤ B) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) : let S_zeros := zerosetKfR R1 ⋯ f; have inst_fintype_S_zeros := h_finite_zeros.fintype; ↑S_zeros.toFinset.card ≤ 1 / Real.log (R / R1) * Real.log B

theorem f_zero_ne_zero {f : ℂ → ℂ} (h_f_zero : f 0 = 1) : f 0 ≠ 0

theorem Bf_is_analytic_on_disk (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) : AnalyticOnNhd ℂ (Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ) (Metric.closedBall 0 R)

theorem lem_Bf_eq_prod_Cf (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) : Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ z = (∏ ρ ∈ h_finite_zeros.toFinset, (↑R - star ρ * z / ↑R) ^ (analyticOrderAt f ρ).toNat) * Cf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic h_f_nonzero_at_zero h_finite_zeros h_σ z

theorem lem_num_prod_never_zero_all (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_nonzero_at_zero : f 0 ≠ 0) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) : z ∈ Metric.closedBall 0 R1 → ∏ ρ ∈ h_finite_zeros.toFinset, (↑R - star ρ * z / ↑R) ^ (analyticOrderAt f ρ).toNat ≠ 0

theorem Bf_never_zero (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) : z ∈ Metric.closedBall 0 R1 → Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ z ≠ 0

theorem Bf0_not_zero (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) : Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ 0 ≠ 0

noncomputable def Lf {R R1 r : ℝ} {f : ℂ → ℂ} {h_σ : ℂ → ℂ → ℂ} (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (hR1_pos : 0 < R1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) : ℂ → ℂ

Equations

• Lf hr_pos hr_lt_R1 hR1_lt_R hR_lt_1 hR1_pos h_f_analytic h_f_zero h_finite_zeros h_σ_spec = Classical.choose ⋯

theorem Lf_is_analytic (r R R1 : ℝ) (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) : AnalyticOnNhd ℂ (Lf hr_pos hr_lt_R1 hR1_lt_R hR_lt_1 hR1_pos h_f_analytic h_f_zero h_finite_zeros h_σ_spec) (Metric.closedBall 0 r)

theorem Lf_at_0_is_0 (r R R1 : ℝ) (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) : Lf hr_pos hr_lt_R1 hR1_lt_R hR_lt_1 hR1_pos h_f_analytic h_f_zero h_finite_zeros h_σ_spec 0 = 0

theorem lem_BCII {L : ℂ → ℂ} {r M r₁ : ℝ} (hr_pos : 0 < r) (hM_pos : 0 < M) (hr₁_pos : 0 < r₁) (hr₁_lt_r : r₁ < r) (hL_domain : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 r ⊆ U ∧ DifferentiableOn ℂ L U) (hL0 : L 0 = 0) (hre_L_le_M : ∀ w ∈ Metric.closedBall 0 r, (L w).re ≤ M) {z : ℂ} (hz : z ∈ Metric.closedBall 0 r₁) : ‖deriv L z‖ ≤ 16 * M * r ^ 2 / (r - r₁) ^ 3

theorem re_Lf_as_diff_of_log_mods (r R R1 : ℝ) (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) : z ∈ Metric.closedBall 0 r → (Lf hr_pos hr_lt_R1 hR1_lt_R hR_lt_1 hR1_pos h_f_analytic h_f_zero h_finite_zeros h_σ_spec z).re = Real.log ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ z‖ - Real.log ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ 0‖

theorem log_Bf_le_log_B (B R R1 : ℝ) (hB : 1 < B) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (h_Bf_pos : ∀ (z : ℂ), ‖z‖ ≤ R1 → 0 < ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ z‖) (h_Bf_bound : ∀ (z : ℂ), ‖z‖ ≤ R1 → ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ z‖ ≤ B) (z : ℂ) : ‖z‖ ≤ R1 → Real.log ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ z‖ ≤ Real.log B

theorem log_Bf_le_log_B2 (B R R1 : ℝ) (hB : 1 < B) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (h_Bf_bound : ∀ (z : ℂ), ‖z‖ ≤ R → ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ z‖ ≤ B) (z : ℂ) : ‖z‖ ≤ R1 → Real.log ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ z‖ ≤ Real.log B

theorem log_Bf_le_log_B3 (B R R1 : ℝ) (hB : 1 < B) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (h_f_bound : ∀ (z : ℂ), ‖z‖ ≤ R → ‖f z‖ ≤ B) (z : ℂ) : ‖z‖ ≤ R1 → Real.log ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ z‖ ≤ Real.log B

theorem log_Bf0_ge_0 (R R1 : ℝ) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) : 0 ≤ Real.log ‖Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ 0‖

theorem re_Lf_le_log_B (B r R R1 : ℝ) (hB : 1 < B) (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (h_f_bound : ∀ (z : ℂ), ‖z‖ ≤ R → ‖f z‖ ≤ B) (z : ℂ) : ‖z‖ ≤ r → (Lf hr_pos hr_lt_R1 hR1_lt_R hR_lt_1 hR1_pos h_f_analytic h_f_zero h_finite_zeros h_σ_spec z).re ≤ Real.log B

theorem analyticOnNhd_closedBall_exists_open_differentiableOn {L : ℂ → ℂ} {r : ℝ} (h : AnalyticOnNhd ℂ L (Metric.closedBall 0 r)) : ∃ (U : Set ℂ), IsOpen U ∧ Metric.closedBall 0 r ⊆ U ∧ DifferentiableOn ℂ L U

theorem log_pos_of_one_lt {B : ℝ} (hB : 1 < B) : 0 < Real.log B

theorem apply_BC_to_Lf (B r1 r R R1 : ℝ) (hB : 1 < B) (hr1_pos : 0 < r1) (hr1_lt_r : r1 < r) (hr_lt_R1 : r < R1) (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (h_f_bound : ∀ (z : ℂ), ‖z‖ ≤ R → ‖f z‖ ≤ B) (z : ℂ) : ‖z‖ ≤ r1 → ‖deriv (Lf ⋯ hr_lt_R1 hR1_lt_R hR_lt_1 hR1_pos h_f_analytic h_f_zero h_finite_zeros h_σ_spec) z‖ ≤ 16 * Real.log B * r ^ 2 / (r - r1) ^ 3

theorem analyticOnNhd_Bf_closedBall {R R1 r : ℝ} {f : ℂ → ℂ} {h_σ : ℂ → ℂ → ℂ} (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (hR1_pos : 0 < R1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) : AnalyticOnNhd ℂ (Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ) (Metric.closedBall 0 R)

theorem helper_Bf_analytic_on_disk {R R1 r : ℝ} {f : ℂ → ℂ} {h_σ : ℂ → ℂ → ℂ} (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (hR1_pos : 0 < R1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) : z ∈ Metric.closedBall 0 R → AnalyticAt ℂ (Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ) z

theorem closedBall_R1_subset_R {R R1 : ℝ} (hR1_nonneg : 0 ≤ R1) (hR1_lt_R : R1 < R) : Metric.closedBall 0 R1 ⊆ Metric.closedBall 0 R

theorem logDerivconst {a : ℂ} {g : ℂ → ℂ} (ha : a ≠ 0) (z : ℂ) : logDeriv (fun (w : ℂ) => a * g w) z = logDeriv g z

theorem oneBneq0 {R R1 r : ℝ} {f : ℂ → ℂ} {h_σ : ℂ → ℂ → ℂ} (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (hR1_pos : 0 < R1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) : Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ 0 ≠ 0 ∧ (Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ 0)⁻¹ ≠ 0

theorem Lf_deriv_is_logBf_deriv {R R1 r : ℝ} {f : ℂ → ℂ} {h_σ : ℂ → ℂ → ℂ} (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (hR1_pos : 0 < R1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) : z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f → logDeriv (fun (w : ℂ) => Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ w / Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ 0) z = logDeriv (fun (w : ℂ) => Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ w) z

theorem logDeriv_div_const {a : ℂ} {g : ℂ → ℂ} (ha : a ≠ 0) (z : ℂ) : logDeriv (fun (w : ℂ) => g w / a) z = logDeriv g z

theorem deriv_over_fun_is_logDeriv {g : ℂ → ℂ} (z : ℂ) : deriv g z / g z = logDeriv g z

theorem logDerivmul {f g : ℂ → ℂ} {z : ℂ} (hf : DifferentiableAt ℂ f z) (hg : DifferentiableAt ℂ g z) (hf_ne : f z ≠ 0) (hg_ne : g z ≠ 0) : logDeriv (fun (w : ℂ) => f w * g w) z = logDeriv f z + logDeriv g z

theorem logDerivprod {K : Finset ℂ} {g : ℂ → ℂ → ℂ} {z : ℂ} (hg_diff : ∀ ρ ∈ K, DifferentiableAt ℂ (g ρ) z) (hg_ne : ∀ ρ ∈ K, g ρ z ≠ 0) : logDeriv (fun (w : ℂ) => ∏ ρ ∈ K, g ρ w) z = ∑ ρ ∈ K, logDeriv (g ρ) z

theorem logDerivdiv {h g : ℂ → ℂ} {z : ℂ} (hh : DifferentiableAt ℂ h z) (hg : DifferentiableAt ℂ g z) (hh_ne : h z ≠ 0) (hg_ne : g z ≠ 0) : logDeriv (fun (w : ℂ) => h w / g w) z = logDeriv h z - logDeriv g z

theorem logDerivfunpow {g : ℂ → ℂ} {z : ℂ} {m : ℕ} (hg : DifferentiableAt ℂ g z) : logDeriv (fun (w : ℂ) => g w ^ m) z = ↑m * logDeriv g z

theorem z_minus_rho_diff_nonzero {R R1 : ℝ} {f : ℂ → ℂ} (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (ρ : ℂ) : ρ ∈ zerosetKfR R1 ⋯ f → ∀ z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f, z - ρ ≠ 0 ∧ DifferentiableAt ℂ (fun (w : ℂ) => w - ρ) z

theorem blaschke_num_diff_nonzero {R R1 : ℝ} {f : ℂ → ℂ} (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (ρ : ℂ) : ρ ∈ zerosetKfR R1 ⋯ f → ∀ z ∈ Metric.closedBall 0 R, ↑R - star ρ * z / ↑R ≠ 0 ∧ DifferentiableAt ℂ (fun (w : ℂ) => ↑R - star ρ * w / ↑R) z

theorem blaschke_frac_diff_nonzero {R R1 : ℝ} {f : ℂ → ℂ} (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (ρ : ℂ) : ρ ∈ zerosetKfR R1 ⋯ f → ∀ z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f, (↑R - star ρ * z / ↑R) / (z - ρ) ≠ 0 ∧ DifferentiableAt ℂ (fun (w : ℂ) => (↑R - star ρ * w / ↑R) / (w - ρ)) z

theorem blaschke_pow_diff_nonzero {R R1 : ℝ} {f : ℂ → ℂ} (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (ρ : ℂ) : ρ ∈ zerosetKfR R1 ⋯ f → ∀ z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f, ((↑R - star ρ * z / ↑R) / (z - ρ)) ^ (analyticOrderAt f ρ).toNat ≠ 0 ∧ DifferentiableAt ℂ (fun (w : ℂ) => ((↑R - star ρ * w / ↑R) / (w - ρ)) ^ (analyticOrderAt f ρ).toNat) z

theorem blaschke_prod_diff_nonzero {R R1 : ℝ} {f : ℂ → ℂ} (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (z : ℂ) : z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f → ∏ ρ ∈ h_finite_zeros.toFinset, ((↑R - star ρ * z / ↑R) / (z - ρ)) ^ (analyticOrderAt f ρ).toNat ≠ 0 ∧ DifferentiableAt ℂ (fun (w : ℂ) => ∏ ρ ∈ h_finite_zeros.toFinset, ((↑R - star ρ * w / ↑R) / (w - ρ)) ^ (analyticOrderAt f ρ).toNat) z

theorem f_diff_nonzero_outside_Kf {R R1 : ℝ} {f : ℂ → ℂ} (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (z : ℂ) : z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f → f z ≠ 0 ∧ DifferentiableAt ℂ f z

theorem Bf_diff_nonzero_outside_Kf {R R1 r : ℝ} {f : ℂ → ℂ} {h_σ : ℂ → ℂ → ℂ} (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (hR1_pos : 0 < R1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) : z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f → Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ z ≠ 0 ∧ DifferentiableAt ℂ (Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ) z

theorem logDeriv_fprod_is_sum {R R1 : ℝ} {f : ℂ → ℂ} (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (z : ℂ) : z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f → logDeriv (fun (w : ℂ) => f w * ∏ ρ ∈ h_finite_zeros.toFinset, ((↑R - star ρ * w / ↑R) / (w - ρ)) ^ (analyticOrderAt f ρ).toNat) z = logDeriv f z + logDeriv (fun (w : ℂ) => ∏ ρ ∈ h_finite_zeros.toFinset, ((↑R - star ρ * w / ↑R) / (w - ρ)) ^ (analyticOrderAt f ρ).toNat) z

theorem nhds_avoids_finset {z : ℂ} (K : Finset ℂ) (hz : z ∉ ↑K) : ∀ᶠ (w : ℂ) in nhds z, ∀ ρ ∈ K, w ≠ ρ

theorem pow_div_pow_eq_div_pow (a b : ℂ) (n : ℕ) : a ^ n / b ^ n = (a / b) ^ n

theorem Cf_eventually_eq_f_div_prod {R R1 : ℝ} {f : ℂ → ℂ} (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ : ℂ → ℂ → ℂ) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) {z : ℂ} (hz : z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f) : (fun (w : ℂ) => Cf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ w) =ᶠ[nhds z] fun (w : ℂ) => f w / ∏ ρ ∈ h_finite_zeros.toFinset, (w - ρ) ^ (analyticOrderAt f ρ).toNat

theorem eventuallyEq_mul_right_fun {α : Type u_1} {β : Type u_2} {l : Filter α} [Mul β] {f g h : α → β} (hfg : f =ᶠ[l] g) : (fun (x : α) => f x * h x) =ᶠ[l] fun (x : α) => g x * h x

theorem inv_prod_complex {ι : Type u_1} (s : Finset ι) (f : ι → ℂ) : (∏ x ∈ s, f x)⁻¹ = ∏ x ∈ s, (f x)⁻¹

theorem prod_num_mul_inv_den_eq_prod_ratio (K : Finset ℂ) (N D : ℂ → ℂ) (m : ℂ → ℕ) : (∏ ρ ∈ K, N ρ ^ m ρ) * (∏ ρ ∈ K, D ρ ^ m ρ)⁻¹ = ∏ ρ ∈ K, (N ρ / D ρ) ^ m ρ

theorem prod_num_mul_inv_den_eq_prod_ratio_fun (K : Finset ℂ) (N D : ℂ → ℂ → ℂ) (m : ℂ → ℕ) : (fun (w : ℂ) => (∏ ρ ∈ K, N ρ w ^ m ρ) * (∏ ρ ∈ K, D ρ w ^ m ρ)⁻¹) = fun (w : ℂ) => ∏ ρ ∈ K, (N ρ w / D ρ w) ^ m ρ

theorem div_mul_eq_mul_mul_inv_fun {α : Sort u_1} (f A B : α → ℂ) : (fun (w : α) => f w / A w * B w) = fun (w : α) => f w * (B w * (A w)⁻¹)

theorem assoc_fun_mul {α : Sort u_1} (f g h : α → ℂ) : (fun (w : α) => f w * (g w * h w)) = fun (w : α) => f w * g w * h w

theorem prod_num_mul_inv_den_eq_prod_ratio_fun_mem (K : Finset ℂ) (N D : ℂ → ℂ → ℂ) (m : ℂ → ℕ) : (fun (w : ℂ) => (∏ ρ ∈ K, N ρ w ^ m ρ) * (∏ ρ ∈ K, D ρ w ^ m ρ)⁻¹) = fun (w : ℂ) => ∏ ρ ∈ K, (N ρ w / D ρ w) ^ m ρ

theorem eventuallyEq_of_eq {α : Type u_1} {β : Type u_2} {l : Filter α} {f g : α → β} (h : f = g) : f =ᶠ[l] g

theorem logDeriv_congr_of_eventuallyEq {f g : ℂ → ℂ} {z : ℂ} (hfg : f =ᶠ[nhds z] g) : logDeriv f z = logDeriv g z

theorem logDeriv_Bf_is_sum {R R1 r : ℝ} {f : ℂ → ℂ} {h_σ : ℂ → ℂ → ℂ} (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (hR1_pos : 0 < R1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (z : ℂ) : z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f → logDeriv (Bf R R1 hR1_pos hR1_lt_R hR_lt_1 f h_f_analytic ⋯ h_finite_zeros h_σ) z = logDeriv f z + logDeriv (fun (w : ℂ) => ∏ ρ ∈ h_finite_zeros.toFinset, ((↑R - star ρ * w / ↑R) / (w - ρ)) ^ (analyticOrderAt f ρ).toNat) z

theorem logDeriv_def_as_frac {f : ℂ → ℂ} {z : ℂ} (hf : DifferentiableAt ℂ f z) (hf_ne : f z ≠ 0) : logDeriv f z = deriv f z / f z

def ball_containment {r R1 : ℝ} (_hr_pos : 0 < r) (hr_lt_R1 : r < R1) (z : ℂ) (hz : z ∈ Metric.closedBall 0 r) : z ∈ Metric.closedBall 0 R1

Equations

• ⋯ = ⋯

theorem in_r_minus_kf {R1 r : ℝ} {f : ℂ → ℂ} (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (z : ℂ) (hz : z ∈ Metric.closedBall 0 r \ zerosetKfR R1 ⋯ f) : z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f

theorem Lf_deriv_step1 {R R1 r : ℝ} {f : ℂ → ℂ} {h_σ : ℂ → ℂ → ℂ} (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (hR1_pos : 0 < R1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) : z ∈ Metric.closedBall 0 r \ zerosetKfR R1 ⋯ f → deriv (Lf hr_pos hr_lt_R1 hR1_lt_R hR_lt_1 hR1_pos h_f_analytic h_f_zero h_finite_zeros h_σ_spec) z = deriv f z / f z + logDeriv (fun (w : ℂ) => ∏ ρ ∈ h_finite_zeros.toFinset, ((↑R - star ρ * w / ↑R) / (w - ρ)) ^ (analyticOrderAt f ρ).toNat) z

theorem logDeriv_prod_is_sum {R R1 : ℝ} {f : ℂ → ℂ} (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (z : ℂ) : z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f → logDeriv (fun (w : ℂ) => ∏ ρ ∈ h_finite_zeros.toFinset, ((↑R - star ρ * w / ↑R) / (w - ρ)) ^ (analyticOrderAt f ρ).toNat) z = ∑ ρ ∈ h_finite_zeros.toFinset, logDeriv (fun (w : ℂ) => ((↑R - star ρ * w / ↑R) / (w - ρ)) ^ (analyticOrderAt f ρ).toNat) z

theorem logDeriv_power_is_mul {R R1 : ℝ} {f : ℂ → ℂ} (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (z : ℂ) : z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f → ∀ ρ ∈ h_finite_zeros.toFinset, logDeriv (fun (w : ℂ) => ((↑R - star ρ * w / ↑R) / (w - ρ)) ^ (analyticOrderAt f ρ).toNat) z = ↑(analyticOrderAt f ρ).toNat * logDeriv (fun (w : ℂ) => (↑R - star ρ * w / ↑R) / (w - ρ)) z

theorem logDeriv_prod_is_sum_mul {R R1 : ℝ} {f : ℂ → ℂ} (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (z : ℂ) : z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f → logDeriv (fun (w : ℂ) => ∏ ρ ∈ h_finite_zeros.toFinset, ((↑R - star ρ * w / ↑R) / (w - ρ)) ^ (analyticOrderAt f ρ).toNat) z = ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat * logDeriv (fun (w : ℂ) => (↑R - star ρ * w / ↑R) / (w - ρ)) z

theorem Lf_deriv_step2 {R R1 r : ℝ} {f : ℂ → ℂ} {h_σ : ℂ → ℂ → ℂ} (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (hR1_pos : 0 < R1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) : z ∈ Metric.closedBall 0 r \ zerosetKfR R1 ⋯ f → deriv (Lf hr_pos hr_lt_R1 hR1_lt_R hR_lt_1 hR1_pos h_f_analytic h_f_zero h_finite_zeros h_σ_spec) z = deriv f z / f z + ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat * logDeriv (fun (w : ℂ) => (↑R - star ρ * w / ↑R) / (w - ρ)) z

theorem logDeriv_Blaschke_is_diff {R R1 : ℝ} {f : ℂ → ℂ} (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (z : ℂ) : z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f → ∀ ρ ∈ h_finite_zeros.toFinset, logDeriv (fun (w : ℂ) => (↑R - star ρ * w / ↑R) / (w - ρ)) z = logDeriv (fun (w : ℂ) => ↑R - star ρ * w / ↑R) z - logDeriv (fun (w : ℂ) => w - ρ) z

theorem logDeriv_linear {a b z : ℂ} (ha : a ≠ 0) (hz : z ≠ -b / a) : logDeriv (fun (w : ℂ) => a * w + b) z = a / (a * z + b)

theorem logDeriv_denominator {ρ z : ℂ} (hz : z ≠ ρ) : logDeriv (fun (w : ℂ) => w - ρ) z = 1 / (z - ρ)

theorem logDeriv_numerator_pre {R : ℝ} {ρ z : ℂ} : logDeriv (fun (w : ℂ) => ↑R - star ρ * w / ↑R) z = -star ρ / ↑R / (↑R - star ρ * z / ↑R)

theorem star_ne_zero_of_ne_zero {ρ : ℂ} (hρ : ρ ≠ 0) : star ρ ≠ 0

theorem field_identity_general {K : Type u_1} [Field K] {a b c : K} (ha : a ≠ 0) (hb : b ≠ 0) (hden : a - c * b / a ≠ 0) : -(b / a) / (a - c * b / a) = 1 / (c - a ^ 2 / b)

theorem complex_identity_from_field {R : ℝ} {ρ z : ℂ} (hR : R ≠ 0) (hρ : ρ ≠ 0) (hden : ↑R - star ρ * z / ↑R ≠ 0) : -star ρ / ↑R / (↑R - star ρ * z / ↑R) = 1 / (z - ↑R ^ 2 / star ρ)

theorem logDeriv_numerator_rearranged {R : ℝ} {ρ z : ℂ} (hR : R ≠ 0) (hrho : ρ ≠ 0) (h_denom_ne_zero : ↑R - star ρ * z / ↑R ≠ 0) : -star ρ / ↑R / (↑R - star ρ * z / ↑R) = 1 / (z - ↑R ^ 2 / star ρ)

theorem logDeriv_numerator {R : ℝ} {ρ z : ℂ} (hR : R ≠ 0) (hrho : ρ ≠ 0) (h_denom_ne_zero : ↑R - star ρ * z / ↑R ≠ 0) : logDeriv (fun (w : ℂ) => ↑R - star ρ * w / ↑R) z = 1 / (z - ↑R ^ 2 / star ρ)

theorem logDeriv_Blaschke_is_diff_frac {R R1 : ℝ} {f : ℂ → ℂ} (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (h_f_zero : f 0 = 1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (ρ : ℂ) : ρ ∈ h_finite_zeros.toFinset → ∀ z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f, logDeriv (fun (w : ℂ) => (↑R - star ρ * w / ↑R) / (w - ρ)) z = 1 / (z - ↑R ^ 2 / star ρ) - 1 / (z - ρ)

theorem Lf_deriv_step3 {R R1 r : ℝ} {f : ℂ → ℂ} {h_σ : ℂ → ℂ → ℂ} (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (hR1_pos : 0 < R1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) : z ∈ Metric.closedBall 0 r \ zerosetKfR R1 ⋯ f → deriv (Lf hr_pos hr_lt_R1 hR1_lt_R hR_lt_1 hR1_pos h_f_analytic h_f_zero h_finite_zeros h_σ_spec) z = deriv f z / f z + ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat * (1 / (z - ↑R ^ 2 / star ρ) - 1 / (z - ρ))

theorem sum_of_diff {K : Finset ℂ} {a b : ℂ → ℂ} : ∑ ρ ∈ K, (a ρ - b ρ) = ∑ ρ ∈ K, a ρ - ∑ ρ ∈ K, b ρ

theorem sum_rearranged {r R R1 : ℝ} {f : ℂ → ℂ} (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (z : ℂ) : z ∈ Metric.closedBall 0 r \ zerosetKfR R1 ⋯ f → ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat * (1 / (z - ↑R ^ 2 / star ρ) - 1 / (z - ρ)) = ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat / (z - ↑R ^ 2 / star ρ) - ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat / (z - ρ)

theorem Lf_deriv_final_formula {R R1 r : ℝ} {f : ℂ → ℂ} {h_σ : ℂ → ℂ → ℂ} (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (hR1_pos : 0 < R1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) : z ∈ Metric.closedBall 0 r \ zerosetKfR R1 ⋯ f → deriv (Lf hr_pos hr_lt_R1 hR1_lt_R hR_lt_1 hR1_pos h_f_analytic h_f_zero h_finite_zeros h_σ_spec) z = deriv f z / f z - ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat / (z - ρ) + ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat / (z - ↑R ^ 2 / star ρ)

theorem rearrange_Lf_deriv {R R1 r : ℝ} {f : ℂ → ℂ} {h_σ : ℂ → ℂ → ℂ} (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (hR1_pos : 0 < R1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) : z ∈ Metric.closedBall 0 r \ zerosetKfR R1 ⋯ f → deriv f z / f z - ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat / (z - ρ) = deriv (Lf hr_pos hr_lt_R1 hR1_lt_R hR_lt_1 hR1_pos h_f_analytic h_f_zero h_finite_zeros h_σ_spec) z - ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat / (z - ↑R ^ 2 / star ρ)

theorem triangle_ineq_sum {w₁ w₂ : ℂ} : ‖w₁ - w₂‖ ≤ ‖w₁‖ + ‖w₂‖

theorem target_inequality_setup {R R1 r : ℝ} {f : ℂ → ℂ} {h_σ : ℂ → ℂ → ℂ} (hr_pos : 0 < r) (hr_lt_R1 : r < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (hR1_pos : 0 < R1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (z : ℂ) : z ∈ Metric.closedBall 0 r \ zerosetKfR R1 ⋯ f → ‖deriv f z / f z - ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat / (z - ρ)‖ ≤ ‖deriv (Lf hr_pos hr_lt_R1 hR1_lt_R hR_lt_1 hR1_pos h_f_analytic h_f_zero h_finite_zeros h_σ_spec) z‖ + ‖∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat / (z - ↑R ^ 2 / star ρ)‖

theorem conj_norm_eq_norm (z : ℂ) : ‖star z‖ = ‖z‖

theorem norm_div_eq (a b : ℂ) (hb : b ≠ 0) : ‖a / b‖ = ‖a‖ / ‖b‖

theorem norm_Rsq_div_conj (R : ℝ) (ρ : ℂ) (hρ : ρ ≠ 0) : ‖↑R ^ 2 / star ρ‖ = R ^ 2 / ‖ρ‖

theorem zerosetKfR_subset_closedBall {R1 : ℝ} (hR1 : 0 < R1) {f : ℂ → ℂ} : zerosetKfR R1 hR1 f ⊆ Metric.closedBall 0 R1

theorem mem_zerosetKfR_ne_zero_of_f0_eq_one {R1 : ℝ} (hR1 : 0 < R1) {f : ℂ → ℂ} (hf0 : f 0 = 1) {ρ : ℂ} (hρ : ρ ∈ zerosetKfR R1 hR1 f) : ρ ≠ 0

theorem norm_sub_ge_norm_sub (x y : ℂ) : ‖x - y‖ ≥ ‖y‖ - ‖x‖

theorem mem_zerosetKfR_norm_le {R1 : ℝ} (hR1 : 0 < R1) {f : ℂ → ℂ} {ρ : ℂ} (hρ : ρ ∈ zerosetKfR R1 hR1 f) : ‖ρ‖ ≤ R1

theorem lem_sum_bound_step2 {R R1 : ℝ} {f : ℂ → ℂ} (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (z : ℂ) : z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f → ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat / ‖z - ↑R ^ 2 / star ρ‖ ≤ 1 / (R ^ 2 / R1 - R1) * ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat

theorem sq_div_sub_pos (a b : ℝ) (ha_pos : 0 < a) (hab : a < b) : 0 < b ^ 2 / a - a

theorem final_sum_bound {R R1 B : ℝ} {f : ℂ → ℂ} (hR1_pos : 0 < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (hB : 1 < B) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_f_bounded : ∀ z ∈ Metric.closedBall 0 R, ‖f z‖ ≤ B) (z : ℂ) : z ∈ Metric.closedBall 0 R1 \ zerosetKfR R1 ⋯ f → ‖∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat / (z - ↑R ^ 2 / star ρ)‖ ≤ 1 / ((R ^ 2 / R1 - R1) * Real.log (R / R1)) * Real.log B

theorem final_inequality {h_σ : ℂ → ℂ → ℂ} (B : ℝ) (hB : 1 < B) (r1 r R R1 : ℝ) (hr1pos : 0 < r1) (hr1_lt_r : r1 < r) (hr_lt_R1 : r < R1) (hR1_lt_R : R1 < R) (hR_lt_1 : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (h_f_bounded : ∀ z ∈ Metric.closedBall 0 R, ‖f z‖ ≤ B) (z : ℂ) : z ∈ Metric.closedBall 0 r1 \ zerosetKfR R1 ⋯ f → ‖deriv f z / f z - ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat / (z - ρ)‖ ≤ 16 * r ^ 2 / (r - r1) ^ 3 * Real.log B + 1 / ((R ^ 2 / R1 - R1) * Real.log (R / R1)) * Real.log B

theorem final_ineq1 {h_σ : ℂ → ℂ → ℂ} (B : ℝ) (hB : 1 < B) (r1 r R R1 : ℝ) (hr1pos : 0 < r1) (hr1_lt_r : r1 < r) (hr_lt_R1 : r < R1) (hR1_lt_R : R1 < R) (hR : R < 1) (f : ℂ → ℂ) (h_f_analytic : ∀ z ∈ Metric.closedBall 0 1, AnalyticAt ℂ f z) (h_f_zero : f 0 = 1) (h_finite_zeros : (zerosetKfR R1 ⋯ f).Finite) (h_σ_spec : ∀ σ ∈ zerosetKfR R1 ⋯ f, AnalyticAt ℂ (h_σ σ) σ ∧ h_σ σ σ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds σ, f z = (z - σ) ^ (analyticOrderAt f σ).toNat * h_σ σ z) (h_f_bounded : ∀ z ∈ Metric.closedBall 0 R, ‖f z‖ ≤ B) (z : ℂ) : z ∈ Metric.closedBall 0 r1 \ zerosetKfR R1 ⋯ f → ‖deriv f z / f z - ∑ ρ ∈ h_finite_zeros.toFinset, ↑(analyticOrderAt f ρ).toNat / (z - ρ)‖ ≤ (16 * r ^ 2 / (r - r1) ^ 3 + 1 / ((R ^ 2 / R1 - R1) * Real.log (R / R1))) * Real.log B