OAI/Geometry/BallPacking/SurfaceArea/QuadricEndResidueMass.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveEndAnnulus_coordinates line 15
  2. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveEndCutoff_partition_mass line 21
  3. def OAI.PackingSufficiencySupport.Hamiltonian.partitionOnSubset line 78
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionFormMass_independent_support line 88
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.compactSurfaceFormIntegral_eq_larger_partition line 104
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.compactSurfaceFormIntegral_eq_setIntegral line 113
  7. def OAI.PackingSufficiencySupport.Hamiltonian.surfaceCutoffMass line 132
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceCutoffMass_eq line 138
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceCutoffMass_le_compactIntegral line 163
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.compactIntegral_le_surfaceCutoffMass line 184
  11. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveEndCutoff_surface_mass line 222
  12. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.tendsto_curveEndCutoff_mass line 242
  13. def OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.realSliceChart line 268
  14. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.realSliceChart_source line 272
  15. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.realSliceChart_smooth line 275
  16. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.realSliceChart_symm_smooth line 281
  17. def OAI.PackingSufficiencySupport.DiagonalQuadrics.NormalChart.realSliceDiffeomorph line 293
  18. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.exists_projection_chart line 301
  19. abbrev OAI.PackingSufficiencySupport.DiskPlane line 317
  20. def OAI.PackingSufficiencySupport.diskBoundaryMap line 319
  21. def OAI.PackingSufficiencySupport.diskBoundaryDerivative line 322
  22. theorem OAI.PackingSufficiencySupport.diskBoundaryMap_smooth line 326
  23. theorem OAI.PackingSufficiencySupport.diskBoundaryMap_hasFDerivAt line 330
  24. theorem OAI.PackingSufficiencySupport.diskBoundaryDerivative_bijective line 340
  25. theorem OAI.PackingSufficiencySupport.exists_diskBoundaryDiffeomorph line 367
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.planar_curve_image_null line 408
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.smooth_curve_chart_null line 425
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.countable_smooth_curve_cover_chart_null line 446
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.one_dimensional_image_chart_null line 457
  30. def OAI.PackingSufficiencySupport.Hamiltonian.HasSmoothSurfaceBoundary line 484
  31. theorem OAI.PackingSufficiencySupport.Hamiltonian.smooth_boundary_coordinate_zero line 489
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.smooth_surface_boundary_chart_null line 504