OAI/Probability/GaussianReplacement/CompletedKernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentProjection.StreamKernel.borelKernel line 27
2. instance OAI.CurrentProjection.StreamKernel.borelKernel_markov line 34
3. lemma OAI.CurrentProjection.StreamKernel.borelKernel_ae line 42
4. abbrev OAI.CurrentProjection.StreamKernel.Coins line 52
5. def OAI.CurrentProjection.StreamKernel.coinLaw line 54
6. instance OAI.CurrentProjection.StreamKernel.coinLaw_probability line 55
7. def OAI.CurrentProjection.StreamKernel.foldCoins line 63
8. lemma OAI.CurrentProjection.StreamKernel.measurable_foldCoins line 67
9. lemma OAI.CurrentProjection.StreamKernel.coinLaw_split line 77
10. lemma OAI.CurrentProjection.StreamKernel.map_freshCoin line 89
11. lemma OAI.CurrentProjection.StreamKernel.map_foldCoins_succ line 124