Count dynamics for the v5 policy

This module instantiates the generic delete-then-arrive inventory kernel with the v5 deletion masses and connects it to the harmonic potential with regularizer a / 2.

@[reducible, inline]

abbrev FD1D.V5.Dynamics.aggregatedInventory {L m : ℕ} (x : InventoryState (DyadicNode L) m) : AggregatedInventory L m

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

Equations

• FD1D.V5.Dynamics.aggregatedInventory x = FD1D.HierarchicalDynamics.aggregatedInventory x

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

theorem FD1D.V5.Dynamics.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.V5.Dynamics.deletionRule {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) : DeletionRule (DyadicNode L) m

The v5 leaf deletion probabilities.

Equations

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

@[simp]

theorem FD1D.V5.Dynamics.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 = TreePolicy.deletionMass (aggregatedInventory x) a L w

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

Delete according to the v5 rule and add an independent uniform leaf.

Equations

• FD1D.V5.Dynamics.kernel a ha hm = (FD1D.V5.Dynamics.deletionRule a ha hm).kernel

@[simp]

theorem FD1D.V5.Dynamics.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 TreePolicy.deletionMass (aggregatedInventory x) a L deleted * (1 / ↑(Fintype.card (DyadicNode L))) else 0

theorem FD1D.V5.Dynamics.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.V5.Dynamics.kernel_irreducible {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) : (kernel a ha hm).Irreducible

theorem FD1D.V5.Dynamics.kernel_hasPositiveLoops {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) : (kernel a ha hm).HasPositiveLoops

Node marginals and count updates

noncomputable def FD1D.V5.Dynamics.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.V5.Dynamics.deletionMarginal a ha hm x hdL v = ∑ w ∈ FD1D.leafBlock hdL v, (FD1D.V5.Dynamics.deletionRule a ha hm).prob x w

theorem FD1D.V5.Dynamics.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 = TreePolicy.deletionMass (aggregatedInventory x) a d v

theorem FD1D.V5.Dynamics.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) (HierarchicalDynamics.inBlock (leafBlock hdL v) deleted) (HierarchicalDynamics.inBlock (leafBlock hdL v) arrived)

theorem FD1D.V5.Dynamics.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.V5.Dynamics.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 / 2) ((aggregatedInventory y).count d v) - harmonicPotential (a / 2) ((aggregatedInventory x).count d v)) = expectedNodePotentialChange (a / 2) ((aggregatedInventory x).count d v) (nodeMass d v) (TreePolicy.deletionMass (aggregatedInventory x) a d v)

State observables and exact harmonic drift

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

Aggregated inventory counts viewed as labels on every dyadic level.

Equations

• FD1D.V5.Dynamics.countLabel x = (FD1D.V5.Dynamics.aggregatedInventory x).count

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

Deletion mass at every node of the aggregated inventory tree.

Equations

• FD1D.V5.Dynamics.deletionLabel a x = FD1D.V5.TreePolicy.deletionMass (FD1D.V5.Dynamics.aggregatedInventory x) a

noncomputable def FD1D.V5.Dynamics.rateLabel {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) (d : ℕ) : DyadicNode d → ℝ

Deletion rate at every node of the aggregated inventory tree.

Equations

• FD1D.V5.Dynamics.rateLabel a x = FD1D.V5.TreePolicy.rate (FD1D.V5.Dynamics.aggregatedInventory x) a

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

The manuscript potential Φ, whose harmonic shift is a/2.

Equations

• FD1D.V5.Dynamics.statePotential a x = FD1D.globalHarmonicPotential L (a / 2) (FD1D.V5.Dynamics.countLabel x)

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

The principal restoring term D.

Equations

• FD1D.V5.Dynamics.stateDrift a x = FD1D.potentialDrift L (a / 2) (FD1D.V5.Dynamics.countLabel x) (FD1D.V5.Dynamics.deletionLabel a x)

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

The exact curvature remainder R.

Equations

• FD1D.V5.Dynamics.stateRemainder a x = FD1D.potentialRemainder L (a / 2) (FD1D.V5.Dynamics.countLabel x) (FD1D.V5.Dynamics.deletionLabel a x)

noncomputable def FD1D.V5.Dynamics.stateRateEnergy {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) (d : ℕ) : ℝ

Hazard energy of the state rate labels at the selected dyadic level.

Equations

• FD1D.V5.Dynamics.stateRateEnergy a x d = FD1D.hazardEnergy (FD1D.V5.Dynamics.rateLabel a x) d

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

Transport energy of the aggregated inventory state.

Equations

• FD1D.V5.Dynamics.stateTransportEnergy a x = FD1D.V5.TreePolicy.transportEnergy (FD1D.V5.Dynamics.aggregatedInventory x) a

theorem FD1D.V5.Dynamics.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 / 2) (countLabel x) (deletionLabel a x)

theorem FD1D.V5.Dynamics.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

Pointwise energy and remainder bounds

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

theorem FD1D.V5.Dynamics.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.V5.Dynamics.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.V5.Dynamics.intervalMass_le_count_add_half_mul_rate {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 / 2) * rateLabel a x d v

theorem FD1D.V5.Dynamics.stateDrift_lower_bound {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) : stateDrift a x ≥ a / 1000 * stateRateEnergy a x L + stateTransportEnergy a x / (1000 * a) - 501 * a / (1000 * ↑m ^ 2)

theorem FD1D.V5.Dynamics.stateRateEnergy_step {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) {d : ℕ} (hdL : d < L) : stateRateEnergy a x d ≤ stateRateEnergy a x (d + 1)

theorem FD1D.V5.Dynamics.stateRateEnergy_mono_to_depth {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) {i j : ℕ} (hij : i ≤ j) (hjL : j ≤ L) : stateRateEnergy a x i ≤ stateRateEnergy a x j

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

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

theorem FD1D.V5.Dynamics.sum_stateRateEnergy_le_depth_mul {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) : ∑ d ∈ Finset.range L, stateRateEnergy a x (d + 1) ≤ ↑L * stateRateEnergy a x L

theorem FD1D.V5.Dynamics.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, stateRateEnergy a x (d + 1) ∧ ∑ d ∈ Finset.range L, stateRateEnergy a x (d + 1) ≤ ↑L * stateRateEnergy a x L

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

theorem FD1D.V5.Dynamics.statePotential_le_log_one_add_two_mul_div {L m : ℕ} (a : ℝ) (ha : 0 < a) (x : InventoryState (DyadicNode L) m) : statePotential a x ≤ Real.log (1 + 2 * ↑m / a)