OAI/MeasureTheory/Falconer/Angular/NorthRotation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Sending the prepared direction to the canonical north pole

An orthogonal reflection handles every equal-norm pair, including opposite directions. Normalization and all cap distances commute with this fixed linear isometry, so the original prepared cap can be transported exactly.

  1. theorem OAI.Falconer.exists_isometry_of_norm_eq line 17
  2. theorem OAI.Falconer.linearIsometryEquiv_normalize line 21
  3. theorem OAI.Falconer.linearIsometryEquiv_normalize_sub line 25
  4. theorem OAI.Falconer.linearIsometryEquiv_cap_norm line 29
  5. def OAI.Falconer.northRotation line 34
  6. theorem OAI.Falconer.northRotation_apply line 38
  7. theorem OAI.Falconer.northRotation_sphereMap line 42
  8. theorem OAI.Falconer.northRotation_normalize_sub line 47
  9. theorem OAI.Falconer.northRotation_cap_norm line 51
  10. theorem OAI.Falconer.northRotation_cap_iff line 58
  11. def OAI.Falconer.reverseNorthRotation line 65

    Source documentation

    Preparation uses the direction y-x; the inverse phase uses x-y.

    noncomputable def reverseNorthRotation {n : ℕ} (u : Sphere (n+1)) :
    Space (n+1) ≃ₗᵢ[ℝ] Space (n+1) :=
…

    Mentions: OAI.Falconer.Sphere, OAI.Falconer.Space

  12. theorem OAI.Falconer.reverseNorthRotation_apply line 69
  13. theorem OAI.Falconer.reverseNorthRotation_cap_norm line 75
  14. theorem OAI.Falconer.reverseNorthRotation_cap_lt_iff line 83