UnitSphere: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

The ambient exponential map of the unit sphere
A signed great-circle parameterization
Signed sphere geodesics are smooth
The exponential formula is continuous in its increment
Forward exponential steps equal the signed geodesic
A fourth-order certificate for sphere geodesics
Tangent exponential steps remain on the unit sphere

Samplinglib mathematical lesson

The ambient exponential map of the unit sphere

AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere.unitSphereExp · def · Teaching coverage

Read this first

Mathematical statement

The sphere exponential formula combines the base direction with a sinc-scaled increment.

\[\operatorname{Exp}_w(z)=\cos(\|z\|)w+\operatorname{sinc}(\|z\|)z\]

Lean statement · unitSphereExp

Lean defines a total ambient-space map.

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.

Download module (.lean)

noncomputable def unitSphereExp (w z : E) : E

Exact module and namespace context

Proof roadmap

1Rotate in the span of w and z
Cosine weights the base direction and sine-over-radius weights the increment.

Full assumptions and notation

All objects and hypotheses

E is a real inner-product space.
w and z are ambient vectors.
sinc supplies the continuous value at z=0.

Construction and meaning

1. Rotate in the span of w and z

Cosine weights the base direction and sine-over-radius weights the increment.

\[\cos r\,w+\frac{\sin r}{r}z,\quad r=\|z\|\]

Corresponding Lean step

Real.sinc makes this a total formula.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean construction · unitSphereExp

The later norm theorem states the exact tangency conditions for sphere membership.

Download module (.lean)

noncomputable def unitSphereExp (w z : E) : E :=
  Real.cos ‖z‖ • w + Real.sinc ‖z‖ • z

Exact module and namespace context

Scope and omitted-condition boundaries

Without unit length and tangency, unit norm is not asserted.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Samplinglib compiled source — Exact statement and proof.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Samplinglib mathematical lesson

A signed great-circle parameterization

AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere.unitSphereGeodesic · def · Teaching coverage

Read this first

Mathematical statement

The curve uses cos(t‖z‖) and sin(t‖z‖)/‖z‖, with a constant zero-velocity branch.

\[\gamma_{w,z}(t)=\begin{cases}w,&z=0,\\\cos(t\|z\|)w+\frac{\sin(t\|z\|)}{\|z\|}z,&z\ne0.\end{cases}\]

Lean statement · unitSphereGeodesic

The signed parameterization avoids the absolute value introduced by ‖t • z‖.

Download module (.lean)

noncomputable def unitSphereGeodesic (w z : E) (t : ℝ) : E

Exact module and namespace context

Proof roadmap

1Choose the removable branch
Zero velocity gives the constant curve; nonzero velocity gives the signed trigonometric formula.

Full assumptions and notation

All objects and hypotheses

E is a real inner-product space.
t may be negative, zero, or positive.
The zero-velocity branch is explicit.

Construction and meaning

1. Choose the removable branch

Zero velocity gives the constant curve; nonzero velocity gives the signed trigonometric formula.

\[z=0\Rightarrow\gamma(t)=w\]

Corresponding Lean step

Lean uses an if ‖z‖ = 0 branch.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean construction · unitSphereGeodesic

Subsequent theorems prove its smoothness and relation to the exponential formula.

Download module (.lean)

noncomputable def unitSphereGeodesic (w z : E) (t : ℝ) : E :=
  if ‖z‖ = 0 then w
  else Real.cos (t * ‖z‖) • w +
    (Real.sin (t * ‖z‖) / ‖z‖) • z

Exact module and namespace context

Scope and omitted-condition boundaries

w need not be unit and z need not be tangent for the definition.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Samplinglib compiled source — Exact statement and proof.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Samplinglib mathematical lesson

Signed sphere geodesics are smooth

AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere.unitSphereGeodesic_contDiff · theorem · Teaching coverage

Read this first

Mathematical statement

For fixed base point and velocity, the signed great-circle curve is continuously differentiable to every requested finite order.

\[\gamma_{w,z}\in C^n(\mathbb R;E)\]

Lean statement · unitSphereGeodesic_contDiff

The theorem returns `ContDiff ℝ n`.

Download module (.lean)

theorem unitSphereGeodesic_contDiff (w z : E) (n : WithTop ℕ∞) :
    ContDiff ℝ n (unitSphereGeodesic w z)

Exact module and namespace context

Proof roadmap

