OAI/Probability/SKGap/Matrix/NormalizedRecipeLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Regression.sqrt_sum_smul_unitVector line 111
2. lemma OAI.SKGapCutoff.Regression.completedMatrix_scaled_input line 127
3. theorem OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.unnormalized_query_assembly line 157
4. def OAI.SKGapCutoff.Regression.normalizedRecipeLaw line 251
5. lemma OAI.SKGapCutoff.Regression.normalizedRecipeLaw_probability line 260
6. lemma OAI.SKGapCutoff.Regression.normalizedRecipeLaw_moments line 279
7. theorem OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.nondegenerate_full_query line 342