Ordinary support containment means zero outside the open box
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.eq_zero_off_univ_pi_Ioo_of_support_subset_univ_pi_Ioo · theorem · Teaching coverage
Statement
For endpoints a,b and any F:P→P whose nonzero set is contained in O, F vanishes at every point outside 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.
- F:P→P; ordinary Function.support F⊆O. No endpoint-order or regularity hypothesis.
Mathematical proof
1. Contradict a nonzero value off the box
If x∉O but F(x)≠0, then x belongs to ordinary support and hence to O, contradiction.
Corresponding Lean step
by_contra hne; hx (hsupp hne).
Lean statement · eq_zero_off_univ_pi_Ioo_of_support_subset_univ_pi_Ioo
`Function.support` is just the nonzero set; membership is definitionally a nonzero-value assertion.
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 eq_zero_off_univ_pi_Ioo_of_support_subset_univ_pi_Ioo
{n : ℕ}
(a b : Fin (n + 1) → ℝ)
(F : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
(hsupp : Function.support F ⊆ (Set.univ.pi fun i => Set.Ioo (a i) (b i))) :
∀ x ∉ (Set.univ.pi fun i => Set.Ioo (a i) (b i)), F x = 0Lean proof · eq_zero_off_univ_pi_Ioo_of_support_subset_univ_pi_Ioo
If x∉O but F(x)≠0, then x belongs to ordinary support and hence to O, contradiction. The Lean correspondence in that step identifies the exact existing rule or definitional reduction used.
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 eq_zero_off_univ_pi_Ioo_of_support_subset_univ_pi_Ioo
{n : ℕ}
(a b : Fin (n + 1) → ℝ)
(F : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
(hsupp : Function.support F ⊆ (Set.univ.pi fun i => Set.Ioo (a i) (b i))) :
∀ x ∉ (Set.univ.pi fun i => Set.Ioo (a i) (b i)), F x = 0 := by
intro x hx
by_contra hne
exact hx (hsupp hne)
/-- Smooth finite-dimensional cutoff localized inside a Pi-open box.
For any point of `Set.univ.pi (fun i => Set.Ioo (a i) (b i))`, Mathlib's
finite-dimensional bump theorem supplies a smooth real-valued cutoff whose
topological support is contained in the open box, has compact support, takes
values in `[0, 1]`, and is equal to `1` at the chosen point.
This is only the local smooth-cutoff existence leaf. It does not choose an
exhausting family of boxes, prove derivative formulas for a specific cutoff,
perform a tail limit, or prove weighted integration by parts/invariance. -/Scope and omitted-condition boundaries
- This is not a compact-support theorem.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- Function.support
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.