ASTIS mathematical exposition

The ordinary support lies in the outer closed ball

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

Statement

Let E be a normed additive commutative group and R>0. Every point where χ_R is nonzero lies in the closed ball about zero of radius 2R.

\[\operatorname{supp}\chi_R:=\{x:\chi_R(x)\ne0\}\subseteq\overline B(0,2R)=\{x:\|x\|\le2R\}.\]

All objects and hypotheses

E is a normed additive commutative group.
R∈ℝ with R>0.
Here `Function.support` means the nonzero set, not its closure.

Mathematical proof

1. Exclude a nonzero value beyond the outer ball

Take x in the ordinary support. If x were outside the closed ball, then 2R<‖x‖. The outer zero-value theorem would force χ_R(x)=0, contradicting membership in the support.

\[\chi_R(x)\ne0,\ \|x\|>2R\quad\Longrightarrow\quad\chi_R(x)=0\quad\text{(contradiction)}.\]

Corresponding Lean step

rw [Metric.mem_closedBall, dist_zero_right]; by_contra hout; push Not at hout; have hzero := radialSmoothCutoff_eq_zero_of_two_mul_le_norm hR hout.le; exact hx hzero

Lean statement · radialSmoothCutoff_support_subset_closedBall

The theorem is an inclusion, not an exact support description. No compactness or smoothness is needed to prove it. The source's surrounding Radial section contributes the implicit type E and its NormedAddCommGroup instance; further structures appear explicitly in the declaration.

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 radialSmoothCutoff_support_subset_closedBall {R : ℝ} (hR : 0 < R) :
    Function.support (radialSmoothCutoff R : E → ℝ) ⊆
      Metric.closedBall 0 (2 * R)

Exact module and namespace context

Lean proof · radialSmoothCutoff_support_subset_closedBall

Actual proof outline: Exclude a nonzero value beyond the outer ball: Support membership `hx` is definitionally the assertion that the function value is nonzero. The contradiction proves the closed-ball inequality.

theorem radialSmoothCutoff_support_subset_closedBall {R : ℝ} (hR : 0 < R) :
    Function.support (radialSmoothCutoff R : E → ℝ) ⊆
      Metric.closedBall 0 (2 * R) := by
  intro x hx
  rw [Metric.mem_closedBall, dist_zero_right]
  by_contra hout
  push Not at hout
  have hzero : radialSmoothCutoff R x = 0 :=
    radialSmoothCutoff_eq_zero_of_two_mul_le_norm hR hout.le
  exact hx hzero

/-- The topological support of the radial cutoff lies in the same closed ball. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Ordinary support is not assumed closed, and this statement alone does not assert compact support in an arbitrary normed group.
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

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_eq_zero_of_two_mul_le_norm

Mathlib API called (external library)

Metric.mem_closedBall
dist_zero_right

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.
Metric.mem_closedBall — Exact checked local Mathlib lemma used in this proof.
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_eq_zero_of_two_mul_le_norm — Exact earlier ASTIS definition or theorem used in this declaration; not an independent external-source claim.

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