OAI/Geometry/BallPacking/RelativeJets/EmbeddingAdaptedNeighborhood.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.embedding_adapted_neighborhood line 18
  2. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_relative_jet_patch line 55
  3. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothPartition_eventually_finite_sum line 109
  4. theorem OAI.PackingSufficiencySupport.Hamiltonian.smoothPartition_glues_zero_first_jet line 124
  5. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_smooth_zero_first_jet line 160
  6. def OAI.PackingSufficiencySupport.Hamiltonian.embeddedNormalJet line 183
  7. theorem OAI.PackingSufficiencySupport.Hamiltonian.embeddedNormalJet_apply line 192
  8. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_relative_global_potential line 206
  9. def OAI.PackingSufficiencySupport.Hamiltonian.correctedOneForm line 250
  10. theorem OAI.PackingSufficiencySupport.Hamiltonian.chartOneForm_corrected line 254
  11. theorem OAI.PackingSufficiencySupport.Hamiltonian.ManifoldMoserData.corrected line 262
  12. theorem OAI.PackingSufficiencySupport.Hamiltonian.manifoldSpatialDifferential_of_jet line 308
  13. theorem OAI.PackingSufficiencySupport.Hamiltonian.ManifoldMoserData.skew_intrinsic line 323
  14. theorem OAI.PackingSufficiencySupport.Hamiltonian.relative_moser_field_related line 334