Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.kadiri_laplace_neg_line_weight_bounded_of_continuous

PrimeNumberTheoremAnd.IEANTN.KadiriSupport · PrimeNumberTheoremAnd/IEANTN/KadiriSupport.lean:141 to 154

Source documentation

Global boundedness of the weighted source for -(1+b) < σ < b.

Exact Lean statement

lemma kadiri_laplace_neg_line_weight_bounded_of_continuous {ψ : ℝ → ℂ}
    (hψ : Continuous ψ) {b sigma : ℝ}
    (hlo : -(1 + b) < sigma) (hhi : sigma < b)
    (hψ_decay : (fun x : ℝ ↦ ψ x * exp ((x : ℂ) / 2))
        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|)) :
    ∃ B : ℝ, 0 ≤ B ∧ ∀ x : ℝ, ‖exp (-((sigma : ℂ) * (x : ℂ))) * ψ x‖ ≤ B

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma kadiri_laplace_neg_line_weight_bounded_of_continuous {ψ : ℝ → ℂ}    (hψ : Continuous ψ) {b sigma : ℝ}    (hlo : -(1 + b) < sigma) (hhi : sigma < b)    (hψ_decay : (fun x : ℝ ↦ ψ x * exp ((x : ℂ) / 2))        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|)) :    ∃ B : ℝ, 0 ≤ B ∧ ∀ x : ℝ, ‖exp (-((sigma : ℂ) * (x : ℂ))) * ψ x‖ ≤ B := by  have htop := kadiri_laplace_neg_line_weight_isBigO_atTop (ψ := ψ) (b := b) sigma    (hψ_decay.mono atTop_le_cocompact)  have hbot := kadiri_laplace_neg_line_weight_isBigO_atBot (ψ := ψ) (b := b) sigma    (hψ_decay.mono atBot_le_cocompact)  exact bounded_of_continuous_of_isBigO_exp_atBot_atTop    ((laplaceKernel_contDiff_paren ((sigma : ℝ) : ℂ)).continuous.mul hψ)    (show -(1 + b + sigma) < 0 by linarith) (show 0 < b - sigma by linarith)    htop hbot