Source indexedlemma · leanprover/lean4:v4.32.0

MellinOfDeltaSpikeAt1_asymp

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:700 to 764

Mathematical statement

Exact Lean statement

@[blueprint
  (title := "MellinOfDeltaSpikeAt1-asymp")
  (statement := /--
  As $\epsilon\to 0$, we have
  $$\mathcal{M}(\nu_\epsilon)(1) = 1+O(\epsilon).$$
  -/)
  (proof := /--
  By Lemma \ref{MellinOfDeltaSpikeAt1},
  $$
    \mathcal M(\nu_\epsilon)(1)=\mathcal M(\nu)(\epsilon)
  $$
  which by Definition \ref{MellinTransform} is
  $$
    \mathcal M(\nu)(\epsilon)=\int_0^\infty\nu(x)x^{\epsilon-1}dx
    .
  $$
  Since $\nu(x) x^{\epsilon-1}$ is integrable (because $\nu$ is continuous and compactly
  supported),
  $$
    \mathcal M(\nu)(\epsilon)-\int_0^\infty\nu(x)\frac{dx}x
    =\int_0^\infty\nu(x)(x^{\epsilon-1}-x^{-1})dx
    .
  $$
  By Taylor's theorem,
  $$
    x^{\epsilon-1}-x^{-1}=O(\epsilon)
  $$
  so, since $\nu$ is absolutely integrable,
  $$
    \mathcal M(\nu)(\epsilon)-\int_0^\infty\nu(x)\frac{dx}x=O(\epsilon)
    .
  $$
  We conclude the proof using Theorem \ref{SmoothExistence}.
  -/)
  (latexEnv := "lemma")]
lemma MellinOfDeltaSpikeAt1_asymp {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν)
    (suppν : ν.support ⊆ Set.Icc (1 / 2) 2)
    (mass_one : ∫ x in Set.Ioi 0, ν x / x = 1) :
    (fun (ε : ℝ) ↦ (𝓜 (fun x ↦ (ν x : ℂ)) ε) - 1) =O[𝓝[>]0] id

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  (title := "MellinOfDeltaSpikeAt1-asymp")  (statement := /--  As $\epsilon\to 0$, we have  $$\mathcal{M}(\nu_\epsilon)(1) = 1+O(\epsilon).$$  -/)  (proof := /--  By Lemma \ref{MellinOfDeltaSpikeAt1},  $$    \mathcal M(\nu_\epsilon)(1)=\mathcal M(\nu)(\epsilon)  $$  which by Definition \ref{MellinTransform} is  $$    \mathcal M(\nu)(\epsilon)=\int_0^\infty\nu(x)x^{\epsilon-1}dx    .  $$  Since $\nu(x) x^{\epsilon-1}$ is integrable (because $\nu$ is continuous and compactly  supported),  $$    \mathcal M(\nu)(\epsilon)-\int_0^\infty\nu(x)\frac{dx}x    =\int_0^\infty\nu(x)(x^{\epsilon-1}-x^{-1})dx    .  $$  By Taylor's theorem,  $$    x^{\epsilon-1}-x^{-1}=O(\epsilon)  $$  so, since $\nu$ is absolutely integrable,  $$    \mathcal M(\nu)(\epsilon)-\int_0^\infty\nu(x)\frac{dx}x=O(\epsilon)    .  $$  We conclude the proof using Theorem \ref{SmoothExistence}.  -/)  (latexEnv := "lemma")]lemma MellinOfDeltaSpikeAt1_asymp {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν)    (suppν : ν.support ⊆ Set.Icc (1 / 2) 2)    (mass_one : ∫ x in Set.Ioi 0, ν x / x = 1) :    (fun (ε : ℝ) ↦ (𝓜 (fun x ↦ (ν x : ℂ)) ε) - 1) =O[𝓝[>]0] id := by  have diff : DifferentiableWithinAt ℝ      (fun (ε : ℝ) ↦ 𝓜 (fun x ↦ (ν x : ℂ)) ε - 1) (Ioi 0) 0 := by    apply DifferentiableAt.differentiableWithinAt    simp only [(differentiableAt_const _).fun_sub_iff_left]    refine DifferentiableAt.comp_ofReal ?_    refine mellin_differentiableAt_of_isBigO_rpow (a := 1) (b := -1) ?_ ?_ (by simp) ?_ (by simp)    · apply (Continuous.continuousOn ?_).locallyIntegrableOn (by simp)      have := diffν.continuous; continuity    · apply Asymptotics.IsBigO.trans_le (g' := fun _ ↦ (0 : ℝ)) ?_ (by simp)      apply BigO_zero_atTop_of_support_in_Icc (a := 1 / 2) (b := 2)      rwa [ν.support_ofReal]    · apply Asymptotics.IsBigO.trans_le (g' := fun _ ↦ (0 : ℝ)) ?_ (by simp)      apply BigO_zero_atZero_of_support_in_Icc (a := 1 / 2) (b := 2) (ha := (by norm_num))      rwa [ν.support_ofReal]  have := ofReal_zero ▸ diff.isBigO_sub  simp only [sub_sub_sub_cancel_right, sub_zero] at this  convert! this using 1  simp only [mellin, zero_sub, cpow_neg_one, smul_eq_mul]  funext ε  congr 1  symm  calc (∫ (t : ℝ) in Ioi 0, (↑t)⁻¹ * ↑(ν t) : ℂ)      = ∫ (t : ℝ) in Ioi 0, ((ν t / t : ℝ) : ℂ) :=        integral_congr_ae (Filter.Eventually.of_forall fun t => by push_cast; ring)    _ = ((∫ t in Ioi 0, ν t / t : ℝ) : ℂ) := integral_ofReal    _ = 1 := by rw [mass_one, ofReal_one]