Samplinglib mathematical lesson

Nonpositive Laplacian at a unit-sphere maximum

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

Read this first

Mathematical statement

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

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

Lean statement · unitSphere_isMaxOn_laplacian_nonpos

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_isMaxOn_laplacian_nonpos
    {ι : Type*} [Fintype ι] {f : E → ℝ} {w : E}
    (directions : ι → E) (diagonal : ι → ℝ) (laplacian : ℝ)
    (hw : ‖w‖ = 1)
    (htangent : ∀ i, ⟪w, directions i⟫_ℝ = 0)
    (hmax : IsMaxOn 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) :
    laplacian ≤ 0

Exact module and namespace context

Proof roadmap

1Preserve feasibility along tangent curves
Every scaled tangent direction remains orthogonal to the unit base point, so the exponential curve stays on the sphere.
2Restrict the maximum to one dimension
The sphere maximum is a local maximum at zero along each exponential curve.
3Take the finite trace
Every directional double derivative is nonpositive, and their finite sum is the supplied Laplacian.

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 maximum 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. Preserve feasibility along tangent curves

Every scaled tangent direction remains orthogonal to the unit base point, so the exponential curve stays on the sphere.

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

Corresponding Lean step

Use the public unit-sphere norm theorem.

2. Restrict the maximum to one dimension

The sphere maximum is a local maximum at zero along each exponential curve.

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

Corresponding Lean step

Specialize IsMaxOn to the feasible curve.

3. Take the finite trace

Every directional double derivative is nonpositive, and their finite sum is the supplied Laplacian.

\[h_i\le0\ \forall i\Longrightarrow\sum_i h_i=\Delta f(w)\le0\]

Corresponding Lean step

Rewrite and use Finset.sum_nonpos.

Lean verification

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

Lean proof · unitSphere_isMaxOn_laplacian_nonpos

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_isMaxOn_laplacian_nonpos
    {ι : Type*} [Fintype ι] {f : E → ℝ} {w : E}
    (directions : ι → E) (diagonal : ι → ℝ) (laplacian : ℝ)
    (hw : ‖w‖ = 1)
    (htangent : ∀ i, ⟪w, directions i⟫_ℝ = 0)
    (hmax : IsMaxOn 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) :
    laplacian ≤ 0 := by
  rw [htrace]
  exact Finset.sum_nonpos fun i _ => by
    rw [hdiagonal i]
    exact unitSphere_isMaxOn_expCurve_deriv_deriv_nonpos
      hw (htangent i) hmax (hcontinuous i)

end

end AutoSamplingTheory.TechnicalLemmas.Geometry.SphereSecondOrder

Exact module and namespace context

Scope and omitted-condition boundaries

No parabolic PDE, density evolution, or maximum-principle time argument is included.

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.