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
Mathematical 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.
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)] gProof roadmap
- 1The 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.
- 2Remove 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.
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∈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.
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.
Corresponding Lean step
hs.ae_notMem volume; ae_restrict_iff' measurableSet_Icc; hfg x ⟨hxIoo.mpr hxIcc,hxnot⟩.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
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.
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 := 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⟩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.
Sources, dependencies, and reuse
Source and reuse
Samplinglib 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.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.