Conditioning laws, source atoms and connected sources

Conditioning a map on the preimage of a measurable event conditions its law on that event. This allows conditional distribution identities proved on a canonical law to be used for arbitrary random variables with that law, including null conditioning events. Likewise, almost everywhere measurability for a law pulls back along a random variable with that law.

A finite-mass measurable atom of a source measure is an obstruction to a prescribed law: every almost-everywhere measurable map sends its whole mass to a single point of a standard Borel target. For singleton atoms this needs no condition on the target measurable space, since their image is already explicit. This file records both forms of the constraint and their consequences for transporting Dirac measures and for laws that are null on singletons.

Connectedness of the source is a second obstruction, this time to continuous maps. A map that is continuous on a set s carrying μ, with every point of s in the support of μ, sends all of s into the support of its law. If s is moreover preconnected, the law cannot charge both of two disjoint closed sets that together carry it. So no transport map from a law with connected support onto a law split into two separated pieces is continuous on that support, which is the topological reason why optimal transport maps onto disconnected targets are discontinuous.

Adjoining a coordinate with an s-finite measure to a random variable gives the pair the product measure. Completing the source measure preserves every random variable's law. Nonnegative random variables whose real coercions have a common law are identically distributed.

Main results

• ProbabilityTheory.HasLaw.cond — conditioning transports a prescribed law;
• ProbabilityTheory.HasLaw.aemeasurable_of_ae_eq_comp — a map almost everywhere equal to an a.e. measurable map composed with a random variable of the right law is a.e. measurable;
• ProbabilityTheory.HasLaw.measure_singleton_le — the law of T gives {T x} at least the mass the source gives {x}, with ProbabilityTheory.HasLaw.measure_singleton_eq_zero and TauCeti.Probability.not_hasLaw_of_measure_singleton_ne_zero its reading for a law that is null on singletons;
• ProbabilityTheory.HasLaw.prod_extension — adjoining a coordinate with an s-finite measure to a random variable gives the pair the product measure;
• AEMeasurable.exists_map_restrict_eq_smul_dirac_of_atom — the image of a finite positive measurable atom under an a.e.-measurable map to a standard Borel space is a point mass;
• ProbabilityTheory.HasLaw.exists_measure_atom_le_measure_singleton — a law receiving such an atom has a singleton of at least the atom's mass;
• TauCeti.Probability.hasLaw_dirac_source_iff — an a.e. measurable map has law ν under Measure.dirac x exactly when ν is the Dirac measure at its value at x;
• TauCeti.Probability.not_hasLaw_dirac_source_of_forall_ne_dirac — no map at all has a non-Dirac law under a Dirac measure;
• ProbabilityTheory.HasLaw.mapsTo_support_of_continuousOn — a map continuous on a carrier of μ inside its support sends that carrier into the support of its law;
• ProbabilityTheory.HasLaw.measure_eq_zero_or_measure_eq_zero_of_continuousOn — a map continuous on a preconnected such carrier has a law that does not charge both of two disjoint closed sets carrying it.

Mathlib's ProbabilityTheory.hasLaw_dirac_iff is the statement for a Dirac target; the results here are about a Dirac source, which is what dirac_source records in their names.

