OAI/NumberTheory/Ostmann/Arithmetic/FrequencyModelValidity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.FrequencyModelState.compensation_coprime line 10
2. theorem OAI.Ostmann.FrequencyModelState.relation line 18
3. theorem OAI.Ostmann.FrequencyModelState.products_units line 42
4. theorem OAI.Ostmann.frequencyModel_modularEquations line 64
5. theorem OAI.Ostmann.frequencyModel_coefficient_units line 100

   Source documentation

   Unit factors are retained from the exact local frequency gates.

   theorem frequencyModel_coefficient_units {σ : Type*} (value : σ → ℕ) (R : ℕ)
       (S : Finset ℤ) (n : ℕ) (t : FrequencyTree S n)
       (small bulk : TreeLeafTuple (List σ) n) (a : MovingSampleSlots σ n) (x y : ℤ)
       (hsmall : ∀ i, IsCoprime (value i : ℤ) (R : ℤ))
       (hR : ∀ j : Fin (2 ^ n - 1), (singleTreeNodeFrequencies S n t j.val).root.natAbs ∣ R)
       (hg : movingFrequencyGate value R
         (buildMovingSlotData n (frequencyTreeMap Subtype.val n t) small bulk a) x y)
       (j : Fin (2 ^ n - 1)) :
       let T := buildMovingSlotData n (frequencyTreeMap Subtype.val n t) small bulk a
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.singleTreeNodeFrequencies, OAI.Ostmann.movingFrequencyGate, OAI.Ostmann.buildMovingSlotData, OAI.Ostmann.frequencyTreeMap