ASTIS mathematical exposition

A fixed positive constant bounds the first derivative of the unit cutoff

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

Statement

There exists C>0 such that |q′(t)|≤C for every real t. This constant is chosen before any radial scale.

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

All objects and hypotheses

No radius R occurs in this statement. The derivative is the scalar real derivative of the fixed q.

Mathematical proof

1. Use smoothness to make q′ continuous

Since q is C∞, it is at least C¹ and its first derivative is continuous on ℝ.

\[q\in C^\infty\Longrightarrow q'\text{ continuous}.\]

Corresponding Lean step

have hcont := smoothUnitCutoff_contDiff.continuous_deriv (WithTop.coe_le_coe.mpr (le_top : (1 : ℕ∞) ≤ ⊤))

2. Use compact support to bound the derivative

A derivative vanishes off the closed support of its original function. Thus q′ has compact support, and its continuity gives a global norm bound B.

\[\operatorname{tsupp}(q')\subseteq\operatorname{tsupp}(q),\qquad\exists B\ \forall t,\ |q'(t)|\le B.\]

Corresponding Lean step

obtain ⟨C, hC⟩ := smoothUnitCutoff_hasCompactSupport.deriv.exists_bound_of_continuous hcont

3. Make the bound strictly positive

Replace B by max(B,1). This number is positive and no smaller than B, so it keeps the derivative bound.

\[C=\max(B,1)>0,\qquad |q'(t)|\le B\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_deriv_bounded

The order ∃C then ∀t is a genuine uniform bound. No numerical value for C is computed.

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

Exact module and namespace context

Lean proof · smoothUnitCutoff_deriv_bounded

Actual proof outline: Use smoothness to make q′ continuous: The order proof says one derivative is available from infinite smoothness. Use compact support to bound the derivative: .deriv transfers compact support, and exists_bound_of_continuous supplies the uniform bound. Make the bound strictly positive: The source's C from the intermediate bound is renamed B here to distinguish it from the final positive witness.

theorem smoothUnitCutoff_deriv_bounded :
    ∃ C : ℝ, 0 < C ∧ ∀ x : ℝ, ‖deriv smoothUnitCutoff x‖ ≤ C := by
  have hcont : Continuous (deriv smoothUnitCutoff) :=
    smoothUnitCutoff_contDiff.continuous_deriv
      (WithTop.coe_le_coe.mpr (le_top : (1 : ℕ∞) ≤ ⊤))
  obtain ⟨C, hC⟩ :=
    smoothUnitCutoff_hasCompactSupport.deriv.exists_bound_of_continuous hcont
  exact ⟨max C 1, lt_max_of_lt_right one_pos, fun x =>
    (hC x).trans (le_max_left C 1)⟩

/-- The second derivative of the unit cutoff is continuous. -/

Exact module and namespace context

Scope and omitted-condition boundaries

This is the first-order input to the radial C/R theorem; no second-order API is needed.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ContDiff.continuous_deriv
HasCompactSupport.deriv
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 curated entry for this declaration. Attribution is preserved as local card evidence only, without a new external-source audit or source-equivalence verdict.
ContDiff.continuous_deriv — Exact checked local Mathlib dependency definition or theorem.
HasCompactSupport.deriv — Exact checked local Mathlib dependency definition or theorem.
HasCompactSupport.exists_bound_of_continuous — Additive declaration generated from HasCompactMulSupport.exists_bound_of_continuous by to_additive.
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_contDiff — Exact earlier ASTIS definition or theorem used in this declaration; not an independent external-source claim.
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.