OAI/Combinatorics/ThinTrees/Truncation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrongThinTree.Truncation.sum_sq_le_card_mul_sum_sq line 19
  2. lemma OAI.StrongThinTree.Truncation.two_truncations line 23
  3. def OAI.StrongThinTree.Truncation.dyadicIndex line 109
  4. lemma OAI.StrongThinTree.Truncation.dyadic_interval line 111
  5. lemma OAI.StrongThinTree.Truncation.dyadicIndex_lt line 125
  6. lemma OAI.StrongThinTree.Truncation.same_dyadic_ratio line 132
  7. lemma OAI.StrongThinTree.Truncation.dyadic_pair line 140
  8. lemma OAI.StrongThinTree.Truncation.homogeneous_subset line 181
  9. lemma OAI.StrongThinTree.Truncation.scaled_subset line 237
  10. def OAI.StrongThinTree.MultiGraph.Hierarchy.truncationBins line 324
  11. def OAI.StrongThinTree.MultiGraph.Hierarchy.truncationGain line 325
  12. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.truncationGain_pos line 327
  13. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.diagonal_sq_le line 331
  14. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.positive_bad_bound line 339
  15. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.weighted_boundary_sum line 405
  16. lemma OAI.StrongThinTree.MultiGraph.Hierarchy.hierarchy_numerator_bound line 428