OAI/Probability/SKGap/Localization/IntegrableLinearCombinationSq.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Regression.integrable_linear_combination_sq line 84
2. theorem OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.unbounded_linear_energy line 104
3. theorem OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.normalized_unbounded_linear line 128
4. lemma OAI.SKGapCutoff.Regression.revealedCompletion_mulVec line 169
5. lemma OAI.SKGapCutoff.Regression.revealedCompletion_perpendicular line 175
6. lemma OAI.SKGapCutoff.Regression.queryAnswer_mulVec line 180
7. lemma OAI.SKGapCutoff.Regression.completed_query_answer line 188
8. lemma OAI.SKGapCutoff.Regression.scaled_query_predictor line 196
9. def OAI.SKGapCutoff.Regression.extendFrame line 211
10. lemma OAI.SKGapCutoff.Regression.extendFrame_zero line 214
11. lemma OAI.SKGapCutoff.Regression.extendFrame_succ line 217
12. lemma OAI.SKGapCutoff.Regression.extendFrame_orthonormal line 220
13. lemma OAI.SKGapCutoff.Regression.extendFrame_projection line 244