English
Let hv with ‖v‖ = 1 and x on the sphere with x ≠ v. Then stereoInvFun hv (stereoToFun v x) = x; stereoInvFun is a left inverse of stereoToFun on the sphere minus north pole.
Русский
Пусть hv: ‖v‖=1 и x на единичной сфере с x ≠ v. Тогда stereoInvFun hv (stereoToFun v x) = x; stereoInvFun является левым обратным stereoToFun на сфере без северного полюса.
LaTeX
$$$\\text{stereoInvFun } hv (\\text{stereoToFun } v x) = x\\quad ({\\;x\\;}: {\\text{sphere}}\\setminus \\{v\\})$$$
Lean4
theorem stereo_left_inv (hv : ‖v‖ = 1) {x : sphere (0 : E) 1} (hx : (x : E) ≠ v) :
stereoInvFun hv (stereoToFun v x) = x := by
ext
simp only [stereoToFun_apply, stereoInvFun_apply, smul_add]
-- name two frequently-occurring quantities and write down their basic properties
set a : ℝ := innerSL _ v x
set y := (ℝ ∙ v)ᗮ.orthogonalProjection x
have split : ↑x = a • v + ↑y :=
by
rw [← ((ℝ ∙ v).starProjection_add_starProjection_orthogonal x), Submodule.starProjection_unit_singleton ℝ hv x]
rfl
have hvy : ⟪v, y⟫_ℝ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp y.2
have pythag : 1 = a ^ 2 + ‖y‖ ^ 2 :=
by
have hvy' : ⟪a • v, y⟫_ℝ = 0 := by simp only [inner_smul_left, hvy, mul_zero]
convert norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ hvy' using 2
· simp [← split]
· simp [norm_smul, hv, ← sq, sq_abs]
·
exact
sq
_
-- a fact which will be helpful for clearing denominators in the main calculation
have ha : 0 < 1 - a :=
by
have : a < 1 := (inner_lt_one_iff_real_of_norm_one hv (by simp)).mpr hx.symm
linarith
rw [split, Submodule.coe_smul_of_tower]
simp only [norm_smul, norm_div, RCLike.norm_ofNat, Real.norm_eq_abs, abs_of_nonneg ha.le]
match_scalars
· field_simp
linear_combination 4 * pythag
· field_simp
linear_combination 4 * (a - 1) * pythag
