OAI/Geometry/NearbyLagrangian/MixedGraphs.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Mixed graph equations, displacement bounds and twist regularity.

  1. lemma OAI.NearbyLagrangian.Transport.mixed_partial_derivatives line 20
  2. theorem OAI.NearbyLagrangian.Transport.mixed_graph_iff line 42
  3. lemma OAI.NearbyLagrangian.Transport.mixed_graph_output line 69
  4. theorem OAI.NearbyLagrangian.Transport.mixed_momentum_derivative_bound line 82
  5. lemma OAI.NearbyLagrangian.Transport.mapsTo_compact_support line 100
  6. lemma OAI.NearbyLagrangian.Transport.mixed_image_projection line 111
  7. lemma OAI.NearbyLagrangian.Transport.mixedSigma_zero_off_projection line 129
  8. theorem OAI.NearbyLagrangian.Transport.exists_controlled_mixed_generator line 149
  9. lemma OAI.NearbyLagrangian.Transport.mixedDisplacement_eq_inverse line 220
  10. theorem OAI.NearbyLagrangian.Transport.mixed_twist_surjective line 234
  11. theorem OAI.NearbyLagrangian.Transport.StepData.regular_at_newCritical_of_twist line 283