English
The value of applying the reflection to a vector is given by a simple formula: refl(v) x = 2⟪x,v⟫/⟪v,v⟫ v − x, etc.
Русский
Значение применения отражения к вектору задаётся простой формулой: refl(v) x = 2⟪x,v⟫/⟪v,v⟫ v − x и т.д.
LaTeX
$$$K.reflection(p) = 2\\cdot( p \\cdot v )v - p$$$
Lean4
/-- 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. -/
def reflection : E ≃ₗᵢ[𝕜] E :=
{ K.reflectionLinearEquiv with
norm_map' := by
intro x
let w : K := K.orthogonalProjection x
let v := x - w
have : ⟪v, w⟫ = 0 := starProjection_inner_eq_zero x w w.2
convert norm_sub_eq_norm_add this using 2
· dsimp [reflectionLinearEquiv, v, w]
abel
· simp only [v, add_sub_cancel] }
