Samplinglib mathematical lesson

Strict outer endpoints enclose a closed inner box

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

Read this first

Mathematical 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).\]

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.

Download module (.lean)

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

Proof roadmap

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

Full assumptions and notation

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 verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

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.

Download module (.lean)

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)⟩

Exact module and namespace context

Scope and omitted-condition boundaries

No cutoff function or exhaustion sequence is chosen.

Sources, dependencies, and reuse

Source and reuse

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

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.