borelCaratheodory_closedBall

@[blueprint "borelCaratheodory_closedBall"  (title := "borelCaratheodory-closedBall")  (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$,    $$\sup_{|z|\leq r}|f(z)|\leq\frac{2Mr}{R-r}.$$  -/)  (proof := /--    Let    $$f_M(z)=\frac{f(z)/z}{2M-f(z)}.$$    Note that $2M-f(z)\neq 0$ because    $\Re (2M-f(z))=2M-\Re f(z)\geq M>0$. Additionally, since    $f(z)$ has a zero at $0$, we know that $f(z)/z$ is analytic    on $|z|\leq R$. Likewise, $f_M(z)$ is analytic on    $|z|\leq R$.    Now note that $|f(z)|\leq|2M-f(z)|$ since $\Re f(z)\leq M$.    Thus we have that    $$|f_M(z)|=\frac{|f(z)|/|z|}{|2M-f(z)|}      \leq\frac{1}{|z|}.$$    Now by the maximum modulus principle, we know the maximum of    $|f_M|$ must occur on the boundary where $|z|=R$. Thus,    $|f_M(z)|\leq 1/R$ for all $|z|\leq R$. So for $|z|=r$ we    have    $$|f_M(z)|=\frac{|f(z)|/r}{|2M-f(z)|}\leq\frac{1}{R}    \implies R\,|f(z)|\leq r\,|2M-f(z)|\leq 2Mr+r\,|f(z)|.$$    Which by algebraic manipulation gives    $$|f(z)|\leq\frac{2Mr}{R-r}.$$    Once more, by the maximum modulus principle, we know the    maximum of $|f|$ must occur on the boundary where $|z|=r$.    Thus, the desired result immediately follows  -/)]theorem borelCaratheodory_closedBall {M R r : ℝ} {z : ℂ}    {f : ℂ → ℂ} (Rpos : 0 < R)    (analytic : AnalyticOn ℂ f (Metric.closedBall 0 R))    (zeroAtZero : f 0 = 0) (Mpos : 0 < M)    (realPartBounded : ∀ z ∈ Metric.closedBall 0 R, (f z).re ≤ M)    (hyp_r : r < R)    (hyp_z : z ∈ Metric.closedBall 0 r) :    ‖f z‖ ≤ (2 * M * r) / (R - r) := by  have zInSFunc :      ∀ r ≤ R, ∀ z ∈ Metric.sphere (0 : ℂ) r,      z ∈ Metric.closedBall (0 : ℂ) R := by    intro r hyp_r z hyp_z    exact Set.mem_of_mem_of_subset hyp_z <|      (Metric.sphere_subset_closedBall).trans        (Metric.closedBall_subset_closedBall hyp_r)  have fPosAll :      ∀ z ∈ Metric.closedBall 0 R, 2 * M - f z ≠ 0 := by    intro z zInS    exact Complex.ne_zero_of_re_pos (by      rw [Complex.sub_re, Complex.mul_re, Complex.re_ofNat, Complex.ofReal_re,        Complex.im_ofNat, Complex.ofReal_im, mul_zero, sub_zero, sub_pos]      linarith [realPartBounded z zInS])  have schwartzQuotientBounded :      ∀ z ∈ Metric.sphere 0 R,      ‖schwartzQuotient f M z‖ ≤ 1 / R := by    intro z hyp_z    have zNe0 : z ≠ 0 := by      rw [mem_sphere_zero_iff_norm] at hyp_z      exact ne_zero_of_norm_ne_zero (by linarith)    have zInS : z ∈ Metric.closedBall 0 R :=      zInSFunc R le_rfl z hyp_z    rw [mem_sphere_iff_norm, sub_zero] at hyp_z    calc ‖schwartzQuotient f M z‖      _ = (‖f z‖ / ‖z‖) / ‖2 * M - f z‖ := by        simp only [Complex.norm_div, divRemovable_zero_of_ne_zero f zNe0]      _ ≤ (‖f z‖ / ‖z‖) / ‖f z‖ := by        by_cases h : ‖f z‖ = 0        · simp only [h, zero_div, div_zero, le_refl]        · exact div_le_div_of_nonneg_left            (by positivity) (by positivity)            (Complex.norm_le_norm_two_mul_sub_of_re_le              Mpos (realPartBounded z zInS))      _ ≤ 1 / ‖z‖ := by        rw [div_right_comm]        exact div_le_div_of_nonneg_right (div_self_le_one _) (norm_nonneg _)      _ = 1 / R := by rw [hyp_z]  have maxMod (z) (hz : z ∈ Metric.closedBall 0 R) : ‖schwartzQuotient f M z‖ ≤ 1 / R :=    AnalyticOn.norm_le_of_norm_le_on_sphere le_rfl      (AnalyticOn.schwartzQuotient M Rpos analytic fPosAll zeroAtZero)      schwartzQuotientBounded hz  have boundForF :      ∀ r < R, 0 < r →      ∀ z ∈ Metric.sphere 0 r,      ‖f z‖ ≤ 2 * M * r / (R - r) := by    intro r hyp_r r_pos z zOnR    have zInS : z ∈ Metric.closedBall 0 R :=      zInSFunc r hyp_r.le z zOnR    rw [mem_sphere_zero_iff_norm] at zOnR    have := maxMod z zInS    unfold schwartzQuotient at this    have U : z ≠ 0 := by      rwa [← norm_pos_iff, zOnR]    simp only [divRemovable_zero_of_ne_zero f U, Complex.norm_div, one_div] at this    have U : 0 < r * ‖2 * M - f z‖ := by      simp only [r_pos, mul_pos_iff_of_pos_left, norm_pos_iff, ne_eq, fPosAll z zInS,        not_false_eq_true]    rw [zOnR, div_div, div_le_iff₀' U] at this    have U0 :        ‖f z‖ ≤ 2 * M * r / R + (r / R) * ‖f z‖ := by      calc ‖f z‖        _ ≤ r * ‖2 * M - f z‖ * R⁻¹ := this        _ ≤ r * (‖(2 : ℂ) * M‖ + ‖f z‖) * R⁻¹ := by          grw [norm_sub_le]        _ = r * (2 * M + ‖f z‖) * R⁻¹ := by          simp [Mpos.le]        _ = 2 * M * r / R + (r / R) * ‖f z‖ := by          ring_nf    rw [← tsub_le_iff_right, ← one_sub_mul, ← le_div_iff₀'] at U0    · have hR : (R : ℝ) ≠ 0 := Rpos.ne'      have hRr : R - r ≠ 0 := sub_ne_zero.mpr (ne_of_lt hyp_r).symm      have heq : 2 * M * r / (R - r) = 2 * M * r / R / (1 - r / R) := by        rw [one_sub_div hR]; field_simp      rw [heq]      exact U0    · rwa [sub_pos, div_lt_one₀ Rpos]  have maxBoundForF      (r) (hyp_r : r < R) (pos_r : 0 < r)      (z) (hz : z ∈ Metric.closedBall 0 r) :      ‖f z‖ ≤ 2 * M * r / (R - r) :=    AnalyticOn.norm_le_of_norm_le_on_sphere hyp_r.le analytic (boundForF r hyp_r pos_r) hz  have U : 0 ≤ r := by    rw [mem_closedBall_iff_norm, sub_zero] at hyp_z    exact (norm_nonneg z).trans hyp_z  cases U.eq_or_lt' with  | inl pos_r =>    obtain rfl : z = 0 := by      rwa [pos_r, Metric.closedBall_zero, Set.mem_singleton_iff] at hyp_z    rwa [pos_r, mul_zero, sub_zero, zero_div, norm_le_zero_iff]  | inr pos_r =>    exact maxBoundForF r hyp_r pos_r z hyp_z