OAI/Combinatorics/ThinTrees/Metric/CompactCharging.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Metric compact charging.

  1. def OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.normDistance line 18
  2. def OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.inPolytope line 20
  3. def OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.isProfile line 22
  4. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.normDistance_self line 25
  5. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.normDistance_comm line 29
  6. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.normDistance_triangle line 33
  7. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.isProfile_inPolytope line 38
  8. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.segment_formula line 43
  9. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.inPolytope_segment line 49
  10. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.isProfile_radial_affine line 55
  11. structure OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell line 67
  12. def OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.ball line 77
  13. def OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.hollow line 78
  14. def OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.width line 79
  15. def OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.support line 81
  16. def OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.Valid line 85
  17. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.valid_width_pos line 91
  18. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.support_ball line 94
  19. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.support_hollow line 99
  20. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.valid_support_nonempty line 105
  21. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.restriction_valid line 125
  22. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.restriction_subset line 134
  23. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.ball_subset_of_radial_margin line 141
  24. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.ball_disjoint_hollow_lower line 152
  25. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.ball_disjoint_hollow_upper line 163
  26. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.concentric_disjoint line 173
  27. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.disjoint_balls_distance line 180
  28. def OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.Arrangement line 208
  29. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.arrangement_empty line 212
  30. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.arrangement_subset line 215
  31. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.arrangement_disjoint_finsets line 219
  32. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.arrangement_union line 227
  33. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.image_restriction_injective line 242
  34. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.arrangement_image_restriction line 253
  35. def OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.capacity line 267
  36. def OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.potential line 269
  37. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.capacity_nonneg line 272
  38. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.capacity_ge_formal line 274
  39. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.potential_union line 276
  40. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.potential_erase line 279
  41. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.potential_image_restriction line 283
  42. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.capacity_ball line 291
  43. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.ball_injective line 297
  44. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.potential_balls line 301
  45. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.potential_filter_width line 315
  46. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.arrangement_balls line 322
  47. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.split_shells line 335
  48. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.shrink_shells line 414
  49. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.radial_span line 470
  50. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.compact_phase line 491
  51. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.compact_arrangement line 592
  52. structure OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.CompactFamily line 624
  53. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.CompactFamily.ball_valid line 635
  54. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.RadialShell.CompactFamily.scale line 648
  55. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.arrangement_length_bound line 668
  56. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.metric_compact_bound line 698
  57. lemma OAI.AlgorithmicThinTrees.MetricProfiles.CompactGeometry.doubled_compact_bound line 736