OAI/Geometry/BallPacking/Models/LiouvilleRadialCalculus.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.linearLiouville_variable_smul line 14
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.fsBallMap_primitive line 26
  3. def OAI.PackingSufficiencySupport.largeMomentDomain line 45
  4. theorem OAI.PackingSufficiencySupport.largeMomentDomain_isClosed line 48
  5. theorem OAI.PackingSufficiencySupport.largeMomentDomain_isCompact line 57
  6. theorem OAI.PackingSufficiencySupport.integral_scaled_small_model line 67
  7. def OAI.PackingSufficiencySupport.largeModelMean line 87
  8. theorem OAI.PackingSufficiencySupport.integral_large_model line 90
  9. theorem OAI.PackingSufficiencySupport.continuous_largeModelMean line 135
  10. theorem OAI.PackingSufficiencySupport.largeModelMean_limit_value line 141
  11. def OAI.PackingSufficiencySupport.largeModelBounds line 155
  12. theorem OAI.PackingSufficiencySupport.largeModelBounds_nonneg line 158
  13. theorem OAI.PackingSufficiencySupport.largeModelRegion_eq line 163
  14. theorem OAI.PackingSufficiencySupport.largeModelRegion_isCompact line 191
  15. theorem OAI.PackingSufficiencySupport.largeModelRegion_contains_cap line 196
  16. def OAI.PackingSufficiencySupport.largeModelDensity line 209
  17. def OAI.PackingSufficiencySupport.largeModelGap line 212
  18. theorem OAI.PackingSufficiencySupport.integral_largeModelDensity line 215
  19. theorem OAI.PackingSufficiencySupport.integral_largeModelGap line 228
  20. theorem OAI.PackingSufficiencySupport.largeModelGap_eq_cappedAffine line 246
  21. theorem OAI.PackingSufficiencySupport.continuous_largeModelGap line 254
  22. theorem OAI.PackingSufficiencySupport.largeModelDensity_lower line 259
  23. theorem OAI.PackingSufficiencySupport.exists_large_model_comparison_data line 271
  24. def OAI.PackingSufficiencySupport.DiagonalQuadrics.largeNormalCoefficient line 352
  25. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.largeNormalCoefficient_smooth line 355
  26. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.largeNormalCoefficient_pos line 359
  27. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.largeNormalCoefficient_le_one line 368
  28. def OAI.PackingSufficiencySupport.DiagonalQuadrics.largeHorizontalPrimitive line 377
  29. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.largeHorizontalPrimitive_smooth line 380
  30. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.largeHorizontalPrimitive_exterior line 384
  31. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.largeHorizontalPrimitive_area_limit line 391
  32. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.Explicit.actual_large_normal_packing line 418