ASTIS mathematical exposition

A fixed positive constant bounds the second scalar derivative

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

Statement

There exists C>0 such that |q″(t)|≤C for every real t, before any radial scale is introduced.

\[\exists C>0\ \forall t\in\mathbb R,\quad|q''(t)|\le C.\]

All objects and hypotheses

The function is the fixed scalar q; no R or ambient radial space occurs.

Mathematical proof

1. Bound the continuous compactly supported second derivative

The preceding two theorems show q″ is continuous and compactly supported. The compact-support boundedness theorem therefore gives some global bound B.

\[\exists B\ \forall t,\quad |q''(t)|\le B.\]

Corresponding Lean step

obtain ⟨C, hC⟩ := smoothUnitCutoff_secondDeriv_hasCompactSupport.exists_bound_of_continuous smoothUnitCutoff_secondDeriv_continuous

2. Choose a strictly positive witness

As for the first derivative, enlarge the bound to max(B,1).

\[C=\max(B,1)>0,\qquad |q''(t)|\le C.\]

Corresponding Lean step

exact ⟨max C 1, lt_max_of_lt_right one_pos, fun x => (hC x).trans (le_max_left C 1)⟩

Lean statement · smoothUnitCutoff_secondDeriv_bounded

This is an existing scalar bound. The later radial iterated-second-derivative proof actually bounds the unit radial function directly; it does not call this scalar bound.

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_bounded :
    ∃ C : ℝ, 0 < C ∧ ∀ x : ℝ, ‖deriv (deriv smoothUnitCutoff) x‖ ≤ C

Exact module and namespace context

Lean proof · smoothUnitCutoff_secondDeriv_bounded

Actual proof outline: Bound the continuous compactly supported second derivative: The two existing ASTIS properties discharge the compact-support and continuity premises. Choose a strictly positive witness: This positivity adjustment is explicit; it does not compute a sharp bound.

theorem smoothUnitCutoff_secondDeriv_bounded :
    ∃ C : ℝ, 0 < C ∧ ∀ x : ℝ, ‖deriv (deriv smoothUnitCutoff) x‖ ≤ C := by
  obtain ⟨C, hC⟩ :=
    smoothUnitCutoff_secondDeriv_hasCompactSupport.exists_bound_of_continuous
      smoothUnitCutoff_secondDeriv_continuous
  exact ⟨max C 1, lt_max_of_lt_right one_pos, fun x =>
    (hC x).trans (le_max_left C 1)⟩

section Radial

variable {E : Type*} [NormedAddCommGroup E]

/-- The radial cutoff at scale `R`, given by `x ↦ smoothUnitCutoff (‖x‖ / R)`. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Do not draw this as a prerequisite of the first-order radial C/R route, or invent a Hessian consumer from it.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

HasCompactSupport.exists_bound_of_continuous
lt_max_of_lt_right
le_max_left

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.exists_bound_of_continuous — Additive declaration generated from HasCompactMulSupport.exists_bound_of_continuous by to_additive.
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_secondDeriv_hasCompactSupport — Exact earlier ASTIS definition or theorem used in this declaration; not an independent external-source claim.
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_secondDeriv_continuous — 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.