OAI/Probability/PosteriorReplicas/Gaussian/ConstrainedNoise.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PosteriorReplicas.gaussianResidualRows line 15
2. instance OAI.PosteriorReplicas.(instance at line 18) line 18
3. lemma OAI.PosteriorReplicas.pairings_lift_residual line 25
4. lemma OAI.PosteriorReplicas.constrained_gaussian_weighted_integral line 35
5. lemma OAI.PosteriorReplicas.constrained_gaussian_noise_integral line 63
6. lemma OAI.PosteriorReplicas.constrained_gaussian_noise_limit line 88
7. lemma OAI.PosteriorReplicas.constrained_gaussian_noise_bound line 102