2. Calculational proofs🔗

In Mathlib, proofs by calculation whose steps are equalities of kernels are rare. Each of their structural steps is a chain of rewritings, which buries the meaningful steps. Such steps are, e.g., reassociating a composition, marginalizing an output or moving a kernel along a copy. With Kernel-Hom, the structural steps are proved by kernel_disch, in the same way as cat_disch or monoidal proves the easy steps of categorical proofs. Thus, a proof can be written as a calc whose lines are the meaningful rewrites. With measure_kernel, this also holds for calculations on measures built from kernels. On paper, the structural steps are invisible. Indeed, they relate string diagrams that only differ by a deformation of the wires or by the axioms of copy-discard categories.

2.1. Reversibility of data augmentation🔗

We illustrate this with Douc et al. (2018)Marginal noteRandal Douc, Eric Moulines, Pierre Priouret, and Philippe Soulier, 2018. “Markov Chains”. In Springer Series in Operations Research and Financial Engineering., about data augmentation algorithms.

Statement

Let \mathsf{X} and \mathsf{Y} be Polish spaces, equipped with their Borel σ-fields \mathcal{X} and \mathcal{Y}. Let \pi be a probability measure on \mathsf{X} and R a Markov kernel from \mathsf{X} to \mathsf{Y}. By disintegration, there exist a kernel S from \mathsf{Y} to \mathsf{X} and a probability measure \tilde\pi on \mathsf{Y} such that

\pi(\mathrm{d}x)\, R(x, \mathrm{d}y) = S(y, \mathrm{d}x)\, \tilde\pi(\mathrm{d}y). \qquad (2.3.11)

A data augmentation algorithm draws y from R(x, \cdot), then x from S(y, \cdot). Thus, the sequence of the x is a Markov chain with kernel RS(x, A) = \int R(x, \mathrm{d}y)\, S(y, A).

Lemma 2.3.5. The distribution \pi is reversible with respect to the kernel RS, i.e. the measure \pi \otimes RS on \mathsf{X} \times \mathsf{X} is symmetric (Definition 1.5.1):

\forall A, B \in \mathcal{X}, \quad \pi \otimes RS(A \times B) = \pi \otimes RS(B \times A).

Proof. Let A, B \in \mathcal{X}. Using (2.3.11), we have that

\begin{aligned} \pi \otimes RS(A \times B) &= \int \pi(\mathrm{d}x)\, R(x, \mathrm{d}y)\, \mathbb{1}_A(x)\, S(y, B) \\ &= \int S(y, \mathrm{d}x)\, \tilde\pi(\mathrm{d}y)\, \mathbb{1}_A(x)\, S(y, B) \\ &= \int S(y, A)\, S(y, B)\, \tilde\pi(\mathrm{d}y), \end{aligned}

which is symmetric in A and B.

Formalization

In Mathlib, S is the posterior R†π (posterior) and \tilde\pi is R ∘ₘ π. The kernel RS is S ∘ₖ R, and the measure \pi \otimes RS is π ⊗ₘ (S ∘ₖ R). The reversibility IsReversible is defined by the equality of the integrals of RS(\cdot, B) over A and of RS(\cdot, A) over B. The lemma isReversible_of_map_swap derives it from the symmetry of the measure, stated as its invariance by the swap of the coordinates.

