Tree

Complete dyadic trees

Nodes at depth d are numbered from left to right by Fin (2 ^ d). The module supplies the finite-tree bookkeeping used by the hazard and Bellman arguments. All global estimates are consequences of explicit local hypotheses; no policy-specific algebra is hidden here.

@[reducible, inline]

abbrev FD1D.DyadicNode (d : ℕ) : Type

Nodes of the complete dyadic tree at depth d.

Equations

• FD1D.DyadicNode d = Fin (2 ^ d)

def FD1D.dyadicRoot : DyadicNode 0

The unique node at depth zero.

Equations

• FD1D.dyadicRoot = 0

def FD1D.childrenEquiv (d : ℕ) : DyadicNode d × Fin 2 ≃ DyadicNode (d + 1)

Splitting a level into the two children of every node.

Equations

• FD1D.childrenEquiv d = finProdFinEquiv.trans (finCongr ⋯)

def FD1D.leftChild {d : ℕ} (v : DyadicNode d) : DyadicNode (d + 1)

The left child of a dyadic node.

Equations

• FD1D.leftChild v = (FD1D.childrenEquiv d) (v, 0)

def FD1D.rightChild {d : ℕ} (v : DyadicNode d) : DyadicNode (d + 1)

The right child of a dyadic node.

Equations

• FD1D.rightChild v = (FD1D.childrenEquiv d) (v, 1)

@[simp]

theorem FD1D.leftChild_val {d : ℕ} (v : DyadicNode d) : ↑(leftChild v) = 2 * ↑v

@[simp]

theorem FD1D.rightChild_val {d : ℕ} (v : DyadicNode d) : ↑(rightChild v) = 2 * ↑v + 1

def FD1D.parent {d : ℕ} (v : DyadicNode (d + 1)) : DyadicNode d

The parent of a nonroot node.

Equations

• FD1D.parent v = ((FD1D.childrenEquiv d).symm v).1

@[simp]

theorem FD1D.parent_leftChild {d : ℕ} (v : DyadicNode d) : parent (leftChild v) = v

@[simp]

theorem FD1D.parent_rightChild {d : ℕ} (v : DyadicNode d) : parent (rightChild v) = v

theorem FD1D.leftChild_ne_rightChild {d : ℕ} (v : DyadicNode d) : leftChild v ≠ rightChild v

theorem FD1D.sum_children {M : Type u_1} [AddCommMonoid M] (d : ℕ) (f : DyadicNode (d + 1) → M) : ∑ w : DyadicNode (d + 1), f w = ∑ v : DyadicNode d, (f (leftChild v) + f (rightChild v))

Every node at level d+1 occurs exactly once as a left or right child. This is the basic child-partition identity for finite sums.

def FD1D.descendantsEquiv {d L : ℕ} (hdL : d ≤ L) : DyadicNode d × Fin (2 ^ (L - d)) ≃ DyadicNode L

At levels d ≤ L, a leaf is uniquely a pair consisting of a depth-d ancestor and an offset in that ancestor's consecutive leaf block.

Equations

• FD1D.descendantsEquiv hdL = finProdFinEquiv.trans (finCongr ⋯)

def FD1D.descendantLeaf {d L : ℕ} (hdL : d ≤ L) (v : DyadicNode d) (j : Fin (2 ^ (L - d))) : DyadicNode L

The leaf with offset j in the block below v.

Equations

• FD1D.descendantLeaf hdL v j = (FD1D.descendantsEquiv hdL) (v, j)

theorem FD1D.descendantLeaf_val {d L : ℕ} (hdL : d ≤ L) (v : DyadicNode d) (j : Fin (2 ^ (L - d))) : ↑(descendantLeaf hdL v j) = ↑v * 2 ^ (L - d) + ↑j

Descendant blocks are consecutive in the left-to-right leaf numbering.

