OAI/Combinatorics/ThinTrees/Metric/Profiles.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Metric profiles.

  1. def OAI.AlgorithmicThinTrees.MetricProfiles.profile line 23
  2. def OAI.AlgorithmicThinTrees.MetricProfiles.polytope line 25
  3. lemma OAI.AlgorithmicThinTrees.MetricProfiles.profile_mem line 28
  4. lemma OAI.AlgorithmicThinTrees.MetricProfiles.polytope_convex line 32
  5. lemma OAI.AlgorithmicThinTrees.MetricProfiles.polytope_compact line 34
  6. lemma OAI.AlgorithmicThinTrees.MetricProfiles.profile_norm_sub line 37
  7. lemma OAI.AlgorithmicThinTrees.MetricProfiles.profile_isometry line 51
  8. lemma OAI.AlgorithmicThinTrees.MetricProfiles.norm_coordinate_convex line 55
  9. theorem OAI.AlgorithmicThinTrees.MetricProfiles.radius_eq_coordinate line 73
  10. lemma OAI.AlgorithmicThinTrees.MetricProfiles.coordinate_nonneg line 86
  11. def OAI.AlgorithmicThinTrees.MetricProfiles.commonRadius line 96
  12. lemma OAI.AlgorithmicThinTrees.MetricProfiles.commonRadius_pos line 98
  13. lemma OAI.AlgorithmicThinTrees.MetricProfiles.twice_dist_lt_commonRadius line 104
  14. structure OAI.AlgorithmicThinTrees.MetricProfiles.Doubled line 114
  15. def OAI.AlgorithmicThinTrees.MetricProfiles.doubledDist line 121
  16. lemma OAI.AlgorithmicThinTrees.MetricProfiles.doubledDist_self line 125
  17. lemma OAI.AlgorithmicThinTrees.MetricProfiles.doubledDist_comm line 128
  18. lemma OAI.AlgorithmicThinTrees.MetricProfiles.doubledDist_triangle line 131
  19. instance OAI.AlgorithmicThinTrees.MetricProfiles.(instance at line 149) line 149
  20. def OAI.AlgorithmicThinTrees.MetricProfiles.plus line 155
  21. def OAI.AlgorithmicThinTrees.MetricProfiles.minus line 156
  22. lemma OAI.AlgorithmicThinTrees.MetricProfiles.dist_plus line 158
  23. lemma OAI.AlgorithmicThinTrees.MetricProfiles.dist_minus line 162
  24. lemma OAI.AlgorithmicThinTrees.MetricProfiles.opposite_dist line 166
  25. lemma OAI.AlgorithmicThinTrees.MetricProfiles.profile_opposite_sum line 170
  26. lemma OAI.AlgorithmicThinTrees.MetricProfiles.opposite_coordinate_sum line 176
  27. theorem OAI.AlgorithmicThinTrees.MetricProfiles.opposite_radii line 192
  28. theorem OAI.AlgorithmicThinTrees.MetricProfiles.original_isometry line 197
  29. def OAI.AlgorithmicThinTrees.MetricProfiles.mix line 206
  30. lemma OAI.AlgorithmicThinTrees.MetricProfiles.mix_zero line 208
  31. lemma OAI.AlgorithmicThinTrees.MetricProfiles.mix_one line 209
  32. lemma OAI.AlgorithmicThinTrees.MetricProfiles.mix_sub_mix line 211
  33. lemma OAI.AlgorithmicThinTrees.MetricProfiles.segment_distance line 216
  34. theorem OAI.AlgorithmicThinTrees.MetricProfiles.segment_subdivision_length line 220
  35. lemma OAI.AlgorithmicThinTrees.MetricProfiles.mix_mem line 240
  36. lemma OAI.AlgorithmicThinTrees.MetricProfiles.radius_mix line 244
  37. lemma OAI.AlgorithmicThinTrees.MetricProfiles.inward_radius line 251
  38. lemma OAI.AlgorithmicThinTrees.MetricProfiles.inward_distance line 258
  39. lemma OAI.AlgorithmicThinTrees.MetricProfiles.outward_radius line 263
  40. lemma OAI.AlgorithmicThinTrees.MetricProfiles.outward_distance line 270
  41. theorem OAI.AlgorithmicThinTrees.MetricProfiles.radial_motion line 280
  42. theorem OAI.AlgorithmicThinTrees.MetricProfiles.ball_intersects_shell line 323
  43. def OAI.AlgorithmicThinTrees.MetricProfiles.PiecewiseAffineOn line 351
  44. lemma OAI.AlgorithmicThinTrees.MetricProfiles.PiecewiseAffineOn.mono line 356
  45. lemma OAI.AlgorithmicThinTrees.MetricProfiles.PiecewiseAffineOn.congr line 362
  46. lemma OAI.AlgorithmicThinTrees.MetricProfiles.clamped_affine_piecewise line 368
  47. theorem OAI.AlgorithmicThinTrees.MetricProfiles.clamped_radius_piecewise line 404