Samplinglib mathematical lesson

The second scalar derivative of the unit cutoff is continuous

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_secondDeriv_continuous · theorem · Teaching coverage

Read this first

Mathematical statement

The function t↦q″(t), defined as deriv(deriv q), is continuous on ℝ.

\[q''=(q')'\in C^0(\mathbb R;\mathbb R).\]

Lean statement · smoothUnitCutoff_secondDeriv_continuous

This is the already-existing scalar second-derivative result, not a new radial Hessian statement.

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 smoothUnitCutoff_secondDeriv_continuous :
    Continuous (deriv (deriv smoothUnitCutoff))

Exact module and namespace context

Proof roadmap

1Retain two derivatives from infinite smoothness
C∞ regularity implies C² regularity.
2Differentiate twice and read continuity
The iterated-derivative rule sends a C² scalar function to a C⁰ function after two derivatives. The second iterate of deriv is exactly deriv(deriv q), and C⁰ implies continuity.

Full assumptions and notation

All objects and hypotheses

No extra hypothesis; q is the existing smooth scalar cutoff.

Mathematical proof

1. Retain two derivatives from infinite smoothness

C∞ regularity implies C² regularity.

\[q\in C^\infty\Longrightarrow q\in C^2.\]

Corresponding Lean step

have htwo : ContDiff ℝ 2 smoothUnitCutoff := smoothUnitCutoff_contDiff.of_le (WithTop.coe_le_coe.mpr (le_top : (2 : ℕ∞) ≤ ⊤))

2. Differentiate twice and read continuity

The iterated-derivative rule sends a C² scalar function to a C⁰ function after two derivatives. The second iterate of deriv is exactly deriv(deriv q), and C⁰ implies continuity.

\[\operatorname{deriv}^{[2]}q=q'',\qquad q''\in C^0.\]

Corresponding Lean step

have hzero := htwo.iterate_deriv' 0 2
simp only [Function.iterate_succ, Function.iterate_zero, Function.comp_apply] at hzero
exact hzero.continuous

Lean verification

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

Lean proof · smoothUnitCutoff_secondDeriv_continuous

Actual proof outline: Retain two derivatives from infinite smoothness: of_le weakens the regularity order, not the statement's domain. Differentiate twice and read continuity: deriv^[2] iterates the derivative-taking operation twice; the simplification expands that iteration.

Download module (.lean)

theorem smoothUnitCutoff_secondDeriv_continuous :
    Continuous (deriv (deriv smoothUnitCutoff)) := by
  have htwo : ContDiff ℝ 2 smoothUnitCutoff :=
    smoothUnitCutoff_contDiff.of_le
      (WithTop.coe_le_coe.mpr (le_top : (2 : ℕ∞) ≤ ⊤))
  have hzero : ContDiff ℝ 0 (deriv^[2] smoothUnitCutoff) :=
    htwo.iterate_deriv' 0 2
  simp only [Function.iterate_succ, Function.iterate_zero, Function.comp_apply] at hzero
  exact hzero.continuous

Exact module and namespace context

Scope and omitted-condition boundaries

It asserts continuity only; boundedness and support are distinct following declarations.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_contDiff

Mathlib API called (external library)

ContDiff.of_le
ContDiff.iterate_deriv'
ContDiff.continuous

Mathematical sources

Current ASTIS declaration and complete body — Authority for the statement, local assumptions, and actual proof/construction documented here.
Existing module card — Existing module overview only; no exact per-declaration curated source-memory entry was found in this card.
ContDiff.iterate_deriv' — Exact checked local Mathlib dependency definition or theorem.
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_contDiff — Exact earlier ASTIS definition or theorem used in this declaration; not an independent external-source claim.
Existing test source — Existing direct example invocation inspected; no build or test run was performed.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.