OAI/Probability/PosteriorReplicas/Gaussian/ObservableGaussian.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorReplicas.gaussianRows_split line 10
2. lemma OAI.PosteriorReplicas.pairingColumns_split line 35
3. lemma OAI.PosteriorReplicas.rowMix_pairing line 47
4. lemma OAI.PosteriorReplicas.rowMix_split_cancel line 52
5. lemma OAI.PosteriorReplicas.observable_gaussian_lintegral line 77