Samplinglib mathematical lesson

Nonnegative Laplacian at a unit-sphere minimum

AutoSamplingTheory.TechnicalLemmas.Geometry.SphereSecondOrder.unitSphere_isMinOn_laplacian_nonneg · theorem · Teaching coverage

Read this first

Mathematical statement

At a global minimum on the unit sphere, a finite trace of tangent exponential-curve second derivatives is nonnegative.

\[\Delta f(w)=\sum_i \frac{d^2}{dt^2}f(\operatorname{Exp}_w(tz_i))\big|_{t=0}\ge0\]

Lean statement · unitSphere_isMinOn_laplacian_nonneg

The Lean theorem states the displayed necessary sign with every continuity, tangency, diagonal, and trace premise explicit.

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 unitSphere_isMinOn_laplacian_nonneg
    {ι : Type*} [Fintype ι] {f : E → ℝ} {w : E}
    (directions : ι → E) (diagonal : ι → ℝ) (laplacian : ℝ)
    (hw : ‖w‖ = 1)
    (htangent : ∀ i, ⟪w, directions i⟫_ℝ = 0)
    (hmin : IsMinOn f (Metric.sphere (0 : E) 1) w)
    (hcontinuous : ∀ i, ContinuousAt
      (fun t : ℝ => f (unitSphereExp w (t • directions i))) 0)
    (hdiagonal : ∀ i, diagonal i =
      deriv (deriv (fun t : ℝ =>
        f (unitSphereExp w (t • directions i)))) 0)
    (htrace : laplacian = ∑ i, diagonal i) :
    0 ≤ laplacian

Exact module and namespace context

Proof roadmap

1Keep every curve on the sphere
Unit norm and tangency make Exp_w(t z_i) a sphere point for every real t.
2Restrict the minimum to each curve
The global sphere minimum becomes a local minimum of every scalar curve at t=0.
3Sum the directional signs
The real second-order necessary condition makes every diagonal entry nonnegative; a finite sum preserves the sign.

Full assumptions and notation

All objects and hypotheses

E is a real inner-product space and the index type is finite.
w has unit norm and every direction z_i is tangent at w.
f has a global minimum on the unit sphere at w.
Each exponential-curve restriction is continuous at zero; diagonal entries equal its Mathlib double derivative and the Laplacian equals their finite sum.

Mathematical proof

1. Keep every curve on the sphere

Unit norm and tangency make Exp_w(t z_i) a sphere point for every real t.

\[\|\operatorname{Exp}_w(tz_i)\|=1\]

Corresponding Lean step

Apply unitSphereExp_norm_eq_one after scaling the tangent direction.

2. Restrict the minimum to each curve

The global sphere minimum becomes a local minimum of every scalar curve at t=0.

\[f(w)\le f(\operatorname{Exp}_w(tz_i))\]

Corresponding Lean step

Build an IsLocalMin from the global IsMinOn inequality.

3. Sum the directional signs

The real second-order necessary condition makes every diagonal entry nonnegative; a finite sum preserves the sign.

\[0\le h_i\ \forall i\Longrightarrow0\le\sum_i h_i=\Delta f(w)\]

Corresponding Lean step

Rewrite each diagonal identity and use Finset.sum_nonneg.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · unitSphere_isMinOn_laplacian_nonneg

The proof reduces a forbidden strict sign to simultaneous local minimum and maximum, or restricts the sphere extremum to feasible exponential curves and sums the scalar signs.

Download module (.lean)

theorem unitSphere_isMinOn_laplacian_nonneg
    {ι : Type*} [Fintype ι] {f : E → ℝ} {w : E}
    (directions : ι → E) (diagonal : ι → ℝ) (laplacian : ℝ)
    (hw : ‖w‖ = 1)
    (htangent : ∀ i, ⟪w, directions i⟫_ℝ = 0)
    (hmin : IsMinOn f (Metric.sphere (0 : E) 1) w)
    (hcontinuous : ∀ i, ContinuousAt
      (fun t : ℝ => f (unitSphereExp w (t • directions i))) 0)
    (hdiagonal : ∀ i, diagonal i =
      deriv (deriv (fun t : ℝ =>
        f (unitSphereExp w (t • directions i)))) 0)
    (htrace : laplacian = ∑ i, diagonal i) :
    0 ≤ laplacian := by
  rw [htrace]
  exact Finset.sum_nonneg fun i _ => by
    rw [hdiagonal i]
    exact unitSphere_isMinOn_expCurve_deriv_deriv_nonneg
      hw (htangent i) hmin (hcontinuous i)

Exact module and namespace context

Scope and omitted-condition boundaries

The theorem requires the supplied diagonal/trace identities; it does not construct a tangent orthonormal frame or identify a differential operator with the Laplace–Beltrami operator.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere.unitSphereExp_norm_eq_one

Mathlib API called (external library)

isLocalMax_of_deriv_deriv_neg
isLocalMin_of_deriv_deriv_pos
Filter.EventuallyEq.deriv

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.