OAI/Computability/PerfectCompleteness/Sampling/GoodRowSampling.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PerfectCompleteness.GoodRowSampling.RowFiber line 26
2. def OAI.PerfectCompleteness.GoodRowSampling.rowFiberEquiv line 29
3. theorem OAI.PerfectCompleteness.GoodRowSampling.rowFiberEquiv_val line 42
4. theorem OAI.PerfectCompleteness.GoodRowSampling.witness_rowFiber_nonempty line 48
5. theorem OAI.PerfectCompleteness.GoodRowSampling.witness_column_probability line 54
6. theorem OAI.PerfectCompleteness.GoodRowSampling.witness_row_probability_pos line 75
7. theorem OAI.PerfectCompleteness.GoodRowSampling.witness_conditional_probability line 88