OAI/Geometry/BallPacking/Forms/ChartSupportedDensity.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartSupportedTwoForm_own_chart line 15
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.extendedCoefficient_chartSupported line 25
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartMass_chartSupported line 37
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartCoefficient_integrable line 45
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.extendedChartCoefficient_add line 60
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartMass_add line 67
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartMass_smul line 76
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartMass_sub line 87
  9. def OAI.PackingSufficiencySupport.Hamiltonian.SmoothOneFormFamily line 111
  10. def OAI.PackingSufficiencySupport.Hamiltonian.SmoothTwoFormFamily line 115
  11. def OAI.PackingSufficiencySupport.Hamiltonian.HasCompactPrimitiveFamily line 119
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothOneFormFamily.spatial_smooth line 125
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.HasCompactPrimitiveFamily.zero line 132
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.HasCompactPrimitiveFamily.add line 144
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.HasCompactPrimitiveFamily.smul line 162
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.HasCompactPrimitiveFamily.sum line 179
  17. def OAI.PackingSufficiencySupport.Hamiltonian.SmoothTwoForm line 192
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothTwoFormFamily.const line 195
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothTwoFormFamily.eval line 200
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothTwoFormFamily.add line 207
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothTwoFormFamily.smul line 212
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothTwoFormFamily.neg line 220
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothTwoFormFamily.sub line 226
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartTwoForm_spatial_smul line 233
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothTwoFormFamily.spatial_smul line 242
  26. def OAI.PackingSufficiencySupport.Hamiltonian.PositivePlaneTransitions line 263
  27. structure OAI.PackingSufficiencySupport.Hamiltonian.BoxUnitBump line 268
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.SurfaceCoordinateBox.exists_unit_bump line 280
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.BoxUnitBump.mass_in_chart line 332