OAI/NumberTheory/Ostmann/Construction/HistoryResidueData.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.historyResidueSplit line 15

   Source documentation

   The root frequency and its divisibility are supplied by the actual history, rather than by a hypothesis on an arbitrary arithmetic record.

   def historyResidueSplit (S : Finset ℤ) (hS : ∀ s ∈ S, s ≠ 0)
       (n k : ℕ) (t : FrequencyTree S n) (j : ℕ) (hj : j < 2 ^ n - 1)
       (A B : ZMod (historyFrequencyModulus S n k t))
       (P : (ZMod (historyFrequencyModulus S n k t))ˣ) :
       ArithmeticResidueSplit (historyFrequencyModulus S n k t) where
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.historyFrequencyModulus, OAI.Ostmann.ArithmeticResidueSplit

2. def OAI.Ostmann.historyResidueData line 35

   Source documentation

   Coefficients may use the total product and the exposed split prefix. They cannot inspect a future split coordinate. Invalid unit coefficients are rejected by the exact toData test.

   noncomputable def historyResidueData (S : Finset ℤ) (hS : ∀ s ∈ S, s ≠ 0)
       (n k : ℕ) (t : FrequencyTree S n)
       (A B : (ZMod (historyFrequencyModulus S n k t))ˣ →
         List (ZMod (historyFrequencyModulus S n k t))ˣ → ZMod (historyFrequencyModulus S n k t))
       (P : (ZMod (historyFrequencyModulus S n k t))ˣ →
         List (ZMod (historyFrequencyModulus S n k t))ˣ → (ZMod (historyFrequencyModulus S n k t))ˣ)
       (total : (ZMod (historyFrequencyModulus S n k t))ˣ)
       (past : List (ZMod (historyFrequencyModulus S n k t))ˣ) :
       Option (ArithmeticSplitData (historyFrequencyModulus S n k t)) :=
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.historyFrequencyModulus, OAI.Ostmann.ArithmeticSplitData

3. theorem OAI.Ostmann.historyResidueData_frequencies line 48
4. theorem OAI.Ostmann.historyResidueData_test line 63