Source indexedlemma · leanprover/lean4:v4.32.0

BlaschkeOfZero

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:577 to 610

Mathematical statement

Exact Lean statement

@[blueprint "BlaschkeOfZero"
  (title := "BlaschkeOfZero")
  (statement := /--
    Let $0 < r < R<1$, and $f:\mathbb{C}\to\mathbb{C}$ be analytic on $\overline{\mathbb{D}_1}$ with
    $f(0)\neq 0$. Then
    $$|B_f(0)|=|f(0)|\prod_{\rho\in\mathcal{K}_f(r)}
      \left(\frac{R}{|\rho|}\right)^{m_f(\rho)}.$$
  -/)
  (proof := /--
    Since $f(0)\neq 0$, we know that $0\not\in\mathcal{K}_f(r)$. Thus,
    $$C_f(0)=\frac{f(0)}{\displaystyle\prod_{\rho\in\mathcal{K}_f(r)}(-\rho)^{m_f(\rho)}}.$$
    Thus, substituting this into Definition \ref{BlaschkeB},
    $$|B_f(0)|=|C_f(0)|\prod_{\rho\in\mathcal{K}_f(r)}R^{m_f(\rho)}
      =|f(0)|\prod_{\rho\in\mathcal{K}_f(r)}\left(\frac{R}{|\rho|}\right)^{m_f(\rho)}.$$
  -/)
  (latexEnv := "lemma")]
lemma BlaschkeOfZero {r R : ℝ} {f : ℂ → ℂ}
    (r_pos : 0 < r) (r_lt_one : r < 1) (r_lt_R : r < R)
    (finiteZeros : (SetOfZeros 1 f).Finite)
    (hf_neq_zero_at_zero : f 0 ≠ 0) :
    ‖BlaschkeB r R f 0‖ =
      ‖f 0‖ * (∏ ρ ∈ (finiteSetOfZeros_mono r_lt_one finiteZeros).toFinset, (R / ‖ρ‖) ^ (analyticOrderNatAt f ρ))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint "BlaschkeOfZero"  (title := "BlaschkeOfZero")  (statement := /--    Let $0 < r < R<1$, and $f:\mathbb{C}\to\mathbb{C}$ be analytic on $\overline{\mathbb{D}_1}$ with    $f(0)\neq 0$. Then    $$|B_f(0)|=|f(0)|\prod_{\rho\in\mathcal{K}_f(r)}      \left(\frac{R}{|\rho|}\right)^{m_f(\rho)}.$$  -/)  (proof := /--    Since $f(0)\neq 0$, we know that $0\not\in\mathcal{K}_f(r)$. Thus,    $$C_f(0)=\frac{f(0)}{\displaystyle\prod_{\rho\in\mathcal{K}_f(r)}(-\rho)^{m_f(\rho)}}.$$    Thus, substituting this into Definition \ref{BlaschkeB},    $$|B_f(0)|=|C_f(0)|\prod_{\rho\in\mathcal{K}_f(r)}R^{m_f(\rho)}      =|f(0)|\prod_{\rho\in\mathcal{K}_f(r)}\left(\frac{R}{|\rho|}\right)^{m_f(\rho)}.$$  -/)  (latexEnv := "lemma")]lemma BlaschkeOfZero {r R : ℝ} {f : ℂ → ℂ}    (r_pos : 0 < r) (r_lt_one : r < 1) (r_lt_R : r < R)    (finiteZeros : (SetOfZeros 1 f).Finite)    (hf_neq_zero_at_zero : f 0 ≠ 0) :    ‖BlaschkeB r R f 0‖ =      ‖f 0‖ * (∏ ρ ∈ (finiteSetOfZeros_mono r_lt_one finiteZeros).toFinset, (R / ‖ρ‖) ^ (analyticOrderNatAt f ρ)) := by  have zero_not_zero : ¬(0 ∈ SetOfZeros r f) := by    apply notMem_setOf_iff.mpr    simp only [norm_zero, not_and]    intro r    exact mem_support.mp hf_neq_zero_at_zero  unfold BlaschkeB Cf  simp only [finiteSetOfZeros_mono r_lt_one finiteZeros, zero_not_zero, ↓reduceDIte, zero_sub, zero_mul, zero_div, sub_zero,    Complex.norm_mul, Complex.norm_div, norm_prod, norm_pow, norm_neg, norm_real, norm_eq_abs]  rw[div_eq_mul_inv, mul_assoc, abs_of_pos (by linarith)]  refine (mul_right_inj' (norm_ne_zero_iff.mpr hf_neq_zero_at_zero)).mpr ?_  rw[← Finset.prod_inv_distrib, ← Finset.prod_mul_distrib]  simp only [div_eq_inv_mul, mul_pow, inv_pow]