OAI/NumberTheory/Ostmann/Arithmetic/SplitSampleLists.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.splitSampleList line 10
2. theorem OAI.Ostmann.splitSampleList_cast_symm line 14
3. theorem OAI.Ostmann.splitSampleList_cast_apply line 20
4. theorem OAI.Ostmann.splitSampleList_append line 26
5. theorem OAI.Ostmann.splitSampleList_treeLeafSplit line 43
6. theorem OAI.Ostmann.split_coordinate_parent line 65

   Source documentation

   Each parent recorded by the actual split-coordinate equivalence is computed from the preceding coordinates, including in right subtrees.

   theorem split_coordinate_parent {G : Type} [CommGroup G]
       (n : ℕ) (P : G) (x : TreeLeafFiber G n P) (j : ℕ) (hj : j < 2 ^ n - 1) :
       (actualParentSplits n x.1).getD j (1, 1) =
         (splitPrefixParent n P
           ((splitSampleList (2 ^ n - 1) (treeLeafSplitEquiv n P x)).take j).reverse,
           (splitSampleList (2 ^ n - 1) (treeLeafSplitEquiv n P x)).getD j 1) := by
   …

   Mentions: OAI.Ostmann.TreeLeafFiber, OAI.Ostmann.actualParentSplits, OAI.Ostmann.splitPrefixParent, OAI.Ostmann.splitSampleList, OAI.Ostmann.treeLeafSplitEquiv