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.

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)

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.