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

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