Spatial

Concrete spatial inventory and dyadic quantile selection

This module connects the recursive transport construction to an inventory of actual points. A supply configuration retains both each real location and its certified depth-L cell label. The recursive quantile selector is given a finite leaf index, and its law under Lebesgue-uniform demand is computed exactly, including zero-mass leaves.

def FD1D.dyadicLeafSumEquiv (L : ℕ) : DyadicNode L ⊕ DyadicNode L ≃ DyadicNode (L + 1)

Split the left-to-right leaves of a depth-L + 1 tree into two blocks.

Equations

• FD1D.dyadicLeafSumEquiv L = finSumFinEquiv.trans (finCongr ⋯)

@[simp]

theorem FD1D.dyadicLeafSumEquiv_inl_val {L : ℕ} (i : DyadicNode L) : ↑((dyadicLeafSumEquiv L) (Sum.inl i)) = ↑i

@[simp]

theorem FD1D.dyadicLeafSumEquiv_inr_val {L : ℕ} (i : DyadicNode L) : ↑((dyadicLeafSumEquiv L) (Sum.inr i)) = 2 ^ L + ↑i

def FD1D.DyadicMass.leafMass {L : ℕ} : DyadicMass L → DyadicNode L → ℝ

The mass of a specified leaf, indexed from left to right.

Equations

• (FD1D.DyadicMass.leaf mass).leafMass x_3 = mass
• (left.branch right).leafMass i = match (FD1D.dyadicLeafSumEquiv L).symm i with | Sum.inl j => left.leafMass j | Sum.inr j => right.leafMass j

def FD1D.DyadicMass.lowerMass {L : ℕ} : DyadicMass L → DyadicNode L → ℝ

Total mass strictly to the left of a specified leaf.

Equations

• (FD1D.DyadicMass.leaf mass).lowerMass x_3 = 0
• (left.branch right).lowerMass i = match (FD1D.dyadicLeafSumEquiv L).symm i with | Sum.inl j => left.lowerMass j | Sum.inr j => left.total + right.lowerMass j

def FD1D.DyadicMass.selectedIndex {L : ℕ} : DyadicMass L → ℝ → DyadicNode L

The finite leaf index selected by the same recursive mass comparisons as selectedLeaf and quantile.

Equations

• One or more equations did not get rendered due to their size.
• (FD1D.DyadicMass.leaf mass).selectedIndex x✝ = 0

@[simp]

theorem FD1D.DyadicMass.leafMass_left {L : ℕ} (left right : DyadicMass L) (i : DyadicNode L) : (left.branch right).leafMass ((dyadicLeafSumEquiv L) (Sum.inl i)) = left.leafMass i

@[simp]

theorem FD1D.DyadicMass.leafMass_right {L : ℕ} (left right : DyadicMass L) (i : DyadicNode L) : (left.branch right).leafMass ((dyadicLeafSumEquiv L) (Sum.inr i)) = right.leafMass i

@[simp]

theorem FD1D.DyadicMass.lowerMass_left {L : ℕ} (left right : DyadicMass L) (i : DyadicNode L) : (left.branch right).lowerMass ((dyadicLeafSumEquiv L) (Sum.inl i)) = left.lowerMass i

@[simp]

theorem FD1D.DyadicMass.lowerMass_right {L : ℕ} (left right : DyadicMass L) (i : DyadicNode L) : (left.branch right).lowerMass ((dyadicLeafSumEquiv L) (Sum.inr i)) = left.total + right.lowerMass i

theorem FD1D.DyadicMass.sum_leafMass {L : ℕ} (q : DyadicMass L) : ∑ i : DyadicNode L, q.leafMass i = q.total

theorem FD1D.DyadicMass.leafMass_nonneg {L : ℕ} (q : DyadicMass L) (hq : q.allNonneg) (i : DyadicNode L) : 0 ≤ q.leafMass i

theorem FD1D.DyadicMass.lowerMass_nonneg {L : ℕ} (q : DyadicMass L) (hq : q.allNonneg) (i : DyadicNode L) : 0 ≤ q.lowerMass i

