OAI/NumberTheory/Ostmann/Characters/TreeLeafIndex.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Labeled leaves and bottom quartets of a full binary tree

  1. def OAI.Ostmann.TreeLeafIndex line 12
  2. instance OAI.Ostmann.treeLeafIndexFintype line 16
  3. instance OAI.Ostmann.treeLeafIndexDecidableEq line 21
  4. instance OAI.Ostmann.treeLeafIndexNonempty line 26
  5. def OAI.Ostmann.treeLeafTupleEquiv line 31
  6. theorem OAI.Ostmann.card_treeLeafIndex line 41
  7. def OAI.Ostmann.bottomQuartet line 49
  8. def OAI.Ostmann.indexedRationalAmplitude line 54
  9. theorem OAI.Ostmann.indexedRationalAmplitude_l2_bound line 60