Paper-facing model for fully dynamic matching on the line

This module gives a compact, Mathlib-only statement vocabulary for the main theorem. An online policy sees the current inventory and current demand, selects one live supply, pays their distance, and replaces that supply by an independent uniform replenishment. The path measure below is the homogeneous Markov law driven by iid uniform demand/replenishment pairs.

@[reducible, inline]

abbrev FD1D.V5.Palomar.Inventory (m : ℕ) : Type

A labeled inventory of m supplies in [0,1].

Equations

• FD1D.V5.Palomar.Inventory m = (Fin m → ↑unitInterval)

@[reducible, inline]

abbrev FD1D.V5.Palomar.Noise : Type

One period's independent demand and replenishment coordinates.

Equations

• FD1D.V5.Palomar.Noise = (↑unitInterval × ↑unitInterval)

noncomputable def FD1D.V5.Palomar.noiseLaw : MeasureTheory.Measure Noise

The law of an independent uniform demand/replenishment pair.

Equations

• FD1D.V5.Palomar.noiseLaw = MeasureTheory.volume.prod MeasureTheory.volume

instance FD1D.V5.Palomar.noiseLaw_isProbabilityMeasure : MeasureTheory.IsProbabilityMeasure noiseLaw

structure FD1D.V5.Palomar.OnlinePolicy (m : ℕ) : Type

An online matching policy. The selected label depends only on the current inventory and current demand. The second measurability field records the exact coordinate replacement map used to construct its Markov law.

• select : Inventory m → ↑unitInterval → Fin m

  Selected inventory label as a function of the current state and uniform demand.

• selectMeasurable : Measurable fun (p : Inventory m × ↑unitInterval) => self.select p.1 p.2
• stepMeasurable : Measurable fun (p : Inventory m × Noise) => Function.update p.1 (self.select p.1 p.2.1) p.2.2

def FD1D.V5.Palomar.step {m : ℕ} (P : OnlinePolicy m) (s : Inventory m) (z : Noise) : Inventory m

Replace the selected supply by the replenishment coordinate.

Equations

• FD1D.V5.Palomar.step P s z = Function.update s (P.select s z.1) z.2

@[reducible, inline]

abbrev FD1D.V5.Palomar.ProcessState (m : ℕ) : Type

The pre-match inventory together with the current random coordinates.

Equations

• FD1D.V5.Palomar.ProcessState m = (FD1D.V5.Palomar.Inventory m × FD1D.V5.Palomar.Noise)

def FD1D.V5.Palomar.processAdvance {m : ℕ} (P : OnlinePolicy m) (p : ProcessState m × Noise) : ProcessState m

Apply the current noise and attach fresh noise for the next period.

Equations

• FD1D.V5.Palomar.processAdvance P p = (FD1D.V5.Palomar.step P p.1.1 p.1.2, p.2)

theorem FD1D.V5.Palomar.processAdvance_measurable {m : ℕ} (P : OnlinePolicy m) : Measurable (processAdvance P)

noncomputable def FD1D.V5.Palomar.processKernel {m : ℕ} (P : OnlinePolicy m) : ProbabilityTheory.Kernel (ProcessState m) (ProcessState m)

The homogeneous one-period kernel of an online policy.

Equations

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

instance FD1D.V5.Palomar.processKernel_isMarkovKernel {m : ℕ} (P : OnlinePolicy m) : ProbabilityTheory.IsMarkovKernel (processKernel P)

noncomputable def FD1D.V5.Palomar.initialProcessLaw {m : ℕ} (μ₀ : MeasureTheory.Measure (Inventory m)) : MeasureTheory.Measure (ProcessState m)

Attach an independent first demand/replenishment pair to an inventory law.

Equations

• FD1D.V5.Palomar.initialProcessLaw μ₀ = μ₀.prod FD1D.V5.Palomar.noiseLaw

