Exact ordinary support and nonnegativity give positivity inside the box
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.positive_on_univ_pi_Ioo_of_support_eq_univ_pi_Ioo · theorem · Teaching coverage
Statement
If χ:P→ℝ has ordinary support exactly O and range contained in [0,1], then χ(x)>0 for every specified x∈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→ℝ; supp χ=O; χ(P)⊆[0,1]; x∈O.
- No smoothness or endpoint-order hypothesis.
Mathematical proof
1. Use support membership to rule out zero
Since x∈O=supp χ, χ(x)≠0.
Corresponding Lean step
simpa [hχsupp] using hx; support membership becomes hxne.
2. Combine with the lower range bound
The range premise gives 0≤χ(x). A nonnegative nonzero real number is strictly positive.
Corresponding Lean step
(hχrange ⟨x,rfl⟩).1; lt_of_le_of_ne hnonneg (Ne.symm hxne).
Lean statement · positive_on_univ_pi_Ioo_of_support_eq_univ_pi_Ioo
The prime-free χ is an arbitrary function satisfying support and range conditions; continuity is not 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 positive_on_univ_pi_Ioo_of_support_eq_univ_pi_Ioo
{n : ℕ} {a b : Fin (n + 1) → ℝ}
{χ : (Fin (n + 1) → ℝ) → ℝ}
(hχsupp : Function.support χ = Set.univ.pi (fun i => Set.Ioo (a i) (b i)))
(hχrange : Set.range χ ⊆ Set.Icc 0 1)
{x : Fin (n + 1) → ℝ}
(hx : x ∈ Set.univ.pi (fun i => Set.Ioo (a i) (b i))) :
0 < χ xLean proof · positive_on_univ_pi_Ioo_of_support_eq_univ_pi_Ioo
The source first since x∈O=supp χ, χ(x)≠0. It finishes as follows: The range premise gives 0≤χ(x). A nonnegative nonzero real number is strictly positive. 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 positive_on_univ_pi_Ioo_of_support_eq_univ_pi_Ioo
{n : ℕ} {a b : Fin (n + 1) → ℝ}
{χ : (Fin (n + 1) → ℝ) → ℝ}
(hχsupp : Function.support χ = Set.univ.pi (fun i => Set.Ioo (a i) (b i)))
(hχrange : Set.range χ ⊆ Set.Icc 0 1)
{x : Fin (n + 1) → ℝ}
(hx : x ∈ Set.univ.pi (fun i => Set.Ioo (a i) (b i))) :
0 < χ x := by
have hxmem : x ∈ Function.support χ := by
simpa [hχsupp] using hx
have hxne : χ x ≠ 0 := hxmem
have hnonneg : 0 ≤ χ x := (hχrange ⟨x, rfl⟩).1
exact lt_of_le_of_ne hnonneg (Ne.symm hxne)
/-- A closed inner Pi-box is contained in a strictly larger open Pi-box.
This is a bookkeeping leaf for exhaustion arguments. It only proves the
coordinate set inclusion needed to feed local cutoff construction; it does not
choose an exhausting sequence or construct a cutoff. -/Scope and omitted-condition boundaries
- This is pointwise positivity, not a uniform positive lower bound over O.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- Function.support
- lt_of_le_of_ne
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.