Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

A single smooth plateau on an entire inner closed box

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

Statement

Suppose a≤b, A_i<a_i, and b_i<B_i for every i. Then one smooth χ:P→ℝ equals one at every point of [a,b], takes values in [0,1], and has compact topological support contained in the outer open box O_out=∏_i(A_i,B_i). Ordinary support is also contained there.

\[\exists\chi\in C^\infty(P,\mathbb R),\quad\chi|_{[a,b]}=1,\quad0\le\chi\le1,\quad\operatorname{supp}\chi\subseteq O_{\rm out},\quad\operatorname{tsupp}\chi\subseteq O_{\rm out},\quad\operatorname{tsupp}\chi\text{ compact}.\]

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,A,B∈P; a≤b coordinatewise, ∀i,A_i<a_i, ∀i,b_i<B_i.
  • O_out=∏_i(A_i,B_i); the explicit a≤b hypothesis is retained even though the generic compact-in-open theorem permits empty compact sets.

Mathematical proof

1. Place the compact inner box inside the open outer box

The closed box [a,b] is compact in finite dimensions. Strict endpoint bounds give its containment in O_out, which is open. The source also records nonemptiness using a∈[a,b].

\[[a,b]\text{ compact},\quad[a,b]\subseteq O_{\rm out},\quad O_{\rm out}\text{ open},\quad a\in[a,b].\]
Corresponding Lean step

isCompact_Icc; Icc_subset_univ_pi_Ioo_of_strict_bounds hA hB; isOpen_set_pi; _hinner := ⟨a,le_rfl,hab⟩.

2. Use the generic compact-in-open plateau construction

Apply the Cutoff module's plateau theorem to K=[a,b] and U=O_out. It returns one function with all six properties simultaneously.

\[\chi|_{[a,b]}=1,\qquad\operatorname{tsupp}\chi\subseteq O_{\rm out}.\]
Corresponding Lean step

Cutoff.exists_contDiff_eq_one_tsupport_subset isCompact_Icc hopen (...).

Lean statement · exists_contDiff_cutoff_eq_one_on_Icc_tsupport_subset_outer_univ_pi_Ioo

Unlike the single-point cutoff theorem, `Set.EqOn χ 1 (Set.Icc a b)` is a value-one plateau on the whole inner box. `hab` is an actual retained parameter and must not be omitted.

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_eq_one_on_Icc_tsupport_subset_outer_univ_pi_Ioo
    {n : ℕ} {a b A B : Fin (n + 1) → ℝ}
    (hab : a ≤ b)
    (hA : ∀ i, A i < a i)
    (hB : ∀ i, b 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 ∧
      Set.EqOn χ 1 (Set.Icc a b)

Exact module and namespace context

Lean proof · exists_contDiff_cutoff_eq_one_on_Icc_tsupport_subset_outer_univ_pi_Ioo

The source first the closed box [a,b] is compact in finite dimensions. Strict endpoint bounds give its containment in O_out, which is open. The source also records nonemptiness using a∈[a,b]. It finishes as follows: Apply the Cutoff module's plateau theorem to K=[a,b] and U=O_out. It returns one function with all six properties simultaneously. Intermediate steps below identify the actual helper calls and the conditions each one needs.

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_eq_one_on_Icc_tsupport_subset_outer_univ_pi_Ioo
    {n : ℕ} {a b A B : Fin (n + 1) → ℝ}
    (hab : a ≤ b)
    (hA : ∀ i, A i < a i)
    (hB : ∀ i, b 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 ∧
      Set.EqOn χ 1 (Set.Icc a b) := by
  have _hinner : (Set.Icc a b).Nonempty := ⟨a, le_rfl, hab⟩
  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 Cutoff.exists_contDiff_eq_one_tsupport_subset
    isCompact_Icc hopen (Icc_subset_univ_pi_Ioo_of_strict_bounds hA hB)

/-- Local smooth cutoff for a point in an inner closed Pi-box, supported in a
strictly larger open Pi-box.

This packages the closed-box-to-open-box inclusion with
`exists_contDiff_cutoff_support_subset_univ_pi_Ioo`.  It is a local cutoff at a
single point of the inner box; it does not construct one cutoff equal to `1` on
the whole inner box, choose an exhausting family, prove derivative bounds, or
pass to whole-space limits. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • No radius-indexed family or uniform derivative estimate is part of this existence result.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • isCompact_Icc
  • isOpen_set_pi

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.