Dynamics

Concrete hierarchical inventory dynamics

This module instantiates the finite inventory chain with the hierarchical deletion masses. It also connects the actual delete-then-arrive kernel to the harmonic-potential drift identity.

def FD1D.HierarchicalDynamics.leafInventory {L m : ℕ} (x : InventoryState (DyadicNode L) m) : LeafInventory L m

Regard a fixed-total count vector as a leaf inventory.

Equations

• FD1D.HierarchicalDynamics.leafInventory x = { count := ↑x, total_count := ⋯ }

def FD1D.HierarchicalDynamics.aggregatedInventory {L m : ℕ} (x : InventoryState (DyadicNode L) m) : AggregatedInventory L m

Canonical coherent counts associated with a count-chain state.

Equations

• FD1D.HierarchicalDynamics.aggregatedInventory x = (FD1D.HierarchicalDynamics.leafInventory x).aggregate

@[simp]

theorem FD1D.HierarchicalDynamics.leafInventory_count {L m : ℕ} (x : InventoryState (DyadicNode L) m) (w : DyadicNode L) : (leafInventory x).count w = ↑x w

@[simp]

theorem FD1D.HierarchicalDynamics.aggregatedInventory_leaf_count {L m : ℕ} (x : InventoryState (DyadicNode L) m) (w : DyadicNode L) : (aggregatedInventory x).count L w = ↑x w

