MovingSampleSlots.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Labelled four-slot samples and the concrete occurrence paths

inductive OAI.Ostmann.MovingSampleSlots line 13
Source documentation
The same sampler as MovingGiantSamples, before the prime labels have been evaluated. Four actual positions are used at each child leaf.
```
inductive MovingSampleSlots (σ : Type*) : ℕ → Type _
  | leaf : MovingSampleSlots σ 0
  | node {n : ℕ} (samples : TreeLeafTuple (Fin 4 → σ) n)
      (left right : MovingSampleSlots σ n) : MovingSampleSlots σ (n + 1)
```
Mentions: OAI.Ostmann.TreeLeafTuple
def OAI.Ostmann.movingCompensationSlots line 18
def OAI.Ostmann.flattenMovingSlots line 23
def OAI.Ostmann.appendMovingSlotLeaves line 27
theorem OAI.Ostmann.flattenMovingSlots_append_bound line 32
def OAI.Ostmann.MovingSampleSlots.Levels line 49

def OAI.Ostmann.buildMovingSlotData line 58

Source documentation

This carries the source's compensation product into both child regular lists while retaining the per-leaf distribution of the four samples.

def buildMovingSlotData {σ : Type*} : (n : ℕ) → FrequencyTree ℤ n →
    TreeLeafTuple (List σ) n → TreeLeafTuple (List σ) n →
    MovingSampleSlots σ n → MovingSlotData σ n
  | 0, t, small, bulk, .leaf =>
      .leaf (frequencyRoot 0 t) (flattenMovingSlots 0 small ++ flattenMovingSlots 0 bulk)
  | n + 1, t, small, bulk, .node samples left right =>
      let u := movingCompensationSlots n samples
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.MovingSlotData, OAI.Ostmann.frequencyRoot, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.movingCompensationSlots

theorem OAI.Ostmann.buildMovingSlotData_levels line 72

theorem OAI.Ostmann.buildMovingSlotData_occurrence_absent line 113

Source documentation

Omission is now a proved fact of the actual sample constructor.

theorem buildMovingSlotData_occurrence_absent {σ : Type*} (tier : σ → ℕ) (n : ℕ)
    (t : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n)
    (samples : MovingSampleSlots σ n)
    (hsmall : ∀ i ∈ flattenMovingSlots n small, n ≤ tier i)
    (hbulk : ∀ i ∈ flattenMovingSlots n bulk, n ≤ tier i)
    (hsamples : samples.Levels tier) (o : MovingSlotOccurrence σ)
    (ho : o ∈ (buildMovingSlotData n t small bulk samples).occurrences)
    (i : σ) (hi : tier i < o.level) :
    (∀ s ∈ o.path, i ∉ s.leftSlots ∧ i ∉ s.rightSlots ∧ i ∉ s.compensationSlots) ∧
      i ∉ o.current.leftSlots ∧ i ∉ o.current.rightSlots := by
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.MovingSlotOccurrence, OAI.Ostmann.buildMovingSlotData