OAI/Geometry/BallPacking/SurfaceArea/SurfaceIntegralIndependence.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionFormMass_independent line 19
  2. def OAI.PackingSufficiencySupport.Hamiltonian.chartInverseExtension line 107
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartInverseExtension_measurable line 110
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartInverseExtension_eq line 116
  5. def OAI.PackingSufficiencySupport.Hamiltonian.chartAreaMeasure line 120
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartAreaMeasure_finite line 124
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.integral_chartAreaMeasure line 132
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.integrable_chartAreaMeasure line 150
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartAreaMeasure_null line 168
  10. def OAI.PackingSufficiencySupport.Hamiltonian.partitionChartDensity line 194
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionChartDensity_off_target line 199
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionChartDensity_nonneg line 205
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionChartDensity_spatial_smul line 219
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionChartDensity_properties line 235
  15. def OAI.PackingSufficiencySupport.Hamiltonian.partitionAreaMeasure line 272
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionAreaMeasure_finite line 277
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.integral_partitionAreaMeasure line 286
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.integral_chartAreaMeasure_restrict line 321
  19. def OAI.PackingSufficiencySupport.Hamiltonian.restrictedPartitionFormMass line 354
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.smooth_integrable_partitionAreaMeasure line 363
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.integral_partitionAreaMeasure_restrict line 382
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionAreaMeasure_null line 409
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartRegion_measurable line 423
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.extendedChartCoefficient_indicator line 437
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.extendedChartCoefficient_indicator_integrable line 451
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.restrictedPartitionFormMass_eq_indicator line 457
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionFormMass_independent_integrable line 483