OAI/NumberTheory/Ostmann/Characters/TreeSplitResidues.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.actualChildProducts line 12

   Source documentation

   Both actual child products, in the same preorder as the frequencies.

   def actualChildProducts {G : Type*} [CommMonoid G] : (n : ℕ) → TreeLeafTuple G n → List (G × G)
     | 0, _ => []
     | n + 1, x => (treeLeafProduct n x.1, treeLeafProduct n x.2) ::
         (actualChildProducts n x.1 ++ actualChildProducts n x.2)

   Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.treeLeafProduct

2. theorem OAI.Ostmann.actualChildProducts_length line 17
3. theorem OAI.Ostmann.actualParentSplits_childProducts line 27
4. theorem OAI.Ostmann.actualChildProducts_from_prefix line 35
5. def OAI.Ostmann.treeIntegerResidues line 60

   Source documentation

   Equality of all leaf residues, expressed on the original binary tuple.

   def treeIntegerResidues (Q : ℕ) : (n : ℕ) → TreeLeafTuple ℤ n →
       TreeLeafTuple (ZMod Q)ˣ n → Prop
     | 0, a, u => Units.val (show (ZMod Q)ˣ from u) = ((show ℤ from a) : ZMod Q)
     | n + 1, a, u => treeIntegerResidues Q n a.1 u.1 ∧ treeIntegerResidues Q n a.2 u.2

   Mentions: OAI.Ostmann.TreeLeafTuple

6. theorem OAI.Ostmann.treeIntegerResidues_product line 65
7. theorem OAI.Ostmann.treeIntegerResidues_children line 75
8. theorem OAI.Ostmann.treeIntegerResidues_child line 86
9. theorem OAI.Ostmann.exposed_prefix_children_eq line 105

   Source documentation

   Agreement of the total and the exposed prefix fixes both child-product residues at every earlier node, including nodes in right subtrees.

   theorem exposed_prefix_children_eq {G : Type} [CommGroup G]
       (n : ℕ) (u v : TreeLeafTuple G n) (j : ℕ)
       (htotal : treeLeafProduct n u = treeLeafProduct n v)
       (hpast : (actualSplitValues n u).take j = (actualSplitValues n v).take j)
       (i : ℕ) (hi : i < j) (hj : j ≤ 2 ^ n - 1) :
       (actualChildProducts n u).getD i (1, 1) = (actualChildProducts n v).getD i (1, 1) := by
   …

   Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.actualSplitValues, OAI.Ostmann.actualChildProducts