OAI/NumberTheory/Ostmann/Arithmetic/SequentialActualSupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Passing all actual preorder node tests retains the whole support weight

  1. theorem OAI.Ostmann.sequentialSupport_eq_one_of_prefix line 12
  2. theorem OAI.Ostmann.singleArithmeticLeafSupport_eq_one_of_actual_tests line 30

    Source documentation

    The support is evaluated on the original leaf tuple. Its tests are checked at the actual parent/child product splits, in their true order.

    theorem singleArithmeticLeafSupport_eq_one_of_actual_tests {Q : ℕ} [NeZero Q]
    (n : ℕ) (data : (ZMod Q)ˣ → List (ZMod Q)ˣ → Option (ArithmeticSplitData Q))
    (x : TreeLeafTuple (ZMod Q)ˣ n)
    (htest : ∀ j < 2 ^ n - 1,
      singleArithmeticSplitTest
        (data (treeLeafProduct n x) (((actualSplitValues n x).take j).reverse))
        ((actualSplitValues n x).getD j 1)) :
    singleArithmeticLeafSupport n data x = 1 := by
…

    Mentions: OAI.Ostmann.ArithmeticSplitData, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.singleArithmeticSplitTest, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.actualSplitValues, OAI.Ostmann.singleArithmeticLeafSupport