OAI/Combinatorics/ThinTrees/Shells.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrongThinTree.Geometry.l1dist_self line 15
  2. lemma OAI.StrongThinTree.Geometry.l1dist_triangle line 17
  3. structure OAI.StrongThinTree.Geometry.RadialShell line 22
  4. def OAI.StrongThinTree.Geometry.RadialShell.ball line 32
  5. def OAI.StrongThinTree.Geometry.RadialShell.hollow line 33
  6. def OAI.StrongThinTree.Geometry.RadialShell.width line 34
  7. def OAI.StrongThinTree.Geometry.RadialShell.support line 36
  8. def OAI.StrongThinTree.Geometry.RadialShell.Valid line 40
  9. lemma OAI.StrongThinTree.Geometry.RadialShell.valid_width_pos line 45
  10. lemma OAI.StrongThinTree.Geometry.RadialShell.support_ball line 48
  11. lemma OAI.StrongThinTree.Geometry.RadialShell.support_hollow line 53
  12. lemma OAI.StrongThinTree.Geometry.RadialShell.valid_support_nonempty line 59
  13. lemma OAI.StrongThinTree.Geometry.RadialShell.restriction_valid line 78
  14. lemma OAI.StrongThinTree.Geometry.RadialShell.restriction_subset line 87
  15. lemma OAI.StrongThinTree.Geometry.RadialShell.ball_subset_of_radial_margin line 94
  16. lemma OAI.StrongThinTree.Geometry.RadialShell.ball_disjoint_hollow_lower line 105
  17. lemma OAI.StrongThinTree.Geometry.RadialShell.ball_disjoint_hollow_upper line 116
  18. lemma OAI.StrongThinTree.Geometry.RadialShell.concentric_disjoint line 126
  19. lemma OAI.StrongThinTree.Geometry.RadialShell.disjoint_balls_distance line 133
  20. def OAI.StrongThinTree.Geometry.RadialShell.Arrangement line 161
  21. lemma OAI.StrongThinTree.Geometry.RadialShell.arrangement_empty line 165
  22. lemma OAI.StrongThinTree.Geometry.RadialShell.arrangement_subset line 168
  23. lemma OAI.StrongThinTree.Geometry.RadialShell.arrangement_disjoint_finsets line 172
  24. lemma OAI.StrongThinTree.Geometry.RadialShell.arrangement_union line 180
  25. lemma OAI.StrongThinTree.Geometry.RadialShell.image_restriction_injective line 195
  26. lemma OAI.StrongThinTree.Geometry.RadialShell.arrangement_image_restriction line 206
  27. def OAI.StrongThinTree.Geometry.RadialShell.capacity line 220
  28. def OAI.StrongThinTree.Geometry.RadialShell.potential line 222
  29. lemma OAI.StrongThinTree.Geometry.RadialShell.capacity_nonneg line 225
  30. lemma OAI.StrongThinTree.Geometry.RadialShell.capacity_ge_formal line 227
  31. lemma OAI.StrongThinTree.Geometry.RadialShell.potential_union line 229
  32. lemma OAI.StrongThinTree.Geometry.RadialShell.potential_erase line 232
  33. lemma OAI.StrongThinTree.Geometry.RadialShell.potential_image_restriction line 236
  34. lemma OAI.StrongThinTree.Geometry.RadialShell.capacity_ball line 244
  35. lemma OAI.StrongThinTree.Geometry.RadialShell.ball_injective line 250
  36. lemma OAI.StrongThinTree.Geometry.RadialShell.potential_balls line 254
  37. lemma OAI.StrongThinTree.Geometry.RadialShell.potential_filter_width line 268
  38. lemma OAI.StrongThinTree.Geometry.RadialShell.arrangement_balls line 275
  39. lemma OAI.StrongThinTree.Geometry.RadialShell.split_shells line 288
  40. lemma OAI.StrongThinTree.Geometry.RadialShell.shrink_shells line 367
  41. lemma OAI.StrongThinTree.Geometry.RadialShell.radial_span line 423
  42. lemma OAI.StrongThinTree.Geometry.RadialShell.compact_phase line 444
  43. lemma OAI.StrongThinTree.Geometry.RadialShell.compact_arrangement line 545
  44. structure OAI.StrongThinTree.Geometry.RadialShell.CompactFamily line 577
  45. lemma OAI.StrongThinTree.Geometry.RadialShell.CompactFamily.ball_valid line 588
  46. lemma OAI.StrongThinTree.Geometry.RadialShell.CompactFamily.scale line 601
  47. lemma OAI.StrongThinTree.MultiGraph.arrangement_length_bound line 619
  48. lemma OAI.StrongThinTree.MultiGraph.binary_compact_bound line 639