TreeAncestorScheme.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Ostmann.ancestorNodeIndex line 10
Source documentation
The prefix of length i is an earlier internal node.
```
def ancestorNodeIndex (n : ℕ) (j : Fin (2 ^ n - 1))
    (i : Fin (preorderNodePath n j).length) : Fin (2 ^ n - 1) :=
…
```
Mentions: OAI.Ostmann.preorderNodePath
theorem OAI.Ostmann.ancestorNodeIndex_path line 17
theorem OAI.Ostmann.ancestorNodeIndex_earlier line 24
def OAI.Ostmann.treeAncestorScheme line 46
Source documentation
The selected ancestors are genuine prefixes. Fixed label products and which prefixes enter each coefficient may vary with the actual node.
```
noncomputable def treeAncestorScheme (S : Finset ℤ) (n : ℕ) (t : FrequencyTree S n)
    (CL CR : List Bool → ℤ)
    (AL AR : (p : List Bool) → Finset (Fin p.length)) : PivotDependencyScheme (2 ^ n - 1) where
…
```
Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.PivotDependencyScheme
theorem OAI.Ostmann.treeAncestorScheme_depth line 62