Measure Bridge

Finite laws as measures

This file connects the project's elementary FiniteLaw API to Mathlib probability measures. It also transfers bounds indexed by a finite count state to arbitrary random spatial configurations having that count pushforward.

def FD1D.FiniteLaw.toPMF {α : Type u_1} [Fintype α] (μ : FiniteLaw α) : PMF α

The probability mass function represented by a FiniteLaw.

Equations

• μ.toPMF = PMF.ofFintype (fun (x : α) => ENNReal.ofReal (μ.mass x)) ⋯

@[simp]

theorem FD1D.FiniteLaw.toPMF_apply {α : Type u_1} [Fintype α] (μ : FiniteLaw α) (x : α) : μ.toPMF x = ENNReal.ofReal (μ.mass x)

noncomputable def FD1D.FiniteLaw.toMeasure {α : Type u_1} [Fintype α] [MeasurableSpace α] (μ : FiniteLaw α) : MeasureTheory.Measure α

The probability measure represented by a FiniteLaw.

On a finite type it is enough to assume measurable singletons: this already makes every function from the type measurable.

Equations

• μ.toMeasure = μ.toPMF.toMeasure

instance FD1D.FiniteLaw.toMeasure.isProbabilityMeasure {α : Type u_1} [Fintype α] [MeasurableSpace α] (μ : FiniteLaw α) : MeasureTheory.IsProbabilityMeasure μ.toMeasure

@[simp]

theorem FD1D.FiniteLaw.toMeasure_apply_singleton {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : FiniteLaw α) (x : α) : μ.toMeasure {x} = ENNReal.ofReal (μ.mass x)

@[simp]

theorem FD1D.FiniteLaw.toMeasure_real_singleton {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : FiniteLaw α) (x : α) : μ.toMeasure.real {x} = μ.mass x

@[simp]

theorem FD1D.FiniteLaw.integral_toMeasure_eq_expect {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : FiniteLaw α) (f : α → ℝ) : ∫ (x : α), f x ∂μ.toMeasure = μ.expect f

Integration against the associated measure is FiniteLaw.expect.

theorem FD1D.FiniteLaw.integrable_toMeasure {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : FiniteLaw α) (f : α → ℝ) : MeasureTheory.Integrable f μ.toMeasure

Every real observable is integrable under a finite law's measure.

theorem FD1D.FiniteLaw.integral_le_expect_of_map_eq {α : Type u_1} {Ω : Type u_3} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) (μ : FiniteLaw α) (X : Ω → α) (cost : Ω → ℝ) (bound : α → ℝ) (hX : AEMeasurable X P) (hcost : MeasureTheory.Integrable cost P) (hpoint : ∀ᵐ (ω : Ω) ∂P, cost ω ≤ bound (X ω)) (hmap : MeasureTheory.Measure.map X P = μ.toMeasure) : ∫ (ω : Ω), cost ω ∂P ≤ μ.expect bound

A generic pushforward bridge. If X has finite law μ, then any integrable random cost bounded by a state observable has expectation bounded by the corresponding FiniteLaw.expect.

theorem FD1D.FiniteLaw.integral_le_of_map_eq_of_expect_le {α : Type u_1} {Ω : Type u_3} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) (μ : FiniteLaw α) (X : Ω → α) (cost : Ω → ℝ) (bound : α → ℝ) (B : ℝ) (hX : AEMeasurable X P) (hcost : MeasureTheory.Integrable cost P) (hpoint : ∀ᵐ (ω : Ω) ∂P, cost ω ≤ bound (X ω)) (hmap : MeasureTheory.Measure.map X P = μ.toMeasure) (hbound : μ.expect bound ≤ B) : ∫ (ω : Ω), cost ω ∂P ≤ B

A convenient final-bound form of integral_le_expect_of_map_eq.

def FD1D.FiniteKernel.rowLaw {α : Type u_1} [Fintype α] (K : FiniteKernel α) (x : α) : FiniteLaw α

The probability law represented by one row of a finite kernel.

Equations

• K.rowLaw x = { mass := K.trans x, mass_nonneg := ⋯, sum_mass := ⋯ }

@[simp]

theorem FD1D.FiniteKernel.rowLaw_mass {α : Type u_1} [Fintype α] (K : FiniteKernel α) (x y : α) : (K.rowLaw x).mass y = K.trans x y

