The second scalar derivative has compact support
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_secondDeriv_hasCompactSupport · theorem · Teaching coverage
Mathematical statement
The closed topological support of q″=deriv(deriv q) is compact in ℝ.
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))Proof roadmap
- 1Transfer 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′.
Full assumptions and notation
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 verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
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.derivScope and omitted-condition boundaries
- No radius or radial second-derivative bound is proved by this declaration.
Sources, dependencies, and reuse
Source and reuse
Samplinglib 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.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.