Source indexedlemma · leanprover/lean4:v4.32.0

BlaschkeAnalytic

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:547 to 573

Mathematical statement

Exact Lean statement

@[blueprint "BlaschkeAnalytic"
  (title := "BlaschkeAnalytic")
  (statement := /--
    If $f:\mathbb{C}\to\mathbb{C}$ is analytic on $\overline{\mathbb{D}_R}$ then so too is $B_f$.
  -/)
  (proof := /--
    Expand out $B_f$ as a product, and observe that each part is analytic on $\overline{\mathbb{D}_R}$.
  -/)
  (latexEnv := "lemma")]
lemma BlaschkeAnalytic {r R : ℝ} {f : ℂ → ℂ}
    (r_pos : 0 < r) (r_lt_R : r < R) (R_lt_one : R < 1)
    (finiteZeros : (SetOfZeros 1 f).Finite)
    (hfAnalytic : AnalyticOnNhd ℂ f (Metric.closedBall (0 : ℂ) 1))
    (hf_neq_zero_at_zero : f 0 ≠ 0) :
    AnalyticOnNhd ℂ (BlaschkeB r R f) (Metric.closedBall (0 : ℂ) R)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint "BlaschkeAnalytic"  (title := "BlaschkeAnalytic")  (statement := /--    If $f:\mathbb{C}\to\mathbb{C}$ is analytic on $\overline{\mathbb{D}_R}$ then so too is $B_f$.  -/)  (proof := /--    Expand out $B_f$ as a product, and observe that each part is analytic on $\overline{\mathbb{D}_R}$.  -/)  (latexEnv := "lemma")]lemma BlaschkeAnalytic {r R : ℝ} {f : ℂ → ℂ}    (r_pos : 0 < r) (r_lt_R : r < R) (R_lt_one : R < 1)    (finiteZeros : (SetOfZeros 1 f).Finite)    (hfAnalytic : AnalyticOnNhd ℂ f (Metric.closedBall (0 : ℂ) 1))    (hf_neq_zero_at_zero : f 0 ≠ 0) :    AnalyticOnNhd ℂ (BlaschkeB r R f) (Metric.closedBall (0 : ℂ) R) := by  have R_pos : 0 < R := lt_trans r_pos r_lt_R  have r_lt_one : r < 1 := lt_trans r_lt_R R_lt_one  unfold BlaschkeB  by_cases finite_zeros_mono : (SetOfZeros r f).Finite  · simp only [finite_zeros_mono, ↓reduceDIte]    refine AnalyticOnNhd.mul (CfAnalytic r_lt_R R_lt_one hfAnalytic hf_neq_zero_at_zero) (Finset.analyticOnNhd_fun_prod (finiteSetOfZeros_mono r_lt_one finiteZeros).toFinset ?_)    intro w hw    refine AnalyticOnNhd.fun_pow (AnalyticOnNhd.sub (analyticOnNhd_const) (AnalyticOnNhd.div (AnalyticOnNhd.mul (analyticOnNhd_id) (analyticOnNhd_const)) (analyticOnNhd_const) ?_)) (analyticOrderAt f w).toNat    intro w' hw'    exact_mod_cast ne_of_gt R_pos  · simp only [finite_zeros_mono, ↓reduceDIte]    exact analyticOnNhd_const