OAI/Combinatorics/ThinTrees/Metric/ShellCharging.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Metric shell charging.

  1. def OAI.AlgorithmicThinTrees.MetricProfiles.relativeBall line 19
  2. def OAI.AlgorithmicThinTrees.MetricProfiles.relativeShell line 22
  3. lemma OAI.AlgorithmicThinTrees.MetricProfiles.radius_reverse_triangle line 26
  4. theorem OAI.AlgorithmicThinTrees.MetricProfiles.disjoint_relative_balls_iff line 31
  5. theorem OAI.AlgorithmicThinTrees.MetricProfiles.ball_shell_intersection_iff line 59
  6. theorem OAI.AlgorithmicThinTrees.MetricProfiles.shell_segment_length_bound line 72
  7. theorem OAI.AlgorithmicThinTrees.MetricProfiles.shell_length_bound line 94
  8. theorem OAI.AlgorithmicThinTrees.MetricProfiles.routed_shell_length_bound line 121
  9. theorem OAI.AlgorithmicThinTrees.MetricProfiles.doubled_shell_length_bound line 171