BlaschkeNonzero

@[blueprint "BlaschkeNonZero"  (title := "BlaschkeNonZero")  (statement := /--    Let $0 < r < R<1$ and $f:\overline{\mathbb{D}_1}\to\mathbb{C}$ be analytic on    neighborhoods of points in $\overline{\mathbb{D}_1}$ with $f(0)\neq 0$. Then $B_f(z)\neq 0$    for all $z\in\overline{\mathbb{D}_r}$.  -/)  (proof := /--    Suppose that $z\in\mathcal{K}_f(r)$. Then we have that    $$C_f(z)=\frac{h_z(z)}{\displaystyle\prod_{\rho\in\mathcal{K}_f(r)\setminus\{z\}}      (z-\rho)^{m_f(\rho)}}.$$    where $h_z(z)\neq 0$ according to Lemma \ref{ZeroFactorization}. Thus, substituting    this into Definition \ref{BlaschkeB},    \begin{equation}\label{pickupPoint2}        |B_f(z)|=|h_z(z)|\cdot\left|R-\frac{|z|^2}{R}\right|^{m_f(z)}          \prod_{\rho\in\mathcal{K}_f(r)\setminus\{z\}}          \left|\frac{R-z\overline{\rho}/R}{z-\rho}\right|^{m_f(\rho)}.    \end{equation}    Trivially, $|h_z(z)|\neq 0$. Now note that    $$\left|R-\frac{|z|^2}{R}\right|=0\implies|z|=R.$$    However, this is a contradiction because $z\in\overline{\mathbb{D}_r}$ tells us that    $|z|\leq r < R$. Similarly, note that    $$\left|\frac{R-z\overline{\rho}/R}{z-\rho}\right|=0\implies|z|=\frac{R^2}{|\overline{\rho}|}.$$    However, this is also a contradiction because $\rho\in\mathcal{K}_f(r)$ tells us that    $R < R^2/|\overline{\rho}|=|z|$, but $z\in\overline{\mathbb{D}_r}$ tells us that    $|z|\leq r < R$. So, we know that    $$\left|R-\frac{|z|^2}{R}\right|\neq 0\qquad\text{and}\qquad      \left|\frac{R-z\overline{\rho}/R}{z-\rho}\right|\neq 0      \quad\text{for all}\quad\rho\in\mathcal{K}_f(r)\setminus\{z\}.$$    Applying this to Equation (\ref{pickupPoint2}) we have that $|B_f(z)|\neq 0$.    So, $B_f(z)\neq 0$.     Now suppose that $z\not\in\mathcal{K}_f(r)$. Then we have that    $$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},    \begin{equation}\label{pickupPoint3}        |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)}.    \end{equation}    We know that $|f(z)|\neq 0$ since $z\not\in\mathcal{K}_f(r)$. Now note that    $$\left|\frac{R-z\overline{\rho}/R}{z-\rho}\right|=0\implies|z|=\frac{R^2}{|\overline{\rho}|}.$$    However, this is a contradiction because $\rho\in\mathcal{K}_f(r)$ tells us that    $R < R^2/|\overline{\rho}|=|z|$, but $z\in\overline{\mathbb{D}_r}$ tells us that    $|z|\leq r < R$. So, we know that    $$\left|\frac{R-z\overline{\rho}/R}{z-\rho}\right|\neq 0      \quad\text{for all}\quad\rho\in\mathcal{K}_f(r).$$    Applying this to Equation (\ref{pickupPoint3}) we have that $|B_f(z)|\neq 0$.    So, $B_f(z)\neq 0$.     We have shown that $B_f(z)\neq 0$ for both $z\in\mathcal{K}_f(r)$ and    $z\not\in\mathcal{K}_f(r)$, so the result follows.  -/)  (latexEnv := "lemma")]lemma BlaschkeNonzero {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) :    ∀ z ∈ Metric.closedBall (0 : ℂ) r, BlaschkeB r R f z ≠ 0 := 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  intro z hz  have hz_norm_le_r : ‖z‖ ≤ r := by rwa [mem_closedBall_iff_norm, sub_zero] at hz  have hz_norm_lt_R : ‖z‖ < R := by linarith  let hFin := finiteSetOfZeros_mono r_lt_one finiteZeros  have hBProd : ∏ ρ ∈ hFin.toFinset,      (↑R - z * (starRingEnd ℂ) ρ / ↑R) ^ analyticOrderNatAt f ρ ≠ 0 := by    apply Finset.prod_ne_zero_iff.mpr    intro ρ hρ    apply pow_ne_zero    norm_num [ sub_eq_zero, Complex.ext_iff ];    simp only [SetOfZeros, Finite.mem_toFinset, mem_setOf_eq] at hρ    rw [ eq_div_iff ] <;> norm_num [ Complex.normSq, Complex.norm_def ] at *;    · rw [Real.sqrt_lt' (by linarith)] at hz_norm_lt_R      rw [ Real.sqrt_le_iff ] at hρ      exact fun h => absurd h ( by nlinarith [ sq_nonneg ( z.re - ρ.re ), sq_nonneg ( z.im - ρ.im ), mul_lt_mul_of_pos_left r_lt_R R_pos ] )    · linarith  unfold BlaschkeB Cf  by_cases z_in_zeros : z ∈ SetOfZeros r f  · simp only [hFin, z_in_zeros, ↓reduceDIte]    obtain ⟨_, _, hne, heq⟩ :=      ZeroFactorization (by linarith) (hfAnalytic.mono (Metric.closedBall_subset_closedBall (by linarith)))        hf_neq_zero_at_zero z_in_zeros    rw [heq.1]    refine mul_ne_zero (div_ne_zero hne (Finset.prod_ne_zero_iff.mpr fun ρ hρ =>      pow_ne_zero _ (sub_ne_zero.mpr fun h =>        (Finset.mem_sdiff.mp hρ).2 (Finset.mem_singleton.mpr h.symm)))) hBProd  · simp only [hFin, z_in_zeros, ↓reduceDIte]    refine mul_ne_zero (div_ne_zero (fun hfz => z_in_zeros ⟨hz_norm_le_r, hfz⟩)      (Finset.prod_ne_zero_iff.mpr fun ρ hρ =>        pow_ne_zero _ (sub_ne_zero.mpr fun h => z_in_zeros (h ▸ hFin.mem_toFinset.mp hρ)))) hBProd