ZerosBound

@[blueprint "ZerosBound"  (title := "ZerosBound")  (statement := /--    Let $0< r < R<1$. If $f:\mathbb{C}\to\mathbb{C}$ is a function analytic on    neighborhoods of points in $\overline{\mathbb{D}_1}$ with $f(0)=1$ and $|f(z)|\leq B$    for $|z|\leq R$, then    $$\sum_{\rho\in\mathcal{K}_f(r)}m_f(\rho)\leq\frac{\log B}{\log(R/r)}.$$  -/)   (proof := /--    Since $f(0)=1$, by Lemma \ref{BlaschkeOfZero} we know that    $$|B_f(0)|      =|f(0)|\prod_{\rho\in\mathcal{K}_f(r)}\left(\frac{R}{|\rho|}\right)^{m_f(\rho)}      =\prod_{\rho\in\mathcal{K}_f(r)}\left(\frac{R}{|\rho|}\right)^{m_f(\rho)}.$$    Thus, substituting this into Definition \ref{BlaschkeB},    $$(R/r)^{\sum_{\rho\in\mathcal{K}_f(r)}m_f(\rho)}      =\prod_{\rho\in\mathcal{K}_f(r)}\left(\frac{R}{r}\right)^{m_f(\rho)}      \leq\prod_{\rho\in\mathcal{K}_f(r)}\left(\frac{R}{|\rho|}\right)^{m_f(\rho)}      =|B_f(0)|\leq B$$    whereby Lemma \ref{DiskBound} we know that $|B_f(z)|\leq B$ for all $|z|\leq R$.    Taking the logarithm of both sides and rearranging gives the desired result.  -/)  (latexEnv := "theorem")]theorem ZerosBound {B r R : ℝ} {f : ℂ → ℂ}    (r_pos : 0 < r) (r_lt_one : r < 1) (r_lt_R : r < R) (R_lt_one : R < 1)    (hfAnalytic : AnalyticOnNhd ℂ f (Metric.closedBall (0 : ℂ) 1)) (hf0_eq_one : f 0 = 1)    (finiteZeros : (SetOfZeros 1 f).Finite) (fz_bound : ∀ z : ℂ, ‖z‖ ≤ R → ‖f z‖ ≤ B) :    ∑ ρ ∈ (finiteSetOfZeros_mono r_lt_one finiteZeros).toFinset, analyticOrderNatAt f ρ ≤      1 / Real.log (R / r) * Real.log B := by  have R_pos : 0 < R := lt_trans r_pos r_lt_R  have hf0_ne_zero : f 0 ≠ 0 := by rw [hf0_eq_one]; exact one_ne_zero  have blaschke_eq := BlaschkeOfZero r_pos r_lt_one r_lt_R finiteZeros hf0_ne_zero  rw[hf0_eq_one, norm_one, one_mul] at blaschke_eq  rw [one_div, inv_mul_eq_div, le_div_iff₀ (Real.log_pos (by simp only [lt_div_iff₀ r_pos, one_mul, r_lt_R])), ← Real.log_pow]  refine Real.log_le_log (pow_pos (div_pos R_pos r_pos) _) ?_  calc (R / r) ^ ∑ ρ ∈ (finiteSetOfZeros_mono r_lt_one finiteZeros).toFinset, analyticOrderNatAt f ρ      = ∏ ρ ∈ (finiteSetOfZeros_mono r_lt_one finiteZeros).toFinset, (R / r) ^ analyticOrderNatAt f ρ := by        rw [Finset.prod_pow_eq_pow_sum]    _ ≤ ∏ ρ ∈ (finiteSetOfZeros_mono r_lt_one finiteZeros).toFinset, (R / ‖ρ‖) ^ analyticOrderNatAt f ρ := by      apply Finset.prod_le_prod      · intro ρ _        exact pow_nonneg (div_nonneg (le_of_lt R_pos) (le_of_lt r_pos)) _      · intro ρ hρ        have hρ_mem := (finiteSetOfZeros_mono r_lt_one finiteZeros).mem_toFinset.mp hρ        refine pow_le_pow_left₀ (div_nonneg (le_of_lt R_pos) (le_of_lt r_pos)) ?_ _        refine div_le_div_of_nonneg_left (le_of_lt R_pos) (norm_pos_iff.mpr ?_) (hρ_mem.1)        rintro rfl        exact hf0_ne_zero hρ_mem.2    _ ≤ B := by      rw[← blaschke_eq]      exact DiskBound r_pos r_lt_R R_lt_one finiteZeros hfAnalytic        hf0_ne_zero fz_bound (Metric.mem_closedBall_self (le_of_lt R_pos))