OAI/Probability/ProjectionMoments/Asymptotics.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NoiselessRegression.Learner.uniformSuccess_le_sum_fixed line 13
2. theorem OAI.NoiselessRegression.FiniteKernelLearner.cap_total_success line 39
3. lemma OAI.NoiselessRegression.FiniteKernelLearner.seededSuccess_eq_integral_pointwise line 87
4. lemma OAI.NoiselessRegression.FiniteKernelLearner.seededSuccess_of_pointwise line 116
5. theorem OAI.NoiselessRegression.FiniteKernelLearner.subquadratic_memory_with_pointwise line 126
6. lemma OAI.NoiselessRegression.FiniteKernelLearner.cap_memory_factor line 144
7. lemma OAI.NoiselessRegression.FiniteKernelLearner.cap_finite_to_asymptotic line 164
8. theorem OAI.NoiselessRegression.FiniteKernelLearner.cap_fixed_stop_asymptotic line 181
9. lemma OAI.NoiselessRegression.FiniteKernelLearner.cap_ceil_cost line 205
10. lemma OAI.NoiselessRegression.FiniteKernelLearner.cap_accuracy_cost line 226
11. theorem OAI.NoiselessRegression.FiniteKernelLearner.cap_total_success_asymptotic line 239