ASTIS mathematical exposition

Ignore the box boundary and a countable exceptional set

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

Statement

In P=ℝ^(n+1), let a,b be arbitrary endpoints, let β be any type, and let f,g:P→β agree on O outside a countable set s. Then f and g agree almost everywhere for Lebesgue measure restricted to K. No order assumption on a,b and no measurability of f or g is required.

\[f=g\text{ on }O\setminus s,\quad s\text{ countable}\quad\Longrightarrow\quad f=g\quad\text{a.e. }[\,dx|_K\,].\]

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.
β is an arbitrary type; f,g:P→β; s⊆P is countable; f(x)=g(x) for every x∈O∖s.
No hypothesis a≤b, continuity, or measurability of f and g.

Mathematical proof

1. The open and closed boxes agree almost everywhere

Product Lebesgue measure assigns zero measure to the finite coordinate boundary pieces. Mathlib supplies O=K almost everywhere, including degenerate or empty boxes.

\[O=K\quad\text{a.e. }[dx].\]

Corresponding Lean step

rw [volume_pi]; Measure.univ_pi_Ioo_ae_eq_Icc.

2. Remove the countable set and restrict

Since d=n+1≥1, volume has no atoms; a countable s is null. For almost every x∈K, x∈O and x∉s, so the assumed equality applies.

\[dx(s)=0,\qquad x\in K\Rightarrow x\in O\setminus s\quad\text{a.e.}\]

Corresponding Lean step

hs.ae_notMem volume; ae_restrict_iff' measurableSet_Icc; hfg x ⟨hxIoo.mpr hxIcc,hxnot⟩.

Lean statement · eventuallyEq_restrict_Icc_of_eqOn_univ_pi_Ioo_diff_countable

`=ᵐ[volume.restrict K]` is equality almost everywhere, not everywhere on the boundary or exceptional set. The positive dimension is built into Fin(n+1).

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 eventuallyEq_restrict_Icc_of_eqOn_univ_pi_Ioo_diff_countable
    {n : ℕ} {β : Type*}
    {a b : Fin (n + 1) → ℝ}
    {f g : (Fin (n + 1) → ℝ) → β}
    {s : Set (Fin (n + 1) → ℝ)}
    (hs : s.Countable)
    (hfg : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, f x = g x) :
    f =ᵐ[volume.restrict (Set.Icc a b)] g

Exact module and namespace context

Lean proof · eventuallyEq_restrict_Icc_of_eqOn_univ_pi_Ioo_diff_countable

The source first product Lebesgue measure assigns zero measure to the finite coordinate boundary pieces. Mathlib supplies O=K almost everywhere, including degenerate or empty boxes. It finishes as follows: Since d=n+1≥1, volume has no atoms; a countable s is null. For almost every x∈K, x∈O and x∉s, so the assumed equality applies. Intermediate steps below identify the actual helper calls and the conditions each one needs.

theorem eventuallyEq_restrict_Icc_of_eqOn_univ_pi_Ioo_diff_countable
    {n : ℕ} {β : Type*}
    {a b : Fin (n + 1) → ℝ}
    {f g : (Fin (n + 1) → ℝ) → β}
    {s : Set (Fin (n + 1) → ℝ)}
    (hs : s.Countable)
    (hfg : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, f x = g x) :
    f =ᵐ[volume.restrict (Set.Icc a b)] g := by
  have hIoo : (Set.univ.pi fun i => Set.Ioo (a i) (b i)) =ᵐ[volume]
      Set.Icc a b := by
    rw [volume_pi]
    exact Measure.univ_pi_Ioo_ae_eq_Icc
  rw [Filter.EventuallyEq, ae_restrict_iff' measurableSet_Icc]
  filter_upwards [hIoo, hs.ae_notMem volume] with x hxIoo hxnot hxIcc
  exact hfg x ⟨hxIoo.mpr hxIcc, hxnot⟩

/-- A.e. bridge from ASTIS wrapped coordinate divergence to Mathlib's Pi-space
trace summand, assuming the Pi-space derivative exists a.e. on the restricted
box.

This theorem intentionally does not derive the a.e. differentiability
assumption from an open-box/off-countable hypothesis.  Boundary-null and
countable-null transfers are separate analytic leaves. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Countable exceptional sets are permitted; the proof does not silently replace them by arbitrary null sets or claim pointwise boundary equality.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.volume_pi
MeasureTheory.Measure.univ_pi_Ioo_ae_eq_Icc
Set.Countable.ae_notMem
MeasureTheory.ae_restrict_iff'

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.
Called library/source declaration: MeasureTheory.volume_pi — Exact existing Mathlib theorem used by the documented argument.
Called library/source declaration: MeasureTheory.Measure.univ_pi_Ioo_ae_eq_Icc — Exact existing Mathlib theorem used by the documented argument.
Called library/source declaration: Set.Countable.ae_notMem — Exact existing Mathlib theorem used by the documented argument.
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.