OAI/Geometry/NearbyLagrangian/MorseTransport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Smooth transport of regular Morse generating families.

  1. lemma OAI.NearbyLagrangian.Transport.contDiffAt_baseGradient line 21
  2. lemma OAI.NearbyLagrangian.Transport.StepData.contDiffAt_carry line 33
  3. lemma OAI.NearbyLagrangian.Transport.StepData.contDiff_recover line 43
  4. lemma OAI.NearbyLagrangian.Transport.StepData.contDiffAt_totalPhase line 50
  5. theorem OAI.NearbyLagrangian.Transport.exists_hamiltonian_step_data line 74
  6. theorem OAI.NearbyLagrangian.Transport.StepData.transported_morse_family line 123