OAI/Combinatorics/TreeEdit/FiniteSpectrum.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.TreeEdit.FiniteTree.instStateFintype line 14
  2. instance OAI.TreeEdit.FiniteTree.instSymbolFintype line 19
  3. def OAI.TreeEdit.FiniteTree.SpectralBound line 28
  4. lemma OAI.TreeEdit.FiniteTree.SpectralBound.child line 32
  5. def OAI.TreeEdit.FiniteTree.activeChildren line 41
  6. lemma OAI.TreeEdit.FiniteTree.chi_u line 45
  7. lemma OAI.TreeEdit.FiniteTree.active_period line 60
  8. lemma OAI.TreeEdit.FiniteTree.active_u_ne_one line 77
  9. lemma OAI.TreeEdit.FiniteTree.sparse_period_bound line 85
  10. def OAI.TreeEdit.FiniteTree.sparse line 105
  11. def OAI.TreeEdit.FiniteTree.sparseMass line 108
  12. lemma OAI.TreeEdit.FiniteTree.sum_activeChildren line 112
  13. lemma OAI.TreeEdit.FiniteTree.branch_pointwise line 122
  14. lemma OAI.TreeEdit.FiniteTree.branch_mass line 132
  15. lemma OAI.TreeEdit.FiniteTree.sparse_estimate line 149
  16. theorem OAI.TreeEdit.FiniteTree.mass_bound line 188