ASTIS mathematical exposition
A smooth compactly supported plateau inside any open neighborhood of a compact set
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.exists_contDiff_eq_one_tsupport_subset · theorem · Teaching coverage
Statement
Let E be a finite-dimensional real normed vector space. If K⊆E is compact, U⊆E is open, and K⊆U, then there exists a real-valued smooth function χ on E which takes values in [0,1], equals one on K, and has compact topological support contained in U. The statement also explicitly includes ordinary support contained in U.
\[\begin{gathered}K\text{ compact},\quad U\text{ open},\quad K\subseteq U\\ \Longrightarrow\ \exists\chi\in C^\infty(E,\mathbb R):\quad \operatorname{supp}\chi\subseteq U,\quad\operatorname{tsupp}\chi\subseteq U,\quad\operatorname{tsupp}\chi\text{ compact},\\ 0\le\chi(x)\le1\quad(\forall x\in E),\qquad\chi(x)=1\quad(\forall x\in K).\end{gathered}\]
All objects and hypotheses
- E is a normed additive commutative group with a real normed-vector-space structure and is finite-dimensional over ℝ.
- K and U are subsets of E, K is compact, U is open, and K⊆U.
- No inner product, nontriviality, or nonemptiness of K or U is assumed.
Mathematical proof
1. Insert a compact neighborhood and obtain an auxiliary smooth function
Choose a compact set L with K⊆interior(L) and L⊆U. Mathlib's smooth-support theorem for an open set supplies a smooth g:E→ℝ with ordinary support exactly interior(L) and all values in [0,1]. Thus g is strictly positive at each point of K.
\[K\subseteq\operatorname{int}L\subseteq L\subseteq U,\qquad\operatorname{supp}g=\operatorname{int}L,\quad g\in C^\infty,\quad0\le g\le1,\quad g|_K>0.\]
Corresponding Lean step
exists_compact_between hK hU hKU; (isOpen_interior : IsOpen (interior L)).exists_contDiff_support_eq (E := E) (n := (⊤ : ℕ∞)); lt_of_le_of_ne (hg_range (Set.mem_range_self x)).1 (Ne.symm hx_support)
2. Choose a uniform positive lower bound on K
Continuity and strict positivity of g on the compact set K give a real m>0 such that m≤g(x) for all x∈K. The library statement also handles K empty; no attained positive minimum is claimed in that case.
\[\exists m>0,\quad\forall x\in K,\quad m\le g(x),\qquad m/2>0.\]
Corresponding Lean step
hK.exists_forall_le' hg_contDiff.continuous.continuousOn hg_pos; have hm_half_pos : 0 < m / 2 := half_pos hm_pos
3. Compress the values through the smooth transition
Define χ using the standard transition S, with threshold m/2 and transition interval up to m. This composition is smooth because g is smooth and the denominator is a fixed nonzero constant. Its values lie in [0,1] because every value of S does.
\[\chi(x):=S\!\left(\frac{g(x)-m/2}{m/2}\right),\qquad \chi\in C^\infty(E,\mathbb R),\qquad0\le\chi\le1.\]
Corresponding Lean step
let χ : E → ℝ := fun x => Real.smoothTransition ((g x - m / 2) / (m / 2)); Real.smoothTransition.contDiff.comp; (hg_contDiff.sub contDiff_const).div_const (m / 2); ⟨Real.smoothTransition.nonneg _, Real.smoothTransition.le_one _⟩
4. Separate the nonzero set from the boundary of the auxiliary support
If χ(x)≠0, then its transition argument must be positive, since S vanishes on nonpositive arguments. Hence g(x)>m/2. In particular the ordinary support lies in the closed superlevel set F={x:g(x)≥m/2}.
\[\chi(x)\ne0\Longrightarrow\frac{g(x)-m/2}{m/2}>0\Longrightarrow g(x)>m/2,\qquad\operatorname{supp}\chi\subseteq F:=\{x:g(x)\ge m/2\}.\]
Corresponding Lean step
Real.smoothTransition.zero_of_nonpos hnonpos; (div_pos_iff_of_pos_right hm_half_pos).mp harg; exact (sub_pos.mp hnum).le
5. Control the closed support and obtain compactness
Continuity of g makes F closed, so tsupp χ⊆F. Because m/2>0, every point of F has g(x)≠0, hence lies in interior(L). Therefore tsupp χ⊆L⊆U. The closed set tsupp χ is a subset of compact L and is compact; ordinary support is contained in tsupport and hence also in U.
\[\operatorname{tsupp}\chi=\overline{\operatorname{supp}\chi}\subseteq F\subseteq\operatorname{int}L\subseteq L\subseteq U,\qquad\operatorname{tsupp}\chi\text{ compact}.\]
Corresponding Lean step
isClosed_le continuous_const hg_contDiff.continuous; closure_minimal hχ_support_superlevel hsuperlevel_closed; hm_half_pos.trans_le hx; (subset_tsupport χ).trans hχ_tsupport_U; hL.of_isClosed_subset isClosed_closure hχ_tsupport_L
6. Verify the plateau and collect all six properties
For x∈K, the bound g(x)≥m forces the transition argument to be at least one. Hence χ(x)=1. Together with the support inclusions, compactness, smoothness, and range bounds already proved, this supplies the required witness.
\[x\in K\Longrightarrow \frac{g(x)-m/2}{m/2}\ge1\Longrightarrow\chi(x)=1.\]
Corresponding Lean step
apply Real.smoothTransition.one_of_one_le; rw [one_le_div hm_half_pos]; linarith [hm_le x hx]; exact ⟨χ, hχ_support_U, hχ_tsupport_U, hχ_compact, hχ_contDiff, hχ_range, hχ_one⟩
Lean statement · exists_contDiff_eq_one_tsupport_subset
This is an existence theorem proved by constructing a witness from two Mathlib existence results and a scalar transition. It is not a definition of a canonical χ: the chosen L, g, and m are not exported as a uniquely determined plateau.
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_eq_one_tsupport_subset
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
{K U : Set E} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) :
∃ χ : E → ℝ,
Function.support χ ⊆ U ∧ tsupport χ ⊆ U ∧ HasCompactSupport χ ∧
ContDiff ℝ (⊤ : ℕ∞) χ ∧ Set.range χ ⊆ Set.Icc 0 1 ∧ Set.EqOn χ 1 K
Exact module and namespace context
Lean proof · exists_contDiff_eq_one_tsupport_subset
Actual proof outline: Insert a compact neighborhood and obtain an auxiliary smooth function: The first two library results provide L and g with their recorded properties. Positivity on K combines nonzero support membership with nonnegativity, rather than assuming g equals one there. Choose a uniform positive lower bound on K: `exists_forall_le'` gives a strict improvement of the lower bound zero, not an extra nonempty-set premise. Compress the values through the smooth transition: This is the construction used to prove the existence theorem. The scalar transition has already been supplied by Mathlib; no new bump formula is postulated. Separate the nonzero set from the boundary of the auxiliary support: The proof weakens the strict lower bound to a non-strict one so that the containing set F is closed and can also contain the closure of the support. Control the closed support and obtain compactness: This is why using a positive superlevel threshold matters: merely knowing supp g⊆U would not by itself control its closure inside U. Verify the plateau and collect all six properties: `Set.EqOn χ 1 K` means equality on K with the constant-one function. The final nested conjunction lists exactly the six requested properties.
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_eq_one_tsupport_subset
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
{K U : Set E} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) :
∃ χ : E → ℝ,
Function.support χ ⊆ U ∧ tsupport χ ⊆ U ∧ HasCompactSupport χ ∧
ContDiff ℝ (⊤ : ℕ∞) χ ∧ Set.range χ ⊆ Set.Icc 0 1 ∧ Set.EqOn χ 1 K := by
obtain ⟨L, hL, hK_intL, hL_U⟩ := exists_compact_between hK hU hKU
obtain ⟨g, hg_support, hg_contDiff, hg_range⟩ :=
(isOpen_interior : IsOpen (interior L)).exists_contDiff_support_eq
(E := E) (n := (⊤ : ℕ∞))
have hg_pos : ∀ x ∈ K, 0 < g x := by
intro x hx
have hx_support : x ∈ Function.support g := by
rw [hg_support]
exact hK_intL hx
exact lt_of_le_of_ne
(hg_range (Set.mem_range_self x)).1 (Ne.symm hx_support)
obtain ⟨m, hm_pos, hm_le⟩ :=
hK.exists_forall_le' hg_contDiff.continuous.continuousOn hg_pos
have hm_half_pos : 0 < m / 2 := half_pos hm_pos
let χ : E → ℝ := fun x =>
Real.smoothTransition ((g x - m / 2) / (m / 2))
have hχ_support_superlevel :
Function.support χ ⊆ {x : E | m / 2 ≤ g x} := by
intro x hx
change χ x ≠ 0 at hx
have harg : 0 < (g x - m / 2) / (m / 2) := by
apply lt_of_not_ge
intro hnonpos
apply hx
exact Real.smoothTransition.zero_of_nonpos hnonpos
have hnum : 0 < g x - m / 2 :=
(div_pos_iff_of_pos_right hm_half_pos).mp harg
exact (sub_pos.mp hnum).le
have hsuperlevel_closed : IsClosed {x : E | m / 2 ≤ g x} :=
isClosed_le continuous_const hg_contDiff.continuous
have hχ_tsupport_superlevel :
tsupport χ ⊆ {x : E | m / 2 ≤ g x} := by
exact closure_minimal hχ_support_superlevel hsuperlevel_closed
have hsuperlevel_intL : {x : E | m / 2 ≤ g x} ⊆ interior L := by
intro x hx
have hgx_pos : 0 < g x := hm_half_pos.trans_le hx
have hx_support : x ∈ Function.support g := hgx_pos.ne'
rwa [hg_support] at hx_support
have hχ_tsupport_L : tsupport χ ⊆ L :=
hχ_tsupport_superlevel.trans (hsuperlevel_intL.trans interior_subset)
have hχ_tsupport_U : tsupport χ ⊆ U := hχ_tsupport_L.trans hL_U
have hχ_support_U : Function.support χ ⊆ U :=
(subset_tsupport χ).trans hχ_tsupport_U
have hχ_compact : HasCompactSupport χ := by
rw [hasCompactSupport_def]
exact hL.of_isClosed_subset isClosed_closure hχ_tsupport_L
have hχ_contDiff : ContDiff ℝ (⊤ : ℕ∞) χ := by
apply Real.smoothTransition.contDiff.comp
exact (hg_contDiff.sub contDiff_const).div_const (m / 2)
have hχ_range : Set.range χ ⊆ Set.Icc (0 : ℝ) 1 := by
rintro _ ⟨x, rfl⟩
exact ⟨Real.smoothTransition.nonneg _, Real.smoothTransition.le_one _⟩
have hχ_one : Set.EqOn χ 1 K := by
intro x hx
apply Real.smoothTransition.one_of_one_le
rw [one_le_div hm_half_pos]
linarith [hm_le x hx]
exact ⟨χ, hχ_support_U, hχ_tsupport_U, hχ_compact,
hχ_contDiff, hχ_range, hχ_one⟩
end Plateau
end Cutoff
end Calculus
end Analysis
end TechnicalLemmas
end AutoSamplingTheory
Exact module and namespace context
Scope and omitted-condition boundaries
- There are no radius-dependent derivative constants, Hessian estimates, or measure-theoretic limits in this theorem.
- This proof does not call the radial cutoff family; its compact-within-open construction is a separate API.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- exists_compact_between
- IsOpen.exists_contDiff_support_eq
- IsCompact.exists_forall_le'
- Real.smoothTransition
- Real.smoothTransition.contDiff
- Real.smoothTransition.nonneg
- Real.smoothTransition.le_one
- Real.smoothTransition.zero_of_nonpos
- Real.smoothTransition.one_of_one_le
- isClosed_le
- closure_minimal
- subset_tsupport
- IsCompact.of_isClosed_subset
Mathematical sources
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.