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.

Download module (.lean)

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.

Download module (.lean)

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