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.

source

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.

Equations

K.reflectionLinearEquiv = LinearEquiv.ofInvolutive (2 • ↑K.starProjection - LinearMap.id) ⋯

Instances For

source

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.

Equations

K.reflection = { toLinearEquiv := K.reflectionLinearEquiv, norm_map' := ⋯ }

Instances For

source

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.

source

@[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.

source

@[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.

source

@[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.

source

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.

source

@[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.

source

@[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.

source

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

source

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 𝕜)

source

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

source

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.

source

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

source

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.

source

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.

source

@[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.

source

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.

source

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.

source

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.

source

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

(span ℝ {v - w})ᗮ.reflection v = w

Documentation

Mathlib.Analysis.InnerProductSpace.Projection.Reflection

Reflection #