SphereSecondOrder: mathematical reading route
Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.
- Second derivative at a local minimum
- Second derivative at a local maximum
- Nonnegative Laplacian at a unit-sphere minimum
- Nonpositive Laplacian at a unit-sphere maximum
Samplinglib mathematical lesson
Second derivative at a local minimum
AutoSamplingTheory.TechnicalLemmas.Geometry.SphereSecondOrder.IsLocalMin.deriv_deriv_nonneg_of_continuousAt · theorem · Teaching coverage
Read this first
Mathematical statement
For a real function continuous at a local minimum, the second derivative represented by deriv (deriv f) is nonnegative.
\[x\text{ local min of }f,\ f\text{ continuous at }x\Longrightarrow (\operatorname{deriv}\operatorname{deriv}f)(x)\ge0\]
Lean statement · deriv_deriv_nonneg_of_continuousAt
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.
theorem IsLocalMin.deriv_deriv_nonneg_of_continuousAt
{f : ℝ → ℝ} {x : ℝ} (hmin : IsLocalMin f x)
(hc : ContinuousAt f x) :
0 ≤ deriv (deriv f) x
Exact module and namespace context
Proof roadmap
- 1Rule out a negative second derivative
If the second derivative were negative, Mathlib’s strict second-derivative test would also make x a local maximum.
- 2Combine the two local inequalities
A point that is both a local minimum and a local maximum has a neighborhood on which f is constant.
- 3Differentiate the local equality twice
The derivative is locally zero, hence its derivative at x is zero, contradicting strict negativity.
Full assumptions and notation
All objects and hypotheses
- f is a real-valued function on the real line.
- x is a local minimum of f.
- f is continuous at x; Mathlib deriv is total and equals zero at nondifferentiable points.
Mathematical proof
1. Rule out a negative second derivative
If the second derivative were negative, Mathlib’s strict second-derivative test would also make x a local maximum.
\[f^{\prime\prime}(x)<0\Longrightarrow x\text{ is a local maximum}\]
Corresponding Lean step
Use isLocalMax_of_deriv_deriv_neg, with Fermat’s identity at the local minimum.
2. Combine the two local inequalities
A point that is both a local minimum and a local maximum has a neighborhood on which f is constant.
\[f(x)\le f(y)\le f(x)\Longrightarrow f(y)=f(x)\]
Corresponding Lean step
Intersect the two neighborhood filters and apply antisymmetry.
3. Differentiate the local equality twice
The derivative is locally zero, hence its derivative at x is zero, contradicting strict negativity.
\[f\equiv f(x)\text{ locally}\Longrightarrow f^\prime\equiv0\text{ locally}\Longrightarrow f^{\prime\prime}(x)=0\]
Corresponding Lean step
Filter.EventuallyEq.deriv and deriv_eq transport the local equality.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · deriv_deriv_nonneg_of_continuousAt
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.
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.
theorem IsLocalMin.deriv_deriv_nonneg_of_continuousAt
{f : ℝ → ℝ} {x : ℝ} (hmin : IsLocalMin f x)
(hc : ContinuousAt f x) :
0 ≤ deriv (deriv f) x := by
by_contra hnonneg
have hneg : deriv (deriv f) x < 0 := lt_of_not_ge hnonneg
have hmax : IsLocalMax f x :=
isLocalMax_of_deriv_deriv_neg hneg hmin.deriv_eq_zero hc
have hconst : f =ᶠ[𝓝 x] fun _ : ℝ => f x := by
filter_upwards [hmin, hmax] with y hymin hymax
exact le_antisymm hymax hymin
have hderiv : deriv f =ᶠ[𝓝 x] fun _ : ℝ => 0 := by
simpa using hconst.deriv
have hzero : deriv (deriv f) x = 0 := by
calc
deriv (deriv f) x = deriv (fun _ : ℝ => 0) x := hderiv.deriv_eq
_ = 0 := by simp
linarith
Exact module and namespace context
Scope and omitted-condition boundaries
- This uses Mathlib’s total deriv; it does not assert existence of a classical second derivative beyond that representation.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- isLocalMax_of_deriv_deriv_neg
- isLocalMin_of_deriv_deriv_pos
- Filter.EventuallyEq.deriv
Mathematical sources
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.
Samplinglib mathematical lesson
Second derivative at a local maximum
AutoSamplingTheory.TechnicalLemmas.Geometry.SphereSecondOrder.IsLocalMax.deriv_deriv_nonpos_of_continuousAt · theorem · Teaching coverage
Read this first
Mathematical statement
For a real function continuous at a local maximum, the second derivative represented by deriv (deriv f) is nonpositive.
\[x\text{ local max of }f,\ f\text{ continuous at }x\Longrightarrow (\operatorname{deriv}\operatorname{deriv}f)(x)\le0\]
Lean statement · deriv_deriv_nonpos_of_continuousAt
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.
theorem IsLocalMax.deriv_deriv_nonpos_of_continuousAt
{f : ℝ → ℝ} {x : ℝ} (hmax : IsLocalMax f x)
(hc : ContinuousAt f x) :
deriv (deriv f) x ≤ 0
Exact module and namespace context
Proof roadmap
- 1Rule out a positive second derivative
A positive second derivative and Fermat’s identity would make x a local minimum.
- 2Force local constancy
The local minimum and maximum inequalities agree, so f equals f(x) near x.
- 3Contradict strict positivity
Differentiating the local constant germ twice gives second derivative zero.
Full assumptions and notation
All objects and hypotheses
- f is a real-valued function on the real line.
- x is a local maximum of f.
- f is continuous at x; Mathlib deriv is total and equals zero at nondifferentiable points.
Mathematical proof
1. Rule out a positive second derivative
A positive second derivative and Fermat’s identity would make x a local minimum.
\[f^{\prime\prime}(x)>0\Longrightarrow x\text{ is a local minimum}\]
Corresponding Lean step
Use isLocalMin_of_deriv_deriv_pos.
2. Force local constancy
The local minimum and maximum inequalities agree, so f equals f(x) near x.
\[f(y)=f(x)\text{ near }x\]
Corresponding Lean step
Intersect the two filters and apply order antisymmetry.
3. Contradict strict positivity
Differentiating the local constant germ twice gives second derivative zero.
\[f^{\prime\prime}(x)=0\]
Corresponding Lean step
Use the congruence theorem for deriv twice.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · deriv_deriv_nonpos_of_continuousAt
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.
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.
theorem IsLocalMax.deriv_deriv_nonpos_of_continuousAt
{f : ℝ → ℝ} {x : ℝ} (hmax : IsLocalMax f x)
(hc : ContinuousAt f x) :
deriv (deriv f) x ≤ 0 := by
by_contra hnonpos
have hpos : 0 < deriv (deriv f) x := lt_of_not_ge hnonpos
have hmin : IsLocalMin f x :=
isLocalMin_of_deriv_deriv_pos hpos hmax.deriv_eq_zero hc
have hconst : f =ᶠ[𝓝 x] fun _ : ℝ => f x := by
filter_upwards [hmin, hmax] with y hymin hymax
exact le_antisymm hymax hymin
have hderiv : deriv f =ᶠ[𝓝 x] fun _ : ℝ => 0 := by
simpa using hconst.deriv
have hzero : deriv (deriv f) x = 0 := by
calc
deriv (deriv f) x = deriv (fun _ : ℝ => 0) x := hderiv.deriv_eq
_ = 0 := by simp
linarith
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
open AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere
Exact module and namespace context
Scope and omitted-condition boundaries
- This is a necessary non-strict sign condition, not a sufficient test for an extremum.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- isLocalMax_of_deriv_deriv_neg
- isLocalMin_of_deriv_deriv_pos
- Filter.EventuallyEq.deriv
Mathematical sources
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.
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.
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.
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.
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
Mathlib API called (external library)
- isLocalMax_of_deriv_deriv_neg
- isLocalMin_of_deriv_deriv_pos
- Filter.EventuallyEq.deriv
Mathematical sources
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.
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.
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.
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.
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
Mathlib API called (external library)
- isLocalMax_of_deriv_deriv_neg
- isLocalMin_of_deriv_deriv_pos
- Filter.EventuallyEq.deriv
Mathematical sources
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.