OAI/Geometry/BallPacking/SurfaceArea/SurfacePrimitiveOperator.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PackingSufficiencySupport.Hamiltonian.surfaceCovectorOperator line 17
  2. def OAI.PackingSufficiencySupport.Hamiltonian.surfaceCovectorSupport line 24
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceCovectorSupport_compact line 29
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceCovectorOperator_spec line 35
  5. def OAI.PackingSufficiencySupport.Hamiltonian.partitionPiece line 154
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionPiece_smooth line 157
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionPiece_add line 161
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionPiece_smul line 171
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionPiece_zero line 182
  10. def OAI.PackingSufficiencySupport.Hamiltonian.correctedPartitionPiece line 187
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.correctedPartitionPiece_smooth line 192
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.correctedPartitionPiece_zero line 199
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.correctedPartitionPiece_smul line 215
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceCovectorOperator_smul line 231
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.correctedPartitionPiece_add line 242
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfaceCovectorOperator_add line 268
  17. def OAI.PackingSufficiencySupport.Hamiltonian.smoothSupportedTwoForms line 311
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothSupportedTwoForms.smooth line 354
  19. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothSupportedTwoForms.skew line 357
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothSupportedTwoForms.zero_off line 361
  21. def OAI.PackingSufficiencySupport.Hamiltonian.surfacePrimitiveLinearMap line 372
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionFormMass_smul line 382
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionFormMass_add line 389
  24. def OAI.PackingSufficiencySupport.Hamiltonian.surfaceIntegralLinearMap line 407
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.surfacePrimitiveLinearMap_spec line 415
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionFormMass_eq_chartMass line 436
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.partitionFormMass_compact_stokes line 491
  28. theorem OAI.PackingSufficiencySupport.Hamiltonian.compactSurfaceFormIntegral_compact_stokes line 540