Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
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

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

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 :=
  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 prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.