OAI/Geometry/NearbyLagrangian/NegativeEquivalence.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Smooth tangent-band flows and equivalence of close negative families.

  1. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.bandBump line 18
  2. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.radialShellOuter line 21
  3. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.radialShellInner line 22
  4. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.radialShell line 23
  5. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.radialShell_sphere line 26
  6. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.tangentBandField line 34
  7. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.tangentBandField_radial line 37
  8. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.tangentBandField_zero line 41
  9. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.tangentGradient_lower line 47
  10. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.tangentBandField_transverse line 59
  11. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.contMDiff_tangentBandField line 111
  12. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.contMDiff_family_spatial_fderiv line 145
  13. theorem OAI.NearbyLagrangian.ODE.param_compact_field_bounds line 166
  14. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.close_negative_family_equiv line 209