Concrete Transport

Concrete transport for the hierarchical count chain

This module identifies the recursive dyadic mass used by the analytic transport argument with the deletion probabilities of the concrete hierarchical policy.

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

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

Equations

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

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

The complete depth-L deletion-mass tree of a count state.

Equations

• FD1D.HierarchicalDynamics.stateDyadicMass a x = FD1D.HierarchicalDynamics.stateDyadicMassAt a x 0 L FD1D.dyadicRoot

@[simp]

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

@[simp]

theorem FD1D.HierarchicalDynamics.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.HierarchicalDynamics.stateDyadicMassAt_total {L m : ℕ} (a : ℝ) (ha : 0 < a) (x : InventoryState (DyadicNode L) m) {d k : ℕ} (hdk : d + k ≤ L) (v : DyadicNode d) : (stateDyadicMassAt a x d k v).total = deletionLabel a x d v

Every concrete recursive subtree has its policy deletion mass as total.

theorem FD1D.HierarchicalDynamics.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.HierarchicalDynamics.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 ((deletionRule a ha hm).prob x w)

At remaining depth zero, the recursive leaf is the concrete deletion probability of that leaf.

@[simp]

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

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

theorem FD1D.HierarchicalDynamics.stateDyadicMassAt_rootCoefficient {L m : ℕ} (a : ℝ) (ha : 0 < 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 = HierarchicalPolicy.imbalance (aggregatedInventory x) a d v

The root coefficient of every recursive subtree is the concrete policy imbalance at the same node.

theorem FD1D.HierarchicalDynamics.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 = (deletionRule a ha hm).prob x w

Every indexed leaf mass of the concrete dyadic tree is exactly the probability assigned by the concrete deletion rule.

theorem FD1D.HierarchicalDynamics.stateDyadicMass_nodeCoefficient {L m : ℕ} (a : ℝ) (ha : 0 < a) (x : InventoryState (DyadicNode L) m) (i : CompleteHaarNode L) : (stateDyadicMass a x).nodeCoefficient i = HierarchicalPolicy.imbalance (aggregatedInventory x) a (↑i.fst) i.snd

Every canonical Haar coefficient of the concrete mass tree is exactly the policy imbalance at the same depth and node.

theorem FD1D.HierarchicalDynamics.stateDyadicMass_haarSeries_eq {L m : ℕ} (a : ℝ) (ha : 0 < a) (x : InventoryState (DyadicNode L) m) {z : ℝ} (hz : z ∈ Set.Icc 0 1) : (stateDyadicMass a x).haarSeries z = haarCombination haarNodeLeft haarNodeWidth (fun (i : CompleteHaarNode L) => HierarchicalPolicy.imbalance (aggregatedInventory x) a (↑i.fst) i.snd) z

The recursive Haar series of the concrete policy is the canonical complete-tree tent combination with the policy imbalances as coefficients.

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

The concrete coefficient family in the canonical complete-tree index.

Equations

• FD1D.HierarchicalDynamics.stateHaarCoefficient a x i = FD1D.HierarchicalPolicy.imbalance (FD1D.HierarchicalDynamics.aggregatedInventory x) a (↑i.fst) i.snd

noncomputable def FD1D.HierarchicalDynamics.stateQuantilePolicy {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) : MonotoneQuantilePolicy (stateDyadicMass a x).piecewiseCDF

The monotone quantile policy associated with a concrete count state.

Equations

• FD1D.HierarchicalDynamics.stateQuantilePolicy a ha hm x = (FD1D.HierarchicalDynamics.stateDyadicMass a x).quantilePolicy ⋯

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

Cost of the continuous quantile map before rounding to a cell endpoint.

Equations

• FD1D.HierarchicalDynamics.stateQuantileCost a ha hm x = (FD1D.HierarchicalDynamics.stateQuantilePolicy a ha hm x).quantileDistance

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

Cost of the demand-driven selected cell endpoint.

Equations

• FD1D.HierarchicalDynamics.stateCellCost a ha hm x = (FD1D.HierarchicalDynamics.stateQuantilePolicy a ha hm x).expectedDistance

theorem FD1D.HierarchicalDynamics.stateQuantileCost_eq_haarArea {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) : stateQuantileCost a ha hm x = cdfTransportArea (haarCombination haarNodeLeft haarNodeWidth (stateHaarCoefficient a x))

The continuous quantile cost is the CDF area of the canonical concrete Haar combination.

theorem FD1D.HierarchicalDynamics.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))

