The v5 hierarchical tree policy

This module propagates the local three-cap rule through a complete dyadic tree. It proves the invariant domain, rate-energy monotonicity, the lifted local Bellman inequality, and the deterministic aggregate estimate.

noncomputable def FD1D.V5.TreePolicy.childRate (a p h : ℝ) (x y : ℕ) (side : Fin 2) : ℝ

Select the left or right rate of the local rule for one dyadic child.

Equations

• FD1D.V5.TreePolicy.childRate a p h x y side = if side = 0 then FD1D.V5.LocalPolicy.rateLeft a p h x y else FD1D.V5.LocalPolicy.rateRight a p h x y

def FD1D.V5.TreePolicy.rate {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) : DyadicNode d → ℝ

Recursively propagated analytic rate, rooted at 1/m.

Equations

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

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

Inventory count coerced to ℝ.

Equations

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

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

Node interval mass.

Equations

• FD1D.V5.TreePolicy.intervalMass d v = FD1D.nodeMass d v

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

Deletion mass q_v = N_v h_v.

Equations

• FD1D.V5.TreePolicy.deletionMass I a d v = FD1D.V5.TreePolicy.inventory I d v * FD1D.V5.TreePolicy.rate I a d v

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

Discrepancy t_v = (p_v-q_v)/a.

Equations

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

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

Regularized mass Z_v = p_v/(N_v+a/2).

Equations

• FD1D.V5.TreePolicy.regularizedMass I a d v = FD1D.V5.TreePolicy.intervalMass d v / (FD1D.V5.TreePolicy.inventory I d v + a / 2)

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

Quadratic Bellman correction at a node.

Equations

• FD1D.V5.TreePolicy.bellmanValue I a d v = FD1D.V5.LocalPolicy.bellman (FD1D.V5.TreePolicy.rate I a d v) (FD1D.V5.TreePolicy.discrepancy I a d v) (FD1D.V5.TreePolicy.regularizedMass I a d v)

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

Fixed-spatial-label child deletion imbalance.

Equations

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

@[simp]

theorem FD1D.V5.TreePolicy.rate_root {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) : rate I a 0 dyadicRoot = 1 / ↑m

@[simp]

