OAI/Probability/Ballisticity/Walk/Kernel.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TailDecorrelation.randomization_projection_preserving line 18
2. lemma OAI.TailDecorrelation.randomized_density line 24
3. lemma OAI.TailDecorrelation.measurableSet_eventually_nat line 51
4. lemma OAI.TailDecorrelation.integral_comp_preserving line 64
5. lemma OAI.TailDecorrelation.swap_seed_preserving line 75
6. lemma OAI.TailDecorrelation.sampled_kernel_integral line 82
7. lemma OAI.TailDecorrelation.sampled_kernel_integrable line 114
8. lemma OAI.TailDecorrelation.kernel_escape_sampled line 143
9. lemma OAI.TailDecorrelation.kernel_density_integrable line 177
10. lemma OAI.TailDecorrelation.kernel_entropy_decorrelation line 199