Samplinglib mathematical lesson

The ordinary support lies in the outer closed ball

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

Read this first

Mathematical 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\}.\]

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.

Download module (.lean)

theorem radialSmoothCutoff_support_subset_closedBall {R : ℝ} (hR : 0 < R) :
    Function.support (radialSmoothCutoff R : E → ℝ) ⊆
      Metric.closedBall 0 (2 * R)

Exact module and namespace context

Proof roadmap

1Exclude 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.

Full assumptions and notation

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 verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

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.

Download module (.lean)

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

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.

Sources, dependencies, and reuse

Source and reuse

Samplinglib 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.

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