Disintegrating a measure over a countable coordinate #
A measure σ on a product Y × Z disintegrates over Y when it is the composition-product
σ.fst ⊗ₘ κ of its first marginal with a Markov kernel κ : Kernel Y Z. Mathlib supplies such a
kernel when the second factor Z is standard Borel
(MeasureTheory.Measure.condKernel). For a finite σ, this file supplies one in the complementary
regime: when the first factor Y is countable with measurable singletons, and Z is any
nonempty measurable space.
On a countable Y no analytic input is needed — the disintegration is the elementary formula
κ y s = (σ.fst {y})⁻¹ * σ ({y} ×ˢ s), conditioning on the atom {y}. The one point that needs
care is the atoms of zero mass, where that formula reads ∞ * 0 and carries no information: they
are given a default value, and the disintegration still holds there because such an atom carries
no σ-mass to begin with (measure_singleton_prod_eq_zero_of_fst_eq_zero).
Main definitions #
TauCeti.MeasureTheory.countableCondKernel— the conditional kernel of a finite measure onY × Zover a countableY.
Main results #
TauCeti.MeasureTheory.measure_singleton_prod_eq_zero_of_fst_eq_zero— an atom of zero first-marginal mass carries no mass at all: the fact that makes the default value at such an atom harmless;TauCeti.MeasureTheory.countableCondKernel_apply,TauCeti.MeasureTheory.countableCondKernel_apply_of_ne_zeroandTauCeti.MeasureTheory.countableCondKernel_apply_of_eq_zero— the eliminator and the two branches of the construction, made explicit;TauCeti.MeasureTheory.compProd_countableCondKernel— the disintegration,σ.fst ⊗ₘ countableCondKernel σ = σ, registered as aMeasureTheory.Measure.IsCondKernelinstance;TauCeti.MeasureTheory.eq_countableCondKernel_of_ne_zero— every conditional kernel ofσagrees with this one at every atom of positive mass;
The file also contains two private regression examples showing that the contract cannot be strengthened and that its finiteness hypothesis cannot be dropped.
Implementation notes #
The kernel is built with ProbabilityTheory.Kernel.ofFunOfCountable, which upgrades an arbitrary
function on a countable space with measurable singletons to a kernel; the measurability of the
disintegration, the only nontrivial requirement in the standard Borel setting, is free here.
The value at an atom of zero mass is a Dirac measure at Classical.arbitrary Z, hence the
[Nonempty Z] hypothesis. Some choice is forced: a Markov kernel must return a probability
measure at every point of Y, σ prescribes none at a null atom, and on an empty Z no Markov
kernel exists at all, by ProbabilityTheory.Kernel.eq_zero_of_isEmpty_right together with
ProbabilityTheory.Kernel.not_isMarkovKernel_zero. The choice is deliberately not hidden —
countableCondKernel_apply_of_eq_zero names it. A private regression below exhibits two
conditional kernels of one measure that differ at a null atom, so no strengthening of
eq_countableCondKernel_of_ne_zero to all atoms is available.
References #
- Roadmap:
TauCetiRoadmap/DenseGraphLimits/README.md, the design-validation milestone preceding the arbitrary-carrier triangle inequality of Layer 1 — "finite coupling gluing with zero-mass middle atoms explicit". This file is the disintegration half of that gluing; the gluing itself isTauCeti.MeasureTheory.exists_glue_of_countable_middle. - S. Janson, Graphons, cut norm and distance, couplings and rearrangements, NYJM Monographs 4 (2013), Lemma 6.5 and its finite reduction.
An atom of Y whose first-marginal mass vanishes carries no mass in any slice.
This is the fact that makes the default value of countableCondKernel at a null atom harmless:
such an atom contributes nothing to the disintegration, whatever the kernel does there.
The countable-coordinate kernel construction for a measure σ on Y × Z. When σ is
finite, this is its conditional kernel over the first coordinate.
At an atom y of positive first-marginal mass this is the normalised slice
s ↦ (σ.fst {y})⁻¹ * σ ({y} ×ˢ s); at a null atom, where σ prescribes nothing, it is a Dirac
measure. Unlike MeasureTheory.Measure.condKernel, this needs no standard-Borel or other
regularity hypothesis on the nonempty second factor Z.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The two branches of countableCondKernel, before either is evaluated. The pair of branch
lemmas below is the interface to prefer; neither of those mentions the if.
At a null atom the conditional kernel takes its default value. It is a genuine choice, not a
quantity read off σ; see the private uniqueness regression below.
At an atom of positive mass the conditional kernel is the normalised slice.
The disintegration of a measure over a countable coordinate.
Any conditional kernel of σ agrees with countableCondKernel σ at every atom of positive
mass. The restriction to such atoms is sharp, as shown by the first private regression below;
global finiteness is necessary at infinite-mass atoms, as shown by the second.
Regressions #
Two examples that break the contract of countableCondKernel if it is read more strongly than it
is stated. The first shows the conclusion of eq_countableCondKernel_of_ne_zero cannot be
extended to null atoms; the second shows that IsFiniteMeasure σ cannot be dropped. (That
Nonempty Z cannot be dropped either is immediate from Mathlib:
ProbabilityTheory.Kernel.eq_zero_of_isEmpty_right and
ProbabilityTheory.Kernel.not_isMarkovKernel_zero leave no Markov kernel at all on an empty
target.)