OAI/Geometry/NearbyLagrangian/PhaseErrors.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Uniform phase and joint derivative error estimates.

  1. def OAI.NearbyLagrangian.Transport.shiftError line 20
  2. lemma OAI.NearbyLagrangian.Transport.shiftError_hasCompactSupport line 25
  3. lemma OAI.NearbyLagrangian.Transport.compactSmooth_uniform_jet_bounds line 41
  4. lemma OAI.NearbyLagrangian.Transport.StepData.contDiff_shiftError line 54
  5. theorem OAI.NearbyLagrangian.Transport.StepData.shiftError_uniform_bounds line 71
  6. def OAI.NearbyLagrangian.Transport.homogeneousReference line 89
  7. def OAI.NearbyLagrangian.Transport.phaseError line 92
  8. lemma OAI.NearbyLagrangian.Transport.phaseError_eq line 97
  9. def OAI.NearbyLagrangian.Transport.verticalForget line 104
  10. lemma OAI.NearbyLagrangian.Transport.verticalForget_apply line 108
  11. lemma OAI.NearbyLagrangian.Transport.norm_verticalForget_le line 111
  12. def OAI.NearbyLagrangian.Transport.verticalMomentum line 119
  13. lemma OAI.NearbyLagrangian.Transport.verticalMomentum_apply line 122
  14. lemma OAI.NearbyLagrangian.Transport.norm_verticalMomentum_le line 125
  15. lemma OAI.NearbyLagrangian.Transport.hasFDerivAt_phaseError line 132
  16. lemma OAI.NearbyLagrangian.Transport.norm_phaseError_fderiv_le line 153
  17. theorem OAI.NearbyLagrangian.Transport.StepData.phaseError_uniform_bounds line 188
  18. def OAI.NearbyLagrangian.Transport.jointForget line 222
  19. def OAI.NearbyLagrangian.Transport.jointOld line 227
  20. def OAI.NearbyLagrangian.Transport.jointMixed line 231
  21. lemma OAI.NearbyLagrangian.Transport.norm_jointForget_le line 235
  22. lemma OAI.NearbyLagrangian.Transport.norm_jointOld_le line 243
  23. lemma OAI.NearbyLagrangian.Transport.norm_jointMixed_le line 250
  24. lemma OAI.NearbyLagrangian.Transport.hasFDerivAt_jointPhaseError line 258
  25. lemma OAI.NearbyLagrangian.Transport.norm_jointPhaseError_fderiv_le line 273
  26. theorem OAI.NearbyLagrangian.Transport.StepData.jointPhaseError_uniform_bounds line 306