Quantile transport for the v5 policy

This module realizes the v5 leaf deletion probabilities as a recursive dyadic mass, identifies its integrated Haar coefficients with the v5 deletion imbalances, and proves the exact invariant-law L² identity.

The concrete v5 dyadic mass

def FD1D.V5.Transport.stateDyadicMassAt {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) (d k : ℕ) : DyadicNode d → DyadicMass k

The v5 deletion-mass tree below v, with k levels left to descend.

Equations

• One or more equations did not get rendered due to their size.
• FD1D.V5.Transport.stateDyadicMassAt a x x✝¹ 0 x✝ = FD1D.DyadicMass.leaf (FD1D.V5.Dynamics.deletionLabel a x x✝¹ x✝)

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

The complete v5 deletion-mass tree.

Equations

• FD1D.V5.Transport.stateDyadicMass a x = FD1D.V5.Transport.stateDyadicMassAt a x 0 L FD1D.dyadicRoot

@[simp]

theorem FD1D.V5.Transport.stateDyadicMassAt_zero {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) (d : ℕ) (v : DyadicNode d) : stateDyadicMassAt a x d 0 v = DyadicMass.leaf (Dynamics.deletionLabel a x d v)

@[simp]

theorem FD1D.V5.Transport.stateDyadicMassAt_succ {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) (d k : ℕ) (v : DyadicNode d) : stateDyadicMassAt a x d (k + 1) v = (stateDyadicMassAt a x (d + 1) k (leftChild v)).branch (stateDyadicMassAt a x (d + 1) k (rightChild v))

theorem FD1D.V5.Transport.stateDyadicMassAt_total {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) {d k : ℕ} (hdk : d + k ≤ L) (v : DyadicNode d) : (stateDyadicMassAt a x d k v).total = Dynamics.deletionLabel a x d v

theorem FD1D.V5.Transport.stateDyadicMassAt_allNonneg {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) {d k : ℕ} (hdk : d + k ≤ L) (v : DyadicNode d) : (stateDyadicMassAt a x d k v).allNonneg

theorem FD1D.V5.Transport.stateDyadicMassAt_leaf_probability {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) (w : DyadicNode L) : stateDyadicMassAt a x L 0 w = DyadicMass.leaf ((Dynamics.deletionRule a ha hm).prob x w)

@[simp]

theorem FD1D.V5.Transport.stateDyadicMass_total {L m : ℕ} (a : ℝ) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) : (stateDyadicMass a x).total = 1

theorem FD1D.V5.Transport.stateDyadicMass_isProbability {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) : (stateDyadicMass a x).IsProbability

theorem FD1D.V5.Transport.stateDyadicMassAt_rootCoefficient {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) {d k : ℕ} (hdk : d + (k + 1) ≤ L) (v : DyadicNode d) : (stateDyadicMassAt a x (d + 1) k (leftChild v)).total - (stateDyadicMassAt a x (d + 1) k (rightChild v)).total = TreePolicy.imbalance (Dynamics.aggregatedInventory x) a d v

Canonical tree indexing

theorem FD1D.V5.Transport.stateDyadicMass_leafMass_eq_deletionRule {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) (w : DyadicNode L) : (stateDyadicMass a x).leafMass w = (Dynamics.deletionRule a ha hm).prob x w

theorem FD1D.V5.Transport.stateDyadicMass_nodeCoefficient {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) (i : CompleteHaarNode L) : (stateDyadicMass a x).nodeCoefficient i = TreePolicy.imbalance (Dynamics.aggregatedInventory x) a (↑i.fst) i.snd

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

The canonical v5 integrated-Haar coefficient family.

Equations

• FD1D.V5.Transport.stateHaarCoefficient a x i = FD1D.V5.TreePolicy.imbalance (FD1D.V5.Dynamics.aggregatedInventory x) a (↑i.fst) i.snd

theorem FD1D.V5.Transport.stateDyadicMass_haarSeries_eq {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) {z : ℝ} (hz : z ∈ Set.Icc 0 1) : (stateDyadicMass a x).haarSeries z = haarCombination haarNodeLeft haarNodeWidth (stateHaarCoefficient a x) z

theorem FD1D.V5.Transport.stateDyadicMass_cdf_sub_id_eq {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) {z : ℝ} (hz : z ∈ Set.Icc 0 1) : (stateDyadicMass a x).piecewiseCDF z - z = haarCombination haarNodeLeft haarNodeWidth (stateHaarCoefficient a x) z

Symmetry and exact expected Haar energy

theorem FD1D.V5.Transport.haarCoefficient_swapNode {L m : ℕ} (a : ℝ) (i : CompleteHaarNode L) (x : InventoryState (DyadicNode L) m) : stateHaarCoefficient a ((TreeSymmetry.inventorySwap ⋯ i.snd) x) i = -stateHaarCoefficient a x i

