OAI/Geometry/NearbyLagrangian/RelativeApproximation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Relative smooth approximation of homogeneous functions and tubes.

  1. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.exists_smooth_family_approx_relative line 22
  2. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.exists_smooth_negative_equiv_relative line 99
  3. theorem OAI.NearbyLagrangian.Tubes.exists_smooth_tube_relative line 133
  4. lemma OAI.NearbyLagrangian.Tubes.contDiff_standardForm line 157