OAI/NumberTheory/Ostmann/Arithmetic/FrequencyModelAdaptiveSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.frequencyModelHistory line 11
2. theorem OAI.Ostmann.frequencyModelHistory_valid line 23
3. def OAI.Ostmann.frequencyModelAdaptiveData line 40
4. theorem OAI.Ostmann.frequencyModelAdaptiveData_frequencies line 52
5. theorem OAI.Ostmann.frequencyModelAdaptiveData_support line 70

   Source documentation

   Every residue tuple accepted by the existing frequency gate lies in the constructed sequential support. No prime-line or integer-integrality test has been reintroduced.

   theorem frequencyModelAdaptiveData_support {σ : Type*} (value : σ → ℕ)
       (S : Finset ℤ) (n R : ℕ) [NeZero (R ^ (n - 1 + 2))] (t : FrequencyTree S n)
       (hS : ∀ s ∈ S, s ≠ 0) (hR : ∀ j : Fin (2 ^ n - 1), (singleTreeNodeFrequencies S n t j.val).root.natAbs ∣ R)
       (small bulk : TreeLeafTuple (List σ) n) (a : MovingSampleSlots σ n) (x y : ℤ)
       (hsmall : ∀ i, IsCoprime (value i : ℤ) (R : ℤ))
       (z : TreeLeafTuple (ZMod (R ^ (n - 1 + 2)))ˣ n)
       (hz : treeIntegerResidues (R ^ (n - 1 + 2)) n
         (treeLeafMap (fun q : ℕ => (q : ℤ)) n (movingSlotValues value n bulk)) z)
       (hg : movingFrequencyGate value R
         (buildMovingSlotData n (frequencyTreeMap Subtype.val n t) small bulk a) x y) :
       singleArithmeticLeafSupport n
         (frequencyModelAdaptiveData value S n R t hS hR small a x y) z = 1 := by
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.singleTreeNodeFrequencies, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.treeIntegerResidues, OAI.Ostmann.treeLeafMap, OAI.Ostmann.movingSlotValues, OAI.Ostmann.movingFrequencyGate, OAI.Ostmann.buildMovingSlotData, OAI.Ostmann.frequencyTreeMap, OAI.Ostmann.singleArithmeticLeafSupport, OAI.Ostmann.frequencyModelAdaptiveData