2. Calculational proofs
Proofs by calculation on kernels are rare in Mathlib: each step, such as reassociating a composition, marginalizing with Kernel.discard, or moving a kernel along Kernel.copy, needs its own lemma or a computation with integrals. With Kernel-Hom, these steps are closed by kernel_disch, in the same way as cat_disch closes easy steps of categorical proofs.
A proof can therefore be written as a calc whose lines are the mathematically meaningful rewrites, typically by hypotheses. To apply a rewrite, the kernels are first arranged so that the hypothesis appears, and the remaining equality only differs by the structure of the kernels (composition, parallel composition, copy, discard, swap). kernel_disch closes it. Each step of the calculation can moreover be visualized with string diagrams.
2.1. Basu's theorem
As an example, we formalize Theorem 15.8 of (Fritz, 2020)Tobias Fritz, 2020. “A synthetic approach to Markov kernels, conditional independence and theorems
on sufficient statistics”. In Advances in Mathematics., which is the main ingredient of the classical Basu theorem: a complete sufficient statistic is independent of any ancillary statistic, for every value of the parameter. A statistical model is a Markov kernel p : Kernel Θ X, and almost sure equality, sufficiency, completeness and ancillarity are all defined by equalities of kernels:
/-- The kernels `f` and `g` are `p`-almost surely equal (Definition 13.1). -/
def AEEq {Y : Type*} [MeasurableSpace Y] (p : Kernel Θ X) (f g : Kernel X Y) : Prop :=
(f ∥ₖ Kernel.id) ∘ₖ copy X ∘ₖ p = (g ∥ₖ Kernel.id) ∘ₖ copy X ∘ₖ p/-- The statistic `s` is sufficient for the statistical model `p` (Definition 14.3). -/
def IsSufficient (p : Kernel Θ X) (s : Kernel X V) : Prop :=
∃ α : Kernel V X, IsMarkovKernel α ∧
(Kernel.id ∥ₖ s) ∘ₖ copy X ∘ₖ p = (α ∥ₖ Kernel.id) ∘ₖ copy V ∘ₖ s ∘ₖ p/-- The kernel `f` is complete with respect to kernels with values in `Z` (Definition 15.1, which
quantifies over all `Z`). -/
def IsComplete (f : Kernel Θ X) (Z : Type*) [MeasurableSpace Z] : Prop :=
∀ (g h : Kernel X Z) [IsMarkovKernel g] [IsMarkovKernel h], g ∘ₖ f = h ∘ₖ f → AEEq f g h/-- The statistic `a` is ancillary for the statistical model `p` (Definition 15.7). -/
def IsAncillary (p : Kernel Θ X) (a : Kernel X W) : Prop :=
∃ ψ : Kernel Unit W, IsMarkovKernel ψ ∧ a ∘ₖ p = ψ ∘ₖ discard Θ
The proof consists of two calculations. The first one shows that a ∘ₖ α and ψ ∘ₖ discard V agree after s ∘ₖ p, where α witnesses the sufficiency of s and ψ the ancillarity of a:
/-- The kernels `a ∘ₖ α` and `ψ ∘ₖ discard V` agree after `s ∘ₖ p`, where `α` witnesses the
sufficiency of `s` and `ψ` the ancillarity of `a` (first computation of the proof of
Theorem 15.8). -/
lemma basu_aux
(hα : (Kernel.id ∥ₖ s) ∘ₖ copy X ∘ₖ p = (α ∥ₖ Kernel.id) ∘ₖ copy V ∘ₖ s ∘ₖ p)
(hψ : a ∘ₖ p = ψ ∘ₖ discard Θ) :
(a ∘ₖ α) ∘ₖ (s ∘ₖ p) = (ψ ∘ₖ discard V) ∘ₖ (s ∘ₖ p) := Θ:Type u_1X:Type u_2V:Type u_3W:Type u_4inst✝⁸:MeasurableSpace Θinst✝⁷:MeasurableSpace Xinst✝⁶:MeasurableSpace Vinst✝⁵:MeasurableSpace Wp:Kernel Θ Xs:Kernel X Va:Kernel X Wα:Kernel V Xψ:Kernel Unit Winst✝⁴:IsMarkovKernel pinst✝³:IsMarkovKernel sinst✝²:IsMarkovKernel ainst✝¹:IsMarkovKernel αinst✝:IsMarkovKernel ψhα:Kernel.id ∥ₖ s ∘ₖ copy X ∘ₖ p = α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ s ∘ₖ phψ:a ∘ₖ p = ψ ∘ₖ discard Θ⊢ a ∘ₖ α ∘ₖ (s ∘ₖ p) = ψ ∘ₖ discard V ∘ₖ (s ∘ₖ p)
calc (a ∘ₖ α) ∘ₖ (s ∘ₖ p)
_ = Kernel.id.map Prod.fst ∘ₖ (a ∥ₖ (discard V : Kernel V Unit)) ∘ₖ
((α ∥ₖ Kernel.id) ∘ₖ copy V ∘ₖ s ∘ₖ p) := Θ:Type u_1X:Type u_2V:Type u_3W:Type u_4inst✝⁸:MeasurableSpace Θinst✝⁷:MeasurableSpace Xinst✝⁶:MeasurableSpace Vinst✝⁵:MeasurableSpace Wp:Kernel Θ Xs:Kernel X Va:Kernel X Wα:Kernel V Xψ:Kernel Unit Winst✝⁴:IsMarkovKernel pinst✝³:IsMarkovKernel sinst✝²:IsMarkovKernel ainst✝¹:IsMarkovKernel αinst✝:IsMarkovKernel ψhα:Kernel.id ∥ₖ s ∘ₖ copy X ∘ₖ p = α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ s ∘ₖ phψ:a ∘ₖ p = ψ ∘ₖ discard Θ⊢ a ∘ₖ α ∘ₖ (s ∘ₖ p) = Kernel.id.map Prod.fst ∘ₖ (a ∥ₖ discard V) ∘ₖ (α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ s ∘ₖ p)
All goals completed! 🐙
_ = a ∘ₖ p := Θ:Type u_1X:Type u_2V:Type u_3W:Type u_4inst✝⁸:MeasurableSpace Θinst✝⁷:MeasurableSpace Xinst✝⁶:MeasurableSpace Vinst✝⁵:MeasurableSpace Wp:Kernel Θ Xs:Kernel X Va:Kernel X Wα:Kernel V Xψ:Kernel Unit Winst✝⁴:IsMarkovKernel pinst✝³:IsMarkovKernel sinst✝²:IsMarkovKernel ainst✝¹:IsMarkovKernel αinst✝:IsMarkovKernel ψhα:Kernel.id ∥ₖ s ∘ₖ copy X ∘ₖ p = α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ s ∘ₖ phψ:a ∘ₖ p = ψ ∘ₖ discard Θ⊢ Kernel.id.map Prod.fst ∘ₖ (a ∥ₖ discard V) ∘ₖ (α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ s ∘ₖ p) = a ∘ₖ p
Θ:Type u_1X:Type u_2V:Type u_3W:Type u_4inst✝⁸:MeasurableSpace Θinst✝⁷:MeasurableSpace Xinst✝⁶:MeasurableSpace Vinst✝⁵:MeasurableSpace Wp:Kernel Θ Xs:Kernel X Va:Kernel X Wα:Kernel V Xψ:Kernel Unit Winst✝⁴:IsMarkovKernel pinst✝³:IsMarkovKernel sinst✝²:IsMarkovKernel ainst✝¹:IsMarkovKernel αinst✝:IsMarkovKernel ψhα:Kernel.id ∥ₖ s ∘ₖ copy X ∘ₖ p = α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ s ∘ₖ phψ:a ∘ₖ p = ψ ∘ₖ discard Θ⊢ Kernel.id.map Prod.fst ∘ₖ (a ∥ₖ discard V) ∘ₖ (Kernel.id ∥ₖ s ∘ₖ copy X ∘ₖ p) = a ∘ₖ p
All goals completed! 🐙
_ = (ψ ∘ₖ discard V) ∘ₖ (s ∘ₖ p) := Θ:Type u_1X:Type u_2V:Type u_3W:Type u_4inst✝⁸:MeasurableSpace Θinst✝⁷:MeasurableSpace Xinst✝⁶:MeasurableSpace Vinst✝⁵:MeasurableSpace Wp:Kernel Θ Xs:Kernel X Va:Kernel X Wα:Kernel V Xψ:Kernel Unit Winst✝⁴:IsMarkovKernel pinst✝³:IsMarkovKernel sinst✝²:IsMarkovKernel ainst✝¹:IsMarkovKernel αinst✝:IsMarkovKernel ψhα:Kernel.id ∥ₖ s ∘ₖ copy X ∘ₖ p = α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ s ∘ₖ phψ:a ∘ₖ p = ψ ∘ₖ discard Θ⊢ a ∘ₖ p = ψ ∘ₖ discard V ∘ₖ (s ∘ₖ p)
Θ:Type u_1X:Type u_2V:Type u_3W:Type u_4inst✝⁸:MeasurableSpace Θinst✝⁷:MeasurableSpace Xinst✝⁶:MeasurableSpace Vinst✝⁵:MeasurableSpace Wp:Kernel Θ Xs:Kernel X Va:Kernel X Wα:Kernel V Xψ:Kernel Unit Winst✝⁴:IsMarkovKernel pinst✝³:IsMarkovKernel sinst✝²:IsMarkovKernel ainst✝¹:IsMarkovKernel αinst✝:IsMarkovKernel ψhα:Kernel.id ∥ₖ s ∘ₖ copy X ∘ₖ p = α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ s ∘ₖ phψ:a ∘ₖ p = ψ ∘ₖ discard Θ⊢ ψ ∘ₖ discard Θ = ψ ∘ₖ discard V ∘ₖ (s ∘ₖ p)
All goals completed! 🐙
The visible rewrites are the sufficiency equation hα and the ancillarity equation hψ. The first line marginalizes the right-hand side of the sufficiency equation, so that hα can be applied. After each rewrite, kernel_disch proves the remaining equality.
The second calculation uses the completeness of s ∘ₖ p on the first one:
/-- **Theorem 15.8** of Fritz: if `s` is a sufficient statistic such that `s ∘ₖ p` is complete, and
`a` is ancillary, then for every value of the parameter, the joint distribution of `s` and `a` is
the product of their distributions. The kernel `a` does not need to be deterministic. -/
theorem basu {p : Kernel Θ X} [IsMarkovKernel p] {s : Kernel X V} [IsMarkovKernel s]
{a : Kernel X W} [IsMarkovKernel a] (hs : IsSufficient p s) (hc : IsComplete (s ∘ₖ p) W)
(ha : IsAncillary p a) : (s ∥ₖ a) ∘ₖ copy X ∘ₖ p = (s ∘ₖ p) ×ₖ (a ∘ₖ p) := Θ:Type u_1X:Type u_2V:Type u_3W:Type u_4inst✝⁶:MeasurableSpace Θinst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Vinst✝³:MeasurableSpace Wp:Kernel Θ Xinst✝²:IsMarkovKernel ps:Kernel X Vinst✝¹:IsMarkovKernel sa:Kernel X Winst✝:IsMarkovKernel ahs:p.IsSufficient shc:(s ∘ₖ p).IsComplete Wha:p.IsAncillary a⊢ s ∥ₖ a ∘ₖ copy X ∘ₖ p = s ∘ₖ p ×ₖ (a ∘ₖ p)
with_panel_widgets [Mathlib.Tactic.Widget.StringDiagram, KernelDiagram]
Θ:Type u_1X:Type u_2V:Type u_3W:Type u_4inst✝⁶:MeasurableSpace Θinst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Vinst✝³:MeasurableSpace Wp:Kernel Θ Xinst✝²:IsMarkovKernel ps:Kernel X Vinst✝¹:IsMarkovKernel sa:Kernel X Winst✝:IsMarkovKernel ahc:(s ∘ₖ p).IsComplete Wha:p.IsAncillary aα:Kernel V Xleft✝:IsMarkovKernel αhα:Kernel.id ∥ₖ s ∘ₖ copy X ∘ₖ p = α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ s ∘ₖ p⊢ s ∥ₖ a ∘ₖ copy X ∘ₖ p = s ∘ₖ p ×ₖ (a ∘ₖ p)
Θ:Type u_1X:Type u_2V:Type u_3W:Type u_4inst✝⁶:MeasurableSpace Θinst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Vinst✝³:MeasurableSpace Wp:Kernel Θ Xinst✝²:IsMarkovKernel ps:Kernel X Vinst✝¹:IsMarkovKernel sa:Kernel X Winst✝:IsMarkovKernel ahc:(s ∘ₖ p).IsComplete Wα:Kernel V Xleft✝¹:IsMarkovKernel αhα:Kernel.id ∥ₖ s ∘ₖ copy X ∘ₖ p = α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ s ∘ₖ pψ:Kernel Unit Wleft✝:IsMarkovKernel ψhψ:a ∘ₖ p = ψ ∘ₖ discard Θ⊢ s ∥ₖ a ∘ₖ copy X ∘ₖ p = s ∘ₖ p ×ₖ (a ∘ₖ p)
Θ:Type u_1X:Type u_2V:Type u_3W:Type u_4inst✝⁶:MeasurableSpace Θinst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Vinst✝³:MeasurableSpace Wp:Kernel Θ Xinst✝²:IsMarkovKernel ps:Kernel X Vinst✝¹:IsMarkovKernel sa:Kernel X Winst✝:IsMarkovKernel ahc:(s ∘ₖ p).IsComplete Wα:Kernel V Xleft✝¹:IsMarkovKernel αhα:Kernel.id ∥ₖ s ∘ₖ copy X ∘ₖ p = α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ s ∘ₖ pψ:Kernel Unit Wleft✝:IsMarkovKernel ψhψ:a ∘ₖ p = ψ ∘ₖ discard Θh:(s ∘ₖ p).AEEq (a ∘ₖ α) (ψ ∘ₖ discard V)⊢ s ∥ₖ a ∘ₖ copy X ∘ₖ p = s ∘ₖ p ×ₖ (a ∘ₖ p)
calc (s ∥ₖ a) ∘ₖ copy X ∘ₖ p
_ = swap W V ∘ₖ ((a ∥ₖ Kernel.id) ∘ₖ ((Kernel.id ∥ₖ s) ∘ₖ copy X ∘ₖ p)) := Θ:Type u_1X:Type u_2V:Type u_3W:Type u_4inst✝⁶:MeasurableSpace Θinst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Vinst✝³:MeasurableSpace Wp:Kernel Θ Xinst✝²:IsMarkovKernel ps:Kernel X Vinst✝¹:IsMarkovKernel sa:Kernel X Winst✝:IsMarkovKernel ahc:(s ∘ₖ p).IsComplete Wα:Kernel V Xleft✝¹:IsMarkovKernel αhα:Kernel.id ∥ₖ s ∘ₖ copy X ∘ₖ p = α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ s ∘ₖ pψ:Kernel Unit Wleft✝:IsMarkovKernel ψhψ:a ∘ₖ p = ψ ∘ₖ discard Θh:(s ∘ₖ p).AEEq (a ∘ₖ α) (ψ ∘ₖ discard V)⊢ s ∥ₖ a ∘ₖ copy X ∘ₖ p = swap W V ∘ₖ (a ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ s ∘ₖ copy X ∘ₖ p))
All goals completed! 🐙
_ = swap W V ∘ₖ (((a ∘ₖ α) ∥ₖ Kernel.id) ∘ₖ copy V ∘ₖ (s ∘ₖ p)) := Θ:Type u_1X:Type u_2V:Type u_3W:Type u_4inst✝⁶:MeasurableSpace Θinst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Vinst✝³:MeasurableSpace Wp:Kernel Θ Xinst✝²:IsMarkovKernel ps:Kernel X Vinst✝¹:IsMarkovKernel sa:Kernel X Winst✝:IsMarkovKernel ahc:(s ∘ₖ p).IsComplete Wα:Kernel V Xleft✝¹:IsMarkovKernel αhα:Kernel.id ∥ₖ s ∘ₖ copy X ∘ₖ p = α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ s ∘ₖ pψ:Kernel Unit Wleft✝:IsMarkovKernel ψhψ:a ∘ₖ p = ψ ∘ₖ discard Θh:(s ∘ₖ p).AEEq (a ∘ₖ α) (ψ ∘ₖ discard V)⊢ swap W V ∘ₖ (a ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ s ∘ₖ copy X ∘ₖ p)) =
swap W V ∘ₖ (a ∘ₖ α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ (s ∘ₖ p))
Θ:Type u_1X:Type u_2V:Type u_3W:Type u_4inst✝⁶:MeasurableSpace Θinst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Vinst✝³:MeasurableSpace Wp:Kernel Θ Xinst✝²:IsMarkovKernel ps:Kernel X Vinst✝¹:IsMarkovKernel sa:Kernel X Winst✝:IsMarkovKernel ahc:(s ∘ₖ p).IsComplete Wα:Kernel V Xleft✝¹:IsMarkovKernel αhα:Kernel.id ∥ₖ s ∘ₖ copy X ∘ₖ p = α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ s ∘ₖ pψ:Kernel Unit Wleft✝:IsMarkovKernel ψhψ:a ∘ₖ p = ψ ∘ₖ discard Θh:(s ∘ₖ p).AEEq (a ∘ₖ α) (ψ ∘ₖ discard V)⊢ swap W V ∘ₖ (a ∥ₖ Kernel.id ∘ₖ (α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ s ∘ₖ p)) =
swap W V ∘ₖ (a ∘ₖ α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ (s ∘ₖ p))
All goals completed! 🐙
_ = swap W V ∘ₖ (((ψ ∘ₖ discard V) ∥ₖ Kernel.id) ∘ₖ copy V ∘ₖ (s ∘ₖ p)) := Θ:Type u_1X:Type u_2V:Type u_3W:Type u_4inst✝⁶:MeasurableSpace Θinst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Vinst✝³:MeasurableSpace Wp:Kernel Θ Xinst✝²:IsMarkovKernel ps:Kernel X Vinst✝¹:IsMarkovKernel sa:Kernel X Winst✝:IsMarkovKernel ahc:(s ∘ₖ p).IsComplete Wα:Kernel V Xleft✝¹:IsMarkovKernel αhα:Kernel.id ∥ₖ s ∘ₖ copy X ∘ₖ p = α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ s ∘ₖ pψ:Kernel Unit Wleft✝:IsMarkovKernel ψhψ:a ∘ₖ p = ψ ∘ₖ discard Θh:(s ∘ₖ p).AEEq (a ∘ₖ α) (ψ ∘ₖ discard V)⊢ swap W V ∘ₖ (a ∘ₖ α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ (s ∘ₖ p)) =
swap W V ∘ₖ (ψ ∘ₖ discard V ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ (s ∘ₖ p))
All goals completed! 🐙
_ = (s ∘ₖ p) ×ₖ (ψ ∘ₖ discard Θ) := Θ:Type u_1X:Type u_2V:Type u_3W:Type u_4inst✝⁶:MeasurableSpace Θinst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Vinst✝³:MeasurableSpace Wp:Kernel Θ Xinst✝²:IsMarkovKernel ps:Kernel X Vinst✝¹:IsMarkovKernel sa:Kernel X Winst✝:IsMarkovKernel ahc:(s ∘ₖ p).IsComplete Wα:Kernel V Xleft✝¹:IsMarkovKernel αhα:Kernel.id ∥ₖ s ∘ₖ copy X ∘ₖ p = α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ s ∘ₖ pψ:Kernel Unit Wleft✝:IsMarkovKernel ψhψ:a ∘ₖ p = ψ ∘ₖ discard Θh:(s ∘ₖ p).AEEq (a ∘ₖ α) (ψ ∘ₖ discard V)⊢ swap W V ∘ₖ (ψ ∘ₖ discard V ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ (s ∘ₖ p)) = s ∘ₖ p ×ₖ (ψ ∘ₖ discard Θ)
All goals completed! 🐙
_ = (s ∘ₖ p) ×ₖ (a ∘ₖ p) := Θ:Type u_1X:Type u_2V:Type u_3W:Type u_4inst✝⁶:MeasurableSpace Θinst✝⁵:MeasurableSpace Xinst✝⁴:MeasurableSpace Vinst✝³:MeasurableSpace Wp:Kernel Θ Xinst✝²:IsMarkovKernel ps:Kernel X Vinst✝¹:IsMarkovKernel sa:Kernel X Winst✝:IsMarkovKernel ahc:(s ∘ₖ p).IsComplete Wα:Kernel V Xleft✝¹:IsMarkovKernel αhα:Kernel.id ∥ₖ s ∘ₖ copy X ∘ₖ p = α ∥ₖ Kernel.id ∘ₖ copy V ∘ₖ s ∘ₖ pψ:Kernel Unit Wleft✝:IsMarkovKernel ψhψ:a ∘ₖ p = ψ ∘ₖ discard Θh:(s ∘ₖ p).AEEq (a ∘ₖ α) (ψ ∘ₖ discard V)⊢ s ∘ₖ p ×ₖ (ψ ∘ₖ discard Θ) = s ∘ₖ p ×ₖ (a ∘ₖ p)
All goals completed! 🐙
The visible rewrites are the sufficiency equation hα, the completeness of s ∘ₖ p (h) and the ancillarity equation hψ. The last calculation step before the ancillarity is the factorization of Theorem 15.8 of (Fritz, 2020)Tobias Fritz, 2020. “A synthetic approach to Markov kernels, conditional independence and theorems
on sufficient statistics”. In Advances in Mathematics., where the joint distribution of s and a is the product of s ∘ₖ p and of the distribution ψ.
2.2. String diagrams of the calculation
Each step of the two calculations is stated as a lemma in KernelHomTests/Basu.lean, so that its string diagrams can be drawn. The diagrams are read from top to bottom.
2.2.1. First calculation
Step 1. Marginalization of the right-hand side of the sufficiency equation.
Step 2. By sufficiency.
Step 3. By ancillarity.
2.2.2. Second calculation
Step 1. Arrangement of the kernels so that the sufficiency equation appears.
Step 2. By sufficiency.
Step 3. By completeness, with the first calculation.
Step 4. The factorization of Theorem 15.8.
Step 5. By ancillarity.