OAI/Probability/Ballisticity/Estimates/AnchorMoments.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.AnchorSampling.atomError line 14
2. lemma OAI.DirectionalTransience.AnchorSampling.atomMass_mem line 18
3. lemma OAI.DirectionalTransience.AnchorSampling.atomError_bound line 22
4. lemma OAI.DirectionalTransience.AnchorSampling.atomError_integrable line 29
5. lemma OAI.DirectionalTransience.AnchorSampling.integral_atomError line 34
6. lemma OAI.DirectionalTransience.AnchorSampling.pair_sampling_test line 44
7. lemma OAI.DirectionalTransience.AnchorSampling.infinitePi_sampling_test line 56
8. lemma OAI.DirectionalTransience.AnchorSampling.infinitePi_pair_fresh line 66
9. lemma OAI.DirectionalTransience.AnchorSampling.infinitePi_atomError_cross_fresh line 76
10. lemma OAI.DirectionalTransience.AnchorSampling.infinitePi_atomError_cross line 95
11. lemma OAI.DirectionalTransience.AnchorSampling.atomError_eval_measurable line 104
12. lemma OAI.DirectionalTransience.AnchorSampling.atomError_eval_product_integrable line 110
13. theorem OAI.DirectionalTransience.AnchorSampling.infinitePi_sample_sum_sq line 121
14. theorem OAI.DirectionalTransience.AnchorSampling.infinitePi_sample_average_sq line 161