instance FD1D.V5.Palomar.initialProcessLaw_isProbabilityMeasure {m : ℕ} (μ₀ : MeasureTheory.Measure (Inventory m)) [MeasureTheory.IsProbabilityMeasure μ₀] : MeasureTheory.IsProbabilityMeasure (initialProcessLaw μ₀)

noncomputable def FD1D.V5.Palomar.historyKernel {m : ℕ} (P : OnlinePolicy m) (n : ℕ) : ProbabilityTheory.Kernel (↥(Finset.Iic n) → ProcessState m) (ProcessState m)

A homogeneous kernel viewed as a history-dependent kernel.

Equations

• FD1D.V5.Palomar.historyKernel P n = (FD1D.V5.Palomar.processKernel P).comap (fun (h : ↥(Finset.Iic n) → FD1D.V5.Palomar.ProcessState m) => h ⟨n, ⋯⟩) ⋯

instance FD1D.V5.Palomar.historyKernel_isMarkovKernel {m : ℕ} (P : OnlinePolicy m) (n : ℕ) : ProbabilityTheory.IsMarkovKernel (historyKernel P n)

noncomputable def FD1D.V5.Palomar.trajectoryFrom {m : ℕ} (P : OnlinePolicy m) (μ₀ : MeasureTheory.Measure (Inventory m)) : MeasureTheory.Measure (ℕ → ProcessState m)

The path-space law generated from an arbitrary initial inventory law.

Equations

• FD1D.V5.Palomar.trajectoryFrom P μ₀ = ProbabilityTheory.Kernel.trajMeasure (FD1D.V5.Palomar.initialProcessLaw μ₀) (FD1D.V5.Palomar.historyKernel P)

noncomputable def FD1D.V5.Palomar.trajectoryFromState {m : ℕ} (P : OnlinePolicy m) (s₀ : Inventory m) : MeasureTheory.Measure (ℕ → ProcessState m)

The trajectory law from a fixed initial inventory.

Equations

• FD1D.V5.Palomar.trajectoryFromState P s₀ = FD1D.V5.Palomar.trajectoryFrom P (MeasureTheory.Measure.dirac s₀)

noncomputable def FD1D.V5.Palomar.uniformInventoryLaw (m : ℕ) : MeasureTheory.Measure (Inventory m)

The iid uniform law of the inventory produced by scheduled replacement.

Equations

• FD1D.V5.Palomar.uniformInventoryLaw m = MeasureTheory.Measure.pi fun (x : Fin m) => MeasureTheory.volume

instance FD1D.V5.Palomar.uniformInventoryLaw_isProbabilityMeasure {m : ℕ} : MeasureTheory.IsProbabilityMeasure (uniformInventoryLaw m)

noncomputable def FD1D.V5.Palomar.uniformTrajectory {m : ℕ} (P : OnlinePolicy m) : MeasureTheory.Measure (ℕ → ProcessState m)

The policy trajectory after iid uniform initialization.

Equations

• FD1D.V5.Palomar.uniformTrajectory P = FD1D.V5.Palomar.trajectoryFrom P (FD1D.V5.Palomar.uniformInventoryLaw m)

def FD1D.V5.Palomar.processCost {m : ℕ} (P : OnlinePolicy m) (z : ProcessState m) : ℝ

The distance paid in one period.

Equations

• FD1D.V5.Palomar.processCost P z = |↑(z.1 (P.select z.1 z.2.1)) - ↑z.2.1|

noncomputable def FD1D.V5.Palomar.trajectoryRMSCostFromState {m : ℕ} (P : OnlinePolicy m) (s₀ : Inventory m) (t : ℕ) : ℝ

Root mean square one-period cost from a fixed initial inventory.

Equations

• FD1D.V5.Palomar.trajectoryRMSCostFromState P s₀ t = √(∫ (path : ℕ → FD1D.V5.Palomar.ProcessState m), FD1D.V5.Palomar.processCost P (path t) ^ 2 ∂FD1D.V5.Palomar.trajectoryFromState P s₀)

