OAI/NumberTheory/Ostmann/Construction/ModularAdaptiveSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.modularAdaptiveResidueSplit line 13
2. def OAI.Ostmann.modularAdaptiveData line 26
3. theorem OAI.Ostmann.modularAdaptiveData_frequencies line 36
4. theorem OAI.Ostmann.modularAdaptiveData_actual_test line 49

   Source documentation

   A valid actual history passes every test. The coefficients in that test were constructed using only the root product and the preceding split prefix.

   theorem modularAdaptiveData_actual_test (n R k : ℕ)
       (D : PivotDependencyScheme (2 ^ n - 1)) (U : Fin (2 ^ n - 1) → ℤ)
       (hU : ∀ i, IsCoprime (U i) (R : ℤ))
       (hdepth : ∀ i, D.depth i ≤ k) (hs : ∀ i, (D.frequencies i).root ≠ 0)
       (hsR : ∀ i, (D.frequencies i).root.natAbs ∣ R)
       (a : SampledPivotHistory n (R ^ (k + 2))) (ha : a.modularValid D R k U)
       (j : ℕ) (hj : j < 2 ^ n - 1) :
       singleArithmeticSplitTest
         (modularAdaptiveData n R k D U hs hsR (treeLeafProduct n a.residue)
           ((actualSplitValues n a.residue).take j).reverse)
         ((actualSplitValues n a.residue).getD j 1) := by
   …

   Mentions: OAI.Ostmann.PivotDependencyScheme, OAI.Ostmann.SampledPivotHistory, OAI.Ostmann.singleArithmeticSplitTest, OAI.Ostmann.modularAdaptiveData, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.actualSplitValues

5. theorem OAI.Ostmann.modularAdaptiveData_actual_support line 111

   Source documentation

   The entire original residue tuple remains in the arithmetic support.

   theorem modularAdaptiveData_actual_support (n R k : ℕ) [NeZero (R ^ (k + 2))]
       (D : PivotDependencyScheme (2 ^ n - 1)) (U : Fin (2 ^ n - 1) → ℤ)
       (hU : ∀ i, IsCoprime (U i) (R : ℤ))
       (hdepth : ∀ i, D.depth i ≤ k) (hs : ∀ i, (D.frequencies i).root ≠ 0)
       (hsR : ∀ i, (D.frequencies i).root.natAbs ∣ R)
       (a : SampledPivotHistory n (R ^ (k + 2))) (ha : a.modularValid D R k U) :
       singleArithmeticLeafSupport n (modularAdaptiveData n R k D U hs hsR) a.residue = 1 := by
   …

   Mentions: OAI.Ostmann.PivotDependencyScheme, OAI.Ostmann.SampledPivotHistory, OAI.Ostmann.singleArithmeticLeafSupport, OAI.Ostmann.modularAdaptiveData