Source indexedlemma · leanprover/lean4:v4.32.0

ZeroFactorization

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:382 to 427

Mathematical statement

Exact Lean statement

@[blueprint "ZeroFactorization"
  (title := "ZeroFactorization")
  (statement := /--
    Let $f:\mathbb{C}\to\mathbb{C}$ be analytic on $\overline{\mathbb{D}_1}$ with $f(0)\neq 0$.
    For all $\rho\in\mathcal{K}_f(R)$ with $R<1$ there exists $h_\rho(z)$ such that
    $h_\rho(z)$ is analytic at $\rho$, $h_\rho(\rho)\neq 0$, and
    $f(z)=(z-\rho)^{m_f(\rho)}\,h_\rho(z)$.
  -/)
  (proof := /--
    Since $f$ is analytic on neighborhoods of points in $\overline{\mathbb{D}_1}$ we know
    that there exists a series expansion about $\rho$:
    $$f(z)=\sum_{0\leq n}a_n\,(z-\rho)^n.$$
    Now if we let $m$ be the smallest number such that $a_m\neq 0$, then
    $$f(z)=\sum_{0\leq n}a_n\,(z-\rho)^n=\sum_{m\leq n}a_n\,(z-\rho)^n
      =(z-\rho)^m\sum_{m\leq n}a_n\,(z-\rho)^{n-m}=(z-\rho)^m\,h_\rho(z).$$
    Trivially, $h_\rho(z)$ is analytic at $\rho$ (we have written down the series
    expansion); now note that
    $$h_\rho(\rho)=\sum_{m\leq n}a_n(\rho-\rho)^{n-m}=\sum_{m\leq n}a_n0^{n-m}=a_m\neq 0.$$
  -/)
  (latexEnv := "lemma")]
lemma ZeroFactorization {R : ℝ} {f : ℂ → ℂ} {ρ : ℂ}
    (RleOne : R < 1)
    (hfAnalytic : AnalyticOnNhd ℂ f (Metric.closedBall (0 : ℂ) 1))
    (hf_neq_zero_at_zero : f 0 ≠ 0)
    (hρ : ρ ∈ SetOfZeros R f) :
    ∃ h_ρ : ℂ → ℂ, AnalyticAt ℂ h_ρ ρ ∧ h_ρ ρ ≠ 0 ∧ ZeroFactor f ρ = h_ρ ρ ∧
      f =ᶠ[nhds ρ] fun z ↦ (z - ρ) ^ analyticOrderNatAt f ρ * h_ρ z

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint "ZeroFactorization"  (title := "ZeroFactorization")  (statement := /--    Let $f:\mathbb{C}\to\mathbb{C}$ be analytic on $\overline{\mathbb{D}_1}$ with $f(0)\neq 0$.    For all $\rho\in\mathcal{K}_f(R)$ with $R<1$ there exists $h_\rho(z)$ such that    $h_\rho(z)$ is analytic at $\rho$, $h_\rho(\rho)\neq 0$, and    $f(z)=(z-\rho)^{m_f(\rho)}\,h_\rho(z)$.  -/)  (proof := /--    Since $f$ is analytic on neighborhoods of points in $\overline{\mathbb{D}_1}$ we know    that there exists a series expansion about $\rho$:    $$f(z)=\sum_{0\leq n}a_n\,(z-\rho)^n.$$    Now if we let $m$ be the smallest number such that $a_m\neq 0$, then    $$f(z)=\sum_{0\leq n}a_n\,(z-\rho)^n=\sum_{m\leq n}a_n\,(z-\rho)^n      =(z-\rho)^m\sum_{m\leq n}a_n\,(z-\rho)^{n-m}=(z-\rho)^m\,h_\rho(z).$$    Trivially, $h_\rho(z)$ is analytic at $\rho$ (we have written down the series    expansion); now note that    $$h_\rho(\rho)=\sum_{m\leq n}a_n(\rho-\rho)^{n-m}=\sum_{m\leq n}a_n0^{n-m}=a_m\neq 0.$$  -/)  (latexEnv := "lemma")]lemma ZeroFactorization {R : ℝ} {f : ℂ → ℂ} {ρ : ℂ}    (RleOne : R < 1)    (hfAnalytic : AnalyticOnNhd ℂ f (Metric.closedBall (0 : ℂ) 1))    (hf_neq_zero_at_zero : f 0 ≠ 0)    (hρ : ρ ∈ SetOfZeros R f) :    ∃ h_ρ : ℂ → ℂ, AnalyticAt ℂ h_ρ ρ ∧ h_ρ ρ ≠ 0 ∧ ZeroFactor f ρ = h_ρ ρ ∧      f =ᶠ[nhds ρ] fun z ↦ (z - ρ) ^ analyticOrderNatAt f ρ * h_ρ z := by  have zero_mem_closedBall : 0 ∈ Metric.closedBall (0 : ℂ) 1 := by    rw[mem_closedBall_iff_norm, sub_zero, norm_zero]    exact zero_le_one  have ρ_mem_closedBall : ρ ∈ Metric.closedBall (0 : ℂ) 1 := by    rw[mem_closedBall_iff_norm, sub_zero]    linarith[hρ.1]  have orderAtZeroIsZero : analyticOrderAt f 0 = 0 := by    rw[analyticOrderAt_eq_zero]    exact Or.symm (Decidable.not_or_of_imp fun a a_1 ↦ hf_neq_zero_at_zero a)  have finiteOrder : analyticOrderAt f ρ ≠ ⊤ := by    refine AnalyticOnNhd.analyticOrderAt_ne_top_of_isPreconnected hfAnalytic (Metric.isPreconnected_closedBall) zero_mem_closedBall ρ_mem_closedBall (lt_top_iff_ne_top.mp ?_)    rw[orderAtZeroIsZero]    exact ENat.top_pos  have AnalyticAt_ρ : AnalyticAt ℂ f ρ := by exact (hfAnalytic ρ ρ_mem_closedBall)  obtain ⟨h_ρ, h_ρ_neq_zero_at_zero, f_eq⟩ := (AnalyticAt_ρ.analyticOrderAt_ne_top.mp finiteOrder).choose_spec  set g := (AnalyticAt_ρ.analyticOrderAt_ne_top.mp finiteOrder).choose  refine ⟨g, h_ρ, h_ρ_neq_zero_at_zero, ?_, f_eq⟩  simp only [ZeroFactor, AnalyticAt_ρ, ↓reduceDIte, ne_eq, finiteOrder, not_false_eq_true,    smul_eq_mul, g]