Documentation

LeanPool.FullyDynamicMatching.FD1D.V5.CostBounds

RMS matching-cost bounds for the v5 count chain #

This module combines the v5 energy estimates with squared quantile transport, discharges the parameter arithmetic, and records stationary, transient, and ordinary-convergence bounds for the count-state cost envelope.

source
theorem FD1D.V5.Transport.sqrt_average_stateSquaredCostEnvelope_le {L m : ℕ} (a : ℝ) (mu : ℕ → FiniteLaw (InventoryState (DyadicNode L) m)) (T : ℕ) (hT : 0 < T) (hinv : ∀ (t : ℕ) (d : Fin L) (v : DyadicNode ↑d), FiniteKernel.LawInvariant (mu t) (TreeSymmetry.inventorySwap ⋯ v)) :
√((∑ t ∈ Finset.range T, (mu t).expect (stateSquaredCostEnvelope a)) / ↑T) ≤ dyadicCellWidth L + √(1 / 12 * ((∑ t ∈ Finset.range T, (mu t).expect (Dynamics.stateTransportEnergy a)) / ↑T))

RMS transport for a uniform mixture of finite count laws. Each law may be different, but each must retain the child-subtree swap symmetries.

Parameterized count chain #

source
noncomputable def FD1D.V5.parameterizedKernel (m : ℕ) (hm : 1 ≤ m) :
FiniteKernel (InventoryState (DyadicNode (treeDepth m)) m)

Inventory transition kernel at the manuscript parameters determined by m.

Equations
Instances For
    source
    noncomputable def FD1D.V5.parameterizedTransportEnergy (m : ℕ) (x : InventoryState (DyadicNode (treeDepth m)) m) :
    ℝ

    Transport energy at the manuscript parameters determined by m.

    Equations
    Instances For
      source
      noncomputable def FD1D.V5.parameterizedSquaredCostEnvelope (m : ℕ) (x : InventoryState (DyadicNode (treeDepth m)) m) :
      ℝ

      Squared transport-cost envelope at the manuscript parameters.

      Equations
      Instances For
        source
        noncomputable def FD1D.V5.refreshedIterate (m : ℕ) (hm : 1 ≤ m) (t : ℕ) :
        FiniteLaw (InventoryState (DyadicNode (treeDepth m)) m)

        Inventory law after t steps starting from independently refreshed supply.

        Equations
        Instances For
          source
          theorem FD1D.V5.parameterizedKernel_irreducible {m : ℕ} (hm : 1 ≤ m) :
          (parameterizedKernel m hm).Irreducible
          source
          theorem FD1D.V5.parameterizedKernel_hasPositiveLoops {m : ℕ} (hm : 1 ≤ m) :
          (parameterizedKernel m hm).HasPositiveLoops
          source
          theorem FD1D.V5.stationary_sqrt_expected_squaredCostEnvelope_le {m : ℕ} (hm : 1 ≤ m) (pi : FiniteLaw (InventoryState (DyadicNode (treeDepth m)) m)) (hpi : (parameterizedKernel m hm).IsStationary pi) :
          √(pi.expect (parameterizedSquaredCostEnvelope m)) ≤ 17 / 2 * ↑(parameterA m) / ↑m

          The stationary count-state RMS envelope is strictly below 8.5 a/m.

          source
          theorem FD1D.V5.refreshed_average_rms_squaredCostEnvelope_le {m T : ℕ} (hm : 1 ≤ m) (hT : m ^ 2 ≤ T) :
          √((∑ t ∈ Finset.range T, (refreshedIterate m hm t).expect (parameterizedSquaredCostEnvelope m)) / ↑T) ≤ 17 / 2 * ↑(parameterA m) / ↑m

          The refreshed transient average RMS envelope is at most 8.5 a/m.

          Ordinary convergence from arbitrary count laws #

          source
          noncomputable def FD1D.V5.rmsSquaredCostExpectation (m : ℕ) (hm : 1 ≤ m) (mu0 : FiniteLaw (InventoryState (DyadicNode (treeDepth m)) m)) (t : ℕ) :
          ℝ

          Expected squared-cost envelope at time t from the chosen initial inventory law.

          Equations
          Instances For
            source
            theorem FD1D.V5.exists_stationary_rmsSquaredCost_tendsto {m : ℕ} (hm : 1 ≤ m) (mu0 : FiniteLaw (InventoryState (DyadicNode (treeDepth m)) m)) :
            ∃ (pi : FiniteLaw (InventoryState (DyadicNode (treeDepth m)) m)), (parameterizedKernel m hm).IsStationary pi ∧ Filter.Tendsto (rmsSquaredCostExpectation m hm mu0) Filter.atTop (nhds √(pi.expect (parameterizedSquaredCostEnvelope m))) ∧ √(pi.expect (parameterizedSquaredCostEnvelope m)) ≤ 17 / 2 * ↑(parameterA m) / ↑m
            source
            theorem FD1D.V5.limsup_rmsSquaredCostExpectation_le {m : ℕ} (hm : 1 ≤ m) (mu0 : FiniteLaw (InventoryState (DyadicNode (treeDepth m)) m)) :
            Filter.limsup (rmsSquaredCostExpectation m hm mu0) Filter.atTop ≤ 17 / 2 * ↑(parameterA m) / ↑m