OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternTwoPrimeBulkIdentity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingPattern_two_prime_bulk_supported_identity line 14

   Source documentation

   An exact identity for every original prime tuple. Its bulk collision indicator is derived from the original regular-product support, before any prime replacement or change of normalization.

   theorem movingPattern_two_prime_bulk_supported_identity {B C I : Type*} [Fintype I] {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)
       (hsmall : ∀ b, ∀ i ∈ flattenMovingSlots n (small b), i ∉ Set.range slot)
       (hB : ∀ i, n ≤ tierB i) (htier : ∀ i, tierC (pattern i) = movingSampleTier i.2)
       (base value : Fin (N + 1) → ℕ)
       (hv : ∀ i ∉ Set.range (movingPatternBulkEmbedding e slot), value i = base i)
       (hprime : ∀ i, (value i).Prime) (childBound pivotBound : ℕ → ℕ)
       (hfreq : ∀ b, ∀ s ∈ allFrequencyList n (t b), s ≠ 0)
       (F : Bool → {k : ℕ} → MovingSlotData (Fin (N + 1)) k → ℤ → ℂ)
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.movingSampleTier, OAI.Ostmann.movingPatternBulkEmbedding, OAI.Ostmann.allFrequencyList, OAI.Ostmann.MovingSlotData