Source indexedtheorem · leanprover/lean4:v4.32.0

Phi_analyticOnNhd

PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:316 to 326

Source documentation

The bilateral Laplace transform is analytic on the strip -(1+b) < Re s < b.

Exact Lean statement

theorem Phi_analyticOnNhd {φ : ℝ → ℂ} {b : ℝ} (hφc : Continuous φ)
    (hφ_decay : (fun x : ℝ ↦ φ x * Complex.exp ((x:ℂ)/2)) =O[cocompact ℝ]
      fun x ↦ Real.exp (-(1/2+b)*|x|)) :
    AnalyticOnNhd ℂ (fun s ↦ ∫ y, φ y * Complex.exp (-s*(y:ℂ)))
      {s : ℂ | -(1+b) < s.re ∧ s.re < b}

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem Phi_analyticOnNhd {φ : ℝ → ℂ} {b : ℝ} (hφc : Continuous φ)    (hφ_decay : (fun x : ℝ ↦ φ x * Complex.exp ((x:ℂ)/2)) =O[cocompact ℝ]      fun x ↦ Real.exp (-(1/2+b)*|x|)) :    AnalyticOnNhd ℂ (fun s ↦ ∫ y, φ y * Complex.exp (-s*(y:ℂ)))      {s : ℂ | -(1+b) < s.re ∧ s.re < b} := by  have hSopen : IsOpen {s : ℂ | -(1+b) < s.re ∧ s.re < b} := by    rw [show {s : ℂ | -(1+b) < s.re ∧ s.re < b} = Complex.re ⁻¹' (Set.Ioo (-(1+b)) b) from by      ext s; simp [Set.mem_Ioo, and_comm]]    exact isOpen_Ioo.preimage Complex.continuous_re  exact DifferentiableOn.analyticOnNhd    (fun s hs ↦ (Phi_differentiableAt hφc hφ_decay hs.1 hs.2).differentiableWithinAt) hSopen