theorem FD1D.V5.Transport.haarCoefficient_strictAncestor {L m : ℕ} (a : ℝ) (i j : CompleteHaarNode L) (hji : ↑j.fst < ↑i.fst) (x : InventoryState (DyadicNode L) m) : stateHaarCoefficient a ((TreeSymmetry.inventorySwap ⋯ i.snd) x) j = stateHaarCoefficient a x j

theorem FD1D.V5.Transport.haar_crossTerm_symmetry_of_swapInvariant {L m : ℕ} (a : ℝ) (μ : FiniteLaw (InventoryState (DyadicNode L) m)) (hinv : ∀ (d : Fin L) (v : DyadicNode ↑d), FiniteKernel.LawInvariant μ (TreeSymmetry.inventorySwap ⋯ v)) (i j : CompleteHaarNode L) : i ≠ j → IntervalsSeparated haarNodeLeft haarNodeWidth i j ∨ μ.OddSymmetry fun (x : InventoryState (DyadicNode L) m) => stateHaarCoefficient a x i * stateHaarCoefficient a x j

theorem FD1D.V5.Transport.stationary_haar_crossTerm_symmetry {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (μ : FiniteLaw (InventoryState (DyadicNode L) m)) (hμ : (Dynamics.kernel a ha hm).IsStationary μ) (i j : CompleteHaarNode L) : i ≠ j → IntervalsSeparated haarNodeLeft haarNodeWidth i j ∨ μ.OddSymmetry fun (x : InventoryState (DyadicNode L) m) => stateHaarCoefficient a x i * stateHaarCoefficient a x j

theorem FD1D.V5.Transport.iterate_lawInvariant_of_swapInvariant {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (μ : FiniteLaw (InventoryState (DyadicNode L) m)) (hinv : ∀ (d : Fin L) (v : DyadicNode ↑d), FiniteKernel.LawInvariant μ (TreeSymmetry.inventorySwap ⋯ v)) (n : ℕ) (d : Fin L) (v : DyadicNode ↑d) : FiniteKernel.LawInvariant ((Dynamics.kernel a ha hm).iterate n μ) (TreeSymmetry.inventorySwap ⋯ v)

theorem FD1D.V5.Transport.iterate_refreshedLaw_lawInvariant {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (n : ℕ) (d : Fin L) (v : DyadicNode ↑d) : FiniteKernel.LawInvariant ((Dynamics.kernel a ha hm).iterate n (refreshedLaw L m)) (TreeSymmetry.inventorySwap ⋯ v)

theorem FD1D.V5.Transport.expected_haarL2_eq_transportEnergy {L m : ℕ} (a : ℝ) (μ : FiniteLaw (InventoryState (DyadicNode L) m)) (hinv : ∀ (d : Fin L) (v : DyadicNode ↑d), FiniteKernel.LawInvariant μ (TreeSymmetry.inventorySwap ⋯ v)) : (μ.expect fun (x : InventoryState (DyadicNode L) m) => haarL2 haarNodeLeft haarNodeWidth (stateHaarCoefficient a x)) = 1 / 12 * μ.expect (Dynamics.stateTransportEnergy a)

Cancellation and transport energy: E ||F_Q-id||₂² = E G / 12.

theorem FD1D.V5.Transport.stationary_expected_haarL2_eq_transportEnergy {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (μ : FiniteLaw (InventoryState (DyadicNode L) m)) (hμ : (Dynamics.kernel a ha hm).IsStationary μ) : (μ.expect fun (x : InventoryState (DyadicNode L) m) => haarL2 haarNodeLeft haarNodeWidth (stateHaarCoefficient a x)) = 1 / 12 * μ.expect (Dynamics.stateTransportEnergy a)

First-moment quantile cost

noncomputable def FD1D.V5.Transport.stateCellCost {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) : ℝ

Expected distance under the quantile policy of the state dyadic mass.

Equations

• FD1D.V5.Transport.stateCellCost a ha hm x = ((FD1D.V5.Transport.stateDyadicMass a x).quantilePolicy ⋯).expectedDistance

theorem FD1D.V5.Transport.stateCellCost_pointwise {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) : stateCellCost a ha hm x ≤ 1 / ↑(2 ^ L) + cdfTransportArea (haarCombination haarNodeLeft haarNodeWidth (stateHaarCoefficient a x))

theorem FD1D.V5.Transport.expected_stateCellCost_le {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (μ : FiniteLaw (InventoryState (DyadicNode L) m)) (hinv : ∀ (d : Fin L) (v : DyadicNode ↑d), FiniteKernel.LawInvariant μ (TreeSymmetry.inventorySwap ⋯ v)) : μ.expect (stateCellCost a ha hm) ≤ 1 / ↑(2 ^ L) + √(1 / 12 * μ.expect (Dynamics.stateTransportEnergy a))