SplitPrefixProducts.lean`

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Computing every current parent product from previously exposed splits

def OAI.Ostmann.pendingSplitBranch line 11
Source documentation
Pending subtrees are visited in preorder. Depth-zero branches require no split coordinate, so they are never stored in the frontier.
```
def pendingSplitBranch {G : Type*} (n : ℕ) (P : G) (rest : List (ℕ × G)) : List (ℕ × G) :=
…
```
def OAI.Ostmann.splitFrontierStep line 16
def OAI.Ostmann.currentSplitParent line 22
def OAI.Ostmann.splitPrefixParent line 27
def OAI.Ostmann.actualSplitValues line 31
def OAI.Ostmann.actualParentSplits line 35
def OAI.Ostmann.splitFrontierTrace line 40
theorem OAI.Ostmann.splitFrontierTrace_append line 45
theorem OAI.Ostmann.splitFrontier_after_actual line 53
theorem OAI.Ostmann.splitFrontierTrace_actual line 66
theorem OAI.Ostmann.splitPrefixParent_eq_foldl line 83
Source documentation
The stored prefix uses the same reverse chronological convention as sequentialSupport: the most recently exposed split is the head.
```
theorem splitPrefixParent_eq_foldl {G : Type*} [Div G] [One G]
    (n : ℕ) (P : G) (past : List G) :
    splitPrefixParent n P past = currentSplitParent
      (past.reverse.foldl splitFrontierStep (pendingSplitBranch n P [])) := by
…
```
Mentions: OAI.Ostmann.splitPrefixParent, OAI.Ostmann.currentSplitParent, OAI.Ostmann.splitFrontierStep, OAI.Ostmann.pendingSplitBranch
theorem OAI.Ostmann.actualSplitValues_length line 89
theorem OAI.Ostmann.splitFrontierTrace_getD line 99
theorem OAI.Ostmann.actualParentSplits_from_prefix line 115
Source documentation
The actual parent product at a node is a function of the initial total and the preceding split coordinates alone, with the same prefix convention as the arithmetic support estimator.
```
theorem actualParentSplits_from_prefix {G : Type*} [CommGroup G]
    (n : ℕ) (x : TreeLeafTuple G n) (j : ℕ) (hj : j < 2 ^ n - 1) :
    (actualParentSplits n x).getD j (1, 1) =
      (splitPrefixParent n (treeLeafProduct n x) ((actualSplitValues n x).take j).reverse,
        (actualSplitValues n x).getD j 1) := by
…
```
Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.actualParentSplits, OAI.Ostmann.splitPrefixParent, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.actualSplitValues