Samplinglib mathematical lesson

A smooth compactly supported cutoff at one point of an open box

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.exists_contDiff_cutoff_tsupport_subset_univ_pi_Ioo · theorem · Teaching coverage

Read this first

Mathematical statement

For endpoints a,b and x∈O, there is χ:P→ℝ smooth on all P, with values in [0,1], compact topological support contained in O, and χ(x)=1.

\[\exists\chi:P\to\mathbb R,\quad\operatorname{tsupp}\chi\subseteq O,\quad\operatorname{tsupp}\chi\text{ compact},\quad\chi\in C^\infty,\quad0\le\chi\le1,\quad\chi(x)=1.\]

Lean statement · exists_contDiff_cutoff_tsupport_subset_univ_pi_Ioo

This is an existence theorem, not a new definition or a canonical cutoff choice. Its proof reuses the finite-dimensional neighborhood-bump theorem.

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 exists_contDiff_cutoff_tsupport_subset_univ_pi_Ioo
    {n : ℕ} {a b x : Fin (n + 1) → ℝ}
    (hx : x ∈ Set.univ.pi fun i => Set.Ioo (a i) (b i)) :
    ∃ χ : (Fin (n + 1) → ℝ) → ℝ,
      tsupport χ ⊆ Set.univ.pi (fun i => Set.Ioo (a i) (b i)) ∧
      HasCompactSupport χ ∧
      ContDiff ℝ (⊤ : ℕ∞) χ ∧
      Set.range χ ⊆ Set.Icc 0 1 ∧
      χ x = 1

Exact module and namespace context

Proof roadmap

1The open Pi-box is a neighborhood of x
Each coordinate interval is open; the finite product O is therefore open. Its membership assumption at x makes O a neighborhood of x.
2Specialize the existing local smooth-bump existence theorem
Mathlib's finite-dimensional bump theorem gives a smooth [0,1]-valued function equal to one at x, with compact topological support in that neighborhood. These are exactly the requested properties.

Full assumptions and notation

All objects and hypotheses

n∈ℕ, d=n+1≥1, P=(Fin d→ℝ) with its usual supremum norm, V=EuclideanSpace ℝ (Fin d) with its ℓ² norm. T:P→V is WithLp.toLp 2, a continuous linear equivalence, and e=T⁻¹=WithLp.ofLp.
a,b∈P; K=[a,b]={x:∀i,a_i≤x_i≤b_i} is the closed box and O=∏_i(a_i,b_i) is the open box. All unspecified integrals and a.e. assertions use Lebesgue volume on P, restricted to K when indicated.
x∈P with x∈O; no separate a≤b hypothesis.
Topological support is the closure of the nonzero set; the conclusion concerns one chosen point, not a whole inner box.

Mathematical proof

1. The open Pi-box is a neighborhood of x

Each coordinate interval is open; the finite product O is therefore open. Its membership assumption at x makes O a neighborhood of x.

\[O=\prod_i(a_i,b_i)\text{ open},\qquad O\in\mathcal N(x).\]

Corresponding Lean step

isOpen_set_pi Set.finite_univ (fun _ _ => isOpen_Ioo); hopen.mem_nhds hx.

2. Specialize the existing local smooth-bump existence theorem

Mathlib's finite-dimensional bump theorem gives a smooth [0,1]-valued function equal to one at x, with compact topological support in that neighborhood. These are exactly the requested properties.

\[\exists\chi:P\to\mathbb R,\quad\operatorname{tsupp}\chi\subseteq O,\quad\operatorname{tsupp}\chi\text{ compact},\quad\chi\in C^\infty,\quad0\le\chi\le1,\quad\chi(x)=1.\]

Corresponding Lean step

exists_contDiff_tsupport_subset (n := (⊤ : ℕ∞)) (hopen.mem_nhds hx).

Lean verification

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

Lean proof · exists_contDiff_cutoff_tsupport_subset_univ_pi_Ioo

The source first each coordinate interval is open; the finite product O is therefore open. Its membership assumption at x makes O a neighborhood of x. It finishes as follows: Mathlib's finite-dimensional bump theorem gives a smooth [0,1]-valued function equal to one at x, with compact topological support in that neighborhood. These are exactly the requested properties. Intermediate steps below identify the actual helper calls and the conditions each one needs.

Download module (.lean)

theorem exists_contDiff_cutoff_tsupport_subset_univ_pi_Ioo
    {n : ℕ} {a b x : Fin (n + 1) → ℝ}
    (hx : x ∈ Set.univ.pi fun i => Set.Ioo (a i) (b i)) :
    ∃ χ : (Fin (n + 1) → ℝ) → ℝ,
      tsupport χ ⊆ Set.univ.pi (fun i => Set.Ioo (a i) (b i)) ∧
      HasCompactSupport χ ∧
      ContDiff ℝ (⊤ : ℕ∞) χ ∧
      Set.range χ ⊆ Set.Icc 0 1 ∧
      χ x = 1 := by
  have hopen : IsOpen (Set.univ.pi fun i => Set.Ioo (a i) (b i)) := by
    exact isOpen_set_pi Set.finite_univ fun _ _ => isOpen_Ioo
  exact exists_contDiff_tsupport_subset (n := (⊤ : ℕ∞)) (hopen.mem_nhds hx)

Exact module and namespace context

Scope and omitted-condition boundaries

No exhausting family or derivative bound is constructed.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

isOpen_set_pi
exists_contDiff_tsupport_subset

Mathematical sources

Current ASTIS source — Exact statement and actual proof/construction authority; raw code intentionally omitted from this packet.
Existing curated module card — Existing declaration-specific attribution entry, read as documentation without a new source-equivalence verdict.
Called library/source declaration: exists_contDiff_tsupport_subset — Exact existing Mathlib theorem used by the documented argument.
Existing focused test — Exact named declaration invocation located in an existing example; no test was run.

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