English
Let hv with ‖v‖ = 1 and w ∈ (ℝ·v)⊥. Then stereoToFun v (stereoInvFun hv w) = w; stereoToFun is a right inverse of stereoInvFun.
Русский
Пусть hv: ‖v‖=1 и w ∈ (ℝ·v)⊥. Тогда stereoToFun v (stereoInvFun hv w) = w; stereoToFun является правым обратным stereoInvFun.
LaTeX
$$$\\text{stereoToFun } v (\\text{stereoInvFun } hv\, w) = w$$$
Lean4
theorem stereo_right_inv (hv : ‖v‖ = 1) (w : (ℝ ∙ v)ᗮ) : stereoToFun v (stereoInvFun hv w) = w :=
by
simp only [stereoToFun, stereoInvFun, stereoInvFunAux, smul_add, map_add, map_smul, innerSL_apply,
Submodule.orthogonalProjection_mem_subspace_eq_self]
have h₁ : (ℝ ∙ v)ᗮ.orthogonalProjection v = 0 :=
Submodule.orthogonalProjection_orthogonalComplement_singleton_eq_zero v
have h₂ : ⟪v, w⟫ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2
have h₃ : ⟪v, v⟫ = 1 := by simp [real_inner_self_eq_norm_mul_norm, hv]
rw [h₁, h₂, h₃]
match_scalars
simp [field]
ring
