OAI/Probability/SKGap/Entropy/RegeneratedNormalizedQuery.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.regenerated_normalized_query line 116
2. theorem OAI.SKGapCutoff.Regression.ExponentialEmpiricalConcentration.regenerated_nondegenerate_step line 177
3. lemma OAI.SKGapCutoff.Regression.measurable_extendFrame_comp line 277
4. lemma OAI.SKGapCutoff.Regression.extended_normalized_columns_bound line 288
5. theorem OAI.SKGapCutoff.Regression.regenerated_good_history line 295