MovingPrimePatternFrozenMultiplier.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Original bulk law for the two-prime symbolic factors

def OAI.Ostmann.movingPrimePatternFeasible line 11

theorem OAI.Ostmann.movingPatternPrimeFlagProduct_eq line 22

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 movingPatternPrimeFlagProduct_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) :
    movingPatternPrimeFlagProduct e prime n t small bulk pattern rep x =
      if movingPrimePatternFeasible e n t small bulk pattern rep then
        ∏ c : C, (internalLineScalar false (prime (x (e.symm (.inr c)))) : ℂ) else 0 := by
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingPatternPrimeFlagProduct, OAI.Ostmann.movingPrimePatternFeasible, OAI.Ostmann.internalLineScalar

theorem OAI.Ostmann.movingPatternPrimeFlagProduct_congr line 42

theorem OAI.Ostmann.movingPatternPrimeFlagProduct_bulk_frozen line 55

Source documentation

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

theorem movingPatternPrimeFlagProduct_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) :
    movingPatternPrimeFlagProduct e prime n t small (movingPatternBulkLeaves n m slot perm) pattern rep
        (joinBulkNonbulk (movingPatternBulkEmbedding e slot) x a) =
      movingPatternPrimeFlagProduct 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.movingPatternPrimeFlagProduct, OAI.Ostmann.movingPatternBulkLeaves, OAI.Ostmann.joinBulkNonbulk