ASTIS mathematical exposition

A smooth nonnegative function with exactly the open box as nonzero set

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

Statement

For arbitrary endpoints a,b, there exists χ:P→ℝ which is smooth, has all values in [0,1], and whose ordinary support is exactly O. This includes empty open boxes.

\[\exists\chi:P\to\mathbb R,\quad\operatorname{supp}\chi=O,\quad\chi\in C^\infty,\quad0\le\chi\le1.\]

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.
a,b arbitrary; no point in O or endpoint-order assumption is required.

Mathematical proof

1. Verify openness of the prescribed support

O is a finite product of open real intervals, so it is open even when it is empty.

\[O=\prod_i(a_i,b_i)\text{ is open}.\]

Corresponding Lean step

isOpen_set_pi Set.finite_univ ... isOpen_Ioo.

2. Apply the smooth exact-support theorem

Mathlib supplies a smooth [0,1]-valued function whose ordinary support equals any prescribed open set in a finite-dimensional real normed space.

\[\operatorname{supp}\chi=O,\qquad\chi\in C^\infty,\quad\chi(P)\subseteq[0,1].\]

Corresponding Lean step

hopen.exists_contDiff_support_eq (n := (⊤ : ℕ∞)).

Lean statement · exists_contDiff_support_eq_univ_pi_Ioo

Exact `Function.support` means χ is nonzero at every point of O and zero outside it. The exported conclusion does not include `HasCompactSupport` or tsupport⊆O.

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

Exact module and namespace context

Lean proof · exists_contDiff_support_eq_univ_pi_Ioo

The source first o is a finite product of open real intervals, so it is open even when it is empty. It finishes as follows: Mathlib supplies a smooth [0,1]-valued function whose ordinary support equals any prescribed open set in a finite-dimensional real normed space. Intermediate steps below identify the actual helper calls and the conditions each one needs.

theorem exists_contDiff_support_eq_univ_pi_Ioo
    {n : ℕ} (a b : Fin (n + 1) → ℝ) :
    ∃ χ : (Fin (n + 1) → ℝ) → ℝ,
      Function.support χ = Set.univ.pi (fun i => Set.Ioo (a i) (b i)) ∧
      ContDiff ℝ (⊤ : ℕ∞) χ ∧
      Set.range χ ⊆ Set.Icc 0 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 hopen.exists_contDiff_support_eq (n := (⊤ : ℕ∞))

/-- A `[0,1]`-valued function whose support is exactly a finite Pi-open box is
strictly positive at every point of that box.

This is only a support/range consequence.  It does not construct a compactly
supported cutoff, prove a plateau on an inner closed box, choose an exhaustion,
or prove any boundary/tail/integration-by-parts statement. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Do not strengthen ordinary-support equality to topological-support containment inside the same open box.
No value-one plateau is asserted.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

isOpen_set_pi
IsOpen.exists_contDiff_support_eq

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: IsOpen.exists_contDiff_support_eq — 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.