Kernel Bridge

Finite-law and finite-kernel measure bridges

This file proves that the measure representations in MeasureBridge commute with the project's finite pushforward and one-step kernel operations.

theorem FD1D.FiniteLaw.measure_ext_of_singletons {α : Type u_1} [Finite α] [MeasurableSpace α] {μ ν : MeasureTheory.Measure α} (h : ∀ (x : α), μ {x} = ν {x}) : μ = ν

Measures on a finite measurable-singleton space are determined by point masses.

def FD1D.FiniteLaw.product {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (μ : FiniteLaw α) (ν : FiniteLaw β) : FiniteLaw (α × β)

The independent product of two finite laws.

Equations

• μ.product ν = { mass := fun (p : α × β) => μ.mass p.1 * ν.mass p.2, mass_nonneg := ⋯, sum_mass := ⋯ }

@[simp]

theorem FD1D.FiniteLaw.mass_product {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (μ : FiniteLaw α) (ν : FiniteLaw β) (x : α) (y : β) : (μ.product ν).mass (x, y) = μ.mass x * ν.mass y

@[simp]

theorem FD1D.FiniteLaw.toMeasure_product {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : FiniteLaw α) (ν : FiniteLaw β) : (μ.product ν).toMeasure = μ.toMeasure.prod ν.toMeasure

Finite-law products become ordinary product measures.

@[simp]

theorem FD1D.FiniteLaw.toMeasure_map {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : FiniteLaw α) (f : α → β) (hf : Measurable f) : MeasureTheory.Measure.map f μ.toMeasure = (map f μ).toMeasure

Converting a finite-law pushforward to a measure is ordinary measure pushforward.

theorem FD1D.FiniteKernel.toKernel_apply_singleton {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (K : FiniteKernel α) (x y : α) : (K.toKernel x) {y} = ENNReal.ofReal (K.trans x y)

A finite kernel's measure-valued row has the prescribed transition mass.

theorem FD1D.FiniteKernel.integral_toKernel {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (K : FiniteKernel α) (x : α) (f : α → ℝ) : ∫ (y : α), f y ∂K.toKernel x = ∑ y : α, K.trans x y * f y

Integrating one finite-kernel row agrees with its elementary weighted sum.

@[simp]

theorem FD1D.FiniteKernel.toMeasure_step {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (K : FiniteKernel α) (μ : FiniteLaw α) : μ.toMeasure.bind ⇑K.toKernel = (K.step μ).toMeasure

Mathlib kernel composition realizes the project's finite-law step.