Documentation

LeanPool.FullyDynamicMatching.FD1D.UniformArrival

Uniform Arrival #

Uniform continuous arrivals and dyadic leaf labels #

This module identifies a uniform point of [0,1] with its depth-L dyadic leaf. The continuous arrival law pushes forward to the uniform finite law on DyadicNode L, and the point lies in the closed cell certified by its selected label.

source
def FD1D.DyadicMass.constantLeafMass (L : ℕ) :
ℝ → DyadicMass L

A complete depth-L mass tree whose leaves all have mass c.

Equations
Instances For
    source
    @[simp]
    theorem FD1D.DyadicMass.leafMass_constantLeafMass (L : ℕ) (c : ℝ) (i : DyadicNode L) :
    (constantLeafMass L c).leafMass i = c
    source
    @[simp]
    theorem FD1D.DyadicMass.total_constantLeafMass (L : ℕ) (c : ℝ) :
    (constantLeafMass L c).total = ↑(2 ^ L) * c
    source
    theorem FD1D.DyadicMass.allNonneg_constantLeafMass (L : ℕ) {c : ℝ} (hc : 0 ≤ c) :
    (constantLeafMass L c).allNonneg
    source
    noncomputable def FD1D.DyadicMass.uniformArrivalMass (L : ℕ) :
    DyadicMass L

    The depth-L dyadic mass with mass 1 / 2^L at every leaf.

    Equations
    Instances For
      source
      @[simp]
      theorem FD1D.DyadicMass.uniformArrivalMass_leafMass (L : ℕ) (i : DyadicNode L) :
      (uniformArrivalMass L).leafMass i = 1 / ↑(2 ^ L)
      source
      theorem FD1D.DyadicMass.uniformArrivalMass_isProbability (L : ℕ) :
      (uniformArrivalMass L).IsProbability
      source
      @[simp]
      theorem FD1D.DyadicMass.uniformArrivalMass_piecewiseCDF (L : ℕ) {z : ℝ} (hz : z ∈ Set.Icc 0 1) :
      (uniformArrivalMass L).piecewiseCDF z = z
      source
      @[simp]
      theorem FD1D.DyadicMass.uniformArrivalMass_quantile (L : ℕ) {u : ℝ} (hu : u ∈ Set.Icc 0 1) :
      (uniformArrivalMass L).quantile u = u
      source
      noncomputable def FD1D.DyadicMass.uniformArrivalLeaf (L : ℕ) (u : ℝ) :
      DyadicNode L

      The dyadic label assigned to the continuous arrival coordinate u.

      Equations
      Instances For
        source
        noncomputable def FD1D.DyadicMass.uniformArrivalLeafLaw (L : ℕ) :
        FiniteLaw (DyadicNode L)

        The finite pushforward law of the selected uniform-arrival label.

        Equations
        Instances For
          source
          theorem FD1D.DyadicMass.uniformArrivalLeafLaw_eq_uniform (L : ℕ) :
          uniformArrivalLeafLaw L = FiniteLaw.uniform

          A continuous uniform arrival induces the uniform law on depth-L leaves.

          source
          theorem FD1D.DyadicMass.uniformArrival_mem_dyadicCell (L : ℕ) {u : ℝ} (hu : u ∈ Set.Icc 0 1) :
          u ∈ dyadicCell (uniformArrivalLeaf L u)

          Every arrival in [0,1] lies in the closed cell carrying its label.

          source
          theorem FD1D.DyadicMass.uniformArrival_mem_dyadicCell_ae (L : ℕ) :
          ∀ᵐ (u : ℝ) ∂uniformDemand, u ∈ dyadicCell (uniformArrivalLeaf L u)

          Under Lebesgue-uniform demand on [0,1], the continuous arrival and its finite label are almost surely compatible with the certified dyadic cell.