ASTIS mathematical exposition

A scalar cutoff zero off the box localizes any vector field

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

Statement

For endpoints a,b and arbitrary χ:P→ℝ and G:P→P, assume χ(x)=0 for every x∉O. Then the ordinary support of the product H(x)=χ(x)G(x) lies in O.

\[\chi|_{P\setminus O}=0\quad\Longrightarrow\quad\operatorname{supp}(\chi G)\subseteq O.\]

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.
χ:P→ℝ and G:P→P are arbitrary; H(x)=χ(x)G(x). No continuity, differentiability, or endpoint-order hypothesis.
χ(x)=0 for every x∉O.

Mathematical proof

1. A product cannot be nonzero off the cutoff's allowed region

For x∉O, χ(x)=0, hence H(x)=0·G(x)=0. Therefore any point in supp H must lie in O.

\[x\notin O\Longrightarrow H(x)=0,\qquad\operatorname{supp}H\subseteq O.\]

Corresponding Lean step

support_smul_subset_univ_pi_Ioo_of_eq_zero_off_univ_pi_Ioo: hχ0 := hχ x hxbox; simp [hχ0]; contradiction with nonzero support membership.

Lean statement · support_smul_subset_univ_pi_Ioo_of_eq_zero_off_univ_pi_Ioo

The conclusion is `Function.support (fun x => χ x • G x) ⊆ O`. No derivative or compactness property of the product is implicit.

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 support_smul_subset_univ_pi_Ioo_of_eq_zero_off_univ_pi_Ioo
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (χ : (Fin (n + 1) → ℝ) → ℝ)
    (G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (hχ : ∀ x ∉ (Set.univ.pi fun i => Set.Ioo (a i) (b i)), χ x = 0) :
    Function.support (fun x => χ x • G x) ⊆
      (Set.univ.pi fun i => Set.Ioo (a i) (b i))

Exact module and namespace context

Lean proof · support_smul_subset_univ_pi_Ioo_of_eq_zero_off_univ_pi_Ioo

For x∉O, χ(x)=0, hence H(x)=0·G(x)=0. Therefore any point in supp H must lie in O. The Lean correspondence in that step identifies the exact existing rule or definitional reduction used.

theorem support_smul_subset_univ_pi_Ioo_of_eq_zero_off_univ_pi_Ioo
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (χ : (Fin (n + 1) → ℝ) → ℝ)
    (G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (hχ : ∀ x ∉ (Set.univ.pi fun i => Set.Ioo (a i) (b i)), χ x = 0) :
    Function.support (fun x => χ x • G x) ⊆
      (Set.univ.pi fun i => Set.Ioo (a i) (b i)) := by
  intro x hx
  by_contra hxbox
  have hχ0 : χ x = 0 := hχ x hxbox
  have hzero : χ x • G x = 0 := by simp [hχ0]
  exact hx hzero

/-- If a scalar cutoff is supported in the open Pi-box, then multiplying any
Pi-space vector field by this cutoff gives a vector field supported in the open
Pi-box.

This only uses `Function.support`; it is not a `HasCompactSupport` theorem and
does not build a cutoff. -/

Exact module and namespace context

Scope and omitted-condition boundaries

This produces ordinary support containment, not a compact-support or regularity theorem.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

zero_smul

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