Source indexedlemma · leanprover/lean4:v4.32.0

DiskBound

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:653 to 710

Mathematical statement

Exact Lean statement

@[blueprint "DiskBound"
  (title := "DiskBound")
  (statement := /--
    Let $0 < r < R<1$. If $f:\mathbb{C}\to\mathbb{C}$ is a function analytic on
    $\overline{\mathbb{D}_1}$ with $f(0)\neq0$ such that $|f(z)|\leq B$ for $|z|\leq R$,
    then $|B_f(z)|\leq B$ for $|z|\leq R$ also.
  -/)
  (proof := /--
    For $|z|=R$, we know that $z\not\in\mathcal{K}_f(r)$. Thus,
    $$C_f(z)=\frac{f(z)}{\displaystyle\prod_{\rho\in\mathcal{K}_f(r)}(z-\rho)^{m_f(\rho)}}.$$
    Thus, substituting this into Definition \ref{BlaschkeB},
    $$|B_f(z)|=|f(z)|\prod_{\rho\in\mathcal{K}_f(r)}
      \left|\frac{R-z\overline{\rho}/R}{z-\rho}\right|^{m_f(\rho)}.$$
    But note that
    $$\left|\frac{R-z\overline{\rho}/R}{z-\rho}\right|
      =\frac{|R^2-z\overline{\rho}|/R}{|z-\rho|}
      =\frac{|z|\cdot|\overline{z-\rho}|/R}{|z-\rho|}=1.$$
    So we have that $|B_f(z)|=|f(z)|\leq B$ when $|z|=R$. Now by the maximum modulus
    principle, we know that the maximum of $|B_f|$ must occur on the boundary where
    $|z|=R$. Thus $|B_f(z)|\leq B$ for all $|z|\leq R$.
  -/)
  (latexEnv := "lemma")]
lemma DiskBound {B r R : ℝ} {f : ℂ → ℂ} {z : ℂ}
    (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) (fz_bound : ∀ (z : ℂ), ‖z‖ ≤ R → ‖f z‖ ≤ B)
    (hz : z ∈ Metric.closedBall (0 : ℂ) R) :
    ‖BlaschkeB r R f z‖ ≤ B

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint "DiskBound"  (title := "DiskBound")  (statement := /--    Let $0 < r < R<1$. If $f:\mathbb{C}\to\mathbb{C}$ is a function analytic on    $\overline{\mathbb{D}_1}$ with $f(0)\neq0$ such that $|f(z)|\leq B$ for $|z|\leq R$,    then $|B_f(z)|\leq B$ for $|z|\leq R$ also.  -/)  (proof := /--    For $|z|=R$, we know that $z\not\in\mathcal{K}_f(r)$. Thus,    $$C_f(z)=\frac{f(z)}{\displaystyle\prod_{\rho\in\mathcal{K}_f(r)}(z-\rho)^{m_f(\rho)}}.$$    Thus, substituting this into Definition \ref{BlaschkeB},    $$|B_f(z)|=|f(z)|\prod_{\rho\in\mathcal{K}_f(r)}      \left|\frac{R-z\overline{\rho}/R}{z-\rho}\right|^{m_f(\rho)}.$$    But note that    $$\left|\frac{R-z\overline{\rho}/R}{z-\rho}\right|      =\frac{|R^2-z\overline{\rho}|/R}{|z-\rho|}      =\frac{|z|\cdot|\overline{z-\rho}|/R}{|z-\rho|}=1.$$    So we have that $|B_f(z)|=|f(z)|\leq B$ when $|z|=R$. Now by the maximum modulus    principle, we know that the maximum of $|B_f|$ must occur on the boundary where    $|z|=R$. Thus $|B_f(z)|\leq B$ for all $|z|\leq R$.  -/)  (latexEnv := "lemma")]lemma DiskBound {B r R : ℝ} {f : ℂ → ℂ} {z : ℂ}    (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) (fz_bound : ∀ (z : ℂ), ‖z‖ ≤ R → ‖f z‖ ≤ B)    (hz : z ∈ Metric.closedBall (0 : ℂ) R) :    ‖BlaschkeB r R f z‖ ≤ B := by  have r_lt_one : r < 1 := lt_trans r_lt_R R_lt_one  have R_pos : 0 < R := lt_trans r_pos r_lt_R  refine AnalyticOn.norm_le_of_norm_le_on_sphere (Std.IsPreorder.le_refl R) (AnalyticOnNhd.analyticOn (BlaschkeAnalytic r_pos r_lt_R R_lt_one finiteZeros hfAnalytic hf_neq_zero_at_zero)) ?_ hz  intro w hw  rw[mem_sphere_iff_norm, sub_zero] at hw  have hw_not_in : ¬(w ∈ SetOfZeros r f) := by    apply notMem_setOf_iff.mpr    intro le_r    linarith  have Bf_eq_f_at_w : ‖BlaschkeB r R f w‖ = ‖f w‖ := by    unfold BlaschkeB Cf    simp only [finiteSetOfZeros_mono r_lt_one finiteZeros, hw_not_in, ↓reduceDIte, Complex.norm_mul, Complex.norm_div, norm_prod, norm_pow]    rw[div_eq_mul_inv, mul_assoc, mul_right_eq_self₀]    by_cases fw_normZero : ‖f w‖ = 0    · exact Or.inr fw_normZero    · apply Or.inl      rw[← Finset.prod_inv_distrib, ← Finset.prod_mul_distrib]      apply Finset.prod_eq_one      intro w' hw'_in      have hfact : (R : ℂ) - w * starRingEnd ℂ w' / R = (conj w - conj w') * w / R := by        rw[sub_mul, ← Complex.normSq_eq_conj_mul_self, Complex.normSq_eq_norm_sq, hw, ofReal_pow]        field_simp      rw [hfact, norm_div, norm_mul, ← map_sub, norm_conj, Complex.norm_real, hw, Real.norm_of_nonneg (le_of_lt R_pos)]      field_simp      rw[← div_pow, div_self, one_pow]      rw[Set.Finite.mem_toFinset] at hw'_in      exact norm_ne_zero_iff.mpr (sub_ne_zero.mpr (fun h => hw_not_in (h ▸ hw'_in)))  rw[Bf_eq_f_at_w]  exact fz_bound w (le_of_eq hw)