OAI/Geometry/NearbyLagrangian/PhaseConjugacy.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Critical-locus conjugacy, transport fibers and tame packages.

  1. abbrev OAI.NearbyLagrangian.Transport.PhaseCritical line 19
  2. def OAI.NearbyLagrangian.Transport.phaseGenerate line 22
  3. def OAI.NearbyLagrangian.Transport.MorseOn line 25
  4. lemma OAI.NearbyLagrangian.Transport.baseDifferential_eq_partial line 30
  5. lemma OAI.NearbyLagrangian.Transport.StepData.phase_critical_iff line 39
  6. def OAI.NearbyLagrangian.Transport.StepData.newPhaseCriticalHomeomorph line 48
  7. def OAI.NearbyLagrangian.Transport.StepData.phaseCriticalHomeomorph line 57
  8. theorem OAI.NearbyLagrangian.Transport.StepData.phaseGenerate_conjugacy line 61
  9. def OAI.NearbyLagrangian.Transport.TransportFiber line 87
  10. instance OAI.NearbyLagrangian.Transport.transportFiberNorm line 91
  11. instance OAI.NearbyLagrangian.Transport.transportFiberSpace line 98
  12. instance OAI.NearbyLagrangian.Transport.transportFiberFinite line 105
  13. def OAI.NearbyLagrangian.Transport.iterReference line 116
  14. theorem OAI.NearbyLagrangian.Transport.StepData.tame_phase_package line 134
  15. theorem OAI.NearbyLagrangian.Transport.PreparedMixedStep.tame_step line 152