OAI/Geometry/NearbyLagrangian/Phase.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Shifted generating phases, partial derivatives and critical-point bounds.

  1. def OAI.NearbyLagrangian.Transport.shiftedPhase line 16
  2. def OAI.NearbyLagrangian.Transport.baseDifferential line 20
  3. def OAI.NearbyLagrangian.Transport.verticalDifferential line 23
  4. lemma OAI.NearbyLagrangian.Transport.derivative_split line 26
  5. lemma OAI.NearbyLagrangian.Transport.hasFDerivAt_shiftedPhase_p line 33
  6. lemma OAI.NearbyLagrangian.Transport.hasFDerivAt_shiftedPhase_z line 40
  7. lemma OAI.NearbyLagrangian.Transport.hasFDerivAt_shiftedPhase_w line 64
  8. lemma OAI.NearbyLagrangian.Transport.hasFDerivAt_shiftedPhase_X line 86
  9. lemma OAI.NearbyLagrangian.Transport.displacement_bound_of_critical_p line 120
  10. lemma OAI.NearbyLagrangian.Transport.norm_shiftedPhase_w_lower line 130
  11. lemma OAI.NearbyLagrangian.Transport.shiftedPhase_w_ne_zero line 160
  12. def OAI.NearbyLagrangian.Transport.productCutoff line 175
  13. lemma OAI.NearbyLagrangian.Transport.fderiv_productCutoff_w line 179
  14. lemma OAI.NearbyLagrangian.Transport.norm_fderiv_productCutoff_w_le line 186