MATHLIBANNEX / CANONICAL DECLARATION CARD

Gluing one almost-everywhere constant over a countable cover

MathlibAnnex.aeConstantOn_of_countableCover

theorem

Combines local exceptional sets using an inequality between restricted measures.

Statement

Let be a measure space, any set of values, , and . Let , let be any family of subsets, and let be countable. Suppose Then almost everywhere for .

Assumptions

There is no topology on or in this statement. The function , the cover members , and need not be measurable. Only is countable; the index set need not be. All members use the same constant .

Conclusion

The one exceptional set has measure zero for . The result includes the empty cover: the covering hypothesis then forces .

The notation means restriction of a measure to a set in the library’s sense, which is defined even for a nonmeasurable . The proof uses inequalities of measures and does not replace every restricted evaluation by an intersection formula requiring measurability.

Proof route

Compare with the sum of the restricted measures of the countable cover, and evaluate this inequality on the exceptional set.

Proof steps

  1. Form a countable family of measures. Reindex by itself and write . Restriction is monotone in its restricting set, and restriction to a countable union is bounded by the sum of the restrictions. Thus

    These are measure inequalities; the restriction-to-union inequality does not require measurable cover members.

  2. Evaluate on the exceptional set. Almost-everywhere equality on says . Evaluation of a countable sum of measures on any set therefore gives

    Hence , which is exactly the required almost-everywhere equality. No uncountable union of null sets enters this argument.

Main citations

Lean source signature (exact)

theorem aeConstantOn_of_countableCover
    {U : Set X} {u : X → Y} {c : Y}
    {ι : Type*} {V : ι → Set X} {T : Set ι}
    (hT : T.Countable) (hcover : U ⊆ ⋃ i ∈ T, V i)
    (hae : ∀ i ∈ T, AEConstantOn μ u (V i) c) :
    AEConstantOn μ u U c
In the source Mathematical meaning
{X Y : Type*} [MeasurableSpace X] (μ : Measure X) The measure space and arbitrary set of values ; no topology or linear structure is needed.
{U : Set X} {u : X → Y} {c : Y} The domain , function and one fixed value .
{ι : Type*} {V : ι → Set X} {T : Set ι} (hT : T.Countable) The family and countable subset of selected indices. The whole index set need not be countable.
(hcover : U ⊆ ⋃ i ∈ T, V i) The covering hypothesis .
In the source Mathematical meaning
(hae : ∀ i ∈ T, AEConstantOn μ u (V i) c) For every selected , almost everywhere for , always with the same constant.
AEConstantOn μ u U c The conclusion is almost everywhere for . No measurability of is silently imposed.
Exact surrounding binder context (separate excerpts)

Exact source lines 12–18:

noncomputable section
open Set MeasureTheory Filter TopologicalSpace
open scoped ENNReal Topology
namespace MathlibAnnex

section Measurable
variable {X Y : Type*} [MeasurableSpace X] (μ : Measure X)

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Exact content identity

Declaration: MathlibAnnex.aeConstantOn_of_countableCover

Accepted content SHA-256: 7073f259f8ecabc04b8f2aca208c67c5742d15bea096432658b0aefe35a6057b

Accepted source guide SHA-256: edf9847bd4ae748ce15f59448e57dfea1082708eb4241091f282939ecb186b40

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