def FD1D.V5.Palomar.initializationCost {m : ℕ} (initial demand : Inventory m) : ℝ

The total cost of matching once to every original labeled supply during the first m periods.

Equations

• FD1D.V5.Palomar.initializationCost initial demand = ∑ j : Fin m, |↑(demand j) - ↑(initial j)|

noncomputable def FD1D.V5.Palomar.initializedAverageCost {m : ℕ} (P : OnlinePolicy m) (initial demand : Inventory m) (N : ℕ) (path : ℕ → ProcessState m) : ℝ

Average cost over N periods: scheduled replacement first, followed by the online policy on the resulting iid uniform inventory.

Equations

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

def FD1D.V5.Palomar.regularization (m : ℕ) : ℕ

The manuscript's regularization parameter.

Equations

• FD1D.V5.Palomar.regularization m = 2000 * Nat.clog 2 (m + 1)

def FD1D.V5.Palomar.treeDepth (m : ℕ) : ℕ

The dyadic tree depth used by the policy.

Equations

• FD1D.V5.Palomar.treeDepth m = Nat.log 2 (max 1 (m / FD1D.V5.Palomar.regularization m))

def FD1D.V5.Palomar.leafCount (m : ℕ) : ℕ

The dyadic leaf count used by the policy.

Equations

• FD1D.V5.Palomar.leafCount m = 2 ^ FD1D.V5.Palomar.treeDepth m

def FD1D.V5.Palomar.operationCount (m : ℕ) : ℕ

Abstract primitive-operation count in the real-arithmetic model.

Equations

• FD1D.V5.Palomar.operationCount m = 20 * (FD1D.V5.Palomar.treeDepth m + 1)

def FD1D.V5.Palomar.memoryCount (m : ℕ) : ℕ

Abstract memory-word count in the real-arithmetic model.

Equations

• FD1D.V5.Palomar.memoryCount m = m + 4 * FD1D.V5.Palomar.leafCount m

noncomputable def FD1D.V5.Palomar.universalConstant : ℝ

One explicit universal constant for both cost bounds.

Equations

• FD1D.V5.Palomar.universalConstant = 72000 / Real.log 2

structure FD1D.V5.Palomar.PolicyGuarantees (m : ℕ) (P : OnlinePolicy m) : Prop

The two quantitative guarantees for one inventory size.

• arbitraryInitialRMS (s₀ : Inventory m) : Filter.limsup (trajectoryRMSCostFromState P s₀) Filter.atTop ≤ universalConstant * Real.log ↑(m + 1) / ↑m
• initializedFiniteHorizon (N : ℕ) : 2 * m ^ 2 ≤ N → ∀ (initial demand : Inventory m), ∫ (path : ℕ → ProcessState m), initializedAverageCost P initial demand N path ∂uniformTrajectory P ≤ universalConstant * Real.log ↑(m + 1) / ↑m

structure FD1D.V5.Palomar.ResourceGuarantees : Prop

Explicit and asymptotic resource accounting for the policy family.

• operationsExplicit {m : ℕ} : 2 ≤ m → ↑(operationCount m) ≤ 100 / Real.log 2 * Real.log ↑m
• memoryExplicit {m : ℕ} : 1 ≤ m → memoryCount m ≤ 5 * m
• operationsAsymptotic : (fun (m : ℕ) => ↑(operationCount m)) =O[Filter.atTop] fun (m : ℕ) => Real.log ↑m
• memoryAsymptotic : (fun (m : ℕ) => ↑(memoryCount m)) =O[Filter.atTop] fun (m : ℕ) => ↑m

structure FD1D.V5.Palomar.OptimalDynamicMatchingUpperBound : Prop

Exact compared content of the formalized stochastic cost upper bound.

• policy (m : ℕ) : 2 ≤ m → ∃ (P : OnlinePolicy m), PolicyGuarantees m P