OAI/Geometry/NearbyLagrangian/SmoothTubeApproximation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

First-jet relative approximation and smooth localized tube representatives.

  1. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.norm_value_sub_le_jet_C1 line 19
  2. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.norm_derivative_sub_le_jet_C1 line 24
  3. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.exists_smooth_family_approx_C1 line 33
  4. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.exists_smooth_family_approx_relative_C1 line 156
  5. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.exists_smooth_negative_equiv_relative_C1 line 239
  6. theorem OAI.NearbyLagrangian.Tubes.exists_smooth_tube_relative_C1 line 278
  7. theorem OAI.NearbyLagrangian.Tubes.smooth_localized_tube_C1 line 314
  8. theorem OAI.NearbyLagrangian.Tubes.smooth_localized_kernel_C1 line 338