theorem FD1D.V5.TreePolicy.rate_leftChild {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : rate I a (d + 1) (leftChild v) = LocalPolicy.rateLeft a (intervalMass d v) (rate I a d v) (I.count (d + 1) (leftChild v)) (I.count (d + 1) (rightChild v))

@[simp]

theorem FD1D.V5.TreePolicy.rate_rightChild {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : rate I a (d + 1) (rightChild v) = LocalPolicy.rateRight a (intervalMass d v) (rate I a d v) (I.count (d + 1) (leftChild v)) (I.count (d + 1) (rightChild v))

@[simp]

theorem FD1D.V5.TreePolicy.intervalMass_root : intervalMass 0 dyadicRoot = 1

@[simp]

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

@[simp]

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

theorem FD1D.V5.TreePolicy.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.V5.TreePolicy.deletionMass_leftChild {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : deletionMass I a (d + 1) (leftChild v) = LocalPolicy.massLeft a (intervalMass d v) (rate I a d v) (I.count (d + 1) (leftChild v)) (I.count (d + 1) (rightChild v))

theorem FD1D.V5.TreePolicy.deletionMass_rightChild {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : deletionMass I a (d + 1) (rightChild v) = LocalPolicy.massRight a (intervalMass d v) (rate I a d v) (I.count (d + 1) (leftChild v)) (I.count (d + 1) (rightChild v))

theorem FD1D.V5.TreePolicy.deletionMass_children {L m : ℕ} (I : AggregatedInventory L m) (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.V5.TreePolicy.deletionMass_root {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (hm : 0 < m) : deletionMass I a 0 dyadicRoot = 1

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

theorem FD1D.V5.TreePolicy.discrepancy_eq_local {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (hdL : d < L) (v : DyadicNode d) : discrepancy I a d v = LocalPolicy.discrepancy a (intervalMass d v) (rate I a d v) (I.count (d + 1) (leftChild v)) (I.count (d + 1) (rightChild v))

theorem FD1D.V5.TreePolicy.regularizedMass_eq_local {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (hdL : d < L) (v : DyadicNode d) : regularizedMass I a d v = LocalPolicy.regularizedMass a (intervalMass d v) (I.count (d + 1) (leftChild v)) (I.count (d + 1) (rightChild v))

theorem FD1D.V5.TreePolicy.discrepancy_leftChild {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : discrepancy I a (d + 1) (leftChild v) = LocalPolicy.discrepancyLeft a (intervalMass d v) (rate I a d v) (I.count (d + 1) (leftChild v)) (I.count (d + 1) (rightChild v))

theorem FD1D.V5.TreePolicy.discrepancy_rightChild {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : discrepancy I a (d + 1) (rightChild v) = LocalPolicy.discrepancyRight a (intervalMass d v) (rate I a d v) (I.count (d + 1) (leftChild v)) (I.count (d + 1) (rightChild v))

theorem FD1D.V5.TreePolicy.regularizedMass_leftChild {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : regularizedMass I a (d + 1) (leftChild v) = LocalPolicy.regularizedMassLeft a (intervalMass d v) (I.count (d + 1) (leftChild v))

theorem FD1D.V5.TreePolicy.regularizedMass_rightChild {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : regularizedMass I a (d + 1) (rightChild v) = LocalPolicy.regularizedMassRight a (intervalMass d v) (I.count (d + 1) (rightChild v))

Invariant domain and feasibility

theorem FD1D.V5.TreePolicy.node_invariants {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) (d : ℕ) : d ≤ L → ∀ (v : DyadicNode d), 0 < rate I a d v ∧ discrepancy I a d v ≤ rate I a d v / 2 ∧ regularizedMass I a d v ≤ rate I a d v

theorem FD1D.V5.TreePolicy.rate_pos {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) {d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : 0 < rate I a d v

theorem FD1D.V5.TreePolicy.discrepancy_le_half {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 ≤ rate I a d v / 2

theorem FD1D.V5.TreePolicy.regularizedMass_le_rate {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) {d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : regularizedMass I a d v ≤ rate I a d v

theorem FD1D.V5.TreePolicy.intervalMass_le_count_add_half_mul_rate {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 / 2) * rate I a d v

theorem FD1D.V5.TreePolicy.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.V5.TreePolicy.sum_deletionMass {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (hm : 0 < m) {d : ℕ} (hdL : d ≤ L) : ∑ v : DyadicNode d, deletionMass I a d v = 1

theorem FD1D.V5.TreePolicy.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.V5.TreePolicy.leaf_deletionMass_pos_of_count_pos {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) (v : DyadicNode L) (hv : 0 < I.count L v) : 0 < deletionMass I a L v

theorem FD1D.V5.TreePolicy.regularizedMass_pos {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (d : ℕ) (v : DyadicNode d) : 0 < regularizedMass I a d v

theorem FD1D.V5.TreePolicy.bellmanValue_nonpos {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) {d : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : bellmanValue I a d v ≤ 0

Rate-energy monotonicity

theorem FD1D.V5.TreePolicy.local_rate_average_ge {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) (d : ℕ) (hdL : d < L) (v : DyadicNode d) : rate I a d v ≤ childAverage (rate I a) d v

theorem FD1D.V5.TreePolicy.local_rate_energy_nonneg {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) (d : ℕ) (hdL : d < L) (v : DyadicNode d) : 0 ≤ childAverage (fun (d : ℕ) (v : DyadicNode d) => rate I a d v ^ 2) d v - rate I a d v ^ 2

theorem FD1D.V5.TreePolicy.rateEnergy_mono {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) {d : ℕ} (hdL : d < L) : hazardEnergy (rate I a) d ≤ hazardEnergy (rate I a) (d + 1)

theorem FD1D.V5.TreePolicy.rateEnergy_root {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (hm : 0 < m) : hazardEnergy (rate I a) 0 = 1 / ↑m ^ 2

Lifted Bellman inequality

theorem FD1D.V5.TreePolicy.imbalance_eq_local {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) (d : ℕ) (v : DyadicNode d) : imbalance I a d v = LocalPolicy.bias a (intervalMass d v) (rate I a d v) (I.count (d + 1) (leftChild v)) (I.count (d + 1) (rightChild v))

theorem FD1D.V5.TreePolicy.local_bellman_inequality {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) (d : ℕ) (hdL : d < L) (v : DyadicNode d) : childAverage (fun (d : ℕ) (v : DyadicNode d) => discrepancy I a d v * regularizedMass I a d v) d v + childAverage (bellmanValue I a) d v - bellmanValue I a d v ≥ (childAverage (fun (d : ℕ) (v : DyadicNode d) => rate I a d v ^ 2) d v - rate I a d v ^ 2 + imbalance I a d v ^ 2 / a ^ 2) / 1000

theorem FD1D.V5.TreePolicy.local_bellman_inequality_separated {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) (d : ℕ) (hdL : d < L) (v : DyadicNode d) : childAverage (fun (d : ℕ) (v : DyadicNode d) => discrepancy I a d v * regularizedMass I a d v) d v + childAverage (bellmanValue I a) d v - bellmanValue I a d v ≥ (childAverage (fun (d : ℕ) (v : DyadicNode d) => rate I a d v ^ 2) d v - rate I a d v ^ 2) / 1000 + imbalance I a d v ^ 2 / (1000 * a ^ 2)

The local certificate with its two energy terms separated.

Deterministic aggregate estimate

noncomputable def FD1D.V5.TreePolicy.transportEnergy {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) : ℝ

The transport energy G = ∑_{v internal} p_v b_v².

Equations

• FD1D.V5.TreePolicy.transportEnergy I a = FD1D.internalWeightedSum (fun (d : ℕ) (v : FD1D.DyadicNode d) => FD1D.V5.TreePolicy.imbalance I a d v ^ 2) L

noncomputable def FD1D.V5.TreePolicy.restoringDrift {L m : ℕ} (I : AggregatedInventory L m) (a : ℝ) : ℝ

The restoring term in the drift of the harmonic inventory potential.

Equations

• FD1D.V5.TreePolicy.restoringDrift I a = FD1D.bellmanDrift L (a / 2) (FD1D.V5.TreePolicy.inventory I) (FD1D.V5.TreePolicy.deletionMass I a)

theorem FD1D.V5.TreePolicy.restoringDrift_div {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) : restoringDrift I a / a = nonrootWeightedSum (fun (d : ℕ) (v : DyadicNode d) => discrepancy I a d v * regularizedMass I a d v) L

The restoring drift is a times the nonroot weighted t Z sum.

theorem FD1D.V5.TreePolicy.bellmanValue_root_eq {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) : bellmanValue I a 0 dyadicRoot = -1 / (2 * ↑m * (↑m + a / 2))

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

theorem FD1D.V5.TreePolicy.deterministic_aggregate_estimate {L m : ℕ} (I : AggregatedInventory L m) {a : ℝ} (ha : 0 < a) (hm : 0 < m) : restoringDrift I a ≥ a / 1000 * hazardEnergy (rate I a) L + transportEnergy I a / (1000 * a) - 501 * a / (1000 * ↑m ^ 2)

The deterministic aggregate estimate from Proposition 4.3 of the manuscript: D ≥ a H_L / 1000 + G / (1000 a) - 501 a / (1000 m²).