OAI/Probability/Ballisticity/Estimates/SamplingLaw.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.DirectionalTransience.actualArray_borel line 12
2. lemma OAI.DirectionalTransience.restrict_compProd_fst line 27
3. instance OAI.DirectionalTransience.episodeInputLaw_finite line 46
4. lemma OAI.DirectionalTransience.episodeInputLaw_restrict line 51
5. lemma OAI.DirectionalTransience.actualArray_integrable line 64
6. lemma OAI.DirectionalTransience.actual_array_sampling_sq_law line 74
7. lemma OAI.DirectionalTransience.actual_array_sampling_test_law line 114
8. lemma OAI.DirectionalTransience.arrayOffsetTest_shift line 152
9. lemma OAI.DirectionalTransience.arrayProfileTest_shift line 157
10. lemma OAI.DirectionalTransience.arrayOffsetTest_iterate line 162
11. lemma OAI.DirectionalTransience.arrayProfileTest_iterate line 172
12. lemma OAI.DirectionalTransience.arraySamplingError_iterate line 182