theorem FD1D.DyadicMass.lowerMass_add_leafMass_le_total {L : ℕ} (q : DyadicMass L) (hq : q.allNonneg) (i : DyadicNode L) : q.lowerMass i + q.leafMass i ≤ q.total

theorem FD1D.DyadicMass.selectedIndex_measurable {L : ℕ} (q : DyadicMass L) : Measurable q.selectedIndex

theorem FD1D.DyadicMass.selectedLeaf_eq_selectedIndex {L : ℕ} (q : DyadicMass L) (u : ℝ) : q.selectedLeaf u = ↑↑(q.selectedIndex u) / ↑(2 ^ L)

The real endpoint returned by selectedLeaf is the indexed cell's left endpoint.

theorem FD1D.DyadicMass.selectedLeaf_le_quantile {L : ℕ} (q : DyadicMass L) (hq : q.allNonneg) {u : ℝ} (hu0 : 0 ≤ u) (hu1 : u ≤ q.total) : q.selectedLeaf u ≤ q.quantile u

The selected endpoint never lies to the right of the continuous quantile.

theorem FD1D.DyadicMass.selectedIndex_eq_iff_mem_massInterval {L : ℕ} (q : DyadicMass L) (hq : q.allNonneg) {u : ℝ} (hu0 : 0 < u) (hu1 : u ≤ q.total) (i : DyadicNode L) : q.selectedIndex u = i ↔ u ∈ Set.Ioc (q.lowerMass i) (q.lowerMass i + q.leafMass i)

Away from the single boundary point u = 0, a leaf is selected exactly on its right-closed cumulative-mass interval. This formulation handles zero-mass leaves without any positivity assumption on individual masses.

noncomputable def FD1D.DyadicMass.uniformDemand : MeasureTheory.Measure ℝ

Lebesgue-uniform demand on the unit interval.

Equations

• FD1D.DyadicMass.uniformDemand = MeasureTheory.volume.restrict (Set.Icc 0 1)

noncomputable def FD1D.DyadicMass.selectedIndexPushforwardMass {L : ℕ} (q : DyadicMass L) (i : DyadicNode L) : ℝ

Raw singleton mass of the finite pushforward by selectedIndex.

Equations

• q.selectedIndexPushforwardMass i = ((MeasureTheory.Measure.map q.selectedIndex FD1D.DyadicMass.uniformDemand) {i}).toReal

theorem FD1D.DyadicMass.selectedIndexPushforwardMass_eq_leafMass {L : ℕ} (q : DyadicMass L) (hq : q.IsProbability) (i : DyadicNode L) : q.selectedIndexPushforwardMass i = q.leafMass i

The pushforward of Lebesgue-uniform demand assigns exactly the declared mass to every leaf. The only discrepancy between recursive ≤ tie-breaking and the half-open mass intervals is the null singleton u = 0.

noncomputable def FD1D.DyadicMass.selectedIndexLaw {L : ℕ} (q : DyadicMass L) (hq : q.IsProbability) : FiniteLaw (DyadicNode L)

The finite law induced by the demand-driven recursive leaf selector.

Equations

• q.selectedIndexLaw hq = { mass := q.selectedIndexPushforwardMass, mass_nonneg := ⋯, sum_mass := ⋯ }

@[simp]

theorem FD1D.DyadicMass.selectedIndexLaw_mass {L : ℕ} (q : DyadicMass L) (hq : q.IsProbability) (i : DyadicNode L) : (q.selectedIndexLaw hq).mass i = q.leafMass i

Exact spatial configurations

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

Width of one depth-L dyadic cell.

Equations

• FD1D.dyadicCellWidth L = 1 / ↑(2 ^ L)

noncomputable def FD1D.dyadicCellLeft {L : ℕ} (i : DyadicNode L) : ℝ

Left endpoint of a depth-L dyadic cell.

Equations

• FD1D.dyadicCellLeft i = ↑↑i / ↑(2 ^ L)

