Images of measure atoms

A positive finite-mass measurable atom is a measurable set whose measurable subsets have either zero or full mass. Every almost-everywhere measurable map sends such an atom to one point of a standard Borel target: the image of the measure restricted to the atom is a scalar multiple of a Dirac measure.

The finite-mass hypothesis is essential: a zero-infinity measure may make its whole carrier an atom while vanishing on every singleton.

Main definitions

• MeasureTheory.Measure.IsAtom — a measurable positive-mass set whose measurable subsets have either zero measure or the full measure of the set.

Main results

• AEMeasurable.exists_ae_eq_const_restrict_of_atom — an a.e.-measurable map into a standard Borel space is a.e. constant on every positive finite-mass measurable atom;
• AEMeasurable.exists_map_restrict_eq_smul_dirac_of_atom — an a.e.-measurable map from a positive finite-mass measurable atom into a standard Borel space has the corresponding point mass as its restricted pushforward;
• MeasureTheory.Measure.exists_eq_smul_dirac_of_forall_restrict_eq_smul — a finite measure on a standard Borel space that is proportional to each of its restrictions is a multiple of a point mass;
• MeasureTheory.Measure.nullSingletonClass_map_of_injective — an injective measurable map into a space whose singletons are measurable preserves the property that singletons have measure zero.

def MeasureTheory.Measure.IsAtom {X : Type u_1} [MeasurableSpace X] (μ : Measure X) (A : Set X) : Prop

A measure atom is a measurable positive-mass set whose measurable subsets have either zero measure or the full measure of the set.

Equations

• μ.IsAtom A = (MeasurableSet A ∧ 0 < μ A ∧ ∀ ⦃B : Set X⦄, MeasurableSet B → B ⊆ A → μ B = 0 ∨ μ B = μ A)

@[simp]

theorem MeasureTheory.Measure.isAtom_iff {X : Type u_1} [MeasurableSpace X] {μ : Measure X} {A : Set X} : μ.IsAtom A ↔ MeasurableSet A ∧ 0 < μ A ∧ ∀ ⦃B : Set X⦄, MeasurableSet B → B ⊆ A → μ B = 0 ∨ μ B = μ A

The defining characterization of a measure atom.

theorem AEMeasurable.exists_ae_eq_const_restrict_of_atom {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {T : X → Y} {μ : MeasureTheory.Measure X} {A : Set X} (hT : AEMeasurable T (μ.restrict A)) (hAfin : μ A ≠ ⊤) (hAatom : μ.IsAtom A) : ∃ (y : Y), T =ᵐ[μ.restrict A] fun (x : X) => y

An a.e.-measurable map is a.e. constant on a measurable atom. If A has positive finite mass and every measurable subset of A has either zero or full mass, then a map from A into a standard Borel space agrees almost everywhere with a constant.

theorem AEMeasurable.exists_map_restrict_eq_smul_dirac_of_atom {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {T : X → Y} {μ : MeasureTheory.Measure X} {A : Set X} (hT : AEMeasurable T (μ.restrict A)) (hAfin : μ A ≠ ⊤) (hAatom : μ.IsAtom A) : ∃ (y : Y), MeasureTheory.Measure.map T (μ.restrict A) = μ A • MeasureTheory.Measure.dirac y

An a.e.-measurable map sends a measurable atom to a point mass. If A has positive finite mass and every measurable subset of A has either zero or full mass, then the image of μ.restrict A under a map to a standard Borel space is μ A times a Dirac measure.

theorem MeasureTheory.Measure.exists_eq_smul_dirac_of_forall_restrict_eq_smul {Z : Type u_3} [MeasurableSpace Z] [StandardBorelSpace Z] [Nonempty Z] (ν : Measure Z) [IsFiniteMeasure ν] (h : ∀ (s : Set Z), MeasurableSet s → ∃ (c : ENNReal), ν.restrict s = c • ν) : ∃ (z : Z), ν = ν Set.univ • dirac z

A finite measure proportional to each of its restrictions is a point mass. On a standard Borel space, if the restriction of a finite measure ν to every measurable set is a scalar multiple of ν, then ν is its total mass times a Dirac measure.

This identifies the measures spanning extreme rays of the cone of finite measures as the positive multiples of point masses; it is used to show that the extreme rays of the completely monotone cone are exponentials.

theorem MeasureTheory.Measure.nullSingletonClass_map_of_injective {α : Type u_3} {β : Type u_4} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} [NullSingletonClass μ] {f : α → β} [MeasurableSingletonClass β] (hf : Measurable f) (hInj : Function.Injective f) : NullSingletonClass (map f μ)

An injective measurable map into a space whose singletons are measurable sends a measure with null singletons to a measure with null singletons: each singleton has an at-most-singleton preimage, which is null.

Adapted from Cameron Freer's private noAtoms_map_of_injective in Graphon/MeasureIso.lean at commit 9f7be59fa754d260a544b4cfd83d6a5b94f7552e: https://github.com/cameronfreer/graphon/commit/9f7be59fa754d260a544b4cfd83d6a5b94f7552e; the original work is copyright Cameron Freer and licensed under Apache 2.0, and it assumes f to be a measurable embedding, where the measurability and injectivity of f are separated here.