Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.kadiri_laplace_positive_vertical_segment_continuousOn

PrimeNumberTheoremAnd.IEANTN.KadiriEq14 · PrimeNumberTheoremAnd/IEANTN/KadiriEq14.lean:105 to 132

Source documentation

Continuity of the bilateral Laplace integral on the positive vertical line re s = a, obtained by reflecting the shifted contour statement.

Exact Lean statement

lemma kadiri_laplace_positive_vertical_segment_continuousOn
    {φ : ℝ → ℂ} (hφ : ContDiff ℝ 1 φ)
    {b : ℝ} (hb : 0 < b)
    (hφ_decay : (fun x : ℝ ↦ φ x * exp ((x : ℂ) / 2))
        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|))
    {a T : ℝ} (ha : 0 < a) (hab : a < b) (ha1 : a < 1) :
    ContinuousOn (fun t : ℝ => laplaceIntegral φ (((a : ℝ) : ℂ) + (t : ℂ) * I))
      (Set.Icc (-T) T)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma kadiri_laplace_positive_vertical_segment_continuousOn    {φ : ℝ → ℂ} (hφ : ContDiff ℝ 1 φ)    {b : ℝ} (hb : 0 < b)    (hφ_decay : (fun x : ℝ ↦ φ x * exp ((x : ℂ) / 2))        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|))    {a T : ℝ} (ha : 0 < a) (hab : a < b) (ha1 : a < 1) :    ContinuousOn (fun t : ℝ => laplaceIntegral φ (((a : ℝ) : ℂ) + (t : ℂ) * I))      (Set.Icc (-T) T) := by  have hminus := kadiri_laplace_shifted_vertical_segment_continuousOn    (φ := φ) hφ hb hφ_decay (a := a) (T := T) ha hab ha1  have hcomp : ContinuousOn      (fun t : ℝ =>        (fun u : ℝ =>          let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume          let s : ℂ := ((-a : ℝ) : ℂ) + (u : ℂ) * I          Φ (-s)) (-t))      (Set.Icc (-T) T) := by    refine hminus.comp (continuous_neg.continuousOn) ?_    intro t ht    exact ⟨by linarith [ht.2], by linarith [ht.1]⟩  refine hcomp.congr ?_  intro t _ht  dsimp [laplaceIntegral]  apply integral_congr_ae  filter_upwards with y  apply congrArg (fun z : ℂ => φ y * exp (-z * (y : ℂ)))  norm_num  ring_nf