OAI/Probability/SKGap/Brownian/ContinuousPosteriorMass.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.GaussianHistory.continuous_posterior_mass line 13
2. lemma OAI.SKGap.GaussianHistory.continuous_posterior_avg line 18
3. lemma OAI.SKGap.GaussianHistory.continuous_posterior_var line 22
4. lemma OAI.SKGap.GaussianHistory.integrable_posterior_var_weight line 27
5. lemma OAI.SKGap.GaussianHistory.posterior_mass_pos line 36
6. lemma OAI.SKGap.GaussianHistory.posterior_energy_bound line 40
7. lemma OAI.SKGap.GaussianHistory.continuous_posterior_cond line 47
8. lemma OAI.SKGap.GaussianHistory.continuous_posterior_energy line 57
9. lemma OAI.SKGap.GaussianHistory.integrable_posterior_energy_weight line 66
10. theorem OAI.SKGap.GaussianHistory.energy_history_bound line 76
11. lemma OAI.SKGap.GaussianHistory.squarePrior_density line 91
12. lemma OAI.SKGap.GaussianHistory.posterior_square_pos line 103
13. lemma OAI.SKGap.GaussianHistory.squarePrior_posterior line 109
14. lemma OAI.SKGap.GaussianHistory.weighted_energy_identity line 121
15. lemma OAI.SKGap.GaussianHistory.mean_difference_square_le line 129