Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

The unit cutoff has compact closed support

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

Statement

The topological support of q—the closure of {t:q(t)≠0}—is compact in ℝ.

\[\operatorname{supp}(q)\subseteq[-2,2],\qquad\operatorname{tsupp}(q)=\overline{\operatorname{supp}(q)}\text{ compact}.\]

All objects and hypotheses

  • No explicit parameter or additional hypothesis; the ambient space is ℝ.

Mathematical proof

1. Choose a compact enclosure

The interval [−2,2] is compact. It suffices to place the ordinary nonzero support inside it.

\[K=[-2,2]\text{ is compact}.\]
Corresponding Lean step

apply HasCompactSupport.of_support_subset_isCompact (K := Set.Icc (-2 : ℝ) 2) isCompact_Icc

2. Exclude nonzero values outside the interval

If q(t)≠0 but t<−2 or t>2, then |t|≥2, so the vanishing theorem gives q(t)=0, a contradiction. Thus every support point lies in the chosen interval.

\[q(t)\ne0\Longrightarrow -2\le t\le2.\]
Corresponding Lean step
rw [Function.mem_support] at hx
-- The two contradiction branches use smoothUnitCutoff_eq_zero_of_two_le_abs,
-- with abs_of_nonpos on the left and abs_of_nonneg on the right.
Lean statement · smoothUnitCutoff_hasCompactSupport

HasCompactSupport concerns the closed topological support, not merely whether the nonzero set itself is compact.

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_hasCompactSupport : HasCompactSupport smoothUnitCutoff

Exact module and namespace context

Lean proof · smoothUnitCutoff_hasCompactSupport

Actual proof outline: Choose a compact enclosure: The helper converts containment of ordinary support in a compact set into compactness of its closure. Exclude nonzero values outside the interval: Support membership means nonzero value. The proof treats the two interval inequalities separately, using the sign-appropriate absolute-value identity.

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_hasCompactSupport : HasCompactSupport smoothUnitCutoff := by
  apply HasCompactSupport.of_support_subset_isCompact
    (K := Set.Icc (-2 : ℝ) 2) isCompact_Icc
  intro x hx
  rw [Function.mem_support] at hx
  simp only [Set.mem_Icc]
  constructor
  · by_contra hleft
    push Not at hleft
    apply hx
    apply smoothUnitCutoff_eq_zero_of_two_le_abs
    rw [abs_of_nonpos (by linarith : x ≤ 0)]
    linarith
  · by_contra hright
    push Not at hright
    apply hx
    apply smoothUnitCutoff_eq_zero_of_two_le_abs
    rw [abs_of_nonneg (by linarith : 0 ≤ x)]
    linarith

/-- The derivative of the one-dimensional unit cutoff is bounded by one
positive constant.  The constant is chosen before any radial scale. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • The source proves containment and compactness, not equality of topological support with a particular interval.
  • No direct named invocation was found in the inspected cutoff example block Tests/Basic.lean:49–169; this is not a statement about all possible project consumers.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • HasCompactSupport.of_support_subset_isCompact
  • isCompact_Icc
  • Function.mem_support
  • abs_of_nonpos
  • abs_of_nonneg

Mathematical sources

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