MATHLIBANNEX / CANONICAL DECLARATION CARD

From local to global almost-everywhere constancy

MathlibAnnex.exists_aeConstantOn_of_local

theorem

Separates agreement of constants by connectedness from countable measure-theoretic gluing.

Statement

Let be a topological space with a measurable structure, and let be positive on every nonempty open set. Let be any set, , and let be connected and Lindelöf. Suppose that for every there are an open neighborhood and a constant such that Then there is one with almost everywhere for .

Assumptions

Here connected means nonempty and admitting no partition into two disjoint nonempty relatively open subsets. Lindelöf means that every open cover of admits a countable subcover. No finiteness or Haar assumption is imposed on , and need not be second countable. No topology or measurable structure on the value set is required. The supplied neighborhoods in particular make open, although openness is not a separate input.

Conclusion

One common constant works outside a null set for the restricted measure on . Connectedness identifies the local constants; Lindelöf supplies the countability needed to join their exceptional sets. Those are distinct uses of the hypotheses.

The local data at are an open set , the relations , and a value satisfying almost everywhere for . At one chosen point of the nonempty set , these data supply the initial value . Thus no separate nonemptiness assumption on is needed.

Proof route

Fix a constant from one local neighborhood. Its region of local validity and its complement in are disjoint open sets. Connectedness makes that region all of . Select a countable subcover of neighborhoods carrying this same constant and apply countable gluing.

Proof steps

  1. Fix a value and its region. Choose and its local data . Define

    It contains . It is open: a witnessing for is contained in , because the same witnesses membership for every point of .

  2. Show the complementary region is open. For , choose local data . If some were also in , take a witnessing open set for with constant . Then , so this open overlap has positive measure. The open-overlap theorem gives . But would then witness , a contradiction. Thus

    and is open.

  3. Use connectedness to identify the region. The disjoint open sets and cover . Preconnectedness forces to lie in one of them. It cannot lie in the latter because . Hence . In particular, every point of now has an open neighborhood on which the same works almost everywhere.

  4. Use a countable cover to glue. Choose for each one of these neighborhoods . Lindelöf gives a countable set of indices such that

    The countable-cover gluing theorem gives almost everywhere for . Only this selected countable family is used in the measure argument; the original uncountable family of local null sets is never united.

Main citations

Lean source signature (exact)

theorem exists_aeConstantOn_of_local
    {U : Set X} (hU : IsConnected U) (hL : IsLindelof U) {u : X → Y}
    (hlocal : ∀ x ∈ U, Nonempty (LocalAEConstantAt μ U u x)) :
    ∃ c : Y, AEConstantOn μ u U c
In the source Mathematical meaning
[MeasurableSpace X] [TopologicalSpace X] (μ : Measure X) [μ.IsOpenPosMeasure] The topological measure space with positivity on nonempty open sets, and arbitrary value set .
{U : Set X} (hU : IsConnected U) The domain is nonempty and preconnected. This exact theorem excludes the empty domain.
(hL : IsLindelof U) {u : X → Y} Every open cover of has a countable subcover, and takes values in . Second countability of all is not required.
(hlocal : ∀ x ∈ U, Nonempty (LocalAEConstantAt μ U u x)) At every there exists a local record with the six field rows below. Its constant may initially depend on .
neighborhood : Set X The selected neighbourhood of the point ; this and the next five rows read the separately cited local record.
isOpen_neighborhood is open in the ambient topology.
mem_neighborhood The specified point satisfies .
neighborhood_subset .
constant One value for this neighbourhood.
In the source Mathematical meaning
ae_eq for -almost every . The same occur in these six fields.
∃ c : Y, AEConstantOn μ u U c The conclusion supplies one value with almost everywhere for . Connectedness identifies constants, whereas Lindelöf supplies countability for the exceptional sets.
Exact surrounding binder context (separate excerpts)

Exact source lines 12–15:

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

Exact source lines 49–52:


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

Exact source lines 90–90:

variable [μ.IsOpenPosMeasure]

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

Exact content identity

Declaration: MathlibAnnex.exists_aeConstantOn_of_local

Accepted content SHA-256: 32eb30dc10b1168e6498f64852c670422dee306e24e529c37903ca272446043d

Accepted source guide SHA-256: 8f2b48a24d4619c2f6a92822335346698edaba2bc7d32939b663da8392d43bae

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