Documentation

SphereEversion.ToMathlib.Analysis.InnerProductSpace.Rotation

Rotation about an axis, considered as a function in that axis #

source
def Orientation.rot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (p : ℝ × E) :
E →L[ℝ] E

A family of endomorphisms of E, parametrized by ℝ × E. The idea is that for nonzero v : E and t : ℝ this endomorphism will be the rotation by the angle t about the axis spanned by v.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Orientation.rotAux {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (p : ℝ × E) :
    E →L[ℝ] E

    Alternative form of the construction rot, convenient for the smoothness calculation.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Orientation.rot_eq_aux {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) :
      ω.rot = ω.rotAux
      source
      theorem Orientation.contDiff_rot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) {p : ℝ × E} (hp : p.2 ≠ 0) :
      ContDiffAt ℝ ⊤ ω.rot p

      The map rot is smooth on ℝ × (E \ {0}).

      source
      theorem Orientation.rot_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (v : E) :
      ω.rot (0, v) = ContinuousLinearMap.id ℝ E

      The map rot sends {0} × E to the identity.

      source
      theorem Orientation.rot_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (v : E) {w : E} (hw : w ∈ (Submodule.span ℝ {v})ᗮ) :
      (ω.rot (1, v)) w = -w

      The map rot sends (1, v) to a transformation which on (ℝ ∙ v)ᗮ acts as the negation.

      source
      @[simp]
      theorem Orientation.rot_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (p : ℝ × E) :
      (ω.rot p) p.2 = p.2

      The map rot sends (v, t) to a transformation fixing v.

      source
      theorem Orientation.rot_eq_of_mem_span {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (p : ℝ × E) {x : E} (hx : x ∈ Submodule.span ℝ {p.2}) :
      (ω.rot p) x = x

      The map rot sends (t, v) to a transformation preserving span v.

      source
      theorem Orientation.inner_rot_apply_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (p : ℝ × E) (w : E) (hw : w ∈ (Submodule.span ℝ {p.2})ᗮ) :
      inner ℝ ((ω.rot p) w) p.2 = 0

      The map rot sends (v, t) to a transformation preserving the subspace (ℝ ∙ v)ᗮ.

      source
      theorem Orientation.isometry_on_rot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (t : ℝ) (v : ↑(Metric.sphere 0 1)) (w : ↥(Submodule.span ℝ {↑v})ᗮ) :
      ‖(ω.rot (t, ↑v)) ↑w‖ = ‖↑w‖
      source
      theorem Orientation.isometry_rot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (t : ℝ) (v : ↑(Metric.sphere 0 1)) :
      Isometry ⇑(ω.rot (t, ↑v))
      source
      theorem Orientation.injOn_rot_of_ne {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (t : ℝ) {x : E} (hx : x ≠ 0) :
      Set.InjOn ⇑(ω.rot (t, x)) ↑(Submodule.span ℝ {x})ᗮ
      source
      theorem Orientation.injOn_rot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (t : ℝ) (x : ↑(Metric.sphere 0 1)) :
      Set.InjOn ⇑(ω.rot (t, ↑x)) ↑(Submodule.span ℝ {↑x})ᗮ