MovingPatternArithmeticData.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic support of the actual finite pattern trees

theorem OAI.Ostmann.movingPatternFinBulkData_regular_coherent line 11

theorem OAI.Ostmann.movingPatternFinBulkData_internal_cover line 21

Source documentation

Every compensation prime comes from an internal equality class. The strict level separation excludes all external regular slots.

theorem movingPatternFinBulkData_internal_cover {A B C : Type*} [Fintype C] {N n m : ℕ}
    (e : Fin (N + 1) ≃ B ⊕ C) (tierB : B → ℕ) (tierC : 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)
    (hB : ∀ j, n ≤ tierB j) (htier : ∀ i, tierC (pattern i) = movingSampleTier i.2)
    (value : A → ℕ) (x : Fin (N + 1) → A) :
    ∀ b, ∀ o ∈ (movingPatternFinBulkData e n m t small slot perm pattern b).occurrences,
      ∀ i ∈ o.current.compensationSlots,
        value (x i) ∈ Finset.univ.image (fun c : C => value (x (e.symm (.inr c)))) := by
…

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

theorem OAI.Ostmann.movingPatternFinBulkData_regular_product line 53

Source documentation

Both histories have the same top regular product. No sampled internal prime or history frequency enters this product.

theorem movingPatternFinBulkData_regular_product {B C : Type*} {N n m : ℕ}
    (e : Fin (N + 1) ≃ B ⊕ C) (t : Bool → FrequencyTree ℤ n)
    (small : TreeLeafTuple (List B) n) (slot : (TreeLeafIndex n × Fin m) ↪ B)
    (pattern : Bool × MovingSampleIndex n → C) (value : Fin (N + 1) → ℕ) (b : Bool) :
    MovingSlotReversal.naturalProduct value
      (movingPatternFinBulkData e n m t (fun _ => small) slot (Equiv.refl _) pattern b).regularSlots =
    MovingSlotReversal.naturalProduct value
      (flattenMovingSlots n (movingPatternFiniteSmall e n small) ++
        flattenMovingSlots n (bulkSlotLeaves n m (movingPatternBulkEmbedding e slot))) := by
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.MovingSlotReversal.naturalProduct, OAI.Ostmann.movingPatternFinBulkData, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.movingPatternFiniteSmall, OAI.Ostmann.bulkSlotLeaves, OAI.Ostmann.movingPatternBulkEmbedding