MovingRegularSlots.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The original regular slot lists in every moving child

def OAI.Ostmann.MovingSlotData.regularSlots line 11

Source documentation

Current regular slots, before sampling at this node.

def MovingSlotData.regularSlots {σ : Type*} : {n : ℕ} → MovingSlotData σ n → List σ
  | _, .leaf _ regular => regular
  | _, .node _ CL CR _ _ _ => CL ++ CR

/-- The child regular slots contain the same compensation vector and the
corresponding parent's regular slots, with their actual per-leaf allocation. -/

Mentions: OAI.Ostmann.MovingSlotData

def OAI.Ostmann.MovingSlotData.RegularCoherent line 17

Source documentation

The child regular slots contain the same compensation vector and the corresponding parent's regular slots, with their actual per-leaf allocation.

def MovingSlotData.RegularCoherent {σ : Type*} : {n : ℕ} → MovingSlotData σ n → Prop
  | _, .leaf _ _ => True
  | _, .node _ CL CR U left right =>
      left.regularSlots.Perm (U ++ CL) ∧ right.regularSlots.Perm (U ++ CR) ∧
        left.RegularCoherent ∧ right.RegularCoherent

Mentions: OAI.Ostmann.MovingSlotData

theorem OAI.Ostmann.flattenMovingSlots_append_perm line 23
theorem OAI.Ostmann.buildMovingSlotData_regular_perm line 37
theorem OAI.Ostmann.buildMovingSlotData_regular_coherent line 52
Source documentation
Coherence is proved for the actual sampler, not supplied as a new assumption about the original history.
```
theorem buildMovingSlotData_regular_coherent {σ : Type*} (n : ℕ) (t : FrequencyTree ℤ n)
    (small bulk : TreeLeafTuple (List σ) n) (samples : MovingSampleSlots σ n) :
    (buildMovingSlotData n t small bulk samples).RegularCoherent := by
…
```
Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.buildMovingSlotData