OAI/Geometry/BallPacking/Normal/MovingPrimitiveNaturality.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PackingSufficiencySupport.Hamiltonian.movingPrimitivePullback_exterior_comp line 16
  2. def OAI.PackingSufficiencySupport.NormalLift.adjointCLM line 50
  3. def OAI.PackingSufficiencySupport.NormalLift.gram line 56
  4. def OAI.PackingSufficiencySupport.NormalLift.rightLift line 58
  5. theorem OAI.PackingSufficiencySupport.NormalLift.gram_invertible line 61
  6. theorem OAI.PackingSufficiencySupport.NormalLift.rightLift_right_inverse line 73
  7. theorem OAI.PackingSufficiencySupport.NormalLift.gram_contDiff line 76
  8. theorem OAI.PackingSufficiencySupport.NormalLift.rightLift_contDiffAt line 79
  9. theorem OAI.PackingSufficiencySupport.NormalLift.rightLift_family_contDiffAt line 84
  10. abbrev OAI.PackingSufficiencySupport.NormalLift.HilbertModel line 95
  11. def OAI.PackingSufficiencySupport.NormalLift.hilbertEquiv line 98
  12. def OAI.PackingSufficiencySupport.NormalLift.hilbertArrow line 102
  13. def OAI.PackingSufficiencySupport.NormalLift.finiteRightLift line 105
  14. theorem OAI.PackingSufficiencySupport.NormalLift.hilbertArrow_surjective line 111
  15. theorem OAI.PackingSufficiencySupport.NormalLift.finiteRightLift_right_inverse line 119
  16. theorem OAI.PackingSufficiencySupport.NormalLift.finiteRightLift_contDiffAt line 124
  17. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_uniform_short_transport line 140
  18. theorem OAI.PackingSufficiencySupport.Hamiltonian.exists_compact_localized_manifold_flow line 173
  19. theorem OAI.PackingSufficiencySupport.NormalLift.curve_eq_add_of_hasDerivAt line 220
  20. theorem OAI.PackingSufficiencySupport.NormalLift.exists_compact_normal_flow line 234
  21. abbrev OAI.PackingSufficiencySupport.NormalLift.zeroFibre line 282
  22. abbrev OAI.PackingSufficiencySupport.NormalLift.tubeDomain line 283
  23. def OAI.PackingSufficiencySupport.NormalLift.tubeSlice line 285
  24. theorem OAI.PackingSufficiencySupport.NormalLift.tubeSlice_isEmbedding line 290
  25. def OAI.PackingSufficiencySupport.CubicModel.regularLocus line 327
  26. theorem OAI.PackingSufficiencySupport.CubicModel.regularLocus_isOpen line 329
  27. theorem OAI.PackingSufficiencySupport.CubicModel.regular_jacobian_surjective line 334
  28. def OAI.PackingSufficiencySupport.CubicModel.realJacobian line 344
  29. theorem OAI.PackingSufficiencySupport.CubicModel.realJacobian_contDiff line 347
  30. def OAI.PackingSufficiencySupport.CubicModel.normalLift line 353
  31. theorem OAI.PackingSufficiencySupport.CubicModel.normalLift_projects line 356
  32. theorem OAI.PackingSufficiencySupport.CubicModel.normalLift_contDiffOn line 360
  33. theorem OAI.PackingSufficiencySupport.CubicModel.exists_compact_normal_lift line 365
  34. theorem OAI.PackingSufficiencySupport.CubicModel.inclusion_real_contMDiff line 382
  35. theorem OAI.PackingSufficiencySupport.CubicModel.exists_actual_cubic_normal_tube line 386
  36. theorem OAI.PackingSufficiencySupport.Hamiltonian.primitivePullback_smoothAt line 457
  37. theorem OAI.PackingSufficiencySupport.Hamiltonian.primitivePullback_exteriorAt line 462