1Split on zero velocity
The zero branch is constant; in the nonzero branch all scalar trigonometric operations are smooth.

Full assumptions and notation

All objects and hypotheses

E is a real inner-product space.
No unit-length or tangency assumption is needed.
n is any Mathlib differentiability order.

Mathematical proof

1. Split on zero velocity

The zero branch is constant; in the nonzero branch all scalar trigonometric operations are smooth.

\[z=0\Rightarrow\gamma(t)=w;\quad z\ne0\Rightarrow\gamma(t)=\cos(tr)w+\frac{\sin(tr)}r z\]

Corresponding Lean step

fun_prop proves both branches after the case split.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · unitSphereGeodesic_contDiff

The only case split handles the removable zero-velocity denominator.

Download module (.lean)

theorem unitSphereGeodesic_contDiff (w z : E) (n : WithTop ℕ∞) :
    ContDiff ℝ n (unitSphereGeodesic w z) := by
  by_cases hz : ‖z‖ = 0
  · have hgeo : unitSphereGeodesic w z = fun _ : ℝ => w := by
      funext t
      simp [unitSphereGeodesic, hz]
    rw [hgeo]
    fun_prop
  · unfold unitSphereGeodesic
    simp only [hz, ↓reduceIte]
    fun_prop

Exact module and namespace context

Scope and omitted-condition boundaries

Smoothness alone does not imply the curve lies on a sphere.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Samplinglib compiled source — Exact statement and proof.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Samplinglib mathematical lesson

The exponential formula is continuous in its increment

AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere.unitSphereExp_continuous · theorem · Teaching coverage

Read this first

Mathematical statement

For a fixed base point, the ambient sphere exponential formula depends continuously on z.

\[z_n\to z\Longrightarrow\operatorname{Exp}_w(z_n)\to\operatorname{Exp}_w(z)\]

Lean statement · unitSphereExp_continuous

The conclusion is ordinary topological continuity.

Download module (.lean)

theorem unitSphereExp_continuous (w : E) : Continuous (unitSphereExp w)

Exact module and namespace context

Proof roadmap

1Compose continuous operations
The norm, cosine, sinc, scalar multiplication, and addition are continuous.

Full assumptions and notation

All objects and hypotheses

E is a real inner-product space.
w is fixed.
No tangency premise is needed.

Mathematical proof

1. Compose continuous operations

The norm, cosine, sinc, scalar multiplication, and addition are continuous.

\[z\mapsto\cos(\|z\|)w+\operatorname{sinc}(\|z\|)z\]

Corresponding Lean step

After unfolding, fun_prop applies Mathlib's continuity rules.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · unitSphereExp_continuous

The proof is a direct closure argument.

Download module (.lean)

theorem unitSphereExp_continuous (w : E) : Continuous (unitSphereExp w) := by
  unfold unitSphereExp
  fun_prop

Exact module and namespace context

Scope and omitted-condition boundaries

Joint differentiability in both arguments is not claimed.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Samplinglib compiled source — Exact statement and proof.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Samplinglib mathematical lesson

Forward exponential steps equal the signed geodesic

AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere.unitSphereExp_smul_eq_unitSphereGeodesic · theorem · Teaching coverage

Read this first

Mathematical statement

For nonnegative time, exponentiating the scaled increment tz equals the signed geodesic at t.

\[t\ge0\Longrightarrow\operatorname{Exp}_w(tz)=\gamma_{w,z}(t)\]

Lean statement · unitSphereExp_smul_eq_unitSphereGeodesic

The nonnegative-time hypothesis is visible.

Download module (.lean)

theorem unitSphereExp_smul_eq_unitSphereGeodesic
    (w z : E) {t : ℝ} (ht : 0 ≤ t) :
    unitSphereExp w (t • z) = unitSphereGeodesic w z t

Exact module and namespace context

Proof roadmap

1Handle degenerate cases
When t=0 or z=0, both sides reduce to w.
2Rewrite the scaled norm
Nonnegative t gives ‖tz‖=t‖z‖.
3Expand sinc and cancel t
For nonzero t‖z‖, sinc becomes sine divided by its argument.

Full assumptions and notation

All objects and hypotheses

t is nonnegative.
Zero time and zero velocity are allowed.
w and z are arbitrary ambient vectors.

Mathematical proof

1. Handle degenerate cases

When t=0 or z=0, both sides reduce to w.

