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.

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