AdaptivePivotSupport.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Actual integral histories pass the constructed adaptive split tests

def OAI.Ostmann.adaptivePivotResidueSplit line 12
def OAI.Ostmann.adaptivePivotData line 25
theorem OAI.Ostmann.adaptivePivotData_frequencies line 35
theorem OAI.Ostmann.SampledPivotHistory.matches_actual line 46

theorem OAI.Ostmann.adaptivePivotData_actual_test line 56

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 adaptivePivotData_actual_test (n R k : ℕ)
    (D : PivotDependencyScheme (2 ^ n - 1))
    (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.valid D)
    (j : ℕ) (hj : j < 2 ^ n - 1) :
    singleArithmeticSplitTest
      (adaptivePivotData n R k D 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.adaptivePivotData, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.actualSplitValues

theorem OAI.Ostmann.adaptivePivotData_actual_support line 110

Source documentation

The entire original residue tuple remains in the arithmetic support.

theorem adaptivePivotData_actual_support (n R k : ℕ) [NeZero (R ^ (k + 2))]
    (D : PivotDependencyScheme (2 ^ n - 1))
    (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.valid D) :
    singleArithmeticLeafSupport n (adaptivePivotData n R k D hs hsR) a.residue = 1 := by
…

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