OAI/Geometry/BallPacking/SurfaceArea/SurfaceCutoffDefect.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.spatialCutoffDefect line 16
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.spatialCutoffDefect_smooth line 19
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.spatialCutoffDefect_skew line 26
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.spatialCutoffDefect_zero_of_locally_constant line 35
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.spatialCutoffDefect_coefficient line 53
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.cutoffWedge_radial_angular line 74
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.planar_residue_defect line 87
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarCurl_congr_of_eventuallyEq line 111
  9. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveCutoffDefect_zero_off_annuli line 126
  10. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveCutoffDefect_end_coefficient line 135
  11. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_infinityRegularPrimitive_extension line 168
  12. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.regular_extension_germ line 186
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionFormMass_eq_partialChart_supported_integral line 203
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.SmoothTwoForm.indicator line 284
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.indicator_twoForm_skew line 316
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionFormMass_finite_disjoint_charts line 331
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionFormMass_cutoff_defect line 401
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.radialCutoff_deriv_zero_off_annulus line 441
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarResidueDensity_zero_off line 456
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.integral_planar_residue_annulus line 468