ASTIS mathematical exposition

Strict outer endpoints enclose a closed inner box

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

Statement

For a,b,A,B∈P with A_i<a_i and b_i<B_i for every i, the closed inner box [a,b] is contained in the open outer box ∏_i(A_i,B_i). No assumption a≤b is required.

\[\bigl[\forall i,\ A_i<a_i,\ b_i<B_i\bigr]\Longrightarrow [a,b]\subseteq\prod_i(A_i,B_i).\]

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; ∀i,A_i<a_i and ∀i,b_i<B_i. The inner box may be empty.

Mathematical proof

1. Chain the endpoint inequalities coordinatewise

For x∈[a,b], each coordinate satisfies A_i<a_i≤x_i≤b_i<B_i. These are exactly the strict inequalities for membership in the outer open box.

\[A_i<a_i\le x_i\le b_i<B_i\quad\Longrightarrow\quad A_i<x_i<B_i.\]

Corresponding Lean step

lt_of_lt_of_le (hA i) (hx.1 i) and lt_of_le_of_lt (hx.2 i) (hB i).

Lean statement · Icc_subset_univ_pi_Ioo_of_strict_bounds

The Pi order is coordinatewise. The result is a set inclusion and remains valid when the inner box is empty.

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 Icc_subset_univ_pi_Ioo_of_strict_bounds
    {n : ℕ} {a b A B : Fin (n + 1) → ℝ}
    (hA : ∀ i, A i < a i)
    (hB : ∀ i, b i < B i) :
    Set.Icc a b ⊆ Set.univ.pi (fun i => Set.Ioo (A i) (B i))

Exact module and namespace context

Lean proof · Icc_subset_univ_pi_Ioo_of_strict_bounds

For x∈[a,b], each coordinate satisfies A_i<a_i≤x_i≤b_i<B_i. These are exactly the strict inequalities for membership in the outer open box. The Lean correspondence in that step identifies the exact existing rule or definitional reduction used.

theorem Icc_subset_univ_pi_Ioo_of_strict_bounds
    {n : ℕ} {a b A B : Fin (n + 1) → ℝ}
    (hA : ∀ i, A i < a i)
    (hB : ∀ i, b i < B i) :
    Set.Icc a b ⊆ Set.univ.pi (fun i => Set.Ioo (A i) (B i)) := by
  intro x hx i _hi
  exact ⟨lt_of_lt_of_le (hA i) (hx.1 i), lt_of_le_of_lt (hx.2 i) (hB i)⟩

/-- Smooth plateau for a finite closed Pi-box inside a strictly larger open
Pi-box.

The extra hypothesis `a ≤ b` records that the inner box is nonempty in the
intended exhaustion use.  The construction comes from the generic
compact-in-open plateau theorem in `Analysis.Calculus.Cutoff`; it gives both
plain- and topological-support containment, compact support, smoothness,
`[0, 1]` range, and equality to one on the whole inner box.

This is one chosen cutoff, not yet an exhausting family with derivative
bounds.  Tail passage, whole-space weighted integration by parts, generator
domains, invariant Gibbs law, reversibility, and KL/FI dissipation remain
separate obligations. -/

Exact module and namespace context

Scope and omitted-condition boundaries

No cutoff function or exhaustion sequence is chosen.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

lt_of_lt_of_le
lt_of_le_of_lt

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.