OAI/Probability/SKGap/Matrix/MeasurableCompletedMatrix.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Regression.measurable_completedMatrix line 106
2. lemma OAI.SKGapCutoff.Regression.measurable_revealedCompletion_comp line 117
3. theorem OAI.SKGapCutoff.Regression.completedMatrix_section_law line 131