MovingPatternBulkBudgets.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Concrete length and frequency budgets for the original pattern pair

theorem OAI.Ostmann.movingLeafLengthLE_map line 12
theorem OAI.Ostmann.bulkSlotLeaves_length line 19
theorem OAI.Ostmann.movingPatternFinBulkData_size line 30
theorem OAI.Ostmann.movingPatternFinBulkData_regular_length line 43
theorem OAI.Ostmann.movingPatternFinBulkData_follows line 56
theorem OAI.Ostmann.MovingSlotData.Follows.frequencies_iff line 66
Source documentation
The literal frequency list controls every actual formula-node frequency.
```
theorem MovingSlotData.Follows.frequencies_iff {A : Type*} {n : ℕ}
    {T : MovingSlotData A n} {t : FrequencyTree ℤ n} (h : T.Follows t) (P : ℤ → Prop) :
    T.Frequencies P ↔ ∀ s ∈ allFrequencyList n t, P s := by
…
```
Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.allFrequencyList

theorem OAI.Ostmann.movingPatternFinBulkData_frequencies line 82

Source documentation

Frequency bounds are taken from the original histories, not from an additional assumption on each pattern realization.

theorem movingPatternFinBulkData_frequencies {B C : Type*} {N n m : ℕ}
    (e : Fin (N + 1) ≃ B ⊕ C) (t : Bool → FrequencyTree ℤ n)
    (small : Bool → TreeLeafTuple (List B) n) (slot : (TreeLeafIndex n × Fin m) ↪ B)
    (perm : Equiv.Perm (TreeLeafIndex n × Fin m))
    (pattern : Bool × MovingSampleIndex n → C) (P : ℤ → Prop)
    (hP : ∀ b, ∀ s ∈ allFrequencyList n (t b), P s) (b : Bool) :
    (movingPatternFinBulkData e n m t small slot perm pattern b).Frequencies P :=
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.allFrequencyList, OAI.Ostmann.movingPatternFinBulkData