OAI/Probability/ProjectionMoments/Seeded.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NoiselessRegression.FiniteKernelLearner.Realizer.uniform_event_law line 17
2. lemma OAI.NoiselessRegression.FiniteKernelLearner.Realizer.uniformSuccess_eq line 42
3. lemma OAI.NoiselessRegression.FiniteKernelLearner.Realizer.uniformFixedSuccess_eq line 47
4. lemma OAI.NoiselessRegression.FiniteKernelLearner.jointExperimentLaw_congr line 53
5. lemma OAI.NoiselessRegression.FiniteKernelLearner.exists_borel_same_joint line 76
6. theorem OAI.NoiselessRegression.FiniteKernelLearner.exists_equivalent_tape line 92
7. lemma OAI.NoiselessRegression.FiniteKernelLearner.seed_average_bound line 118
8. lemma OAI.NoiselessRegression.FiniteKernelLearner.exists_successful_seed line 125
9. theorem OAI.NoiselessRegression.FiniteKernelLearner.riesz_success line 140
10. theorem OAI.NoiselessRegression.FiniteKernelLearner.haar_success line 159
11. theorem OAI.NoiselessRegression.FiniteKernelLearner.cap_fixed_stop line 178
12. theorem OAI.NoiselessRegression.FiniteKernelLearner.fixed_quadratic_memory line 199
13. def OAI.NoiselessRegression.FiniteKernelLearner.SubquadraticMemory line 210
14. theorem OAI.NoiselessRegression.FiniteKernelLearner.subquadratic_memory line 220
15. lemma OAI.NoiselessRegression.fresh_seed_kernel_version line 235