AlexKontorovich/PrimeNumberTheoremAnd
Source indexedtheorem · leanprover/lean4:v4.32.0
LogOfAnalyticFunction
PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:221 to 306
Source documentation
\begin{definition}[TaxicabIntegral]\label{TaxicabIntegral} Let . Let be analytic on neighborhoods of points in . Define the functon by \end{definition}
Exact Lean statement
@[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)Complete declaration
Lean source
Full Lean sourceLean 4
@[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