Pointwise transport-cost hypothesis used by equation (3).

theorem FD1D.HierarchicalDynamics.stateActualCost_pointwise {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (C : SupplyConfiguration L m) (fallback : Fin m) : C.expectedActualDistance (stateDyadicMass a C.countState) fallback ≤ 1 / ↑(2 ^ L) + cdfTransportArea (haarCombination haarNodeLeft haarNodeWidth (stateHaarCoefficient a C.countState))

Spatial's actual occupied-point selector satisfies the same one-cell pointwise hypothesis for the concrete hierarchical deletion rule.

theorem FD1D.HierarchicalDynamics.expected_equation_two {L m : ℕ} {Ω : Type u_1} [Fintype Ω] (μ : FiniteLaw Ω) (state : Ω → InventoryState (DyadicNode L) m) (a : ℝ) (ha : 0 < a) (hm : 0 < m) : (∑ i : CompleteHaarNode L, haarNodeWidth i * μ.expect fun (ω : Ω) => stateHaarCoefficient a (state ω) i ^ 2) ≤ 2 * a ^ 2 * ((μ.expect fun (ω : Ω) => stateHazardEnergy a (state ω) L) - 1 / ↑m ^ 2)

Expected equation (2), derived pointwise from the concrete policy's hazard-energy telescope. The sample type may contain data besides the count state, which is useful for time averages and spatial configurations.

theorem FD1D.HierarchicalDynamics.expected_hazard_gap_nonneg {L m : ℕ} {Ω : Type u_1} [Fintype Ω] (μ : FiniteLaw Ω) (state : Ω → InventoryState (DyadicNode L) m) (a : ℝ) (ha : 0 < a) : 0 ≤ (μ.expect fun (ω : Ω) => stateHazardEnergy a (state ω) L) - 1 / ↑m ^ 2

theorem FD1D.HierarchicalDynamics.concrete_transport_equation_three {L m : ℕ} {Ω : Type u_1} [Fintype Ω] (μ : FiniteLaw Ω) (state : Ω → InventoryState (DyadicNode L) m) (cost : Ω → ℝ) (a : ℝ) (ha : 0 < a) (hm : 0 < m) (hcost : ∀ (ω : Ω), cost ω ≤ 1 / ↑(2 ^ L) + cdfTransportArea (haarCombination haarNodeLeft haarNodeWidth (stateHaarCoefficient a (state ω)))) (hsym : ∀ (i j : CompleteHaarNode L), i ≠ j → IntervalsSeparated haarNodeLeft haarNodeWidth i j ∨ μ.OddSymmetry fun (ω : Ω) => stateHaarCoefficient a (state ω) i * stateHaarCoefficient a (state ω) j) : μ.expect cost ≤ 1 / ↑(2 ^ L) + a / √6 * √((μ.expect fun (ω : Ω) => stateHazardEnergy a (state ω) L) - 1 / ↑m ^ 2)

Concrete equation (3) for an arbitrary finite sample space and state projection. Callers supply only the pointwise cost comparison and the law-level separated-or-odd hsym condition; equation (2) is discharged internally by expected_equation_two.

theorem FD1D.HierarchicalDynamics.expected_stateCellCost_equation_three {L m : ℕ} {Ω : Type u_1} [Fintype Ω] (μ : FiniteLaw Ω) (state : Ω → InventoryState (DyadicNode L) m) (a : ℝ) (ha : 0 < a) (hm : 0 < m) (hsym : ∀ (i j : CompleteHaarNode L), i ≠ j → IntervalsSeparated haarNodeLeft haarNodeWidth i j ∨ μ.OddSymmetry fun (ω : Ω) => stateHaarCoefficient a (state ω) i * stateHaarCoefficient a (state ω) j) : (μ.expect fun (ω : Ω) => stateCellCost a ha hm (state ω)) ≤ 1 / ↑(2 ^ L) + a / √6 * √((μ.expect fun (ω : Ω) => stateHazardEnergy a (state ω) L) - 1 / ↑m ^ 2)

Equation (3) specialized to the concrete selected-cell endpoint cost.