CompensatedAdaptiveSupport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual integral histories pass the constructed adaptive split tests

def OAI.Ostmann.compensatedAdaptiveResidueSplit line 13
def OAI.Ostmann.compensatedAdaptiveData line 26
theorem OAI.Ostmann.compensatedAdaptiveData_frequencies line 36

theorem OAI.Ostmann.compensatedAdaptiveData_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 compensatedAdaptiveData_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.compensatedValid D U)
    (j : ℕ) (hj : j < 2 ^ n - 1) :
    singleArithmeticSplitTest
      (compensatedAdaptiveData 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.compensatedAdaptiveData, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.actualSplitValues

theorem OAI.Ostmann.compensatedAdaptiveData_actual_support line 107

Source documentation

The entire original residue tuple remains in the arithmetic support.

theorem compensatedAdaptiveData_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.compensatedValid D U) :
    singleArithmeticLeafSupport n (compensatedAdaptiveData n R k D U hs hsR) a.residue = 1 := by
…

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