OAI/Geometry/NearbyLagrangian/PhaseRegularity.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Regularity of pure and exterior phases and the cutoff transition.

  1. lemma OAI.NearbyLagrangian.Transport.verticalDifferential_eq_partial line 22
  2. lemma OAI.NearbyLagrangian.Transport.differentiableAt_purePhase line 28
  3. lemma OAI.NearbyLagrangian.Transport.purePhase_fiberDerivative line 47
  4. lemma OAI.NearbyLagrangian.Transport.differentiableAt_verticalDifferential line 89
  5. lemma OAI.NearbyLagrangian.Transport.differentiableAt_baseGradient line 95
  6. lemma OAI.NearbyLagrangian.Transport.differentiableAt_mixedDisplacement line 103
  7. theorem OAI.NearbyLagrangian.Transport.regular_purePhase line 108
  8. def OAI.NearbyLagrangian.Transport.outsideShift line 180
  9. def OAI.NearbyLagrangian.Transport.forgetMomentum line 186
  10. def OAI.NearbyLagrangian.Transport.outsideDerivative line 191
  11. theorem OAI.NearbyLagrangian.Transport.outsideDerivative_surjective line 197
  12. lemma OAI.NearbyLagrangian.Transport.hasFDerivAt_outsideShift line 212
  13. def OAI.NearbyLagrangian.Transport.outsideSystem line 225
  14. lemma OAI.NearbyLagrangian.Transport.hasFDerivAt_outsideSystem line 229
  15. def OAI.NearbyLagrangian.Transport.outsideMomentum line 251
  16. lemma OAI.NearbyLagrangian.Transport.differentiableAt_outsidePhase line 255
  17. lemma OAI.NearbyLagrangian.Transport.outsidePhase_fiberDerivative line 272
  18. lemma OAI.NearbyLagrangian.Transport.differentiableAt_outsideMomentum line 315
  19. theorem OAI.NearbyLagrangian.Transport.regular_outsidePhase line 333
  20. lemma OAI.NearbyLagrangian.Transport.twist_surjective_of_norm_lt_one line 379
  21. lemma OAI.NearbyLagrangian.Transport.StepData.cutoff_near_critical line 398
  22. lemma OAI.NearbyLagrangian.Transport.StepData.phase_near_supported line 410
  23. lemma OAI.NearbyLagrangian.Transport.StepData.phase_near_outside line 419
  24. theorem OAI.NearbyLagrangian.Transport.StepData.regular_at_newCritical line 428