Documentation

LeanPool.FullyDynamicMatching.FD1D.V5.Balanced

Balanced initial count laws for every inventory size #

For arbitrary m, divisibility by the leaf count need not hold. We avoid that restriction by taking the uniform law on the finite set of global maximizers of the harmonic tree potential. Child-subtree swaps preserve the potential, so this law is tree invariant. Its initial expected potential is maximal, which removes the endpoint term from the finite-horizon energy telescope.

source
theorem FD1D.V5.Balanced.statePotential_inventorySwap {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) (a : ℝ) (x : InventoryState (DyadicNode L) m) :
Dynamics.statePotential a ((TreeSymmetry.inventorySwap hdL v) x) = Dynamics.statePotential a x

Swapping two child subtrees preserves the V5 harmonic tree potential.

The invariant law on potential maximizers #

source
noncomputable def FD1D.V5.Balanced.potentialMaximizers (L m : ℕ) (a : ℝ) :
Finset (InventoryState (DyadicNode L) m)

All count states attaining the largest V5 tree potential.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem FD1D.V5.Balanced.mem_potentialMaximizers_iff {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) :
    x ∈ potentialMaximizers L m a ↔ ∀ (y : InventoryState (DyadicNode L) m), Dynamics.statePotential a y ≤ Dynamics.statePotential a x
    source
    theorem FD1D.V5.Balanced.potentialMaximizers_nonempty (L m : ℕ) (a : ℝ) :
    (potentialMaximizers L m a).Nonempty
    source
    noncomputable def FD1D.V5.Balanced.law (L m : ℕ) (a : ℝ) :
    FiniteLaw (InventoryState (DyadicNode L) m)

    Uniform probability law on the finite set of potential maximizers.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem FD1D.V5.Balanced.law_mass (L m : ℕ) (a : ℝ) (x : InventoryState (DyadicNode L) m) :
      (law L m a).mass x = if x ∈ potentialMaximizers L m a then 1 / ↑(potentialMaximizers L m a).card else 0
      source
      theorem FD1D.V5.Balanced.lawInvariant_inventorySwap {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) (a : ℝ) :
      FiniteKernel.LawInvariant (law L m a) (TreeSymmetry.inventorySwap hdL v)

      The maximizer law is invariant under every child-subtree swap.

      source
      theorem FD1D.V5.Balanced.statePotential_le_law_expect (L m : ℕ) (a : ℝ) (x : InventoryState (DyadicNode L) m) :
      Dynamics.statePotential a x ≤ (law L m a).expect (Dynamics.statePotential a)

      Every state potential is bounded by the maximizer law's expectation.

      All-horizon energy and squared-cost bounds #

      source
      theorem FD1D.V5.Balanced.finite_transport_energy_estimate_of_maximal_potential {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (haL : 2000 * ↑L ≤ a) (mu0 : FiniteLaw (InventoryState (DyadicNode L) m)) (hmax : ∀ (x : InventoryState (DyadicNode L) m), Dynamics.statePotential a x ≤ mu0.expect (Dynamics.statePotential a)) (T : ℕ) (hT : 0 < T) :
      (∑ t ∈ Finset.range T, ((Dynamics.kernel a ha hm).iterate t mu0).expect (Dynamics.stateTransportEnergy a)) / ↑T ≤ 501 * a ^ 2 / ↑m ^ 2

      The V5 master-energy estimate has no endpoint penalty when the initial expected potential globally majorizes every state potential.

      source
      theorem FD1D.V5.Balanced.law_finite_transport_energy_estimate {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (haL : 2000 * ↑L ≤ a) (T : ℕ) (hT : 0 < T) :
      (∑ t ∈ Finset.range T, ((Dynamics.kernel a ha hm).iterate t (law L m a)).expect (Dynamics.stateTransportEnergy a)) / ↑T ≤ 501 * a ^ 2 / ↑m ^ 2

      The maximizer law has the stationary-strength transport bound for every horizon.

      source
      theorem FD1D.V5.Balanced.law_average_rms_squaredCostEnvelope_le {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (haL : 2000 * ↑L ≤ a) (T : ℕ) (hT : 0 < T) :
      √((∑ t ∈ Finset.range T, ((Dynamics.kernel a ha hm).iterate t (law L m a)).expect (Transport.stateSquaredCostEnvelope a)) / ↑T) ≤ dyadicCellWidth L + √(1 / 12 * (501 * a ^ 2 / ↑m ^ 2))

      Count-envelope RMS bound from the balanced maximizer law.

      source
      noncomputable def FD1D.V5.Balanced.parameterizedLaw (m : ℕ) :
      FiniteLaw (InventoryState (DyadicNode (treeDepth m)) m)

      The manuscript-parameter balanced initial count law.

      Equations
      Instances For
        source
        theorem FD1D.V5.Balanced.parameterizedLaw_average_rms_squaredCostEnvelope_le {m T : ℕ} (hm : 1 ≤ m) (hT : 0 < T) :
        √((∑ t ∈ Finset.range T, ((parameterizedKernel m hm).iterate t (parameterizedLaw m)).expect (parameterizedSquaredCostEnvelope m)) / ↑T) ≤ (2 + √(501 / 12)) * ↑(parameterA m) / ↑m

        Balanced-initial-inventory corollary: for every positive horizon, the RMS count-state squared-cost envelope has the stationary constant 2 + sqrt(501/12).