Documentation

LeanPool.FullyDynamicMatching.FD1D.Drift

Drift #

Harmonic-potential drift #

This module separates the stochastic bookkeeping from the concrete tree. The tree module supplies D, R, and H; the lemmas below prove the exact one-coordinate drift identity and the arithmetic implications used in the stationary and finite-horizon arguments.

source
noncomputable def FD1D.harmonicPotential (a : ℝ) (k : ℕ) :
ℝ

The finite harmonic potential used at a node with inventory k.

Equations
Instances For
    source
    @[simp]
    theorem FD1D.harmonicPotential_zero (a : ℝ) :
    harmonicPotential a 0 = 0
    source
    theorem FD1D.harmonicPotential_succ (a : ℝ) (k : ℕ) :
    harmonicPotential a (k + 1) = harmonicPotential a k + 1 / (↑k + 1 + a)
    source
    theorem FD1D.node_harmonic_drift_identity (a N p q : ℝ) (hNa : N + a ≠ 0) (hNa1 : N + a + 1 ≠ 0) :
    p * (1 - q) / (N + a + 1) - q * (1 - p) / (N + a) = (p - q) / (N + a) - p * (1 - q) / ((N + a) * (N + a + 1))

    Exact drift of one node under an independent deletion and arrival.

    source
    theorem FD1D.node_remainder_le {a N p q h : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) (hq1 : q ≤ 1) (hNa : 0 < N + a) (hmajor : p ≤ (N + a) * h) :
    0 ≤ p ^ 3 * (1 - q) / ((N + a) * (N + a + 1)) ∧ p ^ 3 * (1 - q) / ((N + a) * (N + a + 1)) ≤ p * h ^ 2

    The remainder term is bounded by p h² using p ≤ (N+a)h.

    source
    theorem FD1D.stationary_hazard_bound {a L m H : ℝ} (ha : 0 < a) (hm : 0 < m) (hH : 0 ≤ H) (haL : 200 * L ≤ a) (hmain : (a / 100 - L) * H ≤ 103 * a / (300 * m ^ 2)) :
    H ≤ 206 / (3 * m ^ 2)

    The numerical core of the stationary hazard estimate. This is equation (11) after the deterministic Bellman lower bound and the stochastic remainder upper bound have been combined.

    source
    theorem FD1D.transient_hazard_bound {a L m T H logTerm : ℝ} (ha : 0 < a) (hm : 0 < m) (hT : 0 < T) (hH : 0 ≤ H) (haL : 200 * L ≤ a) (hlogA : 200 * logTerm ≤ a) (hmain : (a / 100 - L) * H ≤ 103 * a / (300 * m ^ 2) + logTerm / T) :
    H ≤ 206 / (3 * m ^ 2) + 1 / T

    Algebraic form of the transient averaged hazard estimate (12).

    source
    theorem FD1D.main_horizon_long_enough {m N : ℕ} (hm : 1 ≤ m) (hN : 2 * m ^ 2 ≤ N) :
    m ^ 2 ≤ N - m

    The initialization-period arithmetic used in the final horizon bound.

    source
    theorem FD1D.initialization_average_bound {a m N mainCost : ℝ} (ha : 1 ≤ a) (hm : 0 < m) (hN : m ^ 2 ≤ N) (hmain : mainCost ≤ 6 * a / m) :
    m / N + mainCost ≤ 7 * a / m

    Adding at most m initialization cost preserves the advertised constant.