OAI/Probability/PosteriorReplicas/Regression/ProjectionBlocks.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PosteriorRegression.PolynomialMass line 17
2. def OAI.PosteriorRegression.localNormalize line 20
3. lemma OAI.PosteriorRegression.localNormalize_univ line 24
4. lemma OAI.PosteriorRegression.localNormalize_finite line 34
5. lemma OAI.PosteriorRegression.localNormalize_support line 40
6. lemma OAI.PosteriorRegression.localNormalize_local line 56
7. lemma OAI.PosteriorRegression.replicaConstant_le line 82
8. lemma OAI.PosteriorRegression.projectionLaw_uniform_set_bound line 106
9. lemma OAI.PosteriorRegression.finite_rpow_holder line 129
10. lemma OAI.PosteriorRegression.normalized_routing_bound line 141
11. lemma OAI.PosteriorRegression.localNormalize_reconstruct line 201
12. lemma OAI.PosteriorRegression.projectionLaw_smul line 214
13. lemma OAI.PosteriorRegression.projectionLaw_affine line 219
14. lemma OAI.PosteriorRegression.localized_routing_bound line 229
15. lemma OAI.PosteriorRegression.projectionLaw_withDensity_apply line 259
16. def OAI.PosteriorRegression.blockValue line 278
17. lemma OAI.PosteriorRegression.measurable_finite_select line 282
18. lemma OAI.PosteriorRegression.measurable_blockValue line 292
19. lemma OAI.PosteriorRegression.blockValue_le_one line 301
20. lemma OAI.PosteriorRegression.blockValue_mass_identity line 306
21. lemma OAI.PosteriorRegression.blockValue_mass_bound line 346