AlexKontorovich/PrimeNumberTheoremAnd
Source indexedlemma · leanprover/lean4:v4.32.0
ZetaFixedLowerBound
PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:1121 to 1171
Mathematical statement
Exact Lean statement
@[blueprint "ZetaFixedLowerBound"
(title := "ZetaFixedLowerBound")
(statement := /--
For all $t\in\mathbb{R}$ one has
$$|\zeta(3/2+it)|\geq\frac{\zeta(3)}{\zeta(3/2)}.$$
-/)
(proof := /--
From the Euler product expansion of $\zeta$, we have that for $\Re s>1$
$$\zeta(s)=\prod_p\frac{1}{1-p^{-s}}.$$
Thus, we have that
$$\frac{\zeta(2s)}{\zeta(s)}=\prod_p\frac{1-p^{-s}}{1-p^{-2s}}=\prod_p\frac{1}{1+p^{-s}}.$$
Now note that $|1-p^{-(3/2+it)}|\leq 1+|p^{-(3/2+it)}|=1+p^{-3/2}$. Thus,
$$|\zeta(3/2+it)|=\prod_p\frac{1}{|1-p^{-(3/2+it)}|}
\geq\prod_p\frac{1}{1+p^{-3/2}}=\frac{\zeta(3)}{\zeta(3/2)}$$
for all $t\in\mathbb{R}$ as desired.
-/)
(latexEnv := "theorem")]
lemma ZetaFixedLowerBound (t : ℝ) :
‖ζ (3/2 + I * t)‖₊ ≥ ‖ζ 3 / ζ (3 / 2)‖₊Complete declaration
Lean source
Full Lean sourceLean 4
@[blueprint "ZetaFixedLowerBound" (title := "ZetaFixedLowerBound") (statement := /-- For all $t\in\mathbb{R}$ one has $$|\zeta(3/2+it)|\geq\frac{\zeta(3)}{\zeta(3/2)}.$$ -/) (proof := /-- From the Euler product expansion of $\zeta$, we have that for $\Re s>1$ $$\zeta(s)=\prod_p\frac{1}{1-p^{-s}}.$$ Thus, we have that $$\frac{\zeta(2s)}{\zeta(s)}=\prod_p\frac{1-p^{-s}}{1-p^{-2s}}=\prod_p\frac{1}{1+p^{-s}}.$$ Now note that $|1-p^{-(3/2+it)}|\leq 1+|p^{-(3/2+it)}|=1+p^{-3/2}$. Thus, $$|\zeta(3/2+it)|=\prod_p\frac{1}{|1-p^{-(3/2+it)}|} \geq\prod_p\frac{1}{1+p^{-3/2}}=\frac{\zeta(3)}{\zeta(3/2)}$$ for all $t\in\mathbb{R}$ as desired. -/) (latexEnv := "theorem")]lemma ZetaFixedLowerBound (t : ℝ) : ‖ζ (3/2 + I * t)‖₊ ≥ ‖ζ 3 / ζ (3 / 2)‖₊ := by have mp : ∀ {s : ℂ}, 1 < s.re → Multipliable fun p : Primes ↦ (1 - (p : ℂ) ^ (-s))⁻¹ := by intro s hs exact ⟨ζ s, riemannZeta_eulerProduct_hasProd hs⟩ have h₁ : 1 < ((3 : ℂ) / 2).re := by norm_num have h₂ : 1 < (3 : ℂ).re := by norm_num have h₃ : 1 < (3 / 2 + I * (t : ℂ)).re := by norm_num rw [nnnorm_div, ge_iff_le, div_le_iff₀ (nnnorm_pos.mpr (riemannZeta_ne_zero_of_one_le_re (by norm_num))), ← riemannZeta_eulerProduct_tprod h₁, ← riemannZeta_eulerProduct_tprod h₂, ← riemannZeta_eulerProduct_tprod h₃, (mp h₁).nnnorm_tprod, (mp h₂).nnnorm_tprod, (mp h₃).nnnorm_tprod, ← (mp h₃).nnnorm.tprod_mul (mp h₁).nnnorm] refine (mp h₂).nnnorm.tprod_le_tprod (fun p ↦ ?_) ((mp h₃).nnnorm.mul (mp h₁).nnnorm) simp only [nnnorm_inv, ← mul_inv] have hfact : ‖1 - (p : ℂ) ^ (-3 : ℂ)‖₊ = ‖1 + (p : ℂ) ^ ((-3 : ℂ) / 2)‖₊ * ‖1 - (p : ℂ) ^ (-((3 : ℂ) / 2))‖₊ := by rw [← nnnorm_mul]; congr 1; ring_nf; rw [← Complex.cpow_nat_mul]; ring_nf have hne : ∀ {s : ℂ}, 1 < s.re → (1 - (p : ℂ) ^ (-s)) ≠ 0 := fun hs ↦ Complex.one_sub_prime_cpow_ne_zero p.2 hs rw [inv_le_inv₀, hfact] · apply _root_.mul_le_mul_left rw [← norm_toNNReal, ← norm_toNNReal] apply Real.toNNReal_le_toNNReal calc ‖1 - (p : ℂ) ^ (-(3 / 2 + I * ↑t))‖ ≤ 1 + ‖(p : ℂ) ^ (-(3 / 2 + I * ↑t))‖ := by rw [← Complex.norm_of_nonneg zero_le_one]; exact norm_sub_le _ _ _ = ‖1 + (p : ℂ) ^ (-(3 : ℂ) / 2)‖ := by have : 0 ≤ 1 + (p : ℝ) ^ (-(3 : ℝ) / 2) := by linarith [Real.rpow_nonneg (cast_nonneg' ↑p) (-3 / 2)] simp only [Complex.norm_natCast_cpow_of_pos (Nat.Prime.pos p.2), add_re, neg_re, mul_re, I_re, ofReal_re, zero_mul, I_im, ofReal_im, mul_zero, sub_self, div_ofNat_re, re_ofNat, neg_div', add_zero] rw [← Real.norm_of_nonneg this, ← Complex.norm_real, Complex.ofReal_add, Complex.ofReal_cpow (cast_nonneg' ↑p)] push_cast; rfl · exact norm_pos_iff.mpr (hne h₂) · exact mul_pos (norm_pos_iff.mpr (hne h₃)) (norm_pos_iff.mpr (hne h₁))