OAI/Geometry/BallPacking/Forms/FixedSpatialIntegral.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.planar_fixed_support_integral_smooth line 14
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_planar_unit_bump line 50
  3. structure OAI.PackingSufficiencySupport.Hamiltonian.SurfaceCoordinateBox line 93
  4. def OAI.PackingSufficiencySupport.Hamiltonian.SurfaceCoordinateBox.carrier line 102
  5. def OAI.PackingSufficiencySupport.Hamiltonian.SurfaceCoordinateBox.compactCarrier line 106
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.SurfaceCoordinateBox.isOpen_carrier line 109
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.SurfaceCoordinateBox.isCompact_compactCarrier line 113
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.SurfaceCoordinateBox.compactCarrier_subset line 117
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.SurfaceCoordinateBox.carrier_subset_compactCarrier line 122
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.SurfaceCoordinateBox.nonempty_carrier line 128
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.SurfaceCoordinateBox.exists_mem line 137
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.SurfaceCoordinateBox.exists_compactCarrier_subset line 148
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.SurfaceCoordinateBox.finite_partition line 168
  14. def OAI.PackingSufficiencySupport.Hamiltonian.spatialZeroExtension line 194
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.spatialZeroExtension_smooth line 198
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.spatialZeroExtension_zero line 218
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.planar_skew_coefficient line 233
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartTwoForm_change line 243
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartTwoForm_skew line 256
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartTwoForm_density_change line 261
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.chart_area_integral_change line 271
  22. def OAI.PackingSufficiencySupport.Hamiltonian.extendedChartCoefficient line 335
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartCoefficient_zero line 340
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.extendedChartCoefficient_zero line 352
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.extendedChartCoefficient_smooth line 359
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartSupported_extendedCoefficient line 375
  27. def OAI.PackingSufficiencySupport.Hamiltonian.chartMass line 404
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartMass_eq_setIntegral line 407
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartMass_change line 421
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartMass_smooth line 434
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartOneForm_add line 465
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartOneForm_smul line 471
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartOneForm_zero line 477
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartTwoForm_add line 479
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartTwoForm_smul line 487
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartTwoForm_zero line 495
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclideanExteriorOneForm_add line 497
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.euclideanExteriorOneForm_smul line 506