\[t=0\text{ or }z=0\Rightarrow\operatorname{Exp}_w(tz)=w\]

Corresponding Lean step

Lean discharges both branches by simplification.

2. Rewrite the scaled norm

Nonnegative t gives ‖tz‖=t‖z‖.

\[\|tz\|=t\|z\|\]

Corresponding Lean step

norm_smul and abs_of_nonneg prove the equality.

3. Expand sinc and cancel t

For nonzero t‖z‖, sinc becomes sine divided by its argument.

\[\operatorname{sinc}(t\|z\|)(tz)=\frac{\sin(t\|z\|)}{\|z\|}z\]

Corresponding Lean step

Real.sinc_of_ne_zero and field simplification finish.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · unitSphereExp_smul_eq_unitSphereGeodesic

All denominator and zero cases are handled explicitly.

Download module (.lean)

theorem unitSphereExp_smul_eq_unitSphereGeodesic
    (w z : E) {t : ℝ} (ht : 0 ≤ t) :
    unitSphereExp w (t • z) = unitSphereGeodesic w z t := by
  by_cases hz : z = 0
  · subst z
    simp [unitSphereExp, unitSphereGeodesic]
  by_cases ht0 : t = 0
  · subst t
    simp [unitSphereExp, unitSphereGeodesic]
  have hr : ‖z‖ ≠ 0 := norm_ne_zero_iff.mpr hz
  have htne : t ≠ 0 := ht0
  have hnorm : ‖t • z‖ = t * ‖z‖ := by
    rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht]
  rw [unitSphereExp, unitSphereGeodesic, if_neg hr, hnorm,
    Real.sinc_of_ne_zero (mul_ne_zero htne hr)]
  congr 1
  rw [smul_smul]
  congr 1
  field_simp [htne, hr]

Exact module and namespace context

Scope and omitted-condition boundaries

The same equality is not claimed for negative t because the exponential formula uses ‖tz‖.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Samplinglib compiled source — Exact statement and proof.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Samplinglib mathematical lesson

A fourth-order certificate for sphere geodesics

AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere.unitSphereGeodesic_derivatives_and_bounds · theorem · Teaching coverage

Read this first

Mathematical statement

At a unit base point and nonzero velocity, the first four derivatives have explicit formulas and satisfy ‖γ^(q)(t)‖≤2‖z‖^q for q=1,2,3,4.

\[\|\gamma_{w,z}^{(q)}(t)\|\le2\|z\|^q\quad(q=1,2,3,4)\]

Lean statement · unitSphereGeodesic_derivatives_and_bounds

Consumers receive exact `HasDerivAt` witnesses as well as estimates.

Download module (.lean)

theorem unitSphereGeodesic_derivatives_and_bounds
    {w z : E} (hw : ‖w‖ = 1) (hz : z ≠ 0) (t : ℝ) :
    (HasDerivAt (unitSphereGeodesic w z)
        ((-(‖z‖ * Real.sin (t * ‖z‖))) • w +
          Real.cos (t * ‖z‖) • z) t ∧
      HasDerivAt
        (fun s : ℝ =>
          (-(‖z‖ * Real.sin (s * ‖z‖))) • w +
            Real.cos (s * ‖z‖) • z)
        ((-(‖z‖ ^ (2 : ℕ) * Real.cos (t * ‖z‖))) • w +
          (-(‖z‖ * Real.sin (t * ‖z‖))) • z) t ∧
      HasDerivAt
        (fun s : ℝ =>
          (-(‖z‖ ^ (2 : ℕ) * Real.cos (s * ‖z‖))) • w +
            (-(‖z‖ * Real.sin (s * ‖z‖))) • z)
        ((‖z‖ ^ (3 : ℕ) * Real.sin (t * ‖z‖)) • w +
          (-(‖z‖ ^ (2 : ℕ) * Real.cos (t * ‖z‖))) • z) t ∧
      HasDerivAt
        (fun s : ℝ =>
          (‖z‖ ^ (3 : ℕ) * Real.sin (s * ‖z‖)) • w +
            (-(‖z‖ ^ (2 : ℕ) * Real.cos (s * ‖z‖))) • z)
        ((‖z‖ ^ (4 : ℕ) * Real.cos (t * ‖z‖)) • w +
          (‖z‖ ^ (3 : ℕ) * Real.sin (t * ‖z‖)) • z) t) ∧
    (‖(-(‖z‖ * Real.sin (t * ‖z‖))) • w +
          Real.cos (t * ‖z‖) • z‖ ≤ 2 * ‖z‖ ∧
      ‖(-(‖z‖ ^ (2 : ℕ) * Real.cos (t * ‖z‖))) • w +
          (-(‖z‖ * Real.sin (t * ‖z‖))) • z‖ ≤
        2 * ‖z‖ ^ (2 : ℕ) ∧
      ‖(‖z‖ ^ (3 : ℕ) * Real.sin (t * ‖z‖)) • w +
          (-(‖z‖ ^ (2 : ℕ) * Real.cos (t * ‖z‖))) • z‖ ≤
        2 * ‖z‖ ^ (3 : ℕ) ∧
      ‖(‖z‖ ^ (4 : ℕ) * Real.cos (t * ‖z‖)) • w +
          (‖z‖ ^ (3 : ℕ) * Real.sin (t * ‖z‖)) • z‖ ≤
        2 * ‖z‖ ^ (4 : ℕ))