def FD1D.dyadicCell {L : ℕ} (i : DyadicNode L) : Set ℝ

The closed cell certified for a labeled supply point.

Equations

• FD1D.dyadicCell i = Set.Icc (FD1D.dyadicCellLeft i) (FD1D.dyadicCellLeft i + FD1D.dyadicCellWidth L)

theorem FD1D.dyadicCellWidth_pos (L : ℕ) : 0 < dyadicCellWidth L

theorem FD1D.dyadicCell_subset_unit {L : ℕ} (i : DyadicNode L) : dyadicCell i ⊆ Set.Icc 0 1

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

An exact finite supply configuration: m labeled real points, each in the unit interval and carrying a certified depth-L leaf label.

• location : Fin m → ℝ

  Spatial coordinate of each item in the supply configuration.

• leaf : Fin m → DyadicNode L

  Dyadic cell containing each item in the supply configuration.

• location_mem_unit (j : Fin m) : self.location j ∈ Set.Icc 0 1
• location_mem_cell (j : Fin m) : self.location j ∈ dyadicCell (self.leaf j)

def FD1D.SupplyConfiguration.leafCount {L m : ℕ} (C : SupplyConfiguration L m) (i : DyadicNode L) : ℕ

Number of configured supply points carrying one leaf label.

Equations

• C.leafCount i = {j : Fin m | C.leaf j = i}.card

theorem FD1D.SupplyConfiguration.sum_leafCount {L m : ℕ} (C : SupplyConfiguration L m) : ∑ i : DyadicNode L, C.leafCount i = m

def FD1D.SupplyConfiguration.countState {L m : ℕ} (C : SupplyConfiguration L m) : InventoryState (DyadicNode L) m

Count projection from exact locations to the finite inventory chain.

Equations

• C.countState = ⟨C.leafCount, ⋯⟩

@[simp]

theorem FD1D.SupplyConfiguration.countState_apply {L m : ℕ} (C : SupplyConfiguration L m) (i : DyadicNode L) : ↑C.countState i = C.leafCount i

noncomputable def FD1D.SupplyConfiguration.representative {L m : ℕ} (C : SupplyConfiguration L m) (fallback : Fin m) (i : DyadicNode L) : Fin m

A total representative of a leaf. If the leaf is empty, the supplied fallback is returned; the later a.e. feasibility theorem proves that this case occurs only on the null exceptional demand set.

Equations

• C.representative fallback i = if h : ∃ (j : Fin m), C.leaf j = i then Classical.choose h else fallback

theorem FD1D.SupplyConfiguration.representative_leaf {L m : ℕ} (C : SupplyConfiguration L m) (fallback : Fin m) (i : DyadicNode L) (h : ∃ (j : Fin m), C.leaf j = i) : C.leaf (C.representative fallback i) = i

def FD1D.SupplyConfiguration.Supports {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) : Prop

Every positive-mass leaf contains an actual configured supply point.

Equations

• C.Supports q = ∀ (i : FD1D.DyadicNode L), 0 < q.leafMass i → ∃ (j : Fin m), C.leaf j = i

theorem FD1D.SupplyConfiguration.supports_of_emptyMass {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) (hempty : ∀ (i : DyadicNode L), C.leafCount i = 0 → q.leafMass i = 0) : C.Supports q

noncomputable def FD1D.SupplyConfiguration.selectedSupplyIndex {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) (fallback : Fin m) (u : ℝ) : Fin m

The supply label selected by a uniform demand coordinate.

Equations

• C.selectedSupplyIndex q fallback u = C.representative fallback (q.selectedIndex u)

noncomputable def FD1D.SupplyConfiguration.selectedSupplyPoint {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) (fallback : Fin m) (u : ℝ) : ℝ

The actual configured supply location selected by the policy.

Equations

• C.selectedSupplyPoint q fallback u = C.location (C.selectedSupplyIndex q fallback u)

theorem FD1D.SupplyConfiguration.selectedSupplyPoint_measurable {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) (fallback : Fin m) : Measurable (C.selectedSupplyPoint q fallback)

