noncomputable def ComplexLaplaceIntegrand {α : Type u_1} (E : α → WithTop ℝ) (z : ℂ) (x : α) : ℂ

The integrand of the complex Laplace transform of a possibly infinite-valued energy function.

Equations

• ComplexLaplaceIntegrand E z x = if h : E x = ⊤ then 0 else Complex.exp (-z * ↑((E x).untop h))

noncomputable def ComplexLaplaceTransform {α : Type u_1} [MeasurableSpace α] [MeasureTheory.MeasureSpace α] (E : α → WithTop ℝ) (z : ℂ) : ℂ

The complex Laplace transform of a possibly infinite-valued energy function.

Equations

• ComplexLaplaceTransform E z = ∫ (x : α), ComplexLaplaceIntegrand E z x

def ComplexLaplaceConvergenceDomain {α : Type u_1} [MeasurableSpace α] [MeasureTheory.MeasureSpace α] (E : α → WithTop ℝ) : Set ℂ

The complex convergence domain of a Laplace transform.

Equations

• ComplexLaplaceConvergenceDomain E = {z : ℂ | MeasureTheory.Integrable (ComplexLaplaceIntegrand E z) MeasureTheory.volume}

theorem analyticAt_complexLaplaceIntegrand {α : Type u_1} (E : α → WithTop ℝ) (x : α) (z : ℂ) : AnalyticAt ℂ (fun (w : ℂ) => ComplexLaplaceIntegrand E w x) z

For each configuration, the complex Laplace integrand is analytic in the parameter.

theorem measurable_complexLaplaceIntegrand {α : Type u_1} [MeasurableSpace α] {E : α → WithTop ℝ} (hE : Measurable E) (z : ℂ) : Measurable (ComplexLaplaceIntegrand E z)

theorem eventually_integrable_complexLaplaceIntegrand_of_mem_interior_convergenceDomain {α : Type u_1} [MeasurableSpace α] [MeasureTheory.MeasureSpace α] {E : α → WithTop ℝ} {z : ℂ} (hz : z ∈ interior (ComplexLaplaceConvergenceDomain E)) : ∀ᶠ (w : ℂ) in nhds z, MeasureTheory.Integrable (ComplexLaplaceIntegrand E w) MeasureTheory.volume

Interior convergence gives integrability throughout a neighborhood of the parameter.

theorem continuousAt_complexLaplaceTransform_of_mem_interior_convergenceDomain {α : Type u_1} [MeasurableSpace α] [MeasureTheory.MeasureSpace α] {E : α → WithTop ℝ} {z : ℂ} (hz : z ∈ interior (ComplexLaplaceConvergenceDomain E)) : ContinuousAt (ComplexLaplaceTransform E) z

theorem continuousOn_complexLaplaceTransform_interior_convergenceDomain {α : Type u_1} [MeasurableSpace α] [MeasureTheory.MeasureSpace α] {E : α → WithTop ℝ} : ContinuousOn (ComplexLaplaceTransform E) (interior (ComplexLaplaceConvergenceDomain E))

theorem analyticAt_complexLaplaceTransform_of_mem_interior_convergenceDomain {α : Type u_1} [MeasureTheory.MeasureSpace α] [MeasureTheory.SFinite MeasureTheory.volume] {E : α → WithTop ℝ} {z : ℂ} (hE : Measurable E) (hz : z ∈ interior (ComplexLaplaceConvergenceDomain E)) : AnalyticAt ℂ (ComplexLaplaceTransform E) z

A complex Laplace transform is analytic on the interior of its convergence domain.