Exact module and namespace context

Proof roadmap

1Differentiate four times
Sine and cosine alternate and each differentiation contributes one power of ‖z‖.
2Bound the two components
Use the triangle inequality, ‖w‖=1, and |sin|,|cos|≤1.
3Return one reusable certificate
The public theorem packages four exact derivative witnesses and four bounds.

Full assumptions and notation

All objects and hypotheses

E is any real inner-product space.
‖w‖=1.
z≠0 selects the displayed closed form.
No finite-dimensional or probabilistic hypothesis is used.

Mathematical proof

1. Differentiate four times

Sine and cosine alternate and each differentiation contributes one power of ‖z‖.

\[\gamma'(t)=-r\sin(tr)w+\cos(tr)z,\quad\gamma''(t)=-r^2\cos(tr)w-r\sin(tr)z,\ldots\]

Corresponding Lean step

Private HasDerivAt lemmas prove every displayed derivative.

2. Bound the two components

Use the triangle inequality, ‖w‖=1, and |sin|,|cos|≤1.

\[\|a(t)w+b(t)z\|\le2\|z\|^q\]

Corresponding Lean step

Private norm lemmas prove all four uniform envelopes.

3. Return one reusable certificate

The public theorem packages four exact derivative witnesses and four bounds.

\[(\gamma',\gamma'',\gamma^{(3)},\gamma^{(4)})\text{ and }(2r,2r^2,2r^3,2r^4)\]

Corresponding Lean step

Conjunction introduction assembles the reviewed helpers.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · unitSphereGeodesic_derivatives_and_bounds

All analytic helpers live in the same module and compile with the public theorem.

Download module (.lean)

theorem unitSphereGeodesic_derivatives_and_bounds
    {w z : E} (hw : ‖w‖ = 1) (hz : z ≠ 0) (t : ℝ) :
    (HasDerivAt (unitSphereGeodesic w z)
        ((-(‖z‖ * Real.sin (t * ‖z‖))) • w +
          Real.cos (t * ‖z‖) • z) t ∧
      HasDerivAt
        (fun s : ℝ =>
          (-(‖z‖ * Real.sin (s * ‖z‖))) • w +
            Real.cos (s * ‖z‖) • z)
        ((-(‖z‖ ^ (2 : ℕ) * Real.cos (t * ‖z‖))) • w +
          (-(‖z‖ * Real.sin (t * ‖z‖))) • z) t ∧
      HasDerivAt
        (fun s : ℝ =>
          (-(‖z‖ ^ (2 : ℕ) * Real.cos (s * ‖z‖))) • w +
            (-(‖z‖ * Real.sin (s * ‖z‖))) • z)
        ((‖z‖ ^ (3 : ℕ) * Real.sin (t * ‖z‖)) • w +
          (-(‖z‖ ^ (2 : ℕ) * Real.cos (t * ‖z‖))) • z) t ∧
      HasDerivAt
        (fun s : ℝ =>
          (‖z‖ ^ (3 : ℕ) * Real.sin (s * ‖z‖)) • w +
            (-(‖z‖ ^ (2 : ℕ) * Real.cos (s * ‖z‖))) • z)
        ((‖z‖ ^ (4 : ℕ) * Real.cos (t * ‖z‖)) • w +
          (‖z‖ ^ (3 : ℕ) * Real.sin (t * ‖z‖)) • z) t) ∧
    (‖(-(‖z‖ * Real.sin (t * ‖z‖))) • w +
          Real.cos (t * ‖z‖) • z‖ ≤ 2 * ‖z‖ ∧
      ‖(-(‖z‖ ^ (2 : ℕ) * Real.cos (t * ‖z‖))) • w +
          (-(‖z‖ * Real.sin (t * ‖z‖))) • z‖ ≤
        2 * ‖z‖ ^ (2 : ℕ) ∧
      ‖(‖z‖ ^ (3 : ℕ) * Real.sin (t * ‖z‖)) • w +
          (-(‖z‖ ^ (2 : ℕ) * Real.cos (t * ‖z‖))) • z‖ ≤
        2 * ‖z‖ ^ (3 : ℕ) ∧
      ‖(‖z‖ ^ (4 : ℕ) * Real.cos (t * ‖z‖)) • w +
          (‖z‖ ^ (3 : ℕ) * Real.sin (t * ‖z‖)) • z‖ ≤
        2 * ‖z‖ ^ (4 : ℕ)) := by
  constructor
  · exact ⟨unitSphereGeodesic_hasDerivAt w hz t,
      unitSphereGeodesic_velocity_hasDerivAt w z t,
      unitSphereGeodesic_acceleration_hasDerivAt w z t,
      unitSphereGeodesic_jerk_hasDerivAt w z t⟩
  · exact ⟨unitSphereGeodesic_first_derivative_norm_le hw t,
      unitSphereGeodesic_second_derivative_norm_le hw t,
      unitSphereGeodesic_third_derivative_norm_le hw t,
      unitSphereGeodesic_fourth_derivative_norm_le hw t⟩

Exact module and namespace context

Scope and omitted-condition boundaries

The constant 2 is a simple uniform envelope, not an optimality claim.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Samplinglib compiled source — Exact statement and proof.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Samplinglib mathematical lesson

Tangent exponential steps remain on the unit sphere

AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere.unitSphereExp_norm_eq_one · theorem · Teaching coverage

Read this first

Mathematical statement

A unit base point and an orthogonal increment produce an exponential-map value with exactly unit norm.

\[\|w\|=1,\ \langle w,z\rangle=0\Longrightarrow\|\operatorname{Exp}_w(z)\|=1\]

Lean statement · unitSphereExp_norm_eq_one

The theorem gives exact feasibility, not an asymptotic estimate.

Download module (.lean)

theorem unitSphereExp_norm_eq_one
    {w z : E}
    (hw : ‖w‖ = 1)
    (htan : ⟪w, z⟫_ℝ = 0) :
    ‖unitSphereExp w z‖ = 1

Exact module and namespace context

Proof roadmap

1Handle zero increment
At z=0, the exponential formula is w.
2Use orthogonality
The cosine and sinc components have zero cross inner product.
3Apply Pythagoras and trigonometry
The two squared norms are cos²r and sin²r.
4Use nonnegativity of norm
A nonnegative real with square one equals one.

Full assumptions and notation

All objects and hypotheses

E is a real inner-product space.
‖w‖=1.
⟪w,z⟫=0.
z=0 is allowed.

Mathematical proof

1. Handle zero increment

At z=0, the exponential formula is w.

\[z=0\Rightarrow\operatorname{Exp}_w(z)=w\]

Corresponding Lean step

Simplification uses the unit-norm premise.

2. Use orthogonality

The cosine and sinc components have zero cross inner product.

\[\langle\cos(r)w,\operatorname{sinc}(r)z\rangle=0\]

Corresponding Lean step

Inner-product scalar rules reduce this to ⟪w,z⟫=0.

3. Apply Pythagoras and trigonometry

The two squared norms are cos²r and sin²r.

\[\|\operatorname{Exp}_w(z)\|^2=\cos^2r+\sin^2r=1\]

Corresponding Lean step

norm_add_sq_real, Real.sinc_of_ne_zero, and Real.sin_sq_add_cos_sq prove the identity.

4. Use nonnegativity of norm

A nonnegative real with square one equals one.

\[x\ge0,\ x^2=1\Rightarrow x=1\]

Corresponding Lean step

Nonlinear arithmetic closes the final scalar step.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · unitSphereExp_norm_eq_one

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

Download module (.lean)

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

Scope and omitted-condition boundaries

No algorithmic convergence theorem is included.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Samplinglib compiled source — Exact statement and proof.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.