OAI/Probability/SKGap/Localization/ProdEventSectionLaw.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Regression.prod_event_le_of_section_law line 88
2. lemma OAI.SKGapCutoff.Regression.exponentiallyRare_of_measure_le_add line 118
3. theorem OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.of_section_law line 141
4. theorem OAI.SKGapCutoff.Regression.ExponentialSquareTails.of_section_law line 169
5. def OAI.SKGapCutoff.Regression.unitVector line 203
6. lemma OAI.SKGapCutoff.Regression.unitVector_sq_sum line 206
7. lemma OAI.SKGapCutoff.Regression.unitVector_sq_le line 214
8. lemma OAI.SKGapCutoff.Regression.unitVector_sq_eq line 218
9. lemma OAI.SKGapCutoff.Regression.residualProjection_idem line 222
10. lemma OAI.SKGapCutoff.Regression.normalized_residual_perpendicular line 227
11. lemma OAI.SKGapCutoff.Regression.normalized_residual_fixed line 238
12. lemma OAI.SKGapCutoff.Regression.residual_scaled_predictor line 246
13. lemma OAI.SKGapCutoff.Regression.scaled_unitVector line 264
14. lemma OAI.SKGapCutoff.Regression.measurable_unitVector line 272