OAI/Probability/SKGap/Localization/RegeneratedAnswer.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Regression.extendFrame_compatible line 113
2. lemma OAI.SKGapCutoff.Regression.queryInnovation_perpendicular line 129
3. lemma OAI.SKGapCutoff.Regression.regenerated_frame_compatible line 152
4. lemma OAI.SKGapCutoff.Regression.measurable_completedMatrix_comp line 161
5. lemma OAI.SKGapCutoff.Regression.measurable_matrix_mulVec_comp line 175
6. def OAI.SKGapCutoff.Regression.regeneratedAnswer line 184
7. lemma OAI.SKGapCutoff.Regression.measurable_regeneratedAnswer_comp line 188
8. lemma OAI.SKGapCutoff.Regression.regeneration_event_le line 203
9. theorem OAI.SKGapCutoff.Regression.regenerated_exponentiallyRare line 264