theorem FD1D.SupplyConfiguration.selectedSupplyPoint_mem_unit {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) (fallback : Fin m) (u : ℝ) : C.selectedSupplyPoint q fallback u ∈ Set.Icc 0 1

theorem FD1D.SupplyConfiguration.selectedSupplyIndex_leaf_of_ne_zero {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) (hq : q.IsProbability) (hsupport : C.Supports q) (fallback : Fin m) {u : ℝ} (hu : u ∈ Set.Icc 0 1) (hu0 : u ≠ 0) : C.leaf (C.selectedSupplyIndex q fallback u) = q.selectedIndex u

Except at the zero demand boundary, the total representative really carries the recursively selected leaf label.

theorem FD1D.SupplyConfiguration.selectedSupplyIndex_leaf_ae {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) (hq : q.IsProbability) (hsupport : C.Supports q) (fallback : Fin m) : ∀ᵐ (u : ℝ) ∂DyadicMass.uniformDemand, C.leaf (C.selectedSupplyIndex q fallback u) = q.selectedIndex u

The selected configured item is feasible for almost every uniform demand.

theorem FD1D.SupplyConfiguration.quantile_mem_selectedCell {L : ℕ} (q : DyadicMass L) (hq : q.IsProbability) {u : ℝ} (hu : u ∈ Set.Icc 0 1) : q.quantile u ∈ dyadicCell (q.selectedIndex u)

The continuous quantile belongs to the cell indexed by selectedIndex.

theorem FD1D.SupplyConfiguration.selectedSupplyPoint_sub_quantile_le_of_ne_zero {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) (hq : q.IsProbability) (hsupport : C.Supports q) (fallback : Fin m) {u : ℝ} (hu : u ∈ Set.Icc 0 1) (hu0 : u ≠ 0) : |C.selectedSupplyPoint q fallback u - q.quantile u| ≤ dyadicCellWidth L

For every nonexceptional demand, the actual selected point and continuous quantile lie in one and the same depth-L cell.

theorem FD1D.SupplyConfiguration.selectedSupplyPoint_sub_quantile_le_ae {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) (hq : q.IsProbability) (hsupport : C.Supports q) (fallback : Fin m) : ∀ᵐ (u : ℝ) ∂DyadicMass.uniformDemand, |C.selectedSupplyPoint q fallback u - q.quantile u| ≤ dyadicCellWidth L

The one-cell coupling bound holds almost everywhere under uniform demand.

noncomputable def FD1D.SupplyConfiguration.expectedActualDistance {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) (fallback : Fin m) : ℝ

Expected distance from a uniform demand to the actual selected supply point.

Equations

• C.expectedActualDistance q fallback = ∫ (u : ℝ) in Set.Icc 0 1, |C.selectedSupplyPoint q fallback u - u|

theorem FD1D.SupplyConfiguration.selectedSupplyDistance_integrable {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) (fallback : Fin m) : MeasureTheory.IntegrableOn (fun (u : ℝ) => |C.selectedSupplyPoint q fallback u - u|) (Set.Icc 0 1) MeasureTheory.volume

theorem FD1D.SupplyConfiguration.quantileDistance_integrable {L : ℕ} (q : DyadicMass L) (hq : q.IsProbability) : MeasureTheory.IntegrableOn (fun (u : ℝ) => |q.quantile u - u|) (Set.Icc 0 1) MeasureTheory.volume

theorem FD1D.SupplyConfiguration.expectedActualDistance_le_one_cell {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) (hq : q.IsProbability) (hsupport : C.Supports q) (fallback : Fin m) : C.expectedActualDistance q fallback ≤ dyadicCellWidth L + cdfTransportArea fun (z : ℝ) => q.piecewiseCDF z - z

Selecting an actual occupied point costs at most the exact CDF quantile area plus one cell width. There is only one discretization term.

Matching the finite deletion kernel

