The full rotation of a complex normed space

The full rotation t ↦ e^{2πit} of a complex normed space E, read as a loop of real-linear operators (TauCeti.rotationLoop), is a continuous closed loop (TauCeti.continuous_rotationLoop, TauCeti.rotationLoop_zero_eq_one). On a complex inner product space it preserves the inner product (TauCeti.inner_rotationLoop_apply), so it is a loop of linear symplectic maps for Im ⟪·, ·⟫; it normalizes the Maslov index of such loops.

noncomputable def TauCeti.rotationLoop (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℂ E] (t : ↑unitInterval) : E →L[ℝ] E

The full rotation t ↦ e^{2πit} of a complex normed space, as a loop of real-linear maps.

@[simp]

theorem TauCeti.rotationLoop_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (t : ↑unitInterval) (z : E) : (rotationLoop E t) z = Complex.exp (↑(2 * Real.pi * ↑t) * Complex.I) • z

The full rotation at time t is multiplication by e^{2πit}.

theorem TauCeti.continuous_rotationLoop (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℂ E] : Continuous (rotationLoop E)

The full rotation is a continuous family of operators.

theorem TauCeti.rotationLoop_zero_eq_one (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℂ E] : rotationLoop E 0 = rotationLoop E 1

The full rotation is a closed loop.

theorem TauCeti.inner_rotationLoop_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (t : ↑unitInterval) (x y : E) : inner ℂ ((rotationLoop E t) x) ((rotationLoop E t) y) = inner ℂ x y

The full rotation preserves the inner product, so in particular the symplectic form Im ⟪·, ·⟫.