OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternBulkArithmetic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingPattern_supported_arithmetic line 14

   Source documentation

   The original pattern's Page and spectator factors separate on precisely its selected bulk residues. The unchanged small and sampled data, denominator independence and regular-list distinctness are derived from the constructor.

   theorem movingPattern_supported_arithmetic {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)
       (F : Bool → {k : ℕ} → MovingSlotData (Fin (N + 1)) k → ℤ → ℂ)
       (E : 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.MovingSlotData

2. theorem OAI.Ostmann.movingPattern_arithmetic_collision_gate line 73

   Source documentation

   Bulk collisions are already zero under the original pattern coefficient, so inserting the distinctness indicator precedes all changes of measure.

   theorem movingPattern_arithmetic_collision_gate {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)
       (value : Fin (N + 1) → ℕ) (hprime : ∀ i, (value i).Prime)
       (outside : List ℕ)
       (F : Bool → {k : ℕ} → MovingSlotData (Fin (N + 1)) k → ℤ → ℂ)
       (E : Bool → {k : ℕ} → MovingSlotData (Fin (N + 1)) k → ℤ → ℤ → ℤ → ℝ)
       (nodes : Bool → List MovingFormulaNode) (R : ℤ) (r : ℕ) [NeZero r]
       (input : PublishedProgressionInput) (Q : ℕ) (y : ℝ) (A : ℂ) :
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingFormulaNode, OAI.Ostmann.PublishedProgressionInput