Policy

The hierarchical deletion policy

This module assembles the local two-child formulas into labels on a complete dyadic tree. Counts come from a coherent AggregatedInventory; hazards are defined recursively from the root, and all other policy quantities are then derived from the counts and hazards.

noncomputable def FD1D.HierarchicalPolicy.childHazard (a h : ℝ) (x y : ℕ) (side : Fin 2) : ℝ

Select the appropriate extended child hazard.

Equations

• FD1D.HierarchicalPolicy.childHazard a h x y side = if side = 0 then FD1D.LocalHazard.hL a h x y else FD1D.LocalHazard.hR a h x y

def FD1D.HierarchicalPolicy.hazard {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) : DyadicNode d → ℝ

The recursively propagated extended hazard, rooted at 1 / m.

Equations

• One or more equations did not get rendered due to their size.
• FD1D.HierarchicalPolicy.hazard I a 0 x_2 = 1 / ↑m

def FD1D.HierarchicalPolicy.inventory {L m : ℕ} (I : AggregatedInventory L m) (d : ℕ) (v : DyadicNode d) : ℝ

Inventory counts, coerced to reals.

Equations

• FD1D.HierarchicalPolicy.inventory I d v = ↑(I.count d v)

noncomputable def FD1D.HierarchicalPolicy.splitLeft {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : ℝ

Conditional left-child deletion probability at an internal node.

Equations

• FD1D.HierarchicalPolicy.splitLeft I a d v = FD1D.LocalHazard.dL a (I.count (d + 1) (FD1D.leftChild v)) (I.count (d + 1) (FD1D.rightChild v))

noncomputable def FD1D.HierarchicalPolicy.splitRight {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : ℝ

Conditional right-child deletion probability at an internal node.

Equations

• FD1D.HierarchicalPolicy.splitRight I a d v = FD1D.LocalHazard.dR a (I.count (d + 1) (FD1D.leftChild v)) (I.count (d + 1) (FD1D.rightChild v))

noncomputable def FD1D.HierarchicalPolicy.deletionMass {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : ℝ

Deletion mass q_v = N_v h_v.

Equations

• FD1D.HierarchicalPolicy.deletionMass I a d v = FD1D.HierarchicalPolicy.inventory I d v * FD1D.HierarchicalPolicy.hazard I a d v

noncomputable def FD1D.HierarchicalPolicy.intervalMass (d : ℕ) (v : DyadicNode d) : ℝ

Interval mass p_v.

Equations

• FD1D.HierarchicalPolicy.intervalMass d v = FD1D.nodeMass d v

noncomputable def FD1D.HierarchicalPolicy.discrepancy {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : ℝ

Discrepancy t_v = (p_v - q_v) / a.

Equations

• FD1D.HierarchicalPolicy.discrepancy I a d v = (FD1D.HierarchicalPolicy.intervalMass d v - FD1D.HierarchicalPolicy.deletionMass I a d v) / a

noncomputable def FD1D.HierarchicalPolicy.regularizedMass {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : ℝ

Reciprocal regularized count Z_v = p_v / (N_v + a).

Equations

• FD1D.HierarchicalPolicy.regularizedMass I a d v = FD1D.HierarchicalPolicy.intervalMass d v / (FD1D.HierarchicalPolicy.inventory I d v + a)

noncomputable def FD1D.HierarchicalPolicy.bellmanY {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : ℝ

The normalized Bellman coordinate y_v = Z_v / h_v.

Equations

• FD1D.HierarchicalPolicy.bellmanY I a d v = FD1D.HierarchicalPolicy.regularizedMass I a d v / FD1D.HierarchicalPolicy.hazard I a d v

noncomputable def FD1D.HierarchicalPolicy.bellmanWeight (y : ℝ) : ℝ

The scalar weight in the Bellman function.

Equations

• FD1D.HierarchicalPolicy.bellmanWeight y = FD1D.d y

noncomputable def FD1D.HierarchicalPolicy.bellmanFunction (h t y : ℝ) : ℝ

The Bellman function from equation (6).

Equations

• FD1D.HierarchicalPolicy.bellmanFunction h t y = FD1D.B h t y

noncomputable def FD1D.HierarchicalPolicy.bellmanValue {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : ℝ

The Bellman value attached to a policy node.

Equations

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

@[simp]

theorem FD1D.HierarchicalPolicy.hazard_root {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) : hazard I a 0 dyadicRoot = 1 / ↑m

@[simp]

theorem FD1D.HierarchicalPolicy.hazard_leftChild {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : hazard I a (d + 1) (leftChild v) = LocalHazard.hL a (hazard I a d v) (I.count (d + 1) (leftChild v)) (I.count (d + 1) (rightChild v))

@[simp]

theorem FD1D.HierarchicalPolicy.hazard_rightChild {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : hazard I a (d + 1) (rightChild v) = LocalHazard.hR a (hazard I a d v) (I.count (d + 1) (leftChild v)) (I.count (d + 1) (rightChild v))

@[simp]

theorem FD1D.HierarchicalPolicy.intervalMass_root : intervalMass 0 dyadicRoot = 1

@[simp]

theorem FD1D.HierarchicalPolicy.intervalMass_leftChild (d : ℕ) (v : DyadicNode d) : intervalMass (d + 1) (leftChild v) = intervalMass d v / 2

@[simp]

theorem FD1D.HierarchicalPolicy.intervalMass_rightChild (d : ℕ) (v : DyadicNode d) : intervalMass (d + 1) (rightChild v) = intervalMass d v / 2

theorem FD1D.HierarchicalPolicy.inventory_children {L m : ℕ} (I : AggregatedInventory L m) (d : ℕ) (hdL : d < L) (v : DyadicNode d) : inventory I d v = inventory I (d + 1) (leftChild v) + inventory I (d + 1) (rightChild v)

theorem FD1D.HierarchicalPolicy.split_add {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (d : ℕ) (v : DyadicNode d) : splitLeft I a d v + splitRight I a d v = 1

theorem FD1D.HierarchicalPolicy.hazard_pos {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) (d : ℕ) : d ≤ L → ∀ (v : DyadicNode d), 0 < hazard I a d v

theorem FD1D.HierarchicalPolicy.deletionMass_eq_count_mul_hazard {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : deletionMass I a d v = ↑(I.count d v) * hazard I a d v

theorem FD1D.HierarchicalPolicy.deletionMass_leftChild {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (d : ℕ) (hdL : d < L) (v : DyadicNode d) : deletionMass I a (d + 1) (leftChild v) = deletionMass I a d v * splitLeft I a d v

theorem FD1D.HierarchicalPolicy.deletionMass_rightChild {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (d : ℕ) (hdL : d < L) (v : DyadicNode d) : deletionMass I a (d + 1) (rightChild v) = deletionMass I a d v * splitRight I a d v

theorem FD1D.HierarchicalPolicy.deletionMass_children {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (d : ℕ) (hdL : d < L) (v : DyadicNode d) : deletionMass I a d v = deletionMass I a (d + 1) (leftChild v) + deletionMass I a (d + 1) (rightChild v)

theorem FD1D.HierarchicalPolicy.deletionMass_root {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (hm : 0 < m) : deletionMass I a 0 dyadicRoot = 1

theorem FD1D.HierarchicalPolicy.deletionMass_nonneg {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) {d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : 0 ≤ deletionMass I a d v

theorem FD1D.HierarchicalPolicy.sum_deletionMass {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) {d : ℕ} (hdL : d ≤ L) : ∑ v : DyadicNode d, deletionMass I a d v = 1

At every complete level, the deletion masses form a probability vector.

theorem FD1D.HierarchicalPolicy.leaf_deletionMass_nonneg {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) (v : DyadicNode L) : 0 ≤ deletionMass I a L v

theorem FD1D.HierarchicalPolicy.sum_leaf_deletionMass {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) : ∑ v : DyadicNode L, deletionMass I a L v = 1

theorem FD1D.HierarchicalPolicy.leaf_deletionMass_eq_zero_of_count_eq_zero {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (v : DyadicNode L) (hv : I.count L v = 0) : deletionMass I a L v = 0

theorem FD1D.HierarchicalPolicy.discrepancy_eq {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : discrepancy I a d v = (nodeMass d v - deletionMass I a d v) / a

theorem FD1D.HierarchicalPolicy.regularizedMass_eq {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : regularizedMass I a d v = nodeMass d v / (inventory I d v + a)

theorem FD1D.HierarchicalPolicy.discrepancy_root {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (_ha : 0 < a) (hm : 0 < m) : discrepancy I a 0 dyadicRoot = 0

theorem FD1D.HierarchicalPolicy.discrepancy_eq_local {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (d : ℕ) (hdL : d < L) (v : DyadicNode d) : discrepancy I a d v = LocalHazard.t a (intervalMass d v) (hazard I a d v) (I.count (d + 1) (leftChild v)) (I.count (d + 1) (rightChild v))

theorem FD1D.HierarchicalPolicy.discrepancy_leftChild {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (d : ℕ) (hdL : d < L) (v : DyadicNode d) : discrepancy I a (d + 1) (leftChild v) = LocalHazard.tL a (intervalMass d v) (hazard I a d v) (I.count (d + 1) (leftChild v)) (I.count (d + 1) (rightChild v))

theorem FD1D.HierarchicalPolicy.discrepancy_rightChild {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (d : ℕ) (hdL : d < L) (v : DyadicNode d) : discrepancy I a (d + 1) (rightChild v) = LocalHazard.tR a (intervalMass d v) (hazard I a d v) (I.count (d + 1) (leftChild v)) (I.count (d + 1) (rightChild v))

theorem FD1D.HierarchicalPolicy.discrepancy_div_hazard_le_half {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) (d : ℕ) : d ≤ L → ∀ (v : DyadicNode d), discrepancy I a d v / hazard I a d v ≤ 1 / 2

The invariant t_v / h_v ≤ 1/2, propagated from the root.

theorem FD1D.HierarchicalPolicy.intervalMass_le_regularized_count_mul_hazard {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) {d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : intervalMass d v ≤ (inventory I d v + a) * hazard I a d v

Equation (5), now available at every policy node.

theorem FD1D.HierarchicalPolicy.bellmanY_nonneg {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) {d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : 0 ≤ bellmanY I a d v

theorem FD1D.HierarchicalPolicy.bellmanY_le_one {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) {d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : bellmanY I a d v ≤ 1

theorem FD1D.HierarchicalPolicy.discrepancy_div_hazard_le_bellmanY {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) {d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : discrepancy I a d v / hazard I a d v ≤ bellmanY I a d v

noncomputable def FD1D.HierarchicalPolicy.imbalance {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : ℝ

The signed imbalance at an internal node.

Equations

• FD1D.HierarchicalPolicy.imbalance I a d v = FD1D.HierarchicalPolicy.deletionMass I a (d + 1) (FD1D.leftChild v) - FD1D.HierarchicalPolicy.deletionMass I a (d + 1) (FD1D.rightChild v)

theorem FD1D.HierarchicalPolicy.imbalance_eq_local {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (d : ℕ) (hdL : d < L) (v : DyadicNode d) : imbalance I a d v = LocalHazard.b a (hazard I a d v) (I.count (d + 1) (leftChild v)) (I.count (d + 1) (rightChild v))

theorem FD1D.HierarchicalPolicy.local_hazard_inequality {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (d : ℕ) (hdL : d < L) (v : DyadicNode d) : imbalance I a d v ^ 2 ≤ 2 * a ^ 2 * (childAverage (fun (d : ℕ) (v : DyadicNode d) => hazard I a d v ^ 2) d v - hazard I a d v ^ 2)

The local inequality whose tree sum is the hazard-energy bound.

theorem FD1D.HierarchicalPolicy.hazard_energy_bound {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) : internalWeightedSum (fun (d : ℕ) (v : DyadicNode d) => imbalance I a d v ^ 2) L ≤ 2 * a ^ 2 * (hazardEnergy (hazard I a) L - 1 / ↑m ^ 2)

def FD1D.HierarchicalPolicy.LocalBellmanHypothesis {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) : Prop

The one isolated interface to the polynomial Bellman certificate. A module importing both this policy and FD1D.Bellman can prove this proposition from FD1D.local_bellman_inequality; no certificate algebra is duplicated here.

Equations

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

This is the only proof tied to FD1D.Bellman. It converts the concrete policy labels into the normalized coordinates of the polynomial certificate.

theorem FD1D.HierarchicalPolicy.localBellmanHypothesis {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) : LocalBellmanHypothesis I a

theorem FD1D.HierarchicalPolicy.bellmanValue_leaf_nonpos {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) (v : DyadicNode L) : bellmanValue I a L v ≤ 0

theorem FD1D.HierarchicalPolicy.bellmanValue_root_lower {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) : -(1 / (3 * ↑m ^ 2)) ≤ bellmanValue I a 0 dyadicRoot

theorem FD1D.HierarchicalPolicy.deterministic_bellman_bound {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) : bellmanDrift L a (inventory I) (deletionMass I a) ≥ a * (hazardEnergy (hazard I a) L / 100 - 103 / (300 * ↑m ^ 2))

Equation (9) specialized to the concrete hierarchical policy.