Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

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

Read this first

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

Download module (.lean)
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

Proof roadmap

  1. 1Place 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].

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

Full assumptions and notation

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 verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

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.

Download module (.lean)
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)

Exact module and namespace context

Scope and omitted-condition boundaries
  • No radius-indexed family or uniform derivative estimate is part of this existence result.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • isCompact_Icc
  • isOpen_set_pi

Mathematical sources

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