theorem FD1D.HierarchicalDynamics.aggregatedInventory_count {L m : ℕ} (x : InventoryState (DyadicNode L) m) {d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : (aggregatedInventory x).count d v = ∑ w ∈ leafBlock hdL v, ↑x w

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

Leaf deletion probabilities prescribed by the hierarchical policy.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FD1D.HierarchicalDynamics.deletionRule_prob {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) (w : DyadicNode L) : (deletionRule a ha hm).prob x w = HierarchicalPolicy.deletionMass (aggregatedInventory x) a L w

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

Delete according to the hierarchical rule, then add a uniform leaf.

Equations

• FD1D.HierarchicalDynamics.kernel a ha hm = (FD1D.HierarchicalDynamics.deletionRule a ha hm).kernel

@[simp]

theorem FD1D.HierarchicalDynamics.kernel_apply {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x y : InventoryState (DyadicNode L) m) : (kernel a ha hm).trans x y = ∑ deleted : DyadicNode L, ∑ arrived : DyadicNode L, if x.move deleted arrived = y then HierarchicalPolicy.deletionMass (aggregatedInventory x) a L deleted * (1 / ↑(Fintype.card (DyadicNode L))) else 0

Constructive irreducibility of fixed-total inventory dynamics

def FD1D.HierarchicalDynamics.inventoryDeficit {ι : Type u_1} [Fintype ι] {m : ℕ} (x y : InventoryState ι m) : ℕ

Total target deficit of one fixed-total inventory relative to another.

Equations

• FD1D.HierarchicalDynamics.inventoryDeficit x y = ∑ i : ι, (↑y i - ↑x i)

theorem FD1D.HierarchicalDynamics.inventoryDeficit_eq_zero_iff {ι : Type u_1} [Fintype ι] {m : ℕ} (x y : InventoryState ι m) : inventoryDeficit x y = 0 ↔ x = y

theorem FD1D.HierarchicalDynamics.inventoryDeficit_move_lt {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m : ℕ} (x y : InventoryState ι m) {deleted arrived : ι} (harrived : ↑x arrived < ↑y arrived) (hdeleted : ↑y deleted < ↑x deleted) : inventoryDeficit (x.move deleted arrived) y < inventoryDeficit x y

theorem FD1D.HierarchicalDynamics.deletionRule_kernel_irreducible {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] {m : ℕ} (R : DeletionRule ι m) : R.kernel.Irreducible

Every fixed-total inventory is reachable from every other one under any deletion rule that is strictly positive on occupied coordinates.

theorem FD1D.HierarchicalDynamics.kernel_move_pos {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) {deleted arrived : DyadicNode L} (hdeleted : 0 < ↑x deleted) : 0 < (kernel a ha hm).trans x (x.move deleted arrived)

theorem FD1D.HierarchicalDynamics.kernel_irreducible {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) : (kernel a ha hm).Irreducible

The hierarchical fixed-total count chain is irreducible.

theorem FD1D.HierarchicalDynamics.coherent_eq_sum_leafBlock {L : ℕ} {A : Type u_1} [AddCommMonoid A] (q : CoherentTreeLabel L A) {d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : q.value d v = ∑ w ∈ leafBlock hdL v, q.value L w

A coherent tree label equals the sum of its leaf labels over the corresponding descendant block.

noncomputable def FD1D.HierarchicalDynamics.deletionMarginal {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) {d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : ℝ

Probability that the deleted leaf lies below a given node.

Equations

• FD1D.HierarchicalDynamics.deletionMarginal a ha hm x hdL v = ∑ w ∈ FD1D.leafBlock hdL v, (FD1D.HierarchicalDynamics.deletionRule a ha hm).prob x w

theorem FD1D.HierarchicalDynamics.deletionMarginal_eq {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) {d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : deletionMarginal a ha hm x hdL v = HierarchicalPolicy.deletionMass (aggregatedInventory x) a d v

noncomputable def FD1D.HierarchicalDynamics.arrivalMarginal {L d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : ℝ

Probability that a uniform arriving leaf lies below a given node.

Equations

• FD1D.HierarchicalDynamics.arrivalMarginal hdL v = ∑ _w ∈ FD1D.leafBlock hdL v, 1 / ↑(Fintype.card (FD1D.DyadicNode L))

theorem FD1D.HierarchicalDynamics.arrivalMarginal_eq_nodeMass {L d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : arrivalMarginal hdL v = nodeMass d v

Counts under an actual leaf move

def FD1D.HierarchicalDynamics.inBlock {ι : Type u_1} [DecidableEq ι] (S : Finset ι) (i : ι) : Bool

Boolean membership in a finite block.

Equations

• FD1D.HierarchicalDynamics.inBlock S i = decide (i ∈ S)

@[simp]

theorem FD1D.HierarchicalDynamics.inBlock_eq_true {ι : Type u_1} [DecidableEq ι] {S : Finset ι} {i : ι} : inBlock S i = true ↔ i ∈ S

@[simp]

theorem FD1D.HierarchicalDynamics.inBlock_eq_false {ι : Type u_1} [DecidableEq ι] {S : Finset ι} {i : ι} : inBlock S i = false ↔ i ∉ S

theorem FD1D.HierarchicalDynamics.sum_move_eq_updateCount {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m : ℕ} (x : InventoryState ι m) (S : Finset ι) {deleted arrived : ι} (hdeleted : 0 < ↑x deleted) : ∑ i ∈ S, ↑(x.move deleted arrived) i = updateCount (∑ i ∈ S, ↑x i) (inBlock S deleted) (inBlock S arrived)

The count in any finite block after an occupied deletion and an arrival is the four-case updateCount used by the potential calculation.

theorem FD1D.HierarchicalDynamics.aggregatedInventory_move_count {L m : ℕ} (x : InventoryState (DyadicNode L) m) {deleted arrived : DyadicNode L} (hdeleted : 0 < ↑x deleted) {d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : (aggregatedInventory (x.move deleted arrived)).count d v = updateCount ((aggregatedInventory x).count d v) (inBlock (leafBlock hdL v) deleted) (inBlock (leafBlock hdL v) arrived)

Concrete aggregated count update at every node.

Finite weighted membership partitions

theorem FD1D.HierarchicalDynamics.double_inBlock_partition {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (deleteWeight : ι → ℝ) (arrivalWeight : κ → ℝ) (deleteSet : Finset ι) (arrivalSet : Finset κ) (q p : ℝ) (hdeleteSum : ∑ i : ι, deleteWeight i = 1) (harrivalSum : ∑ j : κ, arrivalWeight j = 1) (hq : ∑ i ∈ deleteSet, deleteWeight i = q) (hp : ∑ j ∈ arrivalSet, arrivalWeight j = p) (f : Bool → Bool → ℝ) : ∑ i : ι, ∑ j : κ, deleteWeight i * arrivalWeight j * f (inBlock deleteSet i) (inBlock arrivalSet j) = ∑ deleted : Bool, ∑ arrived : Bool, bernoulliMass q deleted * bernoulliMass p arrived * f deleted arrived

Expectations under the concrete kernel

theorem FD1D.HierarchicalDynamics.kernel_expectation_eq_delete_arrive {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) (f : InventoryState (DyadicNode L) m → ℝ) : ∑ y : InventoryState (DyadicNode L) m, (kernel a ha hm).trans x y * f y = ∑ deleted : DyadicNode L, ∑ arrived : DyadicNode L, (deletionRule a ha hm).prob x deleted * (1 / ↑(Fintype.card (DyadicNode L))) * f (x.move deleted arrived)

theorem FD1D.HierarchicalDynamics.kernel_expected_nodePotentialChange {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) {d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : ∑ y : InventoryState (DyadicNode L) m, (kernel a ha hm).trans x y * (harmonicPotential a ((aggregatedInventory y).count d v) - harmonicPotential a ((aggregatedInventory x).count d v)) = expectedNodePotentialChange a ((aggregatedInventory x).count d v) (nodeMass d v) (HierarchicalPolicy.deletionMass (aggregatedInventory x) a d v)

Global state observables and exact kernel drift

def FD1D.HierarchicalDynamics.countLabel {L m : ℕ} (x : InventoryState (DyadicNode L) m) (d : ℕ) : DyadicNode d → ℕ

Coherent natural count label of a count-chain state.

Equations

• FD1D.HierarchicalDynamics.countLabel x = (FD1D.HierarchicalDynamics.aggregatedInventory x).count

noncomputable def FD1D.HierarchicalDynamics.deletionLabel {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) (d : ℕ) : DyadicNode d → ℝ

Hierarchical deletion mass at every tree node.

Equations

• FD1D.HierarchicalDynamics.deletionLabel a x = FD1D.HierarchicalPolicy.deletionMass (FD1D.HierarchicalDynamics.aggregatedInventory x) a

noncomputable def FD1D.HierarchicalDynamics.hazardLabel {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) (d : ℕ) : DyadicNode d → ℝ

Extended policy hazard at every tree node.

Equations

• FD1D.HierarchicalDynamics.hazardLabel a x = FD1D.HierarchicalPolicy.hazard (FD1D.HierarchicalDynamics.aggregatedInventory x) a

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

Global harmonic potential of a count-chain state.

Equations

• FD1D.HierarchicalDynamics.statePotential a x = FD1D.globalHarmonicPotential L a (FD1D.HierarchicalDynamics.countLabel x)

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

Bellman drift quantity D of a count-chain state.

Equations

• FD1D.HierarchicalDynamics.stateDrift a x = FD1D.potentialDrift L a (FD1D.HierarchicalDynamics.countLabel x) (FD1D.HierarchicalDynamics.deletionLabel a x)

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

Harmonic drift remainder R of a count-chain state.

Equations

• FD1D.HierarchicalDynamics.stateRemainder a x = FD1D.potentialRemainder L a (FD1D.HierarchicalDynamics.countLabel x) (FD1D.HierarchicalDynamics.deletionLabel a x)

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

Hazard energy at one level in a count-chain state.

Equations

• FD1D.HierarchicalDynamics.stateHazardEnergy a x d = FD1D.hazardEnergy (FD1D.HierarchicalDynamics.hazardLabel a x) d

theorem FD1D.HierarchicalDynamics.kernel_expected_globalPotentialChange {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) : ∑ y : InventoryState (DyadicNode L) m, (kernel a ha hm).trans x y * (statePotential a y - statePotential a x) = expectedGlobalPotentialChange L a (countLabel x) (deletionLabel a x)

theorem FD1D.HierarchicalDynamics.kernel_drift_eq_stateDrift_sub_stateRemainder {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) : ∑ y : InventoryState (DyadicNode L) m, (kernel a ha hm).trans x y * (statePotential a y - statePotential a x) = stateDrift a x - stateRemainder a x

The conditional drift of the actual count-chain kernel is exactly the policy's D - R.

theorem FD1D.HierarchicalDynamics.kernel_drift_eq_potentialDrift_sub_potentialRemainder {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) : ∑ y : InventoryState (DyadicNode L) m, (kernel a ha hm).trans x y * (statePotential a y - statePotential a x) = potentialDrift L a (countLabel x) (deletionLabel a x) - potentialRemainder L a (countLabel x) (deletionLabel a x)

Expanded form of the concrete one-step identity, exposing the generic potentialDrift and potentialRemainder definitions directly.

Per-state bounds used by stationarity and finite-time telescoping

theorem FD1D.HierarchicalDynamics.countLabel_le_total {L m : ℕ} (x : InventoryState (DyadicNode L) m) {d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : countLabel x d v ≤ m

theorem FD1D.HierarchicalDynamics.countLabel_le_total_all {L m : ℕ} (x : InventoryState (DyadicNode L) m) (d : ℕ) (v : DyadicNode d) : countLabel x d v ≤ m

theorem FD1D.HierarchicalDynamics.deletionLabel_nonneg {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) {d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : 0 ≤ deletionLabel a x d v

theorem FD1D.HierarchicalDynamics.deletionLabel_le_one {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) {d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : deletionLabel a x d v ≤ 1

theorem FD1D.HierarchicalDynamics.deletionLabel_eq_zero_of_count_eq_zero {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) {d : ℕ} (v : DyadicNode d) (hzero : countLabel x d v = 0) : deletionLabel a x d v = 0

theorem FD1D.HierarchicalDynamics.intervalMass_le_count_add_a_mul_hazard {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) {d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : nodeMass d v ≤ (↑(countLabel x d v) + a) * hazardLabel a x d v

theorem FD1D.HierarchicalDynamics.stateDrift_lower_bound {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) : stateDrift a x ≥ a * (stateHazardEnergy a x L / 100 - 103 / (300 * ↑m ^ 2))

theorem FD1D.HierarchicalDynamics.stateHazardEnergy_step {L m : ℕ} (a : ℝ) (ha : 0 < a) (x : InventoryState (DyadicNode L) m) {d : ℕ} (hdL : d < L) : stateHazardEnergy a x d ≤ stateHazardEnergy a x (d + 1)

theorem FD1D.HierarchicalDynamics.stateHazardEnergy_mono_to_depth {L m : ℕ} (a : ℝ) (ha : 0 < a) (x : InventoryState (DyadicNode L) m) {i j : ℕ} (hij : i ≤ j) (hjL : j ≤ L) : stateHazardEnergy a x i ≤ stateHazardEnergy a x j

theorem FD1D.HierarchicalDynamics.stateRemainder_nonneg {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) : 0 ≤ stateRemainder a x

theorem FD1D.HierarchicalDynamics.stateRemainder_le_sum_hazardEnergy {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) : stateRemainder a x ≤ ∑ d ∈ Finset.range L, stateHazardEnergy a x (d + 1)

theorem FD1D.HierarchicalDynamics.sum_stateHazardEnergy_le_depth_mul {L m : ℕ} (a : ℝ) (ha : 0 < a) (x : InventoryState (DyadicNode L) m) : ∑ d ∈ Finset.range L, stateHazardEnergy a x (d + 1) ≤ ↑L * stateHazardEnergy a x L

theorem FD1D.HierarchicalDynamics.stateRemainder_bounds {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) : 0 ≤ stateRemainder a x ∧ stateRemainder a x ≤ ∑ d ∈ Finset.range L, stateHazardEnergy a x (d + 1) ∧ ∑ d ∈ Finset.range L, stateHazardEnergy a x (d + 1) ≤ ↑L * stateHazardEnergy a x L

theorem FD1D.HierarchicalDynamics.statePotential_nonneg {L m : ℕ} (a : ℝ) (ha : 0 < a) (x : InventoryState (DyadicNode L) m) : 0 ≤ statePotential a x

theorem FD1D.HierarchicalDynamics.statePotential_le_log_one_add {L m : ℕ} (a : ℝ) (ha : 0 < a) (x : InventoryState (DyadicNode L) m) : statePotential a x ≤ Real.log (1 + ↑m / a)

theorem FD1D.HierarchicalDynamics.statePotential_bounds {L m : ℕ} (a : ℝ) (ha : 0 < a) (x : InventoryState (DyadicNode L) m) : 0 ≤ statePotential a x ∧ statePotential a x ≤ Real.log (1 + ↑m / a)