OAI/Geometry/NearbyLagrangian/StepData.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Small-step data and the homeomorphism of old and new critical loci.

  1. def OAI.NearbyLagrangian.Transport.baseGradient line 20
  2. lemma OAI.NearbyLagrangian.Transport.innerSL_baseGradient line 23
  3. lemma OAI.NearbyLagrangian.Transport.eq_one_near_of_norm_lt line 29
  4. structure OAI.NearbyLagrangian.Transport.StepData line 36
  5. def OAI.NearbyLagrangian.Transport.StepData.κ line 83
  6. def OAI.NearbyLagrangian.Transport.StepData.shiftedBase line 85
  7. lemma OAI.NearbyLagrangian.Transport.StepData.diff_F line 88
  8. lemma OAI.NearbyLagrangian.Transport.StepData.diff_σ_p line 92
  9. lemma OAI.NearbyLagrangian.Transport.StepData.diff_σ_X line 97
  10. lemma OAI.NearbyLagrangian.Transport.StepData.diff_κ_w line 102
  11. lemma OAI.NearbyLagrangian.Transport.StepData.diff_κ_z line 106
  12. lemma OAI.NearbyLagrangian.Transport.StepData.diff_κ_X line 110
  13. lemma OAI.NearbyLagrangian.Transport.StepData.diff_phase line 114
  14. lemma OAI.NearbyLagrangian.Transport.StepData.old_critical_bound line 123
  15. lemma OAI.NearbyLagrangian.Transport.StepData.new_critical_bounds line 133
  16. lemma OAI.NearbyLagrangian.Transport.StepData.κ_one_w line 146
  17. lemma OAI.NearbyLagrangian.Transport.StepData.κ_one_z line 152
  18. lemma OAI.NearbyLagrangian.Transport.StepData.κ_one_X line 158
  19. lemma OAI.NearbyLagrangian.Transport.StepData.κ_zero line 165
  20. theorem OAI.NearbyLagrangian.Transport.StepData.new_to_old line 169
  21. theorem OAI.NearbyLagrangian.Transport.StepData.old_to_new line 216
  22. def OAI.NearbyLagrangian.Transport.StepData.carry line 259
  23. def OAI.NearbyLagrangian.Transport.StepData.recover line 264
  24. def OAI.NearbyLagrangian.Transport.StepData.OldCritical line 267
  25. def OAI.NearbyLagrangian.Transport.StepData.NewCritical line 269
  26. instance OAI.NearbyLagrangian.Transport.StepData.(instance at line 272) line 272
  27. instance OAI.NearbyLagrangian.Transport.StepData.(instance at line 275) line 275
  28. def OAI.NearbyLagrangian.Transport.StepData.carryCritical line 279
  29. def OAI.NearbyLagrangian.Transport.StepData.recoverCritical line 283
  30. lemma OAI.NearbyLagrangian.Transport.StepData.recover_carry line 287
  31. lemma OAI.NearbyLagrangian.Transport.StepData.carry_recover line 295
  32. lemma OAI.NearbyLagrangian.Transport.continuousAt_baseGradient line 304
  33. lemma OAI.NearbyLagrangian.Transport.StepData.continuousAt_carry line 318
  34. lemma OAI.NearbyLagrangian.Transport.StepData.continuousAt_recover line 328
  35. lemma OAI.NearbyLagrangian.Transport.StepData.continuous_carryCritical line 335
  36. lemma OAI.NearbyLagrangian.Transport.StepData.continuous_recoverCritical line 341
  37. def OAI.NearbyLagrangian.Transport.StepData.criticalHomeomorph line 344
  38. theorem OAI.NearbyLagrangian.Transport.StepData.new_output line 352