Source indexedtheorem · leanprover/lean4:v4.32.0

ZetaBoxEval

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:1569 to 1599

Source documentation

We insert this information in $\psi_{\epsilon}$ . We add and subtract the integral over the box $[1-\delta,2] \times_{ℂ} [-T,T]$ , which we evaluate as follows

Exact Lean statement

@[blueprint
  (title := "ZetaBoxEval")
  (statement := /--
  For all $\epsilon > 0$ sufficiently close to $0$, the rectangle integral over $[1-\delta,2] \times_{ℂ} [-T,T]$ of the integrand in
  $\psi_{\epsilon}$ is
  $$
  \frac{X^{1}}{1}\mathcal{M}(\widetilde{1_{\epsilon}})(1)
  = X(1+O(\epsilon))
  ,$$
  where the implicit constant is independent of $X$.
  -/)
  (proof := /-- Unfold the definitions and apply Lemma \ref{MellinOfSmooth1c}. -/)]
theorem ZetaBoxEval {SmoothingF : ℝ → ℝ}
    (suppSmoothingF : Function.support SmoothingF ⊆ Icc (1 / 2) 2)
    (mass_one : ∫ x in Ioi 0, SmoothingF x / x = 1)
    (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) :
    ∃ C, ∀ᶠ ε in (nhdsWithin 0 (Ioi 0)), ∀ X : ℝ, 0 ≤ X →
    ‖𝓜 (fun x ↦ (Smooth1 SmoothingF ε x : ℂ)) 1 * X - X‖ ≤ C * ε * X

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  (title := "ZetaBoxEval")  (statement := /--  For all $\epsilon > 0$ sufficiently close to $0$, the rectangle integral over $[1-\delta,2] \times_{ℂ} [-T,T]$ of the integrand in  $\psi_{\epsilon}$ is  $$  \frac{X^{1}}{1}\mathcal{M}(\widetilde{1_{\epsilon}})(1)  = X(1+O(\epsilon))  ,$$  where the implicit constant is independent of $X$.  -/)  (proof := /-- Unfold the definitions and apply Lemma \ref{MellinOfSmooth1c}. -/)]theorem ZetaBoxEval {SmoothingF : ℝ → ℝ}    (suppSmoothingF : Function.support SmoothingF ⊆ Icc (1 / 2) 2)    (mass_one : ∫ x in Ioi 0, SmoothingF x / x = 1)    (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) :    ∃ C, ∀ᶠ ε in (nhdsWithin 0 (Ioi 0)), ∀ X : ℝ, 0 ≤ X →    ‖𝓜 (fun x ↦ (Smooth1 SmoothingF ε x : ℂ)) 1 * X - X‖ ≤ C * ε * X := by  have := MellinOfSmooth1c ContDiffSmoothingF suppSmoothingF mass_one  clear suppSmoothingF mass_one ContDiffSmoothingF  rw[Asymptotics.isBigO_iff] at this  obtain ⟨C, hC⟩ := this  use C  have εpos : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Ioi 0), ε > 0 :=    eventually_mem_of_tendsto_nhdsWithin fun ⦃U⦄ hU ↦ hU  filter_upwards [hC, εpos] with ε hC εpos  rw[id_eq, norm_of_nonneg (le_of_lt εpos)] at hC  intro X Xnne  nth_rw 2 [← one_mul (X : ℂ)]  rw[← sub_mul, norm_mul, norm_real, norm_of_nonneg Xnne]  exact mul_le_mul_of_nonneg_right hC Xnne