OAI/Geometry/BallPacking/Moments/ConvexRearrangement.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Comparison.exists_gap_parameter line 12
  2. def OAI.PackingSufficiencySupport.Comparison.translate line 25
  3. theorem OAI.PackingSufficiencySupport.Comparison.exists_rearranged_gap line 33
  4. def OAI.PackingSufficiencySupport.Comparison.minimum line 81
  5. theorem OAI.PackingSufficiencySupport.Comparison.minimum_attained line 83
  6. theorem OAI.PackingSufficiencySupport.Comparison.minimum_le line 87
  7. theorem OAI.PackingSufficiencySupport.Comparison.le_minimum line 91
  8. theorem OAI.PackingSufficiencySupport.Comparison.minimum_mono line 94
  9. theorem OAI.PackingSufficiencySupport.Comparison.minimum_add_const line 98
  10. theorem OAI.PackingSufficiencySupport.Comparison.minimum_lipschitz line 109
  11. def OAI.PackingSufficiencySupport.Comparison.sliceDomain line 131
  12. abbrev OAI.PackingSufficiencySupport.Comparison.Slice line 133
  13. abbrev OAI.PackingSufficiencySupport.Comparison.UnitInterval line 134
  14. def OAI.PackingSufficiencySupport.Comparison.sliceBase line 136
  15. def OAI.PackingSufficiencySupport.Comparison.sliceHeight line 140
  16. def OAI.PackingSufficiencySupport.Comparison.sliceLength line 143
  17. theorem OAI.PackingSufficiencySupport.Comparison.intervalEndpoint_mem line 147
  18. def OAI.PackingSufficiencySupport.Comparison.intervalEndpoint line 162
  19. def OAI.PackingSufficiencySupport.Comparison.intervalValue line 173
  20. def OAI.PackingSufficiencySupport.Comparison.rearrange line 178
  21. def OAI.PackingSufficiencySupport.Comparison.pointAtHeight line 182
  22. def OAI.PackingSufficiencySupport.Comparison.intervalCandidate line 185
  23. theorem OAI.PackingSufficiencySupport.Comparison.intervalValue_eq_candidate line 191
  24. theorem OAI.PackingSufficiencySupport.Comparison.exists_unitInterval_mul line 201
  25. theorem OAI.PackingSufficiencySupport.Comparison.rearrange_le_candidate line 211
  26. theorem OAI.PackingSufficiencySupport.Comparison.rearrange_attained line 225
  27. theorem OAI.PackingSufficiencySupport.Comparison.convex_sliceDomain line 238
  28. theorem OAI.PackingSufficiencySupport.Comparison.rearrange_convex line 245
  29. theorem OAI.PackingSufficiencySupport.Comparison.rearrange_mono line 293
  30. theorem OAI.PackingSufficiencySupport.Comparison.rearrange_add_const line 301
  31. theorem OAI.PackingSufficiencySupport.Comparison.rearrange_nonexpansive line 313
  32. theorem OAI.PackingSufficiencySupport.Comparison.convex_le_max_on_slice line 325
  33. theorem OAI.PackingSufficiencySupport.Comparison.rearrange_monotone_height line 370
  34. theorem OAI.PackingSufficiencySupport.Comparison.rearrange_compare_slices line 390
  35. theorem OAI.PackingSufficiencySupport.Comparison.IntervalMinimum.sublevel_volume_eq line 409
  36. theorem OAI.PackingSufficiencySupport.Comparison.IntervalMinimum.integral_eq line 454
  37. def OAI.PackingSufficiencySupport.Comparison.clampPoint line 480
  38. def OAI.PackingSufficiencySupport.Comparison.sliceFunction line 486
  39. theorem OAI.PackingSufficiencySupport.Comparison.sliceFunction_eq line 490
  40. theorem OAI.PackingSufficiencySupport.Comparison.sliceFunction_convex line 497
  41. theorem OAI.PackingSufficiencySupport.Comparison.rearrange_slice_characterization line 520
  42. theorem OAI.PackingSufficiencySupport.Comparison.rearrange_slice_integral line 544
  43. abbrev OAI.PackingSufficiencySupport.MomentPolytope.Moments line 558
  44. abbrev OAI.PackingSufficiencySupport.MomentPolytope.Base line 559
  45. def OAI.PackingSufficiencySupport.MomentPolytope.region line 561
  46. def OAI.PackingSufficiencySupport.MomentPolytope.assemble line 564
  47. theorem OAI.PackingSufficiencySupport.MomentPolytope.assemble_at line 567
  48. theorem OAI.PackingSufficiencySupport.MomentPolytope.assemble_off line 569
  49. def OAI.PackingSufficiencySupport.MomentPolytope.split line 572