AlexKontorovich/PrimeNumberTheoremAnd
Source indexedlemma · leanprover/lean4:v4.32.0
DerivativeBound
PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:124 to 175
Mathematical statement
Exact Lean statement
@[blueprint "DerivativeBound"
(title := "DerivativeBound")
(statement := /--
Let $R,\,M>0$ and $0 < r < r' < R$. 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 we have that
$$|f'(z)|\leq\frac{2M(r')^2}{(R-r')(r'-r)^2}$$
for all $|z|\leq r$.
-/)
(proof := /--
By Lemma \ref{cauchy_formula_deriv} we know that
$$f'(z)=\frac{1}{2\pi i}\oint_{|w|=r'}\frac{f(w)}{(w-z)^2}\,dw
=\frac{1}{2\pi }\int_0^{2\pi}\frac{r'e^{it}\,f(r'e^{it})}{(r'e^{it}-z)^2}\,dt.$$
Thus,
\begin{equation}\label{pickupPoint1}
|f'(z)|=\left|\frac{1}{2\pi}\int_0^{2\pi}
\frac{r'e^{it}\,f(r'e^{it})}{(r'e^{it}-z)^2}\,dt\right|
\leq\frac{1}{2\pi}\int_0^{2\pi}
\left|\frac{r'e^{it}\,f(r'e^{it})}{(r'e^{it}-z)^2}\right|\,dt.
\end{equation}
Now applying Theorem \ref{borelCaratheodory'}, and noting that
$r'-r\leq|r'e^{it}-z|$, we have that
$$\left|\frac{r'e^{it}\,f(r'e^{it})}{(r'e^{it}-z)^2}\right|
\leq\frac{2M(r')^2}{(R-r')(r'-r)^2}.$$
Substituting this into Equation (\ref{pickupPoint1}) and evaluating the integral
completes the proof.
-/)
(latexEnv := "lemma")]
lemma DerivativeBound {M r r' R : ℝ} {f : ℂ → ℂ} {z : ℂ}
(Mpos : 0 < M) (pos_r : 0 < r) (r_lt_r' : r < r') (r'_lt_R : r' < R)
(analytic_f : AnalyticOn ℂ f (Metric.ball 0 R))
(f_zero_at_zero : f 0 = 0)
(re_f_le_M : ∀ z ∈ Metric.ball 0 R, (f z).re ≤ M)
(z_in_r : z ∈ Metric.closedBall 0 r) :
‖(deriv f) z‖ ≤ 2 * M * (r') ^ 2 / ((R - r') * (r' - r) ^ 2)Complete declaration
Lean source
Full Lean sourceLean 4
@[blueprint "DerivativeBound" (title := "DerivativeBound") (statement := /-- Let $R,\,M>0$ and $0 < r < r' < R$. 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 we have that $$|f'(z)|\leq\frac{2M(r')^2}{(R-r')(r'-r)^2}$$ for all $|z|\leq r$. -/) (proof := /-- By Lemma \ref{cauchy_formula_deriv} we know that $$f'(z)=\frac{1}{2\pi i}\oint_{|w|=r'}\frac{f(w)}{(w-z)^2}\,dw =\frac{1}{2\pi }\int_0^{2\pi}\frac{r'e^{it}\,f(r'e^{it})}{(r'e^{it}-z)^2}\,dt.$$ Thus, \begin{equation}\label{pickupPoint1} |f'(z)|=\left|\frac{1}{2\pi}\int_0^{2\pi} \frac{r'e^{it}\,f(r'e^{it})}{(r'e^{it}-z)^2}\,dt\right| \leq\frac{1}{2\pi}\int_0^{2\pi} \left|\frac{r'e^{it}\,f(r'e^{it})}{(r'e^{it}-z)^2}\right|\,dt. \end{equation} Now applying Theorem \ref{borelCaratheodory'}, and noting that $r'-r\leq|r'e^{it}-z|$, we have that $$\left|\frac{r'e^{it}\,f(r'e^{it})}{(r'e^{it}-z)^2}\right| \leq\frac{2M(r')^2}{(R-r')(r'-r)^2}.$$ Substituting this into Equation (\ref{pickupPoint1}) and evaluating the integral completes the proof. -/) (latexEnv := "lemma")]lemma DerivativeBound {M r r' R : ℝ} {f : ℂ → ℂ} {z : ℂ} (Mpos : 0 < M) (pos_r : 0 < r) (r_lt_r' : r < r') (r'_lt_R : r' < R) (analytic_f : AnalyticOn ℂ f (Metric.ball 0 R)) (f_zero_at_zero : f 0 = 0) (re_f_le_M : ∀ z ∈ Metric.ball 0 R, (f z).re ≤ M) (z_in_r : z ∈ Metric.closedBall 0 r) : ‖(deriv f) z‖ ≤ 2 * M * (r') ^ 2 / ((R - r') * (r' - r) ^ 2) := by rw [cauchy_formula_deriv r_lt_r' r'_lt_R analytic_f.differentiableOn z_in_r, one_div] grw [circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const (by linarith) (C := 2 * M * r' / ((R - r') * (r' - r) ^ 2))] · exact le_of_eq (by ring) · intro z' hz' rw [smul_eq_mul, norm_mul] grw[borelCaratheodory' Mpos (by grind) r'_lt_R analytic_f f_zero_at_zero re_f_le_M (Metric.sphere_subset_closedBall hz')] suffices ‖(z' - z)⁻¹ ^ 2‖ ≤ 1 / (r' - r) ^ 2 by grw [this] · exact le_of_eq (by field) · refine mul_nonneg (mul_nonneg ?_ ?_) (inv_nonneg.mpr ?_) <;> linarith have hdist : r' - r ≤ ‖z' - z‖ := by simp only [mem_sphere_iff_norm, sub_zero, Metric.mem_closedBall, dist_zero_right] at hz' z_in_r rw [← hz'] exact le_trans (by linarith) (norm_sub_norm_le z' z) rw [norm_pow, norm_inv, one_div, inv_pow] gcongr