OAI/Geometry/BallPacking/SurfaceArea/QuadricEndAnnuli.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.DiagonalQuadrics.curveEndAnnulus line 14
  2. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.radialAnnulus_in_end line 17
  3. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveEndAnnulus_compact line 29
  4. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveEndAnnulus_subset_target line 35
  5. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.endAnnulus_cover line 41
  6. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveEndCutoff_punctured_germ line 56
  7. theorem OAI.PackingSufficiencySupport.DiagonalQuadrics.curveEndCutoff_locally_constant_off_annuli line 64
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartMass_exterior_eq_zero line 107
  9. structure OAI.PackingSufficiencySupport.Hamiltonian.SurfaceMassTransferData line 159
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_surface_mass_transfer_data line 169
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarMarginal_add line 184
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarMarginal_smul line 190
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarPrimitiveX_add line 194
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarPrimitiveY_add line 203
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarPrimitiveX_smul line 218
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.planarPrimitiveY_smul line 224
  17. def OAI.PackingSufficiencySupport.Hamiltonian.smoothPlanarFunctions line 235
  18. def OAI.PackingSufficiencySupport.Hamiltonian.planarPrimitiveLinear line 248
  19. def OAI.PackingSufficiencySupport.Hamiltonian.primitiveLineBump line 261
  20. def OAI.PackingSufficiencySupport.Hamiltonian.fixedCovectorOperator line 264
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.primitiveLineBump_smooth line 268
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.fixedCovectorOperator_add line 271
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.fixedCovectorOperator_smul line 281
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.fixedCovectorOperator_spec line 288
  25. def OAI.PackingSufficiencySupport.Hamiltonian.translatedCovectorOperator line 352
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.translatedCovectorOperator_add line 355
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.translatedCovectorOperator_smul line 366
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.translated_covector_family_smooth line 374
  29. theorem OAI.PackingSufficiencySupport.Hamiltonian.covector_family_slice_smooth line 379
  30. theorem OAI.PackingSufficiencySupport.Hamiltonian.translatedCovectorOperator_spec line 384
  31. def OAI.PackingSufficiencySupport.Hamiltonian.boxCovectorOperator line 422
  32. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartSupportedOneForm_add line 428
  33. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartSupportedOneForm_smul line 439
  34. theorem OAI.PackingSufficiencySupport.Hamiltonian.extendedChartCoefficient_smul line 450
  35. theorem OAI.PackingSufficiencySupport.Hamiltonian.boxCovectorOperator_smul line 457
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.static_chart_coefficient_smooth line 466
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.boxCovectorOperator_add line 476
  38. theorem OAI.PackingSufficiencySupport.Hamiltonian.boxCovectorOperator_spec line 492