Squared matching cost for the v5 policy

This module combines the exact squared-quantile identity with the one-cell spatial coupling. It proves the manuscript's conditional and count-law RMS bounds while allowing arbitrary occupied locations inside their certified dyadic cells.

noncomputable def FD1D.V5.Transport.expectedActualSquaredDistance {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) (fallback : Fin m) : ℝ

Conditional squared distance to the actual selected supply point.

Equations

• FD1D.V5.Transport.expectedActualSquaredDistance C q fallback = ∫ (u : ℝ) in Set.Icc 0 1, (C.selectedSupplyPoint q fallback u - u) ^ 2

theorem FD1D.V5.Transport.expectedActualSquaredDistance_le {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) (hq : q.IsProbability) (hsupport : C.Supports q) (fallback : Fin m) : expectedActualSquaredDistance C q fallback ≤ (dyadicCellWidth L + √(∫ (u : ℝ) in Set.Icc 0 1, (q.quantile u - u) ^ 2)) ^ 2

Minkowski's inequality for the actual selected supply and the recursive quantile, with the deterministic one-cell error made explicit.

noncomputable def FD1D.V5.Transport.stateSquaredCostEnvelope {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) : ℝ

Count-state envelope for the actual conditional squared matching cost.

Equations

• FD1D.V5.Transport.stateSquaredCostEnvelope a x = (FD1D.dyadicCellWidth L + √(FD1D.haarL2 FD1D.haarNodeLeft FD1D.haarNodeWidth (FD1D.V5.Transport.stateHaarCoefficient a x))) ^ 2

theorem FD1D.V5.Transport.expectedActualSquaredDistance_le_stateEnvelope {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (C : SupplyConfiguration L m) (fallback : Fin m) : expectedActualSquaredDistance C (stateDyadicMass a C.countState) fallback ≤ stateSquaredCostEnvelope a C.countState

theorem FD1D.V5.Transport.sqrt_expect_add_sqrt_sq_le {Omega : Type u_1} [Fintype Omega] (mu : FiniteLaw Omega) (w : ℝ) (hw : 0 ≤ w) (H : Omega → ℝ) (hH : ∀ (omega : Omega), 0 ≤ H omega) : √(mu.expect fun (omega : Omega) => (w + √(H omega)) ^ 2) ≤ w + √(mu.expect H)

Finite-law Minkowski/Jensen inequality for a deterministic error plus a state-dependent nonnegative squared error.

theorem FD1D.V5.Transport.sqrt_expected_stateSquaredCostEnvelope_le {L m : ℕ} (a : ℝ) (μ : FiniteLaw (InventoryState (DyadicNode L) m)) (hinv : ∀ (d : Fin L) (v : DyadicNode ↑d), FiniteKernel.LawInvariant μ (TreeSymmetry.inventorySwap ⋯ v)) : √(μ.expect (stateSquaredCostEnvelope a)) ≤ dyadicCellWidth L + √(1 / 12 * μ.expect (Dynamics.stateTransportEnergy a))

The count-law RMS envelope. Tree symmetry converts its mean Haar energy to E[G]/12, yielding exactly the transport-cost inequality in the manuscript.