OAI/Probability/Ballisticity/Estimates/SamplingLimit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DirectionalTransience.Sampling.ae_tendsto_zero_of_sq_integrals line 14
2. lemma OAI.DirectionalTransience.Sampling.sq_integral_bound_of_weak_limit line 37
3. theorem OAI.DirectionalTransience.Sampling.ae_sampling_of_weak_limit line 46
4. lemma OAI.DirectionalTransience.Sampling.cutoff_tendsto line 71
5. theorem OAI.DirectionalTransience.Sampling.ae_zero_of_sampling_tests line 84
6. theorem OAI.DirectionalTransience.Sampling.sampling_tests_weak_limit line 135