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

A cutoff at one inner-box point with support in the outer box

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

Statement

For strict outer bounds A_i<a_i and b_i<B_i, and a specified x∈[a,b], there exists a smooth [0,1]-valued χ with χ(x)=1 and compact closed support in O_out=∏_i(A_i,B_i); its ordinary support is also in O_out.

\[\exists\chi\in C^\infty,\quad\chi(x)=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,x∈P; ∀i,A_i<a_i; ∀i,b_i<B_i; x∈[a,b]. No separate a≤b parameter.

Mathematical proof

1. Move the chosen point into the outer open box

Apply the strict-box inclusion to the supplied inner-box membership.

\[x\in[a,b]\subseteq O_{\rm out}.\]
Corresponding Lean step

Icc_subset_univ_pi_Ioo_of_strict_bounds hA hB hx.

2. Apply the single-point cutoff theorem

Use the existing local existence theorem with outer endpoints A,B and the newly established membership. It supplies a cutoff equal to one only at the chosen x as stated.

\[\chi(x)=1,\qquad\operatorname{tsupp}\chi\subseteq O_{\rm out}.\]
Corresponding Lean step

exists_contDiff_cutoff_support_subset_univ_pi_Ioo (...).

Lean statement · exists_contDiff_cutoff_support_subset_outer_univ_pi_Ioo_of_mem_Icc

This wrapper does not call the whole-inner-box plateau theorem; its conclusion concerns one point only.

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_outer_univ_pi_Ioo_of_mem_Icc
    {n : ℕ} {a b A B x : Fin (n + 1) → ℝ}
    (hA : ∀ i, A i < a i)
    (hB : ∀ i, b i < B i)
    (hx : x ∈ Set.Icc a b) :
    ∃ χ : (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_outer_univ_pi_Ioo_of_mem_Icc

The source first apply the strict-box inclusion to the supplied inner-box membership. It finishes as follows: Use the existing local existence theorem with outer endpoints A,B and the newly established membership. It supplies a cutoff equal to one only at the chosen x as stated. 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_support_subset_outer_univ_pi_Ioo_of_mem_Icc
    {n : ℕ} {a b A B x : Fin (n + 1) → ℝ}
    (hA : ∀ i, A i < a i)
    (hB : ∀ i, b i < B i)
    (hx : x ∈ Set.Icc a b) :
    ∃ χ : (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 :=
  exists_contDiff_cutoff_support_subset_univ_pi_Ioo
    (Icc_subset_univ_pi_Ioo_of_strict_bounds hA hB hx)

/-- Support contained in the open box implies Mathlib's finite-box signed
face-term sum is zero.

This is still only a finite-box support-to-face producer.  It does not prove
that a concrete Langevin/cutoff vector field has this support, and it does not
prove whole-space integration by parts or stationarity. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • Do not upgrade χ(x)=1 to χ=1 throughout [a,b].

Source and reuse

ASTIS parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the ASTIS parents.

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.