OAI/Analysis/Mahler/Medians.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SymmetricMahler.IsMetricMedian line 16
  2. def OAI.SymmetricMahler.HasMetricMedians line 19
  3. def OAI.SymmetricMahler.ThreeBallIntersection line 23
  4. lemma OAI.SymmetricMahler.segment_point_distances line 28
  5. theorem OAI.SymmetricMahler.threeBallIntersection_of_metricMedians line 51
  6. theorem OAI.SymmetricMahler.metricMedians_of_threeBallIntersection line 78
  7. theorem OAI.SymmetricMahler.metricMedians_iff_threeBallIntersection line 122
  8. theorem OAI.SymmetricMahler.median_of_aggregate_decomposition line 126
  9. lemma OAI.SymmetricMahler.extreme_unit_norm_add line 164
  10. theorem OAI.SymmetricMahler.dist_extreme_unit_eq_two line 190
  11. theorem OAI.SymmetricMahler.finite_extreme_unit_of_medians line 218
  12. theorem OAI.SymmetricMahler.unitBall_eq_finite_convexHull_of_medians line 234
  13. def OAI.SymmetricMahler.aggregateSet line 254
  14. lemma OAI.SymmetricMahler.aggregateSet_eq_image line 258
  15. lemma OAI.SymmetricMahler.isCompact_aggregateSet line 271
  16. lemma OAI.SymmetricMahler.convex_aggregateSet line 278
  17. lemma OAI.SymmetricMahler.exists_unitBall_dual_maximizer line 304
  18. lemma OAI.SymmetricMahler.aggregate_decomposition_of_support line 336
  19. lemma OAI.SymmetricMahler.median_of_aggregate_support line 363
  20. lemma OAI.SymmetricMahler.extreme_unit_scaled_norm_add line 381
  21. theorem OAI.SymmetricMahler.extreme_unit_spear line 394
  22. lemma OAI.SymmetricMahler.dual_eval_le_unit_norm line 429
  23. theorem OAI.SymmetricMahler.extreme_unit_dual_face_norming line 435
  24. structure OAI.SymmetricMahler.SignedUnitRepresentation line 465
  25. def OAI.SymmetricMahler.SignedUnitRepresentation.plus line 480
  26. def OAI.SymmetricMahler.SignedUnitRepresentation.minus line 482
  27. lemma OAI.SymmetricMahler.SignedUnitRepresentation.plus_add_minus line 484
  28. lemma OAI.SymmetricMahler.SignedUnitRepresentation.plus_norm line 495
  29. lemma OAI.SymmetricMahler.SignedUnitRepresentation.minus_norm line 510
  30. lemma OAI.SymmetricMahler.SignedUnitRepresentation.eval_difference line 525
  31. lemma OAI.SymmetricMahler.SignedUnitRepresentation.difference_mem line 532
  32. def OAI.SymmetricMahler.HasEndpointScaling line 537
  33. def OAI.SymmetricMahler.liftedLensCost line 542
  34. def OAI.SymmetricMahler.HasOptimalLiftRepresentations line 545
  35. lemma OAI.SymmetricMahler.endpoint_factor_mem line 554
  36. def OAI.SymmetricMahler.SignedUnitRepresentation.cost line 566
  37. lemma OAI.SymmetricMahler.SignedUnitRepresentation.cost_error line 569
  38. def OAI.SymmetricMahler.medianCompetitor line 598
  39. lemma OAI.SymmetricMahler.medianCompetitor_difference line 614
  40. lemma OAI.SymmetricMahler.aggregate_support_interior_of_optimal line 619
  41. lemma OAI.SymmetricMahler.aggregate_support_of_optimal line 650
  42. theorem OAI.SymmetricMahler.zero_median_of_optimal line 683
  43. lemma OAI.SymmetricMahler.metricMedians_of_zero_medians line 700
  44. theorem OAI.SymmetricMahler.metricMedians_of_optimal_lift line 734