The second scalar derivative has compact support
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_secondDeriv_hasCompactSupport · theorem · Teaching coverage
Statement
The closed topological support of q″=deriv(deriv q) is compact in ℝ.
All objects and hypotheses
- No additional parameter or hypothesis.
Mathematical proof
1. Transfer compact support through both derivatives
Each scalar differentiation preserves compact support because the derivative is zero where the original function is locally zero. Apply this existing rule first to q, then to q′.
Corresponding Lean step
smoothUnitCutoff_hasCompactSupport.deriv.deriv
Lean statement · smoothUnitCutoff_secondDeriv_hasCompactSupport
This is a support-closure reuse theorem; it is separate from continuity of q″.
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 smoothUnitCutoff_secondDeriv_hasCompactSupport :
HasCompactSupport (deriv (deriv smoothUnitCutoff))Lean proof · smoothUnitCutoff_secondDeriv_hasCompactSupport
Actual proof outline: Transfer compact support through both derivatives: The two .deriv calls apply the same Mathlib support theorem at successive derivative orders.
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 smoothUnitCutoff_secondDeriv_hasCompactSupport :
HasCompactSupport (deriv (deriv smoothUnitCutoff)) :=
smoothUnitCutoff_hasCompactSupport.deriv.deriv
/-- One positive constant bounds the second derivative of the fixed unit
cutoff. The constant is chosen before any radial scale, which is the compact
support input needed for a later `C / R^2` radial Hessian bound. -/Scope and omitted-condition boundaries
- No radius or radial second-derivative bound is proved by this declaration.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- HasCompactSupport.deriv
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.
- HasCompactSupport.deriv — Exact checked local Mathlib dependency definition or theorem.
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_hasCompactSupport — 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.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.