The Laplace kernel on ℝ≥0

The exponential kernel p ↦ e^{-xp} of the Laplace transform on ℝ≥0, as a plain function and as a bundled bounded continuous function, together with its basic bounds and its integrability against finite measures. Its extended-nonnegative-valued integral against a measure is TauCeti.laplaceTransformENN. Applying this transform fibrewise to a transition kernel gives ProbabilityTheory.Kernel.laplaceTransform. This lightweight module is shared by the Chafaï approximating-measure machinery and the Laplace-representation theory, which otherwise do not depend on each other.

Main declarations

• TauCeti.laplaceKernelBoundedContinuous: the kernel as a bounded continuous function.
• TauCeti.integrable_exp_neg_mul: the kernel is integrable against any finite measure.
• TauCeti.laplaceTransformENN: the extended-nonnegative-valued Laplace transform of a measure.
• ProbabilityTheory.Kernel.laplaceTransform: the fibrewise Laplace transform q ↦ ∫⁻ p, exp (-t p) ∂(κ q) of a transition kernel κ into ℝ≥0.

theorem TauCeti.continuous_exp_neg_mul (t : ℝ) : Continuous fun (x : NNReal) => Real.exp (-(t * ↑x))

The Laplace kernel p ↦ e^{-tp} is continuous in the coordinate variable.

theorem TauCeti.exp_neg_mul_le_one {x : ℝ} (hx : 0 ≤ x) (p : NNReal) : Real.exp (-(x * ↑p)) ≤ 1

For 0 ≤ x the Laplace kernel is bounded by 1 on ℝ≥0.

theorem TauCeti.antitone_exp_neg_mul (p : NNReal) : Antitone fun (t : NNReal) => Real.exp (-↑t * ↑p)

For fixed nonnegative p, the Laplace kernel is antitone in its nonnegative parameter.

noncomputable def TauCeti.laplaceKernelBoundedContinuous {x : ℝ} (hx : 0 ≤ x) : BoundedContinuousFunction NNReal ℝ

The Laplace kernel as a bundled bounded continuous test function of the nonnegative variable p, for fixed nonnegative x.

Equations

• TauCeti.laplaceKernelBoundedContinuous hx = { toFun := fun (p : NNReal) => Real.exp (-(x * ↑p)), continuous_toFun := ⋯, map_bounded' := ⋯ }

@[simp]

theorem TauCeti.laplaceKernelBoundedContinuous_apply {x : ℝ} (hx : 0 ≤ x) (p : NNReal) : (laplaceKernelBoundedContinuous hx) p = Real.exp (-(x * ↑p))

The bundled Laplace kernel evaluates to the usual exponential kernel on ℝ≥0.

theorem TauCeti.integrable_exp_neg_mul (μ : MeasureTheory.Measure NNReal) [MeasureTheory.IsFiniteMeasure μ] {x : ℝ} (hx : 0 ≤ x) : MeasureTheory.Integrable (fun (p : NNReal) => Real.exp (-(x * ↑p))) μ

The Laplace kernel is integrable against a finite measure. For 0 ≤ x the kernel p ↦ e^{-xp} is bounded and continuous on ℝ≥0, hence integrable against any finite measure.

The extended-nonnegative-valued Laplace transform

noncomputable def TauCeti.laplaceTransformENN (μ : MeasureTheory.Measure NNReal) (t : NNReal) : ENNReal

The extended-nonnegative-valued Laplace transform of a measure on ℝ≥0.

Equations

• TauCeti.laplaceTransformENN μ t = ∫⁻ (p : NNReal), ENNReal.ofReal (Real.exp (-↑t * ↑p)) ∂μ

theorem TauCeti.laplaceTransformENN_apply (μ : MeasureTheory.Measure NNReal) (t : NNReal) : laplaceTransformENN μ t = ∫⁻ (p : NNReal), ENNReal.ofReal (Real.exp (-↑t * ↑p)) ∂μ

The defining formula for TauCeti.laplaceTransformENN.

@[simp]

theorem TauCeti.laplaceTransformENN_zero (μ : MeasureTheory.Measure NNReal) : laplaceTransformENN μ 0 = μ Set.univ

At time 0, the extended-real Laplace transform is the total mass.

theorem TauCeti.laplaceTransformENN_antitone (μ : MeasureTheory.Measure NNReal) : Antitone (laplaceTransformENN μ)

The extended-real Laplace transform decreases in time.

theorem TauCeti.laplaceTransformENN_le_apply_univ (μ : MeasureTheory.Measure NNReal) (t : NNReal) : laplaceTransformENN μ t ≤ μ Set.univ

The extended-real Laplace transform is bounded by the total mass.

@[simp]

theorem TauCeti.laplaceTransformENN_ne_top (μ : MeasureTheory.Measure NNReal) [MeasureTheory.IsFiniteMeasure μ] (t : NNReal) : laplaceTransformENN μ t ≠ ⊤

The extended-real Laplace transform of a finite measure is finite.

The fibrewise Laplace transform of a kernel

noncomputable def ProbabilityTheory.Kernel.laplaceTransform {V : Type u_1} [MeasurableSpace V] (κ : Kernel V NNReal) (t : NNReal) (q : V) : ENNReal

The fibrewise Laplace transform of a kernel κ from V to ℝ≥0: the function q ↦ ∫⁻ p, exp (-t p) ∂(κ q) on V.

Equations

• κ.laplaceTransform t q = TauCeti.laplaceTransformENN (κ q) t

theorem ProbabilityTheory.Kernel.laplaceTransform_apply {V : Type u_1} [MeasurableSpace V] (κ : Kernel V NNReal) (t : NNReal) (q : V) : κ.laplaceTransform t q = TauCeti.laplaceTransformENN (κ q) t

The defining formula for ProbabilityTheory.Kernel.laplaceTransform.

theorem ProbabilityTheory.Kernel.measurable_laplaceTransform {V : Type u_1} [MeasurableSpace V] (κ : Kernel V NNReal) (t : NNReal) : Measurable (κ.laplaceTransform t)

@[simp]

theorem ProbabilityTheory.Kernel.laplaceTransform_zero {V : Type u_1} [MeasurableSpace V] (κ : Kernel V NNReal) (q : V) : κ.laplaceTransform 0 q = (κ q) Set.univ

At time 0, the fibrewise Laplace transform is the total mass of the fibre.

theorem ProbabilityTheory.Kernel.laplaceTransform_antitone {V : Type u_1} [MeasurableSpace V] (κ : Kernel V NNReal) (q : V) : Antitone fun (t : NNReal) => κ.laplaceTransform t q

The fibrewise Laplace transform decreases in time at each base point.

@[simp]

theorem ProbabilityTheory.Kernel.laplaceTransform_zero_of_isMarkovKernel {V : Type u_1} [MeasurableSpace V] (κ : Kernel V NNReal) [IsMarkovKernel κ] : κ.laplaceTransform 0 = 1

A Markov kernel has fibrewise Laplace transform 1 at time 0.