Bounds

theorem FD1D.HierarchicalDynamics.stateHazardEnergy_nonneg {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) (d : ℕ) : 0 ≤ stateHazardEnergy a x d

theorem FD1D.HierarchicalDynamics.stateHazardEnergy_root {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) : stateHazardEnergy a x 0 = 1 / ↑m ^ 2

theorem FD1D.HierarchicalDynamics.stateHazardEnergy_root_le {L m : ℕ} (a : ℝ) (ha : 0 < a) (x : InventoryState (DyadicNode L) m) : 1 / ↑m ^ 2 ≤ stateHazardEnergy a x L

def FD1D.HierarchicalDynamics.concentratedInventory (L m : ℕ) : InventoryState (DyadicNode L) m

A canonical witness that the fixed-total count state space is nonempty.

Equations

• FD1D.HierarchicalDynamics.concentratedInventory L m = ⟨fun (i : FD1D.DyadicNode L) => if i = 0 then m else 0, ⋯⟩

instance FD1D.HierarchicalDynamics.inventoryStateNonempty (L m : ℕ) : Nonempty (InventoryState (DyadicNode L) m)

theorem FD1D.HierarchicalDynamics.stationary_expected_hazard_bound {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (haL : 200 * ↑L ≤ a) (μ : FiniteLaw (InventoryState (DyadicNode L) m)) (hμ : (kernel a ha hm).IsStationary μ) : (μ.expect fun (x : InventoryState (DyadicNode L) m) => stateHazardEnergy a x L) ≤ 206 / (3 * ↑m ^ 2)

Equation (11) for an actual stationary law of the concrete hierarchical count kernel.

theorem FD1D.HierarchicalDynamics.existsUnique_stationaryLaw {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) : ∃! μ : FiniteLaw (InventoryState (DyadicNode L) m), (kernel a ha hm).IsStationary μ

The concrete count chain has a unique stationary law.

theorem FD1D.HierarchicalDynamics.finite_average_expected_hazard_bound {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (haL : 200 * ↑L ≤ a) (hlogA : 200 * Real.log (1 + ↑m / a) ≤ a) (μ₀ : FiniteLaw (InventoryState (DyadicNode L) m)) (T : ℕ) (hT : 0 < T) : (∑ t ∈ Finset.range T, ((kernel a ha hm).iterate t μ₀).expect fun (x : InventoryState (DyadicNode L) m) => stateHazardEnergy a x L) / ↑T ≤ 206 / (3 * ↑m ^ 2) + 1 / ↑T

Equation (12) for the actual kernel iterates, from an arbitrary initial count law. No invariance assumption is needed for this potential estimate.