OAI/Probability/SKGap/Entropy/BoundGood.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Regression.ExponentialConvergence.zero_of_bound_on_good line 97
2. lemma OAI.SKGapCutoff.Regression.matrix_mulVec_sq_bound line 121
3. theorem OAI.SKGapCutoff.Regression.degenerate_matrix_query line 133
4. theorem OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.degenerate_append line 150