Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.kadiri_laplace_exp_hasDerivAt_zero

PrimeNumberTheoremAnd.IEANTN.KadiriSupport · PrimeNumberTheoremAnd/IEANTN/KadiriSupport.lean:256 to 272

Source documentation

Derivative of the two-sided Laplace transform at 0: the s0 = 0 instance of the full-strip derivative formula.

Exact Lean statement

lemma kadiri_laplace_exp_hasDerivAt_zero {φ : ℝ → ℂ} (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|)) :
    HasDerivAt
      (fun s : ℂ => ∫ y : ℝ, φ y * exp (s * (y : ℂ)) ∂volume)
      (∫ y : ℝ, φ y * (y : ℂ) ∂volume) 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma kadiri_laplace_exp_hasDerivAt_zero {φ : ℝ → ℂ} (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|)) :    HasDerivAt      (fun s : ℂ => ∫ y : ℝ, φ y * exp (s * (y : ℂ)) ∂volume)      (∫ y : ℝ, φ y * (y : ℂ) ∂volume) 0 := by  have h := kadiri_laplace_exp_hasDerivAt_of_full_strip (φ := φ) hφ (b := b) (s0 := 0)    (by simp only [Complex.zero_re]; linarith)    (by simp only [Complex.zero_re]; linarith) hφ_decay  have heq : (∫ y : ℝ, φ y * ((y : ℂ) * exp ((0 : ℂ) * (y : ℂ))) ∂volume) =      ∫ y : ℝ, φ y * (y : ℂ) ∂volume := by    apply integral_congr_ae    filter_upwards with y    simp  rw [← heq]  exact h