MovingSampleOccurrence.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

An actual occurrence for every internal sample class

theorem OAI.Ostmann.movingCompensationSlots_mem line 11
theorem OAI.Ostmann.movingSample_occurs line 24
Source documentation
Each independent draw has a genuine node occurrence in the constructed history; subsequent copies in regular lists are irrelevant to this witness.
```
theorem movingSample_occurs {A : Type*} (n : ℕ) (t : FrequencyTree ℤ n)
    (small bulk : TreeLeafTuple (List A) n) (a : MovingSampleSlots A n)
    (i : MovingSampleIndex n) :
    ∃ o ∈ (buildMovingSlotData n t small bulk a).occurrences,
      movingSampleCoordinates A n a i ∈ o.current.compensationSlots := by
…
```
Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.buildMovingSlotData, OAI.Ostmann.movingSampleCoordinates

theorem OAI.Ostmann.movingPattern_representative_nonempty line 58

Source documentation

A representative occurrence exists for every nonempty internal class of the actual paired pattern, without an extra arithmetic assumption.

theorem movingPattern_representative_nonempty {B C : Type*}
    (n : ℕ) (t : Bool → FrequencyTree ℤ n) (small bulk : Bool → TreeLeafTuple (List B) n)
    (pattern : Bool × MovingSampleIndex n → C)
    (rep : ∀ c, {i : Bool × MovingSampleIndex n // pattern i = c}) (c : C) :
    Nonempty (MovingPairRepresentativeOccurrences
      (fun side => movingPatternSlotData n (t side) (small side) (bulk side) pattern side) (.inr c)) := by
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.MovingPairRepresentativeOccurrences, OAI.Ostmann.movingPatternSlotData

def OAI.Ostmann.movingPatternRepresentative line 75