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‖.

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 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.