/-- Definition 1.5.1 of Douc et al.: if the measure `π ⊗ κ` on `X × X` is symmetric, then `π` is
reversible with respect to `κ`. -/
lemma isReversible_of_map_swap {π : Measure X} [SFinite π] {κ : Kernel X X} [IsSFiniteKernel κ]
    (h : (π ⊗ₘ κ).map Prod.swap = π ⊗ₘ κ) :
    IsReversible κ π := byX:Type u_1inst✝²:MeasurableSpace Xπ:Measure Xinst✝¹:SFinite πκ:Kernel X Xinst✝:IsSFiniteKernel κh:Measure.map Prod.swap (π ⊗ₘ κ) = π ⊗ₘ κ⊢ κ.IsReversible π
  intro A B hA hBX:Type u_1inst✝²:MeasurableSpace Xπ:Measure Xinst✝¹:SFinite πκ:Kernel X Xinst✝:IsSFiniteKernel κh:Measure.map Prod.swap (π ⊗ₘ κ) = π ⊗ₘ κA:Set XB:Set XhA:MeasurableSet AhB:MeasurableSet B⊢ ∫⁻ (x : X) in A, (κ x) B ∂π = ∫⁻ (x : X) in B, (κ x) A ∂π
  rw [← Measure.compProd_apply_prod hA hB,X:Type u_1inst✝²:MeasurableSpace Xπ:Measure Xinst✝¹:SFinite πκ:Kernel X Xinst✝:IsSFiniteKernel κh:Measure.map Prod.swap (π ⊗ₘ κ) = π ⊗ₘ κA:Set XB:Set XhA:MeasurableSet AhB:MeasurableSet B⊢ (π ⊗ₘ κ) (A ×ˢ B) = ∫⁻ (x : X) in B, (κ x) A ∂π ← h,X:Type u_1inst✝²:MeasurableSpace Xπ:Measure Xinst✝¹:SFinite πκ:Kernel X Xinst✝:IsSFiniteKernel κh:Measure.map Prod.swap (π ⊗ₘ κ) = π ⊗ₘ κA:Set XB:Set XhA:MeasurableSet AhB:MeasurableSet B⊢ (Measure.map Prod.swap (π ⊗ₘ κ)) (A ×ˢ B) = ∫⁻ (x : X) in B, (κ x) A ∂π Measure.map_apply measurable_swap (hA.prod hB),X:Type u_1inst✝²:MeasurableSpace Xπ:Measure Xinst✝¹:SFinite πκ:Kernel X Xinst✝:IsSFiniteKernel κh:Measure.map Prod.swap (π ⊗ₘ κ) = π ⊗ₘ κA:Set XB:Set XhA:MeasurableSet AhB:MeasurableSet B⊢ (π ⊗ₘ κ) (Prod.swap ⁻¹' A ×ˢ B) = ∫⁻ (x : X) in B, (κ x) A ∂π
    Set.preimage_swap_prod,X:Type u_1inst✝²:MeasurableSpace Xπ:Measure Xinst✝¹:SFinite πκ:Kernel X Xinst✝:IsSFiniteKernel κh:Measure.map Prod.swap (π ⊗ₘ κ) = π ⊗ₘ κA:Set XB:Set XhA:MeasurableSet AhB:MeasurableSet B⊢ (π ⊗ₘ κ) (B ×ˢ A) = ∫⁻ (x : X) in B, (κ x) A ∂π Measure.compProd_apply_prod hB hAX:Type u_1inst✝²:MeasurableSpace Xπ:Measure Xinst✝¹:SFinite πκ:Kernel X Xinst✝:IsSFiniteKernel κh:Measure.map Prod.swap (π ⊗ₘ κ) = π ⊗ₘ κA:Set XB:Set XhA:MeasurableSet AhB:MeasurableSet B⊢ ∫⁻ (a : X) in B, (κ a) A ∂π = ∫⁻ (x : X) in B, (κ x) A ∂π]All goals completed! 🐙

/-- Lemma 2.3.5 of Douc et al.: the distribution `π` is reversible with respect to the kernel `RS`,
where `S = R†π`. -/
theorem isReversible_comp [StandardBorelSpace X] [Nonempty X] (π : Measure X)
    [IsProbabilityMeasure π] (R : Kernel X Y) [IsMarkovKernel R] :
    IsReversible ((R†π) ∘ₖ R) π := byX:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel R⊢ (R†π ∘ₖ R).IsReversible π
  -- By Definition 1.5.1, the measure `π ⊗ RS` on `X × X` must be symmetric.
  apply isReversible_of_map_swapX:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel R⊢ Measure.map Prod.swap (π ⊗ₘ (R†π ∘ₖ R)) = π ⊗ₘ (R†π ∘ₖ R)
  -- Equation (2.3.11) of the book: `π(dx) R(x, dy) = S(y, dx) π̃(dy)`.
  have h : π ⊗ₘ R = swap Y X ∘ₘ ((R ∘ₘ π) ⊗ₘ R†π) := byX:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel R⊢ (R†π ∘ₖ R).IsReversible π
    rw [compProd_posterior_eq_swap_compX:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel R⊢ π ⊗ₘ R = ⇑(swap Y X) ∘ₘ ⇑(swap X Y) ∘ₘ π ⊗ₘ R]X:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel R⊢ π ⊗ₘ R = ⇑(swap Y X) ∘ₘ ⇑(swap X Y) ∘ₘ π ⊗ₘ R
    measure_kernelX:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel R⊢ Kernel.id ×ₖ R ∘ₖ const Unit π = swap Y X ∘ₖ (swap X Y ∘ₖ (Kernel.id ×ₖ R ∘ₖ const Unit π))
    kernel_dischX:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel Rh:π ⊗ₘ R = ⇑(swap Y X) ∘ₘ (⇑R ∘ₘ π) ⊗ₘ R†π⊢ Measure.map Prod.swap (π ⊗ₘ (R†π ∘ₖ R)) = π ⊗ₘ (R†π ∘ₖ R)
  -- The computation of the book: `π ⊗ RS = ∫ S(y, ·) ⊗ S(y, ·) π̃(dy)`.
  have key : π ⊗ₘ ((R†π) ∘ₖ R) = ((R†π) ×ₖ (R†π)) ∘ₘ (R ∘ₘ π) := byX:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel R⊢ (R†π ∘ₖ R).IsReversible π
    calc π ⊗ₘ ((R†π) ∘ₖ R)
    _ = (Kernel.id ∥ₖ R†π) ∘ₘ (π ⊗ₘ R) := byX:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel Rh:π ⊗ₘ R = ⇑(swap Y X) ∘ₘ (⇑R ∘ₘ π) ⊗ₘ R†π⊢ π ⊗ₘ (R†π ∘ₖ R) = ⇑(Kernel.id ∥ₖ R†π) ∘ₘ π ⊗ₘ R measure_kernelX:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel Rh:π ⊗ₘ R = ⇑(swap Y X) ∘ₘ (⇑R ∘ₘ π) ⊗ₘ R†π⊢ Kernel.id ×ₖ (R†π ∘ₖ R) ∘ₖ const Unit π = Kernel.id ∥ₖ R†π ∘ₖ (Kernel.id ×ₖ R ∘ₖ const Unit π); kernel_dischAll goals completed! 🐙
    _ = (Kernel.id ∥ₖ R†π) ∘ₘ (swap Y X ∘ₘ ((R ∘ₘ π) ⊗ₘ R†π)) := byX:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel Rh:π ⊗ₘ R = ⇑(swap Y X) ∘ₘ (⇑R ∘ₘ π) ⊗ₘ R†π⊢ ⇑(Kernel.id ∥ₖ R†π) ∘ₘ π ⊗ₘ R = ⇑(Kernel.id ∥ₖ R†π) ∘ₘ ⇑(swap Y X) ∘ₘ (⇑R ∘ₘ π) ⊗ₘ R†π rw [hX:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel Rh:π ⊗ₘ R = ⇑(swap Y X) ∘ₘ (⇑R ∘ₘ π) ⊗ₘ R†π⊢ ⇑(Kernel.id ∥ₖ R†π) ∘ₘ ⇑(swap Y X) ∘ₘ (⇑R ∘ₘ π) ⊗ₘ R†π = ⇑(Kernel.id ∥ₖ R†π) ∘ₘ ⇑(swap Y X) ∘ₘ (⇑R ∘ₘ π) ⊗ₘ R†π]All goals completed! 🐙
    _ = ((R†π) ×ₖ (R†π)) ∘ₘ (R ∘ₘ π) := byX:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel Rh:π ⊗ₘ R = ⇑(swap Y X) ∘ₘ (⇑R ∘ₘ π) ⊗ₘ R†π⊢ ⇑(Kernel.id ∥ₖ R†π) ∘ₘ ⇑(swap Y X) ∘ₘ (⇑R ∘ₘ π) ⊗ₘ R†π = ⇑(R†π ×ₖ R†π) ∘ₘ ⇑R ∘ₘ π measure_kernelX:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel Rh:π ⊗ₘ R = ⇑(swap Y X) ∘ₘ (⇑R ∘ₘ π) ⊗ₘ R†π⊢ Kernel.id ∥ₖ R†π ∘ₖ (swap Y X ∘ₖ (Kernel.id ×ₖ R†π ∘ₖ (R ∘ₖ const Unit π))) = R†π ×ₖ R†π ∘ₖ (R ∘ₖ const Unit π); kernel_dischX:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel Rh:π ⊗ₘ R = ⇑(swap Y X) ∘ₘ (⇑R ∘ₘ π) ⊗ₘ R†πkey:π ⊗ₘ (R†π ∘ₖ R) = ⇑(R†π ×ₖ R†π) ∘ₘ ⇑R ∘ₘ π⊢ Measure.map Prod.swap (π ⊗ₘ (R†π ∘ₖ R)) = π ⊗ₘ (R†π ∘ₖ R)
  -- This measure is symmetric.
  rw [← Measure.swap_comp,X:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel Rh:π ⊗ₘ R = ⇑(swap Y X) ∘ₘ (⇑R ∘ₘ π) ⊗ₘ R†πkey:π ⊗ₘ (R†π ∘ₖ R) = ⇑(R†π ×ₖ R†π) ∘ₘ ⇑R ∘ₘ π⊢ ⇑(swap X X) ∘ₘ π ⊗ₘ (R†π ∘ₖ R) = π ⊗ₘ (R†π ∘ₖ R) keyX:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel Rh:π ⊗ₘ R = ⇑(swap Y X) ∘ₘ (⇑R ∘ₘ π) ⊗ₘ R†πkey:π ⊗ₘ (R†π ∘ₖ R) = ⇑(R†π ×ₖ R†π) ∘ₘ ⇑R ∘ₘ π⊢ ⇑(swap X X) ∘ₘ ⇑(R†π ×ₖ R†π) ∘ₘ ⇑R ∘ₘ π = ⇑(R†π ×ₖ R†π) ∘ₘ ⇑R ∘ₘ π]X:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel Rh:π ⊗ₘ R = ⇑(swap Y X) ∘ₘ (⇑R ∘ₘ π) ⊗ₘ R†πkey:π ⊗ₘ (R†π ∘ₖ R) = ⇑(R†π ×ₖ R†π) ∘ₘ ⇑R ∘ₘ π⊢ ⇑(swap X X) ∘ₘ ⇑(R†π ×ₖ R†π) ∘ₘ ⇑R ∘ₘ π = ⇑(R†π ×ₖ R†π) ∘ₘ ⇑R ∘ₘ π
  measure_kernelX:Type u_1Y:Type u_2inst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Yinst✝³:StandardBorelSpace Xinst✝²:Nonempty Xπ:Measure Xinst✝¹:IsProbabilityMeasure πR:Kernel X Yinst✝:IsMarkovKernel Rh:π ⊗ₘ R = ⇑(swap Y X) ∘ₘ (⇑R ∘ₘ π) ⊗ₘ R†πkey:π ⊗ₘ (R†π ∘ₖ R) = ⇑(R†π ×ₖ R†π) ∘ₘ ⇑R ∘ₘ π⊢ swap X X ∘ₖ (R†π ×ₖ R†π ∘ₖ (R ∘ₖ const Unit π)) = R†π ×ₖ R†π ∘ₖ (R ∘ₖ const Unit π)
  kernel_dischAll goals completed! 🐙

The formal proof has the structure of the proof of the book. The hypothesis h is equation (2.3.11), which follows from compProd_posterior_eq_swap_comp. The calculation key is the computation of the book, and its only meaningful step is the rewrite with h. The symmetry of the right-hand side of key is the cocommutativity of the copy. All the other steps are structural, and are proved by measure_kernel followed by kernel_disch. Without the tactics, the last step of key can be proved with the lemmas of Mathlib by

rw [Measure.compProd_eq_comp_prod, Measure.comp_assoc, Measure.comp_assoc, Kernel.comp_assoc,
  swap_prod, parallelComp_comp_prod, Kernel.id_comp, Kernel.comp_id]

which requires knowing seven lemmas about kernels and measures, and reassociating the compositions by hand so that each rewrite applies.