OAI/Geometry/NearbyLagrangian/Restoration.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Smooth restoration of prescribed homogeneous tails and critical jets.

  1. def OAI.NearbyLagrangian.InfinityRestore.restoreFamily line 21
  2. lemma OAI.NearbyLagrangian.InfinityRestore.restoreFamily_eq_inner line 25
  3. lemma OAI.NearbyLagrangian.InfinityRestore.restoreFamily_eq_outer line 30
  4. lemma OAI.NearbyLagrangian.InfinityRestore.restoreFamily_near_inner line 36
  5. lemma OAI.NearbyLagrangian.InfinityRestore.restoreFamily_near_outer line 43
  6. lemma OAI.NearbyLagrangian.InfinityRestore.contDiffAt_restoreFamily line 49
  7. lemma OAI.NearbyLagrangian.InfinityRestore.restoreFamily_jets line 60
  8. theorem OAI.NearbyLagrangian.InfinityRestore.restoreFamily_critical_and_jets line 74
  9. lemma OAI.NearbyLagrangian.InfinityRestore.exists_restoration_radius_above line 106
  10. theorem OAI.NearbyLagrangian.InfinityRestore.exists_restored_family line 122
  11. lemma OAI.NearbyLagrangian.InfinityRestore.fiber_jets_of_eventuallyEq line 164
  12. lemma OAI.NearbyLagrangian.InfinityRestore.restoreFamily_joint_germ line 182
  13. lemma OAI.NearbyLagrangian.InfinityRestore.contMDiffAt_restoreFamily line 190
  14. theorem OAI.NearbyLagrangian.InfinityRestore.exists_restored_manifold_family line 202
  15. theorem OAI.NearbyLagrangian.InfinityRestore.exists_smooth_homogeneous_tail line 255
  16. theorem OAI.NearbyLagrangian.InfinityRestore.exists_smooth_homogeneous_tail_of_lower_bound line 305