OAI/Geometry/BallPacking/Forms/ManifoldExteriorAlgebra.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm_sub line 17
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm_smul line 39
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifold_closed_exact_normalization line 50
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_smooth_manifold_cutoff line 85
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifold_local_potential_smooth line 110
  6. theorem OAI.PackingSufficiencySupport.Hamiltonian.scalar_product_tsupport_left line 124
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_global_local_potential line 134
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldFamily_local_potential_smoothOn line 175
  9. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_joint_global_local_potential line 196
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldFamily_scalar_fiber_smooth line 244
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldFamily_scalar_chart_smooth line 252
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.joint_scalar_fderiv_slice line 271
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldFamilyScalarDifferential_smooth line 280
  14. def OAI.PackingSufficiencySupport.Hamiltonian.normalizedManifoldPrimitive line 305
  15. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalizedManifoldPrimitive_chart line 310
  16. theorem OAI.PackingSufficiencySupport.Hamiltonian.normalizedManifoldPrimitive_smooth line 318
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_normalized_manifold_primitive line 341
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_normalized_manifold_primitive_neighborhood line 395
  19. def OAI.PackingSufficiencySupport.Hamiltonian.handlePushforwardOneForm line 434
  20. theorem OAI.PackingSufficiencySupport.Hamiltonian.handlePushforwardOneForm_zero line 440
  21. theorem OAI.PackingSufficiencySupport.Hamiltonian.handlePushforwardOneForm_smooth line 453
  22. theorem OAI.PackingSufficiencySupport.Hamiltonian.handlePushforwardOneForm_tsupport line 476
  23. theorem OAI.PackingSufficiencySupport.Hamiltonian.handlePushforwardOneForm_compact line 488
  24. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldExteriorOneForm_zero line 497
  25. theorem OAI.PackingSufficiencySupport.Hamiltonian.handlePushforwardOneForm_closed line 508
  26. theorem OAI.PackingSufficiencySupport.Hamiltonian.handle_mfderiv_symm_comp line 530
  27. theorem OAI.PackingSufficiencySupport.Hamiltonian.handlePushforwardOneForm_pullback line 544