Source indexedlemma · leanprover/lean4:v4.32.0

Backlund.zetaSurrogate_log_growth

PrimeNumberTheoremAnd.Backlund.ZeroCountCrude · PrimeNumberTheoremAnd/Backlund/ZeroCountCrude.lean:819 to 847

Source documentation

The exponent-3/2 log-growth majorant for the surrogate. The exponent-1 form is FALSE on the left half-plane (|ζ(-2k-1)| ~ 2(2k+1)!/(2π)^{2k+2} via Bernoulli numbers: order 1 but maximal type), and x log x ≤ 2 x^(3/2) restores a true bound. Assembled from the three region lemmas above.

Exact Lean statement

lemma zetaSurrogate_log_growth :
    ∃ C : ℝ, 0 < C ∧
      ∀ z : ℂ, Real.log (1 + ‖zetaSurrogate z‖) ≤ C * (1 + ‖z‖) ^ (3/2 : ℝ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma zetaSurrogate_log_growth :    ∃ C : ℝ, 0 < C ∧      ∀ z : ℂ, Real.log (1 + ‖zetaSurrogate z‖) ≤ C * (1 + ‖z‖) ^ (3/2 : ℝ) := by  obtain ⟨B₁, hB₁0, hB₁⟩ := surrogate_growth_right  obtain ⟨B₂, hB₂0, hB₂⟩ := surrogate_growth_band  obtain ⟨B₃, hB₃0, hB₃⟩ := surrogate_growth_left  refine ⟨B₁ + B₂ + B₃, by linarith, fun z ↦ ?_⟩  have hz1 : (1 : ℝ) ≤ 1 + ‖z‖ := by linarith [norm_nonneg z]  have hpos : (0 : ℝ) < (1 + ‖z‖) ^ (3/2 : ℝ) :=    Real.rpow_pos_of_pos (by linarith [norm_nonneg z]) _  have hpow : (1 + ‖z‖) ≤ (1 + ‖z‖) ^ (3/2 : ℝ) := by    calc (1 + ‖z‖) = (1 + ‖z‖) ^ (1 : ℝ) := (Real.rpow_one _).symm      _ ≤ (1 + ‖z‖) ^ (3/2 : ℝ) :=        Real.rpow_le_rpow_of_exponent_le hz1 (by norm_num)  rcases le_total z.re (-1) with h | h  · refine (hB₃ z h).trans ?_    refine mul_le_mul_of_nonneg_right ?_ hpos.le    linarith  · rcases le_total z.re 2 with h2 | h2    · refine (hB₂ z h h2).trans ?_      calc B₂ * (1 + ‖z‖)          ≤ B₂ * (1 + ‖z‖) ^ (3/2 : ℝ) := mul_le_mul_of_nonneg_left hpow hB₂0.le        _ ≤ (B₁ + B₂ + B₃) * (1 + ‖z‖) ^ (3/2 : ℝ) :=            mul_le_mul_of_nonneg_right (by linarith) hpos.le    · refine (hB₁ z h2).trans ?_      calc B₁ * (1 + ‖z‖)          ≤ B₁ * (1 + ‖z‖) ^ (3/2 : ℝ) := mul_le_mul_of_nonneg_left hpow hB₁0.le        _ ≤ (B₁ + B₂ + B₃) * (1 + ‖z‖) ^ (3/2 : ℝ) :=            mul_le_mul_of_nonneg_right (by linarith) hpos.le