OAI/Probability/Subsphere/Regression/Blocks.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubsphereRegression.Learner.run_congr_labels line 17
2. lemma OAI.SubsphereRegression.Learner.estimate_congr_labels line 31
3. lemma OAI.SubsphereRegression.Learner.angularSuccess_nullMeasurable line 36
4. lemma OAI.SubsphereRegression.Learner.linear_success_bound line 46
5. def OAI.SubsphereRegression.PolynomialMass line 96
6. def OAI.SubsphereRegression.localNormalize line 99
7. lemma OAI.SubsphereRegression.localNormalize_univ line 103
8. lemma OAI.SubsphereRegression.localNormalize_finite line 113
9. lemma OAI.SubsphereRegression.localNormalize_support line 119
10. lemma OAI.SubsphereRegression.localNormalize_local line 135
11. lemma OAI.SubsphereRegression.replicaConstant_le line 161
12. lemma OAI.SubsphereRegression.projectionLaw_uniform_set_bound line 185
13. lemma OAI.SubsphereRegression.finite_rpow_holder line 208
14. lemma OAI.SubsphereRegression.normalized_routing_bound line 220
15. lemma OAI.SubsphereRegression.localNormalize_reconstruct line 280
16. lemma OAI.SubsphereRegression.projectionLaw_smul line 294
17. lemma OAI.SubsphereRegression.projectionLaw_affine line 299
18. lemma OAI.SubsphereRegression.localized_routing_bound line 309
19. lemma OAI.SubsphereRegression.projectionLaw_withDensity_apply line 339
20. def OAI.SubsphereRegression.blockValue line 358
21. lemma OAI.SubsphereRegression.measurable_finite_select line 362
22. lemma OAI.SubsphereRegression.measurable_blockValue line 372
23. lemma OAI.SubsphereRegression.blockValue_le_one line 381
24. lemma OAI.SubsphereRegression.blockValue_mass_identity line 386
25. lemma OAI.SubsphereRegression.blockValue_mass_bound line 426