theorem FD1D.SupplyConfiguration.supports_of_deletionRule {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) (R : DeletionRule (DyadicNode L) m) (hmass : ∀ (i : DyadicNode L), q.leafMass i = R.prob C.countState i) : C.Supports q

If the dyadic leaf masses are a deletion rule's probabilities at the count projection, support by occupied concrete leaves follows automatically.

theorem FD1D.SupplyConfiguration.selectedIndexLaw_mass_eq_deletionRule {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) (hq : q.IsProbability) (R : DeletionRule (DyadicNode L) m) (hmass : ∀ (i : DyadicNode L), q.leafMass i = R.prob C.countState i) (i : DyadicNode L) : (q.selectedIndexLaw hq).mass i = R.prob C.countState i

The selected leaf marginal is exactly the deletion marginal.

theorem FD1D.SupplyConfiguration.selectedIndex_transition_eq_kernel {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) (hq : q.IsProbability) (R : DeletionRule (DyadicNode L) m) (hmass : ∀ (i : DyadicNode L), q.leafMass i = R.prob C.countState i) (y : InventoryState (DyadicNode L) m) : (∑ deleted : DyadicNode L, ∑ arrived : DyadicNode L, if C.countState.move deleted arrived = y then (q.selectedIndexLaw hq).mass deleted * (1 / ↑(Fintype.card (DyadicNode L))) else 0) = R.kernel.trans C.countState y

After an independent uniform arrival leaf, the concrete selected-leaf marginal produces exactly the count transition kernel.

theorem FD1D.SupplyConfiguration.expectedActualDistance_le_one_cell_of_deletionRule {L m : ℕ} (C : SupplyConfiguration L m) (q : DyadicMass L) (hq : q.IsProbability) (R : DeletionRule (DyadicNode L) m) (hmass : ∀ (i : DyadicNode L), q.leafMass i = R.prob C.countState i) (fallback : Fin m) : C.expectedActualDistance q fallback ≤ dyadicCellWidth L + cdfTransportArea fun (z : ℝ) => q.piecewiseCDF z - z

Actual-point transport for a configuration realizing a deletion rule: the empty-leaf condition needed for feasibility is discharged by the rule.

def FD1D.appendDyadicNode {d r : ℕ} (v : DyadicNode d) (w : DyadicNode r) : DyadicNode (d + r)

Prefix a relative dyadic node by an absolute node.

Equations

• FD1D.appendDyadicNode v w = ⟨↑v * 2 ^ r + ↑w, ⋯⟩

@[simp]

theorem FD1D.appendDyadicNode_zero {d : ℕ} (v : DyadicNode d) : appendDyadicNode v 0 = v

theorem FD1D.appendDyadicNode_leftNode_heq {d k : ℕ} (v : DyadicNode d) (j : CompleteHaarNode k) : appendDyadicNode v (DyadicMass.leftNode j).snd ≍ appendDyadicNode (leftChild v) j.snd

theorem FD1D.appendDyadicNode_rightNode_heq {d k : ℕ} (v : DyadicNode d) (j : CompleteHaarNode k) : appendDyadicNode v (DyadicMass.rightNode j).snd ≍ appendDyadicNode (rightChild v) j.snd

theorem FD1D.appendDyadicNode_inl_heq {d k : ℕ} (v : DyadicNode d) (w : DyadicNode k) : appendDyadicNode v ((dyadicLeafSumEquiv k) (Sum.inl w)) ≍ appendDyadicNode (leftChild v) w

theorem FD1D.appendDyadicNode_inr_heq {d k : ℕ} (v : DyadicNode d) (w : DyadicNode k) : appendDyadicNode v ((dyadicLeafSumEquiv k) (Sum.inr w)) ≍ appendDyadicNode (rightChild v) w

theorem FD1D.completeHaarNode_cases {k : ℕ} (i : CompleteHaarNode (k + 1)) : i = ⟨⟨0, ⋯⟩, 0⟩ ∨ (∃ (j : CompleteHaarNode k), i = DyadicMass.leftNode j) ∨ ∃ (j : CompleteHaarNode k), i = DyadicMass.rightNode j