MATHLIBANNEX / CANONICAL DECLARATION CARD

Identifying constants on an open overlap

MathlibAnnex.aeConstants_eq_of_open_overlap

theorem

Uses positive measure to find a point where both almost-everywhere equalities hold.

Statement

Let have a topology and a measurable structure, and let be a measure that assigns positive measure to every nonempty open set. Let be any set, , and . Suppose are open, , and Then .

Assumptions

No topology or measurable structure on is required. There is no Haar, finite-measure, or Borel-compatibility assumption. Openness and nonempty overlap are used through positivity of that overlap, rather than through an assumed measurable-set identity.

Conclusion

The two constants coincide as elements of . A selected point of need not satisfy either equality; positivity permits choosing a point outside both exceptional sets.

As throughout the gluing argument, almost everywhere on means almost everywhere for the restricted measure . The measure of the overlap may be infinite; only its being nonzero is needed.

Proof route

Restrict both equalities to the intersection, combine them there, and use positive measure to obtain a common good point.

Proof steps

  1. Restrict the equalities. Put . Monotonicity of restriction transports the first almost-everywhere equality from to , and the second from to . Their conjunction holds almost everywhere for :

    Taking this finite conjunction is legitimate without any countable-cover assumption.

  2. Choose a good point. The set is nonempty and open, so . The positive-measure existence lemma applied to the preceding conjunction supplies a point at which both equalities hold. Therefore

    This is the step that would fail if the overlap merely contained a point but had measure zero.

Main citations

Lean source signature (exact)

theorem aeConstants_eq_of_open_overlap
    {u : X → Y} {V W : Set X} {c d : Y}
    (hVo : IsOpen V) (hWo : IsOpen W) (hVW : (V ∩ W).Nonempty)
    (hc : AEConstantOn μ u V c) (hd : AEConstantOn μ u W d) : c = d
In the source Mathematical meaning
[MeasurableSpace X] [TopologicalSpace X] (μ : Measure X) [μ.IsOpenPosMeasure] The ambient measure gives positive measure to every nonempty open set. These are surrounding source binders, including the positivity instance.
{u : X → Y} {V W : Set X} {c d : Y} The function into an arbitrary value set , the two subsets, and constants .
(hVo : IsOpen V) (hWo : IsOpen W) (hVW : (V ∩ W).Nonempty) Both sets are open and their intersection is nonempty; consequently that open overlap has positive measure.
In the source Mathematical meaning
(hc : AEConstantOn μ u V c) (hd : AEConstantOn μ u W d) for -almost every point and for -almost every point.
: c = d The output equality of the two values . Positivity supplies a point outside both exceptional sets; an arbitrary overlap point is insufficient.
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.aeConstants_eq_of_open_overlap

Accepted content SHA-256: 4e5de888bc0c487988483f96f900779ad93931a4d8d21fc6add9be9d938246f3

Accepted source guide SHA-256: dfdbe70d1af7ebaba4806aeb68fd5e86d82bc7bac0050ab42fe7350de7477119

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