OAI/Computability/PerfectCompleteness/Decoding/FixedUpperPairErrorLemmas.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.FixedUpperPairError.lower_errors_lt line 21
  2. theorem OAI.PerfectCompleteness.FixedUpperPairError.three_errors_lt line 38
  3. theorem OAI.PerfectCompleteness.FixedUpperCutTriangle.rows_positive line 81
  4. def OAI.PerfectCompleteness.FixedUpperCutTriangle.upperReferenceLaw line 95
  5. def OAI.PerfectCompleteness.FixedUpperCutTriangle.modifiedPairLaw line 112
  6. def OAI.PerfectCompleteness.FixedUpperCutTriangle.originalReferenceLaw line 120
  7. theorem OAI.PerfectCompleteness.FixedUpperCutTriangle.modified_reference_lt line 126
  8. theorem OAI.PerfectCompleteness.FixedUpperCutTriangle.original_reference_lt line 143
  9. theorem OAI.PerfectCompleteness.FixedUpperCutTriangle.original_reference_le_ten line 158
  10. abbrev OAI.PerfectCompleteness.FixedUpperCutFamily.Record line 198
  11. def OAI.PerfectCompleteness.FixedUpperCutFamily.modifiedLaw line 212
  12. def OAI.PerfectCompleteness.FixedUpperCutFamily.referenceLaw line 218
  13. theorem OAI.PerfectCompleteness.FixedUpperCutFamily.totalVariation_le_six line 224
  14. theorem OAI.PerfectCompleteness.FixedUpperCutFamily.observed_totalVariation_le_ten line 240