OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternFrozenMultiplier.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingPatternFeasible line 12
2. theorem OAI.Ostmann.movingPatternFlagProduct_eq line 23

   Source documentation

   The only value-dependent part of the symbolic factor is one reciprocal prime per class. All feasibility decisions are formal polynomial identities.

   theorem movingPatternFlagProduct_eq {A B C : Type*} [Fintype C] {N : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (prime : A → ℕ)
       (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}) (x : Fin (N + 1) → A) :
       movingPatternFlagProduct e prime n t small bulk pattern rep x =
         if movingPatternFeasible e n t small bulk pattern rep then
           ∏ c : C, ((prime (x (e.symm (.inr c))) : ℝ)⁻¹ : ℂ) else 0 := by
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingPatternFlagProduct, OAI.Ostmann.movingPatternFeasible

3. theorem OAI.Ostmann.movingPatternFlagProduct_congr line 43
4. theorem OAI.Ostmann.movingPatternFlagProduct_bulk_frozen line 56

   Source documentation

   In the exact Fubini decomposition of the original law, these factors belong wholly to the fixed nonbulk coefficient.

   theorem movingPatternFlagProduct_bulk_frozen {A B C : Type*} [Fintype C] {N n m : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (prime : A → ℕ)
       (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)
       (rep : ∀ c, {i : Bool × MovingSampleIndex n // pattern i = c})
       (x y : TreeLeafIndex n × Fin m → A)
       (a : {i : Fin (N + 1) // i ∉ Set.range (movingPatternBulkEmbedding e slot)} → A) :
       movingPatternFlagProduct e prime n t small (movingPatternBulkLeaves n m slot perm) pattern rep
           (joinBulkNonbulk (movingPatternBulkEmbedding e slot) x a) =
         movingPatternFlagProduct e prime n t small (movingPatternBulkLeaves n m slot perm) pattern rep
           (joinBulkNonbulk (movingPatternBulkEmbedding e slot) y a) := by
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingPatternBulkEmbedding, OAI.Ostmann.movingPatternFlagProduct, OAI.Ostmann.movingPatternBulkLeaves, OAI.Ostmann.joinBulkNonbulk

5. theorem OAI.Ostmann.movingPairCompensatedMass_bulk_frozen line 75