ASTIS mathematical exposition

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

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

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

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

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.

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)

/-- Topological-support containment implies plain function-support containment
inside a finite Pi-open box.

This is the bridge needed by the finite-box cutoff route: Mathlib's smooth
cutoff theorem naturally returns `tsupport`, while the already-compiled
zero-face handoffs are phrased using `Function.support`.  The lemma is only a
support-API conversion; it does not construct a cutoff or prove any derivative,
tail, or whole-space integration-by-parts statement. -/

Exact module and namespace context

Scope and omitted-condition boundaries

No exhausting family or derivative bound is constructed.

Source and reuse

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

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