ASTIS mathematical exposition

A pointwise cutoff with both support interfaces

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

Statement

For endpoints a,b and x∈O, there exists a smooth χ:P→ℝ taking values in [0,1], equal to one at x, with compact topological support, and with both supp χ⊆O and tsupp χ⊆O.

\[\exists\chi:P\to\mathbb R,\quad\operatorname{supp}\chi\subseteq O,\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∈O; no additional regularity or endpoint-order premise.

Mathematical proof

1. Choose the previously constructed local cutoff

Use the preceding existence theorem to obtain χ with closed-support containment, compact support, smoothness, range and point value.

\[\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_cutoff_tsupport_subset_univ_pi_Ioo hx.

2. Add ordinary-support containment without changing χ

Apply the support-closure inclusion to the same witness, retaining all its other properties.

\[\operatorname{supp}\chi\subseteq\operatorname{tsupp}\chi\subseteq O.\]

Corresponding Lean step

support_subset_univ_pi_Ioo_of_tsupport_subset_univ_pi_Ioo hχtsupp; final tuple keeps the same χ.

Lean statement · exists_contDiff_cutoff_support_subset_univ_pi_Ioo

This is a packaging wrapper. It proves no second existence construction independent of the local cutoff 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_support_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) → ℝ) → ℝ,
      Function.support χ ⊆ Set.univ.pi (fun i => Set.Ioo (a i) (b i)) ∧
      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_support_subset_univ_pi_Ioo

The source first use the preceding existence theorem to obtain χ with closed-support containment, compact support, smoothness, range and point value. It finishes as follows: Apply the support-closure inclusion to the same witness, retaining all its other properties. Intermediate steps below identify the actual helper calls and the conditions each one needs.

theorem exists_contDiff_cutoff_support_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) → ℝ) → ℝ,
      Function.support χ ⊆ Set.univ.pi (fun i => Set.Ioo (a i) (b i)) ∧
      tsupport χ ⊆ Set.univ.pi (fun i => Set.Ioo (a i) (b i)) ∧
      HasCompactSupport χ ∧
      ContDiff ℝ (⊤ : ℕ∞) χ ∧
      Set.range χ ⊆ Set.Icc 0 1 ∧
      χ x = 1 := by
  rcases exists_contDiff_cutoff_tsupport_subset_univ_pi_Ioo hx with
    ⟨χ, hχtsupp, hχcompact, hχsmooth, hχrange, hχone⟩
  exact ⟨χ,
    support_subset_univ_pi_Ioo_of_tsupport_subset_univ_pi_Ioo hχtsupp,
    hχtsupp, hχcompact, hχsmooth, hχrange, hχone⟩

/-- Smooth nonnegative bump whose plain support is exactly a finite Pi-open box.

This is the finite-box specialization of Mathlib's
`IsOpen.exists_contDiff_support_eq`.  It is useful when a later cutoff argument
needs nonvanishing throughout an open box.  Unlike the local cutoff leaves
above, this theorem does not assert compact support, topological-support
containment, equality to `1` on an inner closed box, an exhausting family, tail
decay, weighted IBP, generator domains, invariant law, or reversibility. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Only χ(x)=1 is asserted, not a plateau on all of an inner box.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the ASTIS parents.

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: AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.exists_contDiff_cutoff_tsupport_subset_univ_pi_Ioo — Exact ASTIS parent called in the proof steps above; this anchor adds no source-equivalence verdict.
Called library/source declaration: AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.support_subset_univ_pi_Ioo_of_tsupport_subset_univ_pi_Ioo — Exact ASTIS parent called in the proof steps above; this anchor adds no source-equivalence verdict.
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.