OAI/Geometry/BallPacking/Moments/PolytopeSlices.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.MomentPolytope.weighted_assemble line 10
  2. theorem OAI.PackingSufficiencySupport.MomentPolytope.weighted_affine line 15
  3. theorem OAI.PackingSufficiencySupport.MomentPolytope.convex_region line 21
  4. theorem OAI.PackingSufficiencySupport.MomentPolytope.lower_closed line 32
  5. def OAI.PackingSufficiencySupport.MomentPolytope.baseRegion line 38
  6. theorem OAI.PackingSufficiencySupport.MomentPolytope.assemble_zero_mem_iff line 41
  7. theorem OAI.PackingSufficiencySupport.MomentPolytope.convex_baseRegion line 54
  8. theorem OAI.PackingSufficiencySupport.MomentPolytope.baseRegion_eq_image line 66
  9. theorem OAI.PackingSufficiencySupport.MomentPolytope.isCompact_baseRegion line 80
  10. abbrev OAI.PackingSufficiencySupport.MomentPolytope.Active line 86
  11. theorem OAI.PackingSufficiencySupport.MomentPolytope.active_nonempty line 88
  12. def OAI.PackingSufficiencySupport.MomentPolytope.endpoint line 110
  13. def OAI.PackingSufficiencySupport.MomentPolytope.length line 113
  14. theorem OAI.PackingSufficiencySupport.MomentPolytope.length_le line 116
  15. theorem OAI.PackingSufficiencySupport.MomentPolytope.le_length_iff line 119
  16. theorem OAI.PackingSufficiencySupport.MomentPolytope.continuous_endpoint line 123
  17. theorem OAI.PackingSufficiencySupport.MomentPolytope.continuous_length line 127
  18. theorem OAI.PackingSufficiencySupport.MomentPolytope.endpoint_affine line 132
  19. theorem OAI.PackingSufficiencySupport.MomentPolytope.concave_length line 142
  20. theorem OAI.PackingSufficiencySupport.MomentPolytope.assemble_mem_iff line 151
  21. theorem OAI.PackingSufficiencySupport.MomentPolytope.length_nonneg line 184
  22. theorem OAI.PackingSufficiencySupport.MomentPolytope.length_antitone line 188
  23. theorem OAI.PackingSufficiencySupport.MomentPolytope.zero_mem line 198
  24. theorem OAI.PackingSufficiencySupport.MomentPolytope.assemble_affine line 203
  25. def OAI.PackingSufficiencySupport.MomentPolytope.sliceEquiv line 216
  26. def OAI.PackingSufficiencySupport.MomentPolytope.onSlice line 224
  27. def OAI.PackingSufficiencySupport.MomentPolytope.coordRearrange line 227
  28. theorem OAI.PackingSufficiencySupport.MomentPolytope.onSlice_convex line 231
  29. theorem OAI.PackingSufficiencySupport.MomentPolytope.coordRearrange_convex line 250
  30. def OAI.PackingSufficiencySupport.MomentPolytope.coordOperator line 260
  31. theorem OAI.PackingSufficiencySupport.MomentPolytope.coordRearrange_mono line 264
  32. theorem OAI.PackingSufficiencySupport.MomentPolytope.coordRearrange_add_const line 271
  33. theorem OAI.PackingSufficiencySupport.MomentPolytope.coordRearrange_nonexpansive line 282
  34. def OAI.PackingSufficiencySupport.MomentPolytope.IncreasingIn line 315
  35. theorem OAI.PackingSufficiencySupport.MomentPolytope.coordRearrange_increasing line 320
  36. theorem OAI.PackingSufficiencySupport.MomentPolytope.coordRearrange_preserves_increasing line 340
  37. theorem OAI.PackingSufficiencySupport.MomentPolytope.coordRearrange_bound line 365
  38. theorem OAI.PackingSufficiencySupport.MomentPolytope.measurePreserving_split line 381
  39. def OAI.PackingSufficiencySupport.Comparison.zeroExtend line 397
  40. theorem OAI.PackingSufficiencySupport.Comparison.zeroExtend_coe line 401
  41. theorem OAI.PackingSufficiencySupport.Comparison.zeroExtend_measurable line 405
  42. theorem OAI.PackingSufficiencySupport.Comparison.zeroExtend_continuousOn line 410
  43. theorem OAI.PackingSufficiencySupport.Comparison.indicator_zeroExtend line 418
  44. theorem OAI.PackingSufficiencySupport.Comparison.zeroExtend_integrable line 423
  45. def OAI.PackingSufficiencySupport.Comparison.integralMap line 429
  46. theorem OAI.PackingSufficiencySupport.Comparison.integralMap_mono line 441
  47. theorem OAI.PackingSufficiencySupport.Comparison.integralMap_const line 450
  48. theorem OAI.PackingSufficiencySupport.Comparison.zeroExtend_slice line 466
  49. theorem OAI.PackingSufficiencySupport.Comparison.rearrange_integral line 476
  50. theorem OAI.PackingSufficiencySupport.MomentPolytope.image_split line 507
  51. theorem OAI.PackingSufficiencySupport.MomentPolytope.isCompact_sliceDomain line 517
  52. theorem OAI.PackingSufficiencySupport.MomentPolytope.zeroExtend_onSlice line 522
  53. theorem OAI.PackingSufficiencySupport.MomentPolytope.integralMap_onSlice line 537
  54. theorem OAI.PackingSufficiencySupport.MomentPolytope.coordRearrange_integral line 545
  55. def OAI.PackingSufficiencySupport.MomentPolytope.successive line 568
  56. theorem OAI.PackingSufficiencySupport.MomentPolytope.successive_nonexpansive line 573
  57. theorem OAI.PackingSufficiencySupport.MomentPolytope.successive_mono line 581
  58. theorem OAI.PackingSufficiencySupport.MomentPolytope.successive_translate line 588
  59. theorem OAI.PackingSufficiencySupport.MomentPolytope.successive_integral line 598