Reflection

A linear isometry equivalence K.reflection : E ≃ₗᵢ[𝕜] E in constructed, by choosing for each u : E, K.reflection u = 2 • K.starProjection u - u.

def Submodule.reflectionLinearEquiv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : E ≃ₗ[𝕜] E

Auxiliary definition for reflection: the reflection as a linear equivalence.

def Submodule.reflection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : E ≃ₗᵢ[𝕜] E

Reflection in a complete subspace of an inner product space. The word "reflection" is sometimes understood to mean specifically reflection in a codimension-one subspace, and sometimes more generally to cover operations such as reflection in a point. The definition here, of reflection in a subspace, is a more general sense of the word that includes both those common cases.

theorem Submodule.reflection_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (p : E) : K.reflection p = 2 • K.starProjection p - p

The result of reflecting.

@[simp]

theorem Submodule.reflection_symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] : K.reflection.symm = K.reflection

Reflection is its own inverse.

@[simp]

theorem Submodule.reflection_inv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] : K.reflection⁻¹ = K.reflection

Reflection is its own inverse.

@[simp]

theorem Submodule.reflection_reflection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (p : E) : K.reflection (K.reflection p) = p

Reflecting twice in the same subspace.

theorem Submodule.reflection_involutive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : Function.Involutive ⇑K.reflection

Reflection is involutive.

@[simp]

theorem Submodule.reflection_trans_reflection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : K.reflection.trans K.reflection = LinearIsometryEquiv.refl 𝕜 E

Reflection is involutive.

@[simp]

theorem Submodule.reflection_mul_reflection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : K.reflection * K.reflection = 1

Reflection is involutive.

theorem Submodule.reflection_orthogonal_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (v : E) : Kᗮ.reflection v = -K.reflection v

theorem Submodule.reflection_orthogonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : Kᗮ.reflection = K.reflection.trans (LinearIsometryEquiv.neg 𝕜)

theorem Submodule.reflection_singleton_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (u v : E) : (span 𝕜 {u}).reflection v = 2 • (inner 𝕜 u v / ↑‖u‖ ^ 2) • u - v

theorem Submodule.reflection_eq_self_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (x : E) : K.reflection x = x ↔ x ∈ K

A point is its own reflection if and only if it is in the subspace.

theorem Submodule.reflection_mem_subspace_eq_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] {x : E} (hx : x ∈ K) : K.reflection x = x

theorem Submodule.reflection_map_apply {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_4} {E' : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (x : E') : (map (↑f.toLinearEquiv) K).reflection x = f (K.reflection (f.symm x))

Reflection in the Submodule.map of a subspace.

theorem Submodule.reflection_map {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_4} {E' : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : (map (↑f.toLinearEquiv) K).reflection = f.symm.trans (K.reflection.trans f)

Reflection in the Submodule.map of a subspace.

@[simp]

theorem Submodule.reflection_bot {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : ⊥.reflection = LinearIsometryEquiv.neg 𝕜

Reflection through the trivial subspace {0} is just negation.

theorem Submodule.reflection_mem_subspace_orthogonalComplement_eq_neg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] {v : E} (hv : v ∈ Kᗮ) : K.reflection v = -v

The reflection in K of an element of Kᗮ is its negation.

theorem Submodule.reflection_mem_subspace_orthogonal_precomplement_eq_neg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] {v : E} (hv : v ∈ K) : Kᗮ.reflection v = -v

The reflection in Kᗮ of an element of K is its negation.

theorem Submodule.reflection_orthogonalComplement_singleton_eq_neg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (v : E) : (span 𝕜 {v})ᗮ.reflection v = -v

The reflection in (𝕜 ∙ v)ᗮ of v is -v.

theorem Submodule.reflection_sub {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {v w : F} (h : ‖v‖ = ‖w‖) : (span ℝ {v - w})ᗮ.reflection v = w