OAI/Geometry/NearbyLagrangian/CylinderCutoffs.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Smooth cylinder cutoffs and compact extension of isotopies.

  1. def OAI.NearbyLagrangian.PolarCylinder.squareBump line 19
  2. def OAI.NearbyLagrangian.PolarCylinder.squareCutoff line 25
  3. lemma OAI.NearbyLagrangian.PolarCylinder.contDiff_squareCutoff line 28
  4. lemma OAI.NearbyLagrangian.PolarCylinder.squareCutoff_mem_Icc line 33
  5. lemma OAI.NearbyLagrangian.PolarCylinder.squareCutoff_eq_one line 40
  6. lemma OAI.NearbyLagrangian.PolarCylinder.squareCutoff_eventuallyEq_one line 50
  7. lemma OAI.NearbyLagrangian.PolarCylinder.squareCutoff_support line 56
  8. lemma OAI.NearbyLagrangian.PolarCylinder.squareCutoff_gradient_bound line 88
  9. def OAI.NearbyLagrangian.PolarCylinder.momentumBump line 99
  10. lemma OAI.NearbyLagrangian.PolarCylinder.momentumBump_plateau line 105
  11. lemma OAI.NearbyLagrangian.antisymmetric_CLM_zero_right line 115
  12. lemma OAI.NearbyLagrangian.symplecticForm_zero_right line 120
  13. theorem OAI.NearbyLagrangian.IsCompactHamiltonianIsotopy.cylinder_extension line 124