def FD1D.descendantEmbedding {d L : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : Fin (2 ^ (L - d)) ↪ DyadicNode L

The embedding of offsets into the leaf block below one node.

Equations

• FD1D.descendantEmbedding hdL v = { toFun := FD1D.descendantLeaf hdL v, inj' := ⋯ }

def FD1D.leafBlock {d L : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : Finset (DyadicNode L)

The consecutive block of depth-L leaves below v.

Equations

• FD1D.leafBlock hdL v = Finset.map (FD1D.descendantEmbedding hdL v) Finset.univ

@[simp]

theorem FD1D.card_leafBlock {d L : ℕ} (hdL : d ≤ L) (v : DyadicNode d) : (leafBlock hdL v).card = 2 ^ (L - d)

theorem FD1D.mem_leafBlock_iff {d L : ℕ} (hdL : d ≤ L) (v : DyadicNode d) (w : DyadicNode L) : w ∈ leafBlock hdL v ↔ ∃ (j : Fin (2 ^ (L - d))), descendantLeaf hdL v j = w

theorem FD1D.mem_leafBlock_interval {d L : ℕ} (hdL : d ≤ L) (v : DyadicNode d) (w : DyadicNode L) : w ∈ leafBlock hdL v ↔ ↑v * 2 ^ (L - d) ≤ ↑w ∧ ↑w < (↑v + 1) * 2 ^ (L - d)

Membership in a descendant block, expressed as a half-open index interval.

theorem FD1D.leafBlock_disjoint {d L : ℕ} (hdL : d ≤ L) {v w : DyadicNode d} (hvw : v ≠ w) : Disjoint (leafBlock hdL v) (leafBlock hdL w)

Distinct nodes at one level have disjoint descendant leaf blocks.

theorem FD1D.existsUnique_leafBlock {d L : ℕ} (hdL : d ≤ L) (w : DyadicNode L) : ∃! v : DyadicNode d, w ∈ leafBlock hdL v

Every leaf belongs to a unique block at every shallower level.

theorem FD1D.leafBlock_children {d L : ℕ} (hdL : d < L) (v : DyadicNode d) : leafBlock ⋯ v = leafBlock ⋯ (leftChild v) ∪ leafBlock ⋯ (rightChild v)

A parent's leaf block is the disjoint union of its children's blocks.

noncomputable def FD1D.nodeMass (d : ℕ) : DyadicNode d → ℝ

Interval mass of every node at depth d.

Equations

• FD1D.nodeMass d x✝ = (2 ^ d)⁻¹

theorem FD1D.nodeMass_pos (d : ℕ) (v : DyadicNode d) : 0 < nodeMass d v

theorem FD1D.nodeMass_nonneg (d : ℕ) (v : DyadicNode d) : 0 ≤ nodeMass d v

@[simp]

theorem FD1D.nodeMass_root : nodeMass 0 dyadicRoot = 1

theorem FD1D.nodeMass_child {d : ℕ} (v : DyadicNode d) (side : Fin 2) : nodeMass (d + 1) ((childrenEquiv d) (v, side)) = nodeMass d v / 2

Each child has half its parent's interval mass.

@[simp]

theorem FD1D.nodeMass_leftChild {d : ℕ} (v : DyadicNode d) : nodeMass (d + 1) (leftChild v) = nodeMass d v / 2

@[simp]

theorem FD1D.nodeMass_rightChild {d : ℕ} (v : DyadicNode d) : nodeMass (d + 1) (rightChild v) = nodeMass d v / 2

theorem FD1D.sum_nodeMass (d : ℕ) : ∑ v : DyadicNode d, nodeMass d v = 1

Node masses at every complete level sum to one.

Inventory and coherent labels

structure FD1D.LeafInventory (L m : ℕ) : Type

A leaf inventory vector with a prescribed total inventory m.

• count : DyadicNode L → ℕ

  Number of inventory items in each leaf of the dyadic tree.

• total_count : ∑ v : DyadicNode L, self.count v = m

structure FD1D.AggregatedInventory (L m : ℕ) : Type

Aggregated counts at every level. The explicit child equation states exactly that each internal count is the sum of the inventory in its two child blocks.

• leaf : LeafInventory L m

  Inventory at the finest dyadic level.

• count (d : ℕ) : DyadicNode d → ℕ

  Aggregated inventory count at each dyadic level and node.

• count_leaf : self.count L = self.leaf.count
• count_children (d : ℕ) : d < L → ∀ (v : DyadicNode d), self.count d v = self.count (d + 1) (leftChild v) + self.count (d + 1) (rightChild v)
• count_root : self.count 0 dyadicRoot = m

def FD1D.LeafInventory.nodeCount {L m d : ℕ} (I : LeafInventory L m) (hdL : d ≤ L) (v : DyadicNode d) : ℕ

Concrete aggregate of a leaf inventory over one descendant block.

Equations

• I.nodeCount hdL v = ∑ w ∈ FD1D.leafBlock hdL v, I.count w

@[simp]

theorem FD1D.LeafInventory.nodeCount_leaf {L m : ℕ} (I : LeafInventory L m) (v : DyadicNode L) : I.nodeCount ⋯ v = I.count v

@[simp]

theorem FD1D.LeafInventory.nodeCount_root {L m : ℕ} (I : LeafInventory L m) : I.nodeCount ⋯ dyadicRoot = m

theorem FD1D.LeafInventory.nodeCount_children {L m d : ℕ} (I : LeafInventory L m) (hdL : d < L) (v : DyadicNode d) : I.nodeCount ⋯ v = I.nodeCount ⋯ (leftChild v) + I.nodeCount ⋯ (rightChild v)

Aggregated inventory counts satisfy the parent/children count identity.

def FD1D.LeafInventory.aggregate {L m : ℕ} (I : LeafInventory L m) : AggregatedInventory L m

Every fixed-total leaf vector has canonical coherent aggregate counts.

Equations

• I.aggregate = { leaf := I, count := fun (d : ℕ) (v : FD1D.DyadicNode d) => if hdL : d ≤ L then I.nodeCount hdL v else 0, count_leaf := ⋯, count_children := ⋯, count_root := ⋯ }

structure FD1D.CoherentTreeLabel (L : ℕ) (A : Type u_1) [AddCommMonoid A] : Type u_1

An abstract additive tree labeling. It is useful for q, inventory counts, or any other quantity whose parent is the sum of its children.

• value (d : ℕ) : DyadicNode d → A

  Node labels whose parent value is the sum of its child values.

• children (d : ℕ) : d < L → ∀ (v : DyadicNode d), self.value d v = self.value (d + 1) (leftChild v) + self.value (d + 1) (rightChild v)

def FD1D.levelSum {A : Type u_1} [AddCommMonoid A] (f : (d : ℕ) → DyadicNode d → A) (d : ℕ) : A

Sum of a depth-indexed label over one complete level.

Equations

• FD1D.levelSum f d = ∑ v : FD1D.DyadicNode d, f d v

theorem FD1D.levelSum_succ {A : Type u_1} [AddCommMonoid A] (f : (d : ℕ) → DyadicNode d → A) (d : ℕ) : levelSum f (d + 1) = ∑ v : DyadicNode d, (f (d + 1) (leftChild v) + f (d + 1) (rightChild v))

theorem FD1D.CoherentTreeLabel.levelSum_eq_root {L : ℕ} {A : Type u_1} [AddCommMonoid A] (f : CoherentTreeLabel L A) {d : ℕ} (hdL : d ≤ L) : levelSum f.value d = f.value 0 dyadicRoot

theorem FD1D.AggregatedInventory.level_count_eq {L m : ℕ} (I : AggregatedInventory L m) {d : ℕ} (hdL : d ≤ L) : ∑ v : DyadicNode d, I.count d v = m

theorem FD1D.AggregatedInventory.leaf_count_eq_total {L m : ℕ} (I : AggregatedInventory L m) : ∑ v : DyadicNode L, I.count L v = m

Weighted telescopes

noncomputable def FD1D.weightedLevel (f : (d : ℕ) → DyadicNode d → ℝ) (d : ℕ) : ℝ

Mass-weighted sum of a real label over one complete level.

Equations

• FD1D.weightedLevel f d = ∑ v : FD1D.DyadicNode d, FD1D.nodeMass d v * f d v

@[simp]

theorem FD1D.weightedLevel_zero (f : (d : ℕ) → DyadicNode d → ℝ) : weightedLevel f 0 = f 0 dyadicRoot

noncomputable def FD1D.childAverage (f : (d : ℕ) → DyadicNode d → ℝ) (d : ℕ) (v : DyadicNode d) : ℝ

Arithmetic mean of a real label over the two children of v.

Equations

• FD1D.childAverage f d v = (f (d + 1) (FD1D.leftChild v) + f (d + 1) (FD1D.rightChild v)) / 2

theorem FD1D.weighted_childAverage_sum (f : (d : ℕ) → DyadicNode d → ℝ) (d : ℕ) : ∑ v : DyadicNode d, nodeMass d v * childAverage f d v = weightedLevel f (d + 1)

A child average weighted at the parent equals the next weighted level.

theorem FD1D.weighted_local_sum (f : (d : ℕ) → DyadicNode d → ℝ) (d : ℕ) : ∑ v : DyadicNode d, nodeMass d v * (childAverage f d v - f d v) = weightedLevel f (d + 1) - weightedLevel f d

theorem FD1D.weighted_tree_telescope (f : (d : ℕ) → DyadicNode d → ℝ) (L : ℕ) : ∑ d ∈ Finset.range L, ∑ v : DyadicNode d, nodeMass d v * (childAverage f d v - f d v) = weightedLevel f L - f 0 dyadicRoot

Generic mass-weighted telescope over all internal nodes.

noncomputable def FD1D.nonrootWeightedSum (f : (d : ℕ) → DyadicNode d → ℝ) (L : ℕ) : ℝ

Sum of a mass-weighted label over all nonroot levels through L.

Equations

• FD1D.nonrootWeightedSum f L = ∑ d ∈ Finset.range L, FD1D.weightedLevel f (d + 1)

noncomputable def FD1D.internalWeightedSum (f : (d : ℕ) → DyadicNode d → ℝ) (L : ℕ) : ℝ

Sum of a mass-weighted label over all internal levels before L.

Equations

• FD1D.internalWeightedSum f L = ∑ d ∈ Finset.range L, FD1D.weightedLevel f d

noncomputable def FD1D.hazardEnergy (h : (d : ℕ) → DyadicNode d → ℝ) (d : ℕ) : ℝ

The hazard energy H_d = ∑_{depth(v)=d} p_v h_v².

Equations

• FD1D.hazardEnergy h d = FD1D.weightedLevel (fun (d : ℕ) (v : FD1D.DyadicNode d) => h d v ^ 2) d

theorem FD1D.hazardEnergy_root (h : (d : ℕ) → DyadicNode d → ℝ) : hazardEnergy h 0 = h 0 dyadicRoot ^ 2

theorem FD1D.hazard_energy_telescope (h : (d : ℕ) → DyadicNode d → ℝ) (L : ℕ) : ∑ d ∈ Finset.range L, ∑ v : DyadicNode d, nodeMass d v * (childAverage (fun (d : ℕ) (v : DyadicNode d) => h d v ^ 2) d v - h d v ^ 2) = hazardEnergy h L - hazardEnergy h 0

Exact hazard-energy telescope behind equations (1) and (2).

theorem FD1D.hazard_energy_bound (L : ℕ) (a : ℝ) (h b : (d : ℕ) → DyadicNode d → ℝ) (hlocal : ∀ d < L, ∀ (v : DyadicNode d), b d v ^ 2 ≤ 2 * a ^ 2 * (childAverage (fun (d : ℕ) (v : DyadicNode d) => h d v ^ 2) d v - h d v ^ 2)) : internalWeightedSum (fun (d : ℕ) (v : DyadicNode d) => b d v ^ 2) L ≤ 2 * a ^ 2 * (hazardEnergy h L - hazardEnergy h 0)

Summing the local hazard inequality gives equation (2), before substituting the root value h_root = 1/m.

theorem FD1D.hazard_energy_bound_from_local (L : ℕ) {a : ℝ} (h b : (d : ℕ) → DyadicNode d → ℝ) (ha : a ≠ 0) (hlocal : ∀ d < L, ∀ (v : DyadicNode d), b d v ^ 2 / (2 * a ^ 2) ≤ childAverage (fun (d : ℕ) (v : DyadicNode d) => h d v ^ 2) d v - h d v ^ 2) : internalWeightedSum (fun (d : ℕ) (v : DyadicNode d) => b d v ^ 2) L ≤ 2 * a ^ 2 * (hazardEnergy h L - hazardEnergy h 0)

Equation (2) directly from equation (1), with the latter stated in its displayed divided form.

theorem FD1D.hazard_energy_bound_of_root (L : ℕ) {a m : ℝ} (h b : (d : ℕ) → DyadicNode d → ℝ) (hm : m ≠ 0) (hroot : h 0 dyadicRoot = 1 / m) (hlocal : ∀ d < L, ∀ (v : DyadicNode d), b d v ^ 2 ≤ 2 * a ^ 2 * (childAverage (fun (d : ℕ) (v : DyadicNode d) => h d v ^ 2) d v - h d v ^ 2)) : internalWeightedSum (fun (d : ℕ) (v : DyadicNode d) => b d v ^ 2) L ≤ 2 * a ^ 2 * (hazardEnergy h L - 1 / m ^ 2)

Equation (2) with H₀ = m⁻².

Bellman telescope and deterministic estimate

theorem FD1D.bellman_tree_telescope (c B : (d : ℕ) → DyadicNode d → ℝ) (L : ℕ) : ∑ d ∈ Finset.range L, ∑ v : DyadicNode d, nodeMass d v * (childAverage c d v + childAverage B d v - B d v) = nonrootWeightedSum c L + weightedLevel B L - B 0 dyadicRoot

The exact generic Bellman telescope. c is the child cost (t Z in the paper), while B is any node potential.

theorem FD1D.bellman_global_bound (L : ℕ) (h t Z B : (d : ℕ) → DyadicNode d → ℝ) (hlocal : ∀ d < L, ∀ (v : DyadicNode d), childAverage (fun (d : ℕ) (v : DyadicNode d) => t d v * Z d v) d v + childAverage B d v - B d v ≥ (childAverage (fun (d : ℕ) (v : DyadicNode d) => h d v ^ 2) d v - h d v ^ 2) / 100) : nonrootWeightedSum (fun (d : ℕ) (v : DyadicNode d) => t d v * Z d v) L ≥ (hazardEnergy h L - hazardEnergy h 0) / 100 + B 0 dyadicRoot - weightedLevel B L

Global form of the local Bellman inequality (7). This is the telescope used immediately before equation (9).

noncomputable def FD1D.bellmanDrift (L : ℕ) (a : ℝ) (N q : (d : ℕ) → DyadicNode d → ℝ) : ℝ

The drift quantity D from equation (9).

Equations

• FD1D.bellmanDrift L a N q = ∑ d ∈ Finset.range L, ∑ v : FD1D.DyadicNode (d + 1), FD1D.nodeMass (d + 1) v ^ 2 * (FD1D.nodeMass (d + 1) v - q (d + 1) v) / (N (d + 1) v + a)

theorem FD1D.bellman_cost_eq_drift_div (L : ℕ) (a : ℝ) (N q t Z : (d : ℕ) → DyadicNode d → ℝ) (ht : ∀ (d : ℕ) (v : DyadicNode d), t d v = (nodeMass d v - q d v) / a) (hZ : ∀ (d : ℕ) (v : DyadicNode d), Z d v = nodeMass d v / (N d v + a)) : nonrootWeightedSum (fun (d : ℕ) (v : DyadicNode d) => t d v * Z d v) L = bellmanDrift L a N q / a

theorem FD1D.deterministic_bellman_bound (L : ℕ) {a m : ℝ} (N q h t Z B : (d : ℕ) → DyadicNode d → ℝ) (ha : 0 < a) (hm : 0 < m) (ht : ∀ (d : ℕ) (v : DyadicNode d), t d v = (nodeMass d v - q d v) / a) (hZ : ∀ (d : ℕ) (v : DyadicNode d), Z d v = nodeMass d v / (N d v + a)) (hroot : h 0 dyadicRoot = 1 / m) (hlocal : ∀ d < L, ∀ (v : DyadicNode d), childAverage (fun (d : ℕ) (v : DyadicNode d) => t d v * Z d v) d v + childAverage B d v - B d v ≥ (childAverage (fun (d : ℕ) (v : DyadicNode d) => h d v ^ 2) d v - h d v ^ 2) / 100) (hleaf : ∀ (v : DyadicNode L), B L v ≤ 0) (hBroot : -(1 / (3 * m ^ 2)) ≤ B 0 dyadicRoot) : bellmanDrift L a N q ≥ a * (hazardEnergy h L / 100 - 103 / (300 * m ^ 2))

The deterministic Bellman estimate (9). The hypotheses are exactly the local certificate (7), the definitions of t and Z, and the terminal/root sign bounds proved in the paper.

Squared masses

theorem FD1D.sum_nodeMass_sq (d : ℕ) : ∑ v : DyadicNode d, nodeMass d v ^ 2 = (2 ^ d)⁻¹

Squared interval masses on level d sum to 2⁻ᵈ.

noncomputable def FD1D.nonrootMassSqSum (L : ℕ) : ℝ

Sum of p_v² over every nonroot node through depth L.

Equations

• FD1D.nonrootMassSqSum L = ∑ d ∈ Finset.range L, ∑ v : FD1D.DyadicNode (d + 1), FD1D.nodeMass (d + 1) v ^ 2

theorem FD1D.sum_nonroot_nodeMass_sq (L : ℕ) : nonrootMassSqSum L = 1 - 1 / 2 ^ L

∑_{v ≠ root} p_v² = 1 - 1/n for n = 2^L.