BorelCaratheodoryDeriv

@[blueprint "BorelCaratheodoryDeriv"  (title := "BorelCaratheodoryDeriv")  (statement := /--    Let $R,\,M>0$. Let $f$ be analytic on $|z|\leq R$ such that $f(0)=0$ and suppose    $\Re f(z)\leq M$ for all $|z|\leq R$. Then for any $0 < r < R$,    $$|f'(z)|\leq\frac{16MR^2}{(R-r)^3}$$    for all $|z|\leq r$.  -/)  (proof := /--    Using Lemma \ref{DerivativeBound} with $r'=(R+r)/2$, and noting that $r < R$,    we have that    $$|f'(z)|\leq\frac{4M(R+r)^2}{(R-r)^3}\leq\frac{16MR^2}{(R-r)^3}.$$  -/)  (latexEnv := "theorem")]theorem BorelCaratheodoryDeriv {M r R : ℝ} {f : ℂ → ℂ} {z : ℂ}    (Mpos : 0 < M) (rpos : 0 < r) (hyp_r : r < R)    (analytic_f : AnalyticOn ℂ f (Metric.ball 0 R))    (zeroAtZero : f 0 = 0)    (realPartBounded : ∀ z ∈ Metric.ball 0 R, (f z).re ≤ M)    (hyp_z : z ∈ Metric.closedBall 0 r) :    ‖deriv f z‖ ≤ 16 * M * R ^ 2 / (R - r) ^ 3 := by  have hr' : 2 * M * ((R + r) / 2) ^ 2 / ((R - (R + r) / 2) * ((R + r) / 2 - r) ^ 2) =      4 * M * (R + r) ^ 2 / (R - r) ^ 3 := by field_simp; ring  calc ‖deriv f z‖      _ ≤ 4 * M * (R + r) ^ 2 / (R - r) ^ 3 := hr' ▸          DerivativeBound Mpos rpos (by linarith) (by linarith) analytic_f zeroAtZero realPartBounded hyp_z      _ ≤ 16 * M * R ^ 2 / (R - r) ^ 3 := by          have : 16 * M * R ^ 2 = 4 * M * (2 * R) ^ 2 := by ring_nf          rw [this]; bound