OAI/Computability/PerfectCompleteness/Algebra/MatrixErasure.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.MatrixErasure.erase line 17
  2. def OAI.PerfectCompleteness.MatrixErasure.uniformMass line 20
  3. theorem OAI.PerfectCompleteness.MatrixErasure.erase_eq_none_of line 23
  4. theorem OAI.PerfectCompleteness.MatrixErasure.erase_eq_of_not line 27
  5. theorem OAI.PerfectCompleteness.MatrixErasure.erase_eq_some_iff line 31
  6. theorem OAI.PerfectCompleteness.MatrixErasure.indicator_erase_le line 35
  7. theorem OAI.PerfectCompleteness.MatrixErasure.definedEquality_erase line 42
  8. theorem OAI.PerfectCompleteness.MatrixErasure.definedEquality_le_one line 48
  9. theorem OAI.PerfectCompleteness.MatrixErasure.definedEquality_nonneg line 53
  10. theorem OAI.PerfectCompleteness.MatrixErasure.definedEquality_erase_le line 58
  11. theorem OAI.PerfectCompleteness.MatrixErasure.definedEquality_le_erase_add line 65
  12. theorem OAI.PerfectCompleteness.MatrixErasure.uniformMass_nonneg line 72
  13. theorem OAI.PerfectCompleteness.MatrixErasure.expect_add_right line 77
  14. theorem OAI.PerfectCompleteness.MatrixErasure.step_second_marginal line 86
  15. theorem OAI.PerfectCompleteness.MatrixErasure.nonzero_second_marginal line 92
  16. theorem OAI.PerfectCompleteness.MatrixErasure.stepAgreement_erase_bound line 101
  17. theorem OAI.PerfectCompleteness.MatrixErasure.nonzeroAgreement_erase line 120