JBlaschkeDerivBound

@[blueprint "JBlaschkeDerivBound"  (title := "JBlaschkeDerivBound")  (statement := /--    Let $B>1$ and $0 < r' < 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 all $|z|\leq R$, then for all $|z|\leq r'$    $$|L_f'(z)|\leq\frac{16\log(B)\,r^2}{(r-r')^3}.$$  -/)  (proof := /--    By Lemma \ref{DiskBound} we immediately know that $|B_f(z)|\leq B$ for all $|z|\leq R$.    Now since $L_f=J_{B_f}$ by Definition \ref{JBlaschke}, by Theorem    \ref{LogOfAnalyticFunction} we know that    $$L_f(0)=0\qquad\text{and}\qquad      \Re L_f(z)=\log|B_f(z)|-\log|B_f(0)|\leq\log|B_f(z)|\leq\log B$$    for all $|z|\leq r$. Note that in the above    $$0=\log|f(0)|\leq\log|B_f(0)|$$    because of Lemma \ref{norm_fOfZero_le_norm_BlaschkeOfZero}. So by Theorem \ref{BorelCaratheodoryDeriv}, it follows that    $$|L_f'(z)|\leq\frac{16\log(B)\,r^2}{(r-r')^3}$$    for all $|z|\leq r'$.  -/)  (latexEnv := "theorem")]theorem JBlaschkeDerivBound {B r' r R : ℝ} {f : ℂ → ℂ} {z : ℂ}    (one_lt_B : 1 < B) (r'_pos : 0 < r') (r'_lt_r : r' < r) (r_pos : 0 < r) (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)    (hz : z ∈ Metric.closedBall (0 : ℂ) r') :    ‖deriv (JBlaschke r'_pos r'_lt_r r_pos r_lt_R R_lt_one hfAnalytic hf0_eq_one finiteZeros) z‖      ≤ 16 * Real.log (B) * r ^ 2 / (r - r') ^ 3 := by  have r_pos : 0 < r := lt_trans r'_pos r'_lt_r  let blaschkeAnalytic := BlaschkeAnalytic r_pos r_lt_R R_lt_one finiteZeros hfAnalytic (hf0_eq_one ▸ one_ne_zero)  let blaschkeNonzero := BlaschkeNonzero r_pos r_lt_R R_lt_one finiteZeros hfAnalytic (hf0_eq_one ▸ one_ne_zero)  let logOfAnalytic := LogOfAnalyticFunction' r'_pos r'_lt_r r_lt_R blaschkeAnalytic blaschkeNonzero  set JB := logOfAnalytic.choose with JB_def  obtain ⟨JB_Analytic, JB_0_eq_0, deriv_JB_eq, JB_re⟩ := logOfAnalytic.choose_spec  rw [← JB_def] at JB_Analytic JB_0_eq_0 deriv_JB_eq JB_re  have JB_def' : JB = (JBlaschke r'_pos r'_lt_r r_pos r_lt_R R_lt_one hfAnalytic hf0_eq_one finiteZeros) := by    unfold JBlaschke    rw [← JB_def]  rw[← JB_def']  refine BorelCaratheodoryDeriv (Real.log_pos one_lt_B) r'_pos r'_lt_r (JB_Analytic.analyticOn) JB_0_eq_0 ?_ hz  intro w hw  rw[← JB_re w hw]  have hwr : w ∈ Metric.closedBall (0 : ℂ) r := by exact Metric.ball_subset_closedBall hw  have hlog : 0 ≤ Real.log ‖BlaschkeB r R f 0‖ := by    rw [← Real.log_one]    apply Real.log_le_log zero_lt_one    rw [← norm_one (α := ℂ), ← hf0_eq_one]    exact norm_fOfZero_le_norm_BlaschkeOfZero r_pos r_lt_R R_lt_one finiteZeros (hf0_eq_one ▸ one_ne_zero)  suffices h : Real.log ‖BlaschkeB r R f w‖ ≤ Real.log B by linarith  exact Real.log_le_log (norm_pos_iff.mpr (blaschkeNonzero w hwr))    (DiskBound r_pos r_lt_R R_lt_one finiteZeros hfAnalytic (hf0_eq_one ▸ one_ne_zero) fz_bound (Metric.closedBall_subset_closedBall r_lt_R.le hwr))