English
The equation for stereoInvFunAux stated in functional form holds: stereoInvFunAux v w equals the explicit combination as in the previous lemma.
Русский
Уравнение для stereoInvFunAux в функциональной форме выполняется: stereoInvFunAux v w равно указанной ранее комбинаторике.
LaTeX
$$stereoInvFunAux\ v\ w = (\|w\|^2 + 4)^{-1} \cdot (4 w + (\|w\|^2 - 4) v)$$
Lean4
theorem stereoInvFunAux_mem (hv : ‖v‖ = 1) {w : E} (hw : w ∈ (ℝ ∙ v)ᗮ) : stereoInvFunAux v w ∈ sphere (0 : E) 1 :=
by
have h₁ : (0 : ℝ) < ‖w‖ ^ 2 + 4 := by positivity
suffices ‖(4 : ℝ) • w + (‖w‖ ^ 2 - 4) • v‖ = ‖w‖ ^ 2 + 4 by
simp only [mem_sphere_zero_iff_norm, norm_smul, Real.norm_eq_abs, abs_inv, this, abs_of_pos h₁,
stereoInvFunAux_apply, inv_mul_cancel₀ h₁.ne']
suffices ‖(4 : ℝ) • w + (‖w‖ ^ 2 - 4) • v‖ ^ 2 = (‖w‖ ^ 2 + 4) ^ 2 by
simpa only [sq_eq_sq_iff_abs_eq_abs, abs_norm, abs_of_pos h₁] using this
rw [Submodule.mem_orthogonal_singleton_iff_inner_left] at hw
simp [norm_add_sq_real, norm_smul, inner_smul_left, inner_smul_right, hw, mul_pow, Real.norm_eq_abs, hv]
ring
