OAI/NumberTheory/Ostmann/Arithmetic/FrequencyModelPairSupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.frequencyModelPairData line 12
2. theorem OAI.Ostmann.frequencyModelPairData_frequencies line 25
3. theorem OAI.Ostmann.frequencyModelPairData_support line 56

   Source documentation

   The same tuple of bulk residues tests both histories, under the original unit law. Only the two frequency gates are hypotheses.

   theorem frequencyModelPairData_support {σ : Type*} (value : σ → ℕ)
       (S : Finset ℤ) (n R : ℕ) [NeZero (R ^ (n - 1 + 2))] (t : FrequencyTree (S × S) n)
       (hS : ∀ s ∈ S, s ≠ 0) (hR : ∀ b (j : Fin (2 ^ n - 1)),
       (singleTreeNodeFrequencies S n (frequencyPairProjection S n b t) j.val).root.natAbs ∣ R)
       (small : Bool → TreeLeafTuple (List σ) n) (bulk : TreeLeafTuple (List σ) n)
       (a : Bool → 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 : ∀ b, movingFrequencyGate value R
         (buildMovingSlotData n
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.singleTreeNodeFrequencies, OAI.Ostmann.frequencyPairProjection, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.treeIntegerResidues, OAI.Ostmann.treeLeafMap, OAI.Ostmann.movingSlotValues, OAI.Ostmann.movingFrequencyGate, OAI.Ostmann.buildMovingSlotData