Documentation

LeanPool.FullyDynamicMatching.FD1D.V5.ContinuousState

Continuous State #

Continuous coordinate state #

The spatial state records only the live coordinates. Their dyadic labels are recovered deterministically, so replacing one coordinate updates the exact spatial configuration and its finite count projection pathwise.

source
@[reducible, inline]
abbrev FD1D.V5.SpatialState (m : ℕ) :
Type

The m labeled live supply coordinates in the unit interval.

Equations
Instances For
    source
    noncomputable def FD1D.V5.spatialLeaves {m : ℕ} (L : ℕ) (s : SpatialState m) :
    Fin m → DyadicNode L

    The dyadic leaf assigned to each coordinate of a spatial state.

    Equations
    Instances For
      source
      noncomputable def FD1D.V5.toConfiguration {m : ℕ} (L : ℕ) (s : SpatialState m) :
      SupplyConfiguration L m

      Convert a coordinate state to its certified spatial configuration.

      Equations
      Instances For
        source
        @[simp]
        theorem FD1D.V5.toConfiguration_location {m : ℕ} (L : ℕ) (s : SpatialState m) (j : Fin m) :
        (toConfiguration L s).location j = ↑(s j)
        source
        @[simp]
        theorem FD1D.V5.toConfiguration_leaf {m : ℕ} (L : ℕ) (s : SpatialState m) (j : Fin m) :
        (toConfiguration L s).leaf j = spatialLeaves L s j
        source
        noncomputable def FD1D.V5.spatialCount {m : ℕ} (L : ℕ) (s : SpatialState m) :
        InventoryState (DyadicNode L) m

        The finite inventory-count projection of a coordinate state.

        Equations
        Instances For
          source
          @[simp]
          theorem FD1D.V5.toConfiguration_countState {m : ℕ} (L : ℕ) (s : SpatialState m) :
          (toConfiguration L s).countState = spatialCount L s

          Measurable projections #

          source
          theorem FD1D.V5.spatialState_eval_measurable {m : ℕ} (j : Fin m) :
          Measurable fun (s : SpatialState m) => s j
          source
          theorem FD1D.V5.spatialCoordinate_measurable {m : ℕ} (j : Fin m) :
          Measurable fun (s : SpatialState m) => ↑(s j)
          source
          theorem FD1D.V5.spatialLeaf_measurable {m : ℕ} (L : ℕ) (j : Fin m) :
          Measurable fun (s : SpatialState m) => spatialLeaves L s j
          source
          theorem FD1D.V5.spatialLeaves_measurable {m : ℕ} (L : ℕ) :
          Measurable (spatialLeaves L)
          source
          theorem FD1D.V5.spatialCount_measurable {m : ℕ} (L : ℕ) :
          Measurable (spatialCount L)

          Selected labels and coordinate update #

          source
          noncomputable def FD1D.V5.spatialSelectedLabel {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (s : SpatialState m) (u : ↑unitInterval) :
          Fin m

          The concrete supply label selected from a coordinate state.

          Equations
          Instances For
            source
            theorem FD1D.V5.spatialSelectedLabel_measurable {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) :
            Measurable fun (p : SpatialState m × ↑unitInterval) => spatialSelectedLabel L a fallback p.1 p.2

            Joint measurability of the selected label in state and demand.

            source
            theorem FD1D.V5.spatialSelectedLabel_demand_measurable {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (s : SpatialState m) :
            Measurable fun (u : ↑unitInterval) => spatialSelectedLabel L a fallback s u
            source
            noncomputable def FD1D.V5.spatialStep {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (s : SpatialState m) (z : ↑unitInterval × ↑unitInterval) :
            SpatialState m

            Replace the selected supply coordinate by a replenishment coordinate. The noise pair consists of demand first and replenishment second.

            Equations
            Instances For
              source
              @[simp]
              theorem FD1D.V5.toConfiguration_spatialStep {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (s : SpatialState m) (z : ↑unitInterval × ↑unitInterval) :
              toConfiguration L (spatialStep L a fallback s z) = Dynamics.actualStep a (toConfiguration L s) fallback ↑z.1 ↑z.2 ⋯

              Coordinate update and actualStep are the same certified configuration.

              source
              @[simp]
              theorem FD1D.V5.spatialCount_spatialStep {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (s : SpatialState m) (z : ↑unitInterval × ↑unitInterval) :
              spatialCount L (spatialStep L a fallback s z) = (spatialCount L s).move (Dynamics.selectedDeletedLeaf a (toConfiguration L s) fallback ↑z.1) (DyadicMass.uniformArrivalLeaf L ↑z.2)

              The coordinate update projects to the corresponding finite leaf move.

              source
              theorem FD1D.V5.spatialCount_spatialStep_eq_selectedIndex {m : ℕ} (L : ℕ) (a : ℝ) (ha : 0 < a) (hm : 0 < m) (fallback : Fin m) (s : SpatialState m) (z : ↑unitInterval × ↑unitInterval) (hz : ↑z.1 ≠ 0) :
              spatialCount L (spatialStep L a fallback s z) = (spatialCount L s).move ((Dynamics.stateDyadicMass a (spatialCount L s)).selectedIndex ↑z.1) (DyadicMass.uniformArrivalLeaf L ↑z.2)

              Away from demand zero, the deleted leaf is the policy's selected index.

              source
              theorem FD1D.V5.spatialStep_measurable {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) :
              Measurable fun (p : SpatialState m × ↑unitInterval × ↑unitInterval) => spatialStep L a fallback p.1 p.2

              Joint measurability of one step in the state and its two noise inputs.

              source
              theorem FD1D.V5.spatialStep_noise_measurable {m : ℕ} (L : ℕ) (a : ℝ) (fallback : Fin m) (s : SpatialState m) :
              Measurable (spatialStep L a fallback s)