OAI/Probability/Subsphere/Regression/Precision.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubsphereRegression.measurePreserving_pi_prefix line 20
2. lemma OAI.SubsphereRegression.sphere_sample_observation_quasi line 30
3. lemma OAI.SubsphereRegression.streamRoute_congr line 42
4. lemma OAI.SubsphereRegression.prefix_route_cap_bound line 52
5. lemma OAI.SubsphereRegression.Learner.frozen_success_bound line 80
6. lemma OAI.SubsphereRegression.Learner.streaming_success_bound line 128
7. lemma OAI.SubsphereRegression.Learner.streaming_success_bound_real line 163
8. lemma OAI.SubsphereRegression.precision_from_stream_bound line 188
9. theorem OAI.SubsphereRegression.fixed_quadratic_memory line 268
10. lemma OAI.SubsphereRegression.prod_null_set_lower_bound line 291
11. lemma OAI.SubsphereRegression.Learner.uniformSuccess_of_pointwise line 312
12. theorem OAI.SubsphereRegression.subquadratic_memory line 324

    Source documentation

    The constant is fixed before the memory sequence; only the dimension threshold depends on its little-o convergence.

    theorem subquadratic_memory : SubquadraticMemory.{u} := by
    …

13. theorem OAI.SubsphereRegression.main line 341