Tangent exponential steps remain on the unit sphere

The proof is the orthogonal norm identity plus sin²+cos²=1.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem unitSphereExp_norm_eq_one
    {w z : E}
    (hw : ‖w‖ = 1)
    (htan : ⟪w, z⟫_ℝ = 0) :
    ‖unitSphereExp w z‖ = 1 := by
  by_cases hz : z = 0
  · subst z
    simp [unitSphereExp, hw]
  · have hr : ‖z‖ ≠ 0 := norm_ne_zero_iff.mpr hz
    have hcross :
        ⟪Real.cos ‖z‖ • w, Real.sinc ‖z‖ • z⟫_ℝ = 0 := by
      simp [real_inner_smul_left, real_inner_smul_right, htan]
    have hpyth :
        ‖unitSphereExp w z‖ ^ (2 : ℕ) =
          ‖Real.cos ‖z‖ • w‖ ^ (2 : ℕ) +
          ‖Real.sinc ‖z‖ • z‖ ^ (2 : ℕ) := by
      rw [unitSphereExp, norm_add_sq_real, hcross]
      ring
    have hfirst :
        ‖Real.cos ‖z‖ • w‖ ^ (2 : ℕ) =
          Real.cos ‖z‖ ^ (2 : ℕ) := by
      simp [norm_smul, hw, sq_abs]
    have hsinc :
        Real.sinc ‖z‖ = Real.sin ‖z‖ / ‖z‖ :=
      Real.sinc_of_ne_zero hr
    have hsecond :
        ‖Real.sinc ‖z‖ • z‖ ^ (2 : ℕ) =
          Real.sin ‖z‖ ^ (2 : ℕ) := by
      rw [norm_smul, Real.norm_eq_abs, hsinc]
      have hrpos : 0 < ‖z‖ := norm_pos_iff.mpr hz
      rw [abs_div, abs_of_pos hrpos]
      rw [div_mul_cancel₀ _ hr]
      exact sq_abs (Real.sin ‖z‖)
    have hsq : ‖unitSphereExp w z‖ ^ (2 : ℕ) = 1 := by
      rw [hpyth, hfirst, hsecond]
      nlinarith [Real.sin_sq_add_cos_sq ‖z‖]
    have hnonneg : 0 ≤ ‖unitSphereExp w z‖ := norm_nonneg _
    nlinarith


end

end AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere

Exact module and namespace context