Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.kadiri_laplace_neg_line_weight_integrable_of_continuous

PrimeNumberTheoremAnd.IEANTN.KadiriSupport · PrimeNumberTheoremAnd/IEANTN/KadiriSupport.lean:158 to 171

Source documentation

Integrability of the weighted source for -(1+b) < σ < b: the σ ↦ -σ instance of kadiri_laplace_full_strip_weight_integrable_of_continuous.

Exact Lean statement

lemma kadiri_laplace_neg_line_weight_integrable_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|)) :
    Integrable (fun y : ℝ => exp (-((sigma : ℂ) * (y : ℂ))) * ψ y)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma kadiri_laplace_neg_line_weight_integrable_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|)) :    Integrable (fun y : ℝ => exp (-((sigma : ℂ) * (y : ℂ))) * ψ y) := by  have hbase := kadiri_laplace_full_strip_weight_integrable_of_continuous    (ψ := ψ) hψ (σ := -sigma) (by linarith) (by linarith) hψ_decay  refine hbase.congr ?_  filter_upwards with y  have harg : ((-sigma : ℝ) : ℂ) * (y : ℂ) = -((sigma : ℂ) * (y : ℂ)) := by    push_cast    ring  rw [harg]