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.

Download module (.lean)

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.

Download module (.lean)

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