OAI/Geometry/NearbyLagrangian/FamilyApproximation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Smooth approximation and close homotopies of homogeneous families.

  1. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.regular_of_sphere line 20
  2. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.fderiv_blend line 34
  3. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.controlledBlend line 42
  4. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.controlledBlend_zero line 66
  5. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.controlledBlend_one_apply line 72
  6. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.continuous_controlledBlend line 78
  7. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.norm_value_sub_le_jet line 110
  8. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.norm_derivative_sub_le_jet line 115
  9. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.exists_smooth_family_approx line 124
  10. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.exists_smooth_homotopic line 241
  11. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.norm_jet_error_of_sphere line 310
  12. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.exists_smooth_homotopic_close line 345