Reflection across the orthogonal complement of a line

These lemmas describe reflection across the hyperplane perpendicular to a vector in a real inner product space. They supply the reflection identities used by the half-space Green kernel.

In dimension at least two, composing the reflections in the hyperplanes orthogonal to a nonzero vector v and to a nonzero vector orthogonal to v gives a linear isometry of determinant 1 sending v to -v (TauCeti.exists_det_eq_one_apply_eq_neg).

theorem TauCeti.reflection_orthogonal_singleton_apply {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {v : F} (hv : ‖v‖ = 1) (x : F) : (ℝ ∙ v)ᗮ.reflection x = x - (2 * inner ℝ v x) • v

Reflection through the hyperplane perpendicular to a unit normal v has this explicit formula.

@[simp]

theorem TauCeti.inner_reflection_orthogonal_singleton {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {v : F} (x : F) : inner ℝ v ((ℝ ∙ v)ᗮ.reflection x) = -inner ℝ v x

Reflection negates the component in the normal direction.

theorem TauCeti.reflection_orthogonal_singleton_eq_self_of_inner_eq_zero {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {v x : F} (hx : inner ℝ v x = 0) : (ℝ ∙ v)ᗮ.reflection x = x

A point on the bounding hyperplane is fixed by reflection.

theorem TauCeti.norm_sub_reflection_orthogonal_singleton {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (v x y : F) : ‖y - (ℝ ∙ v)ᗮ.reflection x‖ = ‖(ℝ ∙ v)ᗮ.reflection y - x‖

Reflection moves across a distance to the image point.

theorem TauCeti.norm_sub_reflection_orthogonal_singleton_eq_of_inner_eq_zero {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {v : F} (x : F) {y : F} (hy : inner ℝ v y = 0) : ‖y - (ℝ ∙ v)ᗮ.reflection x‖ = ‖y - x‖

At the boundary, the pole and its image are equidistant from the variable point.

theorem TauCeti.ne_reflection_orthogonal_singleton_of_inner_ne_neg {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {v x y : F} (hinner : inner ℝ v y ≠ -inner ℝ v x) : y ≠ (ℝ ∙ v)ᗮ.reflection x

A point whose normal component differs from the negated component of x is not its reflection.

theorem TauCeti.norm_sub_reflection_orthogonal_singleton_sq {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {v : F} (hv : ‖v‖ = 1) (x y : F) : ‖y - (ℝ ∙ v)ᗮ.reflection x‖ ^ 2 = ‖y - x‖ ^ 2 + 4 * inner ℝ v x * inner ℝ v y

The squared distance to the image pole exceeds the squared distance to the pole by four times the product of the two signed distances to the boundary.

theorem TauCeti.norm_sub_lt_norm_sub_reflection_orthogonal_singleton {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {v x y : F} (hv : ‖v‖ = 1) (hx : 0 < inner ℝ v x) (hy : 0 < inner ℝ v y) : ‖y - x‖ < ‖y - (ℝ ∙ v)ᗮ.reflection x‖

Both points in the positive half-space are closer to each other than to the image pole.

theorem TauCeti.exists_det_eq_one_apply_eq_neg {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (hF : 2 ≤ Module.finrank ℝ F) {v : F} (hv : v ≠ 0) : ∃ (r : F ≃ₗᵢ[ℝ] F), ↑(LinearEquiv.det r.toLinearEquiv) = 1 ∧ r v = -v

In dimension at least two, a nonzero vector v is sent to -v by a linear isometry of determinant 1: the product of the reflections in the hyperplanes orthogonal to v and to a nonzero vector orthogonal to v.