Recover the joint measure from its first marginal and a conditional law

AutoSamplingTheory.TechnicalLemmas.Probability.ConditionalResampling.fst_compProd_condDistrib_snd_eq_self · theorem · Teaching coverage

Statement

Let α be an arbitrary measurable space and β a nonempty Standard Borel measurable space. For every finite measure μ on α × β, combine its first marginal with the selected regular conditional distribution of its second coordinate given its first. The resulting joint measure is exactly μ. This is equality of measures, including when μ is zero, not a claim that every conditional fiber has a canonical pointwise law.

All objects and hypotheses

• {α β : Type*} — Two possibly universe-polymorphic coordinate types α and β.
• [MeasurableSpace α] [MeasurableSpace β] — Both carry measurable-space structures; α × β has the product sigma-algebra.
• [StandardBorelSpace β] — The resampled space β is Standard Borel, supplying the regular-conditional-distribution existence contract.
• [Nonempty β] — β is nonempty, so the selected conditional kernel can be totalized as a probability law even on marginal-null fibers.
• {μ : Measure (α × β)} [IsFiniteMeasure μ] — μ is any finite joint measure. It need not be normalized and may be zero. α need not be Standard Borel or nonempty.

Notation and interpretation

m

The first marginal, represented by μ.map Prod.fst.

\[m=(\operatorname{fst})_\#\mu\]

q

The particular regular conditional probability kernel selected by Mathlib, not a pointwise unique conditional density.

\[q(a)=\operatorname{condDistrib}(\operatorname{snd}\mid\operatorname{fst};\mu)(a)\]

μ ⊗ₘ q

Composition-product of a measure and a kernel, for measurable A ⊆ α × β. It is a joint measure, unlike ordinary kernel composition which forgets the intermediate state.

\[(m\otimes_m q)(A)=\int_\alpha q(a,\{b:(a,b)\in A\})\,m(da)\]

K ∘ₘ μ

The measure after one kernel application. Invariant means exactly K ∘ₘ μ = μ.

\[(K\circ_m\mu)(A)=\int K(x,A)\,\mu(dx)\]

• All sets used to test equality of measures are measurable unless explicitly stated otherwise.
• All measure values, reciprocals and scalar multiplications in the Lean conditional formula are in ℝ≥0∞. Integral displays of kernel probabilities denote nonnegative extended integrals, not Bochner integrals with unstated integrability hypotheses.
• The notation r_i, F_i, e_i, q_i and K_i in the teaching text is explanatory mathematical shorthand, not new public Lean definitions.
• Markovness quantifies over every input; a selected conditional version's law characterization is only marginal-a.e. unless a positive-atom/fiber theorem applies.
• Finite target mass is not probability normalization. Fin (n+1) counts sites, not states. No law is assumed to have a density.

Mathematical proof

theorem fst_compProd_condDistrib_snd_eq_self
    {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    [StandardBorelSpace β] [Nonempty β]
    {μ : Measure (α × β)} [IsFiniteMeasure μ] :
    (μ.map Prod.fst) ⊗ₘ
        ProbabilityTheory.condDistrib Prod.snd Prod.fst μ = μ

theorem fst_compProd_condDistrib_snd_eq_self
    {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    [StandardBorelSpace β] [Nonempty β]
    {μ : Measure (α × β)} [IsFiniteMeasure μ] :
    (μ.map Prod.fst) ⊗ₘ
        ProbabilityTheory.condDistrib Prod.snd Prod.fst μ = μ := by
  have h := ProbabilityTheory.compProd_map_condDistrib
    (μ := μ) (X := Prod.fst) (Y := Prod.snd) (mβ := inferInstance)
    measurable_snd.aemeasurable
  simpa using h

end ConditionalResampling
end Probability
end TechnicalLemmas
end AutoSamplingTheory

Scope and omitted-condition boundaries

• These are existing source-neutral measure/kernel interfaces, not newly proved claims in this research packet. Reading source and historical tests is not a fresh Lean build or independent verification.
• Finite target measure means μ(univ) < ∞, not μ(univ) = 1; zero and finite unnormalized targets are allowed unless a positive-fiber hypothesis rules them out.
• A selected regular conditional distribution is a probability kernel at every conditioning value. Its conditional-law characterization is determined only almost everywhere under the conditioning marginal; null fibers have no asserted feasible/Gibbs-support property.
• No reversibility, irreducibility, ergodicity, convergence from a different initial law, mixing rate, random scan, scan-order correctness, executable conditional sampling or cost bound follows from these declarations alone.