OAI/Probability/SKGap/Matrix/CompletedMatrix.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Regression.completedMatrix line 102
2. lemma OAI.SKGapCutoff.Regression.completedMatrix_symmetric line 106
3. lemma OAI.SKGapCutoff.Regression.completedMatrix_answer line 113
4. lemma OAI.SKGapCutoff.Regression.mul_extendFrame line 119
5. lemma OAI.SKGapCutoff.Regression.extendedProjection_mul_old line 127
6. lemma OAI.SKGapCutoff.Regression.old_mul_extendedProjection line 143
7. lemma OAI.SKGapCutoff.Regression.completedMatrix_new_residual line 150
8. theorem OAI.SKGapCutoff.Regression.completedMatrix_update line 171
9. lemma OAI.SKGapCutoff.Regression.completedMatrix_new_compatibility line 182
10. lemma OAI.SKGapCutoff.Regression.completedMatrix_input_decomposition line 191
11. lemma OAI.SKGapCutoff.Regression.measurable_revealedCompletion line 201
12. lemma OAI.SKGapCutoff.Regression.measurable_extendFrame line 212
13. theorem OAI.SKGapCutoff.Regression.completedMatrix_regeneration line 222