OAI/Geometry/BallPacking/Models/BallVolume.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PackingSufficiencySupport.Ambient line 10
  2. def OAI.PackingSufficiencySupport.capacity line 12
  3. def OAI.PackingSufficiencySupport.closedBall line 15
  4. def OAI.PackingSufficiencySupport.openBall line 18
  5. def OAI.PackingSufficiencySupport.standardForm line 21
  6. def OAI.PackingSufficiencySupport.IsBallEmbedding line 24
  7. def OAI.PackingSufficiencySupport.HasPacking line 31
  8. theorem OAI.PackingSufficiencySupport.isBallEmbedding_id line 38
  9. def OAI.PackingSufficiencySupport.realCoordinates line 45
  10. def OAI.PackingSufficiencySupport.realBasis line 53
  11. theorem OAI.PackingSufficiencySupport.realBasis_repr line 57
  12. theorem OAI.PackingSufficiencySupport.matrix_J_pairing line 61
  13. theorem OAI.PackingSufficiencySupport.det_eq_one_of_preserves_standardForm line 69
  14. theorem OAI.PackingSufficiencySupport.continuous_capacity line 99
  15. theorem OAI.PackingSufficiencySupport.closedBall_isClosed line 103
  16. theorem OAI.PackingSufficiencySupport.openBall_isOpen line 106
  17. theorem OAI.PackingSufficiencySupport.closedBall_isCompact line 109
  18. theorem OAI.PackingSufficiencySupport.IsBallEmbedding.volume_image line 130
  19. theorem OAI.PackingSufficiencySupport.capacity_zero line 157
  20. theorem OAI.PackingSufficiencySupport.capacity_smul line 160
  21. theorem OAI.PackingSufficiencySupport.closedBall_eq_smul line 166
  22. theorem OAI.PackingSufficiencySupport.volume_closedBall line 182
  23. theorem OAI.PackingSufficiencySupport.capacity_nonneg line 189
  24. theorem OAI.PackingSufficiencySupport.unitBall_volume_pos line 192
  25. theorem OAI.PackingSufficiencySupport.unitBall_volume_ne_top line 197
  26. theorem OAI.PackingSufficiencySupport.IsBallEmbedding.closedBall_continuousOn line 200
  27. theorem OAI.PackingSufficiencySupport.IsBallEmbedding.isCompact_image line 206
  28. theorem OAI.PackingSufficiencySupport.HasPacking.exists_smaller_target line 211
  29. theorem OAI.PackingSufficiencySupport.HasPacking.volume_le line 236
  30. theorem OAI.PackingSufficiencySupport.HasPacking.volume_lt line 254
  31. def OAI.PackingSufficiencySupport.dilation line 260
  32. theorem OAI.PackingSufficiencySupport.dilation_apply line 263
  33. theorem OAI.PackingSufficiencySupport.dilation_symm_apply line 266
  34. theorem OAI.PackingSufficiencySupport.IsBallEmbedding.dilate line 269
  35. theorem OAI.PackingSufficiencySupport.HasPacking.dilate line 302
  36. theorem OAI.PackingSufficiencySupport.hasPacking_normalize line 326
  37. theorem OAI.PackingSufficiencySupport.IsBallEmbedding.mono line 339
  38. theorem OAI.PackingSufficiencySupport.HasPacking.mono line 344
  39. theorem OAI.PackingSufficiencySupport.exists_larger_closedBall_subset line 355
  40. theorem OAI.PackingSufficiencySupport.HasPacking.exists_larger_sources line 378
  41. theorem OAI.PackingSufficiencySupport.hasPacking_one_iff line 412
  42. def OAI.PackingSufficiencySupport.Comparison.convexFunctionSet line 432
  43. abbrev OAI.PackingSufficiencySupport.Comparison.ConvexMaps line 437
  44. theorem OAI.PackingSufficiencySupport.Comparison.isClosed_convexFunctionSet line 439
  45. instance OAI.PackingSufficiencySupport.Comparison.convexMaps_nonempty line 448
  46. instance OAI.PackingSufficiencySupport.Comparison.convexMaps_completeSpace line 451
  47. def OAI.PackingSufficiencySupport.Comparison.affineStep line 455
  48. theorem OAI.PackingSufficiencySupport.Comparison.exists_convex_fixedPoint line 465
  49. theorem OAI.PackingSufficiencySupport.Comparison.fixedPoint_negative_maximum line 481