theorem ProbabilityTheory.HasLaw.cond {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {T : X → Y} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (hT : HasLaw T ν μ) {s : Set Y} (hs : MeasurableSet s) : HasLaw T ν[|s] μ[|T ⁻¹' s]

Conditioning a random variable on the preimage of a measurable event gives its law conditioned on that event. The statement includes events of zero or infinite mass, when both conditional measures vanish.

theorem ProbabilityTheory.HasLaw.identDistrib_nnreal {Ω : Type u_3} {Ω' : Type u_4} [MeasurableSpace Ω] [MeasurableSpace Ω'] {P : MeasureTheory.Measure Ω} {Q : MeasureTheory.Measure Ω'} {X : Ω → NNReal} {Y : Ω' → NNReal} {μ : MeasureTheory.Measure ℝ} (hX : HasLaw (fun (ω : Ω) => ↑(X ω)) μ P) (hY : HasLaw (fun (ω : Ω') => ↑(Y ω)) μ Q) : IdentDistrib X Y P Q

Nonnegative random variables whose real coercions have the same law are identically distributed, even when defined on different measure spaces.

theorem ProbabilityTheory.HasLaw.completion {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {T : X → Y} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (hT : HasLaw T ν μ) : HasLaw (fun (x : MeasureTheory.NullMeasurableSpace X μ) => T x) ν μ.completion

Completing the source measure does not change a random variable's law.

theorem ProbabilityTheory.HasLaw.exists_measure_atom_le_measure_singleton {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {T : X → Y} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [StandardBorelSpace Y] (h : HasLaw T ν μ) {A : Set X} (hAfin : μ A ≠ ⊤) (hAatom : μ.IsAtom A) : ∃ (y : Y), μ A ≤ ν {y}

A source atom constrains the law. If A is a positive finite-mass measurable atom of μ, then every law of a map from μ to a standard Borel space has a singleton of mass at least μ A.

theorem TauCeti.Probability.not_hasLaw_of_measure_atom {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [StandardBorelSpace Y] [MeasureTheory.NullSingletonClass ν] {A : Set X} (hAfin : μ A ≠ ⊤) (hAatom : μ.IsAtom A) (T : X → Y) : ¬ProbabilityTheory.HasLaw T ν μ

A measure with a positive finite-mass measurable atom has no map onto a standard Borel law that is null on singletons.

theorem ProbabilityTheory.HasLaw.measure_singleton_le {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {T : X → Y} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (h : HasLaw T ν μ) (x : X) : μ {x} ≤ ν {T x}

A source point mass constrains the law. A map moves all the mass of {x} to the single point T x, so its law weighs {T x} at least as much as the source weighs {x}. No measurability of the singletons is needed: the bound comes from MeasureTheory.Measure.le_map_apply_image, which only uses a.e. measurability of the map.

theorem ProbabilityTheory.HasLaw.measure_singleton_eq_zero {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {T : X → Y} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.NullSingletonClass ν] (h : HasLaw T ν μ) (x : X) : μ {x} = 0

A map whose law is null on singletons has a source that is null on singletons.

theorem ProbabilityTheory.HasLaw.prod_extension {Ω : Type u_3} {α : Type u_4} {E : Type u_5} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace E] {X : Ω → α} {μ : MeasureTheory.Measure α} {P : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure E} [MeasureTheory.SFinite ν] (hX : HasLaw X μ P) : HasLaw (fun (z : Ω × E) => (X z.1, z.2)) (μ.prod ν) (P.prod ν)

Adjoining a coordinate with an s-finite measure ν to a random variable with law μ gives the pair the product measure.

theorem TauCeti.Probability.not_hasLaw_of_measure_singleton_ne_zero {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.NullSingletonClass ν] {x : X} (hx : μ {x} ≠ 0) (T : X → Y) : ¬ProbabilityTheory.HasLaw T ν μ

A nonzero source singleton has no transport onto a law that is null on singletons. This is the basic infeasibility of the Monge problem: no map can push such a source measure onto such a target measure.

theorem ProbabilityTheory.HasLaw.aemeasurable_of_ae_eq_comp {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {T : X → Y} {μ : MeasureTheory.Measure X} {Ω : Type u_3} [MeasurableSpace Ω] {m : MeasureTheory.Measure Ω} {s : Ω → X} {U : Ω → Y} (hs : HasLaw s μ m) (hT : AEMeasurable T μ) (h : U =ᵐ[m] T ∘ s) : AEMeasurable U m

A map almost everywhere equal to T ∘ s, where s has law μ and T is μ-almost everywhere measurable, is almost everywhere measurable.

theorem TauCeti.Probability.hasLaw_dirac_source_iff {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {T : X → Y} {ν : MeasureTheory.Measure Y} {x : X} (hT : AEMeasurable T (MeasureTheory.Measure.dirac x)) : ProbabilityTheory.HasLaw T ν (MeasureTheory.Measure.dirac x) ↔ ν = MeasureTheory.Measure.dirac (T x)

An a.e. measurable map transports a Dirac measure exactly onto the Dirac measure at its value. The a.e. measurability is exactly what ProbabilityTheory.HasLaw already asks for.

theorem TauCeti.Probability.not_hasLaw_dirac_source_of_forall_ne_dirac {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {T : X → Y} {ν : MeasureTheory.Measure Y} (hν : ∀ (y : Y), ν ≠ MeasureTheory.Measure.dirac y) (x : X) : ¬ProbabilityTheory.HasLaw T ν (MeasureTheory.Measure.dirac x)

A Dirac source admits no non-Dirac law. No map at all pushes a Dirac measure onto a measure that is not itself a Dirac measure: a map carries its own a.e. measurability along with the law it is claimed to have.

theorem ProbabilityTheory.HasLaw.mapsTo_support_of_continuousOn {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {T : X → Y} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (h : HasLaw T ν μ) (hμs : ∀ᵐ (x : X) ∂μ, x ∈ s) (hsμ : s ⊆ μ.support) (hT : ContinuousOn T s) : Set.MapsTo T s ν.support

A continuous transport map sends its domain into the support of its law. Let T be continuous on a set s carrying μ and contained in the support of μ. Then T maps all of s, not merely almost all of it, into the support of the law ν of T.

theorem ProbabilityTheory.HasLaw.measure_eq_zero_or_measure_eq_zero_of_continuousOn {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {T : X → Y} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} [OpensMeasurableSpace Y] (h : HasLaw T ν μ) (hs : IsPreconnected s) (hμs : ∀ᵐ (x : X) ∂μ, x ∈ s) (hsμ : s ⊆ μ.support) (hT : ContinuousOn T s) {A B : Set Y} (hA : IsClosed A) (hB : IsClosed B) (hAB : Disjoint A B) (hνAB : ν (A ∪ B)ᶜ = 0) : ν A = 0 ∨ ν B = 0

A continuous map from a connected source cannot split its law. Let T be continuous on a preconnected set s carrying μ and contained in the support of μ. If the law ν of T is carried by the union of two disjoint closed sets, then it does not charge one of them.