Editing De Finetti's theorem (section)

== As a categorical limit == 

De Finetti's theorem can be expressed as a [[limit (category theory)|categorical limit]] in the [[category of Markov kernels]].<ref>{{cite conference | last1 = Jacobs | first1 = Bart | last2 = Staton | first2 = Sam | title = De Finetti's theorem as a categorical limit | book-title = CMCS '20: Proceedings of the 15th IFIP WG 1.3 International Workshop of Coalgebraic Methods in Computer Science | date = 2020 | arxiv = 2003.01964| url = https://link.springer.com/book/10.1007/978-3-030-57201-3}}</ref><ref name="fritz">{{cite journal | first1=Tobias | last1=Fritz | first2=Tomáš | last2=Gonda | first3=Paolo | last3=Perrone | title=De Finetti's theorem in categorical probability | journal=Journal of Stochastic Analysis | volume=2 | issue=4 | year=2021 | doi=10.31390/josa.2.4.06 | url=https://repository.lsu.edu/josa/vol2/iss4/6/ | arxiv=2105.02639}}</ref><ref>{{cite conference | last1 = Moss | first1 = Sean | last2 = Perrone | first2 = Paolo | title = Probability monads with submonads of deterministic states | book-title = LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science | date = 2022 | doi = 10.1145/3531130.3533355 | arxiv = 2204.07003 | url = https://dl.acm.org/doi/10.1145/3531130.3533355}}</ref>

Let <math>(X,\mathcal{A})</math> be a [[standard Borel space]], and consider the space of sequences on <math>X</math>, the countable product <math>X^\mathbb{N}</math> (equipped with the [[product sigma-algebra]]).

Given a finite [[permutation]] <math>\sigma</math>, denote again by <math>\sigma</math> the permutation action on <math>X^\mathbb{N}</math>, as well as the [[Markov kernel]] <math>X^\mathbb{N}\to X^\mathbb{N}</math> induced by it. 
In terms of [[category theory]], we have a [[diagram (category theory)|diagram]] with a single object, <math>X^\mathbb{N}</math>, and a countable number of arrows, one for each permutation.

Recall now that a [[probability measure]] <math>p</math> is equivalently a [[Markov kernel]] from the one-point measurable space. 
A [[probability measure]] <math>p</math> on <math>X^\mathbb{N}</math> is [[exchangeability|exchangeable]] if and only if, as Markov kernels, <math>\sigma\circ p=p</math> for every permutation <math>\sigma</math>.
More generally, given any standard Borel space <math>Y</math>, one can call a Markov kernel <math>k:Y\to X</math> ''exchangeable'' if <math>\sigma\circ k=k</math> for every <math>\sigma</math>, i.e. if the following diagram commutes,

[[File:Definetti-cone.svg|center]]

giving a [[cone (category theory)|cone]].

De Finetti's theorem can be now stated as the fact that the space <math>PX</math> of [[probability measures]] over <math>X</math> ([[Giry monad]]) forms a [[universal property|universal]] (or [[limit (category theory)|limit]]) cone.<ref name="fritz"/>
More in detail, consider the Markov kernel <math>\mathrm{iid}_\mathbb{N}:PX\to X^\mathbb{N}</math> constructed as follows, using the [[Kolmogorov extension theorem]]:
:<math>
\mathrm{iid}_\mathbb{N}(A_1\times\dots\times A_n\times X\times\dots|p) = p(A_1)\cdots p(A_n)
</math>
for all measurable subsets <math>A_1,\dots,A_n</math> of <math>X</math>.
Note that we can interpret this kernel as taking a probability measure <math>p\in PX</math> as input and returning an [[Independent and identically distributed random variables|iid sequence]] on <math>X^\mathbb{N}</math> distributed according to <math>p</math>. Since iid sequences are exchangeable, <math>\mathrm{iid}_\mathbb{N}:PX\to X^\mathbb{N}</math> is an exchangeable kernel in the sense defined above.
The kernel <math>\mathrm{iid}_\mathbb{N}:PX\to X^\mathbb{N}</math> doesn't just form a cone, but a [[limit (category theory)|limit]] cone: given any exchangeable kernel <math>k:Y\to X</math>, there exists a unique kernel <math>\tilde{k}:Y\to PX</math> such that <math>k=\mathrm{iid}_\mathbb{N}\circ\tilde{k}</math>, i.e. making the following diagram commute:

[[File:Definetti-limit.svg|center]]

In particular, for any exchangeable probability measure <math>p</math> on <math>X^\mathbb{N}</math>, there exists a unique probability measure <math>\tilde{p}</math> on <math>PX</math> (i.e. a probability measure over probability measures) such that <math>p=\mathrm{iid}_\mathbb{N}\circ\tilde{p}</math>, i.e. such that for all measurable subsets <math>A_1,\dots,A_n</math> of <math>X</math>,
:<math>
p(A_1\times\dots\times A_n\times X\times\dots) = \int_{PX} \mathrm{iid}_\mathbb{N}(A_1\times\dots\times A_n\times X\times\dots|q) \, \tilde{p}(dq) = \int_{PX} q(A_1)\cdots q(A_n) \, \tilde{p}(dq) .
</math>
In other words, <math>p</math> is a [[compound distribution|mixture]] of [[Independent and identically distributed random variables|iid measures]] on <math>X</math> (the ones formed by <math>q</math> in the integral above).