Log Of Analytic Function

@[blueprint "LogOfAnalyticFunction"  (title := "LogOfAnalyticFunction")  (statement := /--    Let $0<r<R$. Let $B:\overline{\mathbb{D}_{R}}\to\mathbb{C}$ be analytic on neighborhoods of    points in $\overline{\mathbb{D}_{R}}$ with $B(z)\neq 0$ for all    $z\in\overline{\mathbb{D}_{R}}$.Then there exists $J_B:\mathbb{D}_R\to\mathbb{C}$ that is    analytic on neighborhoods of points in $\mathbb{D}_R$ such that    \begin{itemize}        \item $J_B(0)=0$        \item $J_B'(z)=B'(z)/B(z)$ for all $z\in\overline{\mathbb{D}_r}$        \item $\log|B(z)|-\log|B(0)|=\mathfrak{R}J_B(z)$ for all $z\in\mathbb{D}_R$.    \end{itemize}  -/)  (proof := /--    We let $J_B(z)=I_{B'/B}(z)$. Then clearly, $J_B(0)=0$. Now note that    \begin{align*}        I_{B'/B}(z)=z\int_0^1(B'/B)(tz)\,dt=\int_0^z(B'/B)(u)\,du.    \end{align*}    Thus by the fundamental theorem of calculus we have that $J_B'(z)=B'(z)/B(z)$. Now let    $H(z)=\exp(J_B(z))/B(z)$ and note that    $$H'(z)=(B(z)\,J_B'(z)-B'(z))\left(\frac{\exp(J_B(z))}{(B(z))^2}\right).$$    Thus, $H$ is constant since we know that $B(z)\,J_B'(z)-B(z)=0$ from $J_B'(z)=B'(z)/B(z)$. So    since $H(0)=\exp(J_B(0))/B(0)=1/B(0)$ we know $H(z)=1/B(0)$ for all $z$. So we have,    $$\frac{1}{B(0)}=\frac{\exp(J_B(z))}{B(z)}\implies\left|\frac{B(z)}{B(0)}\right|      =\exp(\mathfrak{R}J_B(z)).$$    Taking the logarithm of both sides completes the proof.  -/)  (latexEnv := "theorem")]theorem LogOfAnalyticFunction {r R : ℝ} {B : ℂ → ℂ}    (zero_lt_r : 0 < r) (r_lt_R : r < R)    (BanalyticOnNhdOfDR : AnalyticOnNhd ℂ B (Metric.closedBall (0 : ℂ) R))    (Bnonzero : ∀ z ∈ Metric.closedBall (0 : ℂ) R, B z ≠ 0) :    ∃ (J_B : ℂ → ℂ), (AnalyticOnNhd ℂ J_B (Metric.ball 0 R)) ∧      (J_B 0 = 0) ∧      (∀ z ∈ Metric.closedBall 0 r, (deriv J_B) z = (deriv B) z / (B z)) ∧      (∀ z ∈ Metric.ball 0 R, Real.log ‖B z‖ - Real.log ‖B 0‖ = (J_B z).re) := by  obtain ⟨J_B, hJB⟩ : ∃ J_B : ℂ → ℂ, (∀ z ∈ Metric.ball 0 R, (HasDerivAt J_B (deriv B z / B z) z)) ∧ J_B 0 = 0 ∧ (∀ z ∈ Metric.ball 0 R, Real.log ‖B z‖ - Real.log ‖B 0‖ = (J_B z).re) := by    set f : ℂ → ℂ := fun z => deriv B z / B z;    have hf : AnalyticOnNhd ℂ f (Metric.ball 0 R) :=      (BanalyticOnNhdOfDR.deriv.mono Metric.ball_subset_closedBall).div        (BanalyticOnNhdOfDR.mono Metric.ball_subset_closedBall)        (fun z hz => Bnonzero z <| Metric.ball_subset_closedBall hz)    obtain ⟨J, hJ⟩ := DifferentiableOn.isExactOn_ball hf.differentiableOn    refine ⟨fun z ↦ J z - J 0, fun z hz ↦ (hJ z hz).sub_const _, by simp, ?_⟩    set H : ℂ → ℂ := fun z => Complex.exp (J z - J 0) / B z    have hJB_deriv : ∀ z ∈ Metric.ball 0 R, HasDerivAt (fun z ↦ J z - J 0) (f z) z :=      fun z hz ↦ (hJ z hz).sub_const _    have hH_deriv : ∀ z ∈ Metric.ball 0 R, HasDerivAt H 0 z := by      intro z hz      have := (Complex.hasDerivAt_exp _).comp z (hJB_deriv z hz)      convert! this.div (BanalyticOnNhdOfDR.differentiableOn.differentiableAt        (Metric.closedBall_mem_nhds_of_mem hz) |>.hasDerivAt)        (Bnonzero z <| Metric.ball_subset_closedBall hz) using 1      ring_nf!; grind    have hH_const : ∀ z ∈ Metric.ball 0 R, H z = H 0 := by      intro z hz      have h_diffOn : DifferentiableOn ℂ H (Metric.ball 0 R) :=        fun z hz ↦ (hH_deriv z hz).differentiableAt.differentiableWithinAt      refine Convex.is_const_of_fderivWithin_eq_zero (convex_ball 0 R) h_diffOn ?_ hz        (Metric.mem_ball_self (Metric.pos_of_mem_ball hz))      intro x hx      rw [fderivWithin_of_isOpen Metric.isOpen_ball hx,        ← ContinuousLinearMap.toSpanSingleton_zero]      exact (hH_deriv x hx).hasFDerivAt.fderiv    have h_exp_re : ∀ z ∈ Metric.ball 0 R, Real.exp (J z - J 0).re = ‖B z‖ / ‖B 0‖ := by      intro z hz      have hc := hH_const z hz      simp only [H, sub_self, Complex.exp_zero, one_div] at hc      rw [div_eq_iff (Bnonzero z (Metric.ball_subset_closedBall hz)), mul_comm] at hc      rw [← Complex.norm_exp, ← norm_div, div_eq_mul_inv]      exact enorm_eq_iff_norm_eq.mp (congrArg enorm hc)    intro z hz    have hBz := Bnonzero z (Metric.ball_subset_closedBall hz)    have hB0 := Bnonzero 0 (by norm_num; linarith)    rw [← Real.log_div (norm_ne_zero_iff.mpr hBz) (norm_ne_zero_iff.mpr hB0),      ← h_exp_re z hz, Real.log_exp]  have hmem : ∀ z, z ∈ Metric.ball (0 : ℂ) r → z ∈ Metric.closedBall (0 : ℂ) R := by    intro z hz    apply Metric.mem_closedBall.mpr    rw [Metric.mem_ball] at hz    linarith  refine ⟨J_B, ?_, hJB.2.1, ?_, hJB.2.2⟩  · intro z hz    exact DifferentiableOn.analyticAt (fun w hw ↦ (hJB.1 w hw).differentiableAt.differentiableWithinAt) (IsOpen.mem_nhds Metric.isOpen_ball hz)  · intro z hz    exact (hJB.1 z (Metric.closedBall_subset_ball r_lt_R hz)).deriv