OAI/Geometry/NearbyLagrangian/Latitude.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Controlled latitude deformations on split unit spheres.

  1. def OAI.NearbyLagrangian.RadialTopology.latitudeCap line 16
  2. def OAI.NearbyLagrangian.RadialTopology.latitude line 17
  3. def OAI.NearbyLagrangian.RadialTopology.latitudeRadius line 20
  4. lemma OAI.NearbyLagrangian.RadialTopology.latitudeCap_mem line 23
  5. lemma OAI.NearbyLagrangian.RadialTopology.latitudeCap_of_abs_le line 28
  6. lemma OAI.NearbyLagrangian.RadialTopology.latitudeCap_of_le line 36
  7. lemma OAI.NearbyLagrangian.RadialTopology.latitudeCap_of_neg_le line 42
  8. lemma OAI.NearbyLagrangian.RadialTopology.latitudeCap_sq_of_abs_ge line 48
  9. lemma OAI.NearbyLagrangian.RadialTopology.latitudeCap_ge_of_nonneg line 58
  10. lemma OAI.NearbyLagrangian.RadialTopology.latitudeCap_le_of_nonpos line 65
  11. lemma OAI.NearbyLagrangian.RadialTopology.latitude_mem line 72
  12. lemma OAI.NearbyLagrangian.RadialTopology.abs_le_latitude line 82
  13. lemma OAI.NearbyLagrangian.RadialTopology.sq_le_latitude_sq line 99
  14. lemma OAI.NearbyLagrangian.RadialTopology.latitude_zero line 105
  15. lemma OAI.NearbyLagrangian.RadialTopology.latitude_one line 106
  16. lemma OAI.NearbyLagrangian.RadialTopology.latitudeRadius_nonneg line 107
  17. lemma OAI.NearbyLagrangian.RadialTopology.latitudeRadius_sq line 110
  18. lemma OAI.NearbyLagrangian.RadialTopology.latitudeRadius_le line 118
  19. lemma OAI.NearbyLagrangian.RadialTopology.latitudeRadius_zero_time line 127
  20. lemma OAI.NearbyLagrangian.RadialTopology.latitudeRadius_one_eq_zero line 135
  21. lemma OAI.NearbyLagrangian.RadialTopology.continuous_latitudeCap line 140
  22. lemma OAI.NearbyLagrangian.RadialTopology.continuous_latitude line 144
  23. lemma OAI.NearbyLagrangian.RadialTopology.continuous_latitudeRadius line 149
  24. abbrev OAI.NearbyLagrangian.RadialTopology.NormSphere line 161
  25. abbrev OAI.NearbyLagrangian.RadialTopology.SplitSphere line 162
  26. def OAI.NearbyLagrangian.RadialTopology.splitSphereProjection line 165
  27. lemma OAI.NearbyLagrangian.RadialTopology.splitSphere_abs_latitude line 169
  28. def OAI.NearbyLagrangian.RadialTopology.splitNormalize line 174
  29. lemma OAI.NearbyLagrangian.RadialTopology.splitOrigin_ne_of_radius_ne line 178
  30. abbrev OAI.NearbyLagrangian.RadialTopology.SplitNonzeroRadius line 187
  31. def OAI.NearbyLagrangian.RadialTopology.latitudeAngle line 190
  32. def OAI.NearbyLagrangian.RadialTopology.flowRadiusVector line 206
  33. lemma OAI.NearbyLagrangian.RadialTopology.norm_flowRadiusVector line 212
  34. lemma OAI.NearbyLagrangian.RadialTopology.continuous_flowRadiusVector line 220
  35. lemma OAI.NearbyLagrangian.RadialTopology.flowRadiusVector_of_nonzero line 231
  36. lemma OAI.NearbyLagrangian.RadialTopology.flowRadiusVector_of_zero line 246
  37. def OAI.NearbyLagrangian.RadialTopology.latitudeDeform line 256
  38. lemma OAI.NearbyLagrangian.RadialTopology.latitudeDeform_base line 269
  39. lemma OAI.NearbyLagrangian.RadialTopology.latitudeDeform_zero line 274