noncomputable def FD1D.FiniteKernel.toKernel {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (K : FiniteKernel α) : ProbabilityTheory.Kernel α α

A project FiniteKernel, viewed as a Mathlib Markov kernel.

Equations

• K.toKernel = { toFun := fun (x : α) => (K.rowLaw x).toMeasure, measurable' := ⋯ }

@[simp]

theorem FD1D.FiniteKernel.toKernel_apply {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (K : FiniteKernel α) (x : α) : K.toKernel x = (K.rowLaw x).toMeasure

instance FD1D.FiniteKernel.toKernel.isMarkovKernel {α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (K : FiniteKernel α) : ProbabilityTheory.IsMarkovKernel K.toKernel

noncomputable def FD1D.HierarchicalDynamics.actualConfigurationCost {L m : ℕ} (a : ℝ) (hm : 0 < m) (C : SupplyConfiguration L m) : ℝ

The actual one-period cost of a concrete spatial configuration.

Equations

• FD1D.HierarchicalDynamics.actualConfigurationCost a hm C = C.expectedActualDistance (FD1D.HierarchicalDynamics.stateDyadicMass a C.countState) (FD1D.SupplyConfiguration.canonicalFallback hm)

theorem FD1D.HierarchicalDynamics.integral_actualConfigurationCost_le_expect {L m : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSpace (InventoryState (DyadicNode L) m)] [MeasurableSingletonClass (InventoryState (DyadicNode L) m)] (a : ℝ) (ha : 0 < a) (hm : 0 < m) (P : MeasureTheory.Measure Ω) (μ : FiniteLaw (InventoryState (DyadicNode L) m)) (C : Ω → SupplyConfiguration L m) (hstate : AEMeasurable (fun (ω : Ω) => (C ω).countState) P) (hcost : MeasureTheory.Integrable (fun (ω : Ω) => actualConfigurationCost a hm (C ω)) P) (hmap : MeasureTheory.Measure.map (fun (ω : Ω) => (C ω).countState) P = μ.toMeasure) : ∫ (ω : Ω), actualConfigurationCost a hm (C ω) ∂P ≤ μ.expect fun (x : InventoryState (DyadicNode L) m) => 1 / ↑(2 ^ L) + cdfTransportArea (haarCombination haarNodeLeft haarNodeWidth (stateHaarCoefficient a x))

An arbitrary spatial law is bounded by the finite-law expectation of the canonical Haar pointwise majorant whenever its count-state pushforward is the given finite law.

theorem FD1D.HierarchicalDynamics.stationary_actualConfigurationCost_equation_three {L m : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSpace (InventoryState (DyadicNode L) m)] [MeasurableSingletonClass (InventoryState (DyadicNode L) m)] (a : ℝ) (ha : 0 < a) (hm : 0 < m) (P : MeasureTheory.Measure Ω) (μ : FiniteLaw (InventoryState (DyadicNode L) m)) (C : Ω → SupplyConfiguration L m) (hstate : AEMeasurable (fun (ω : Ω) => (C ω).countState) P) (hcost : MeasureTheory.Integrable (fun (ω : Ω) => actualConfigurationCost a hm (C ω)) P) (hmap : MeasureTheory.Measure.map (fun (ω : Ω) => (C ω).countState) P = μ.toMeasure) (hμ : (kernel a ha hm).IsStationary μ) : ∫ (ω : Ω), actualConfigurationCost a hm (C ω) ∂P ≤ 1 / ↑(2 ^ L) + a / √6 * √((μ.expect fun (x : InventoryState (DyadicNode L) m) => stateHazardEnergy a x L) - 1 / ↑m ^ 2)

Stationary equation (3) for an arbitrary random spatial configuration. Only the count pushforward is required to be stationary; configurations in the same count-state fiber may have any distribution.

theorem FD1D.stationary_expected_actualConfigurationCost_le_six {m : ℕ} (hm : 1 ≤ m) {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSpace (InventoryState (DyadicNode (treeDepth m)) m)] [MeasurableSingletonClass (InventoryState (DyadicNode (treeDepth m)) m)] (P : MeasureTheory.Measure Ω) (μ : FiniteLaw (InventoryState (DyadicNode (treeDepth m)) m)) (C : Ω → SupplyConfiguration (treeDepth m) m) (hstate : AEMeasurable (fun (ω : Ω) => (C ω).countState) P) (hcost : MeasureTheory.Integrable (fun (ω : Ω) => HierarchicalDynamics.actualConfigurationCost ↑(parameterA m) ⋯ (C ω)) P) (hmap : MeasureTheory.Measure.map (fun (ω : Ω) => (C ω).countState) P = μ.toMeasure) (hμ : (parameterizedKernel m hm).IsStationary μ) : ∫ (ω : Ω), HierarchicalDynamics.actualConfigurationCost ↑(parameterA m) ⋯ (C ω) ∂P ≤ 6 * ↑(parameterA m) / ↑m

The stationary 6a/m result transferred from a finite count law to an arbitrary random law of actual spatial configurations.