OAI/Computability/PerfectCompleteness/Foundations/PartialTableInverse.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.PartialTableInverse.indicator line 20
  2. def OAI.PerfectCompleteness.PartialTableInverse.definedEquality line 23
  3. theorem OAI.PerfectCompleteness.PartialTableInverse.indicator_boolean line 27
  4. theorem OAI.PerfectCompleteness.PartialTableInverse.sum_indicator_sq_le line 32
  5. theorem OAI.PerfectCompleteness.PartialTableInverse.definedEquality_eq_sum line 36
  6. theorem OAI.PerfectCompleteness.PartialTableInverse.definedEquality_le_self line 42
  7. def OAI.PerfectCompleteness.PartialTableInverse.stepAgreement line 58
  8. def OAI.PerfectCompleteness.PartialTableInverse.allAgreement line 61
  9. theorem OAI.PerfectCompleteness.PartialTableInverse.uniform_operator_eq_average line 66
  10. theorem OAI.PerfectCompleteness.PartialTableInverse.noiseEnergy_eq_average line 76
  11. theorem OAI.PerfectCompleteness.PartialTableInverse.allAgreement_eq_sum line 84
  12. theorem OAI.PerfectCompleteness.PartialTableInverse.indicator_mass_le_one line 92
  13. theorem OAI.PerfectCompleteness.PartialTableInverse.exists_dense_slice_all line 100
  14. theorem OAI.PerfectCompleteness.PartialTableInverse.stepAgreement_le_zero line 111
  15. def OAI.PerfectCompleteness.PartialTableInverse.nonzeroAgreement line 119
  16. theorem OAI.PerfectCompleteness.PartialTableInverse.nonzeroAgreement_le_all line 124
  17. theorem OAI.PerfectCompleteness.PartialTableInverse.exists_dense_slice_nonzero line 130