OAI/Computability/PerfectCompleteness/Decoding/TwoResponseCollisionLemmas.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.TwoResponseCollision.responds line 23
  2. def OAI.PerfectCompleteness.TwoResponseCollision.goodDefined line 26
  3. def OAI.PerfectCompleteness.TwoResponseCollision.collision line 29
  4. def OAI.PerfectCompleteness.TwoResponseCollision.goodCollision line 32
  5. def OAI.PerfectCompleteness.TwoResponseCollision.GoodResponse line 35
  6. def OAI.PerfectCompleteness.TwoResponseCollision.responseMass line 38
  7. theorem OAI.PerfectCompleteness.TwoResponseCollision.goodDefined_weight_eq_sum line 42
  8. theorem OAI.PerfectCompleteness.TwoResponseCollision.goodDefined_probability_eq_sum line 49
  9. theorem OAI.PerfectCompleteness.TwoResponseCollision.goodCollision_weight_eq_sum line 57
  10. theorem OAI.PerfectCompleteness.TwoResponseCollision.goodCollision_probability_eq_sum_sq line 66
  11. theorem OAI.PerfectCompleteness.TwoResponseCollision.responseMass_eq_zero_of_not_goodResponse line 101
  12. theorem OAI.PerfectCompleteness.TwoResponseCollision.sum_sq_bound_of_support_card_le_two line 112
  13. theorem OAI.PerfectCompleteness.TwoResponseCollision.goodCollision_probability_ge line 135
  14. theorem OAI.PerfectCompleteness.TwoResponseCollision.collision_probability_ge line 145
  15. theorem OAI.PerfectCompleteness.TwoResponseCollision.collision_probability_ge_of_response_set line 155
  16. theorem OAI.PerfectCompleteness.TwoResponseCollision.collision_probability_ge_of_good_defined line 171
  17. theorem OAI.PerfectCompleteness.DecoderTableAdmissibility.event_of_probability_one line 201
  18. theorem OAI.PerfectCompleteness.DecoderTableAdmissibility.probability_one_of_support line 218
  19. theorem OAI.PerfectCompleteness.DecoderTableAdmissibility.expectation_le_of_support line 227
  20. def OAI.PerfectCompleteness.DecoderTableAdmissibility.RowValid line 243
  21. def OAI.PerfectCompleteness.DecoderTableAdmissibility.Admissible line 246
  22. theorem OAI.PerfectCompleteness.DecoderTableAdmissibility.table_admissible_of_support line 249
  23. theorem OAI.PerfectCompleteness.DecoderTableAdmissibility.row_valid_of_probability_one line 260
  24. theorem OAI.PerfectCompleteness.DecoderTableAdmissibility.table_admissible_of_probability_one line 268
  25. theorem OAI.PerfectCompleteness.DecoderTableAdmissibility.table_admissible_probability_one line 276
  26. theorem OAI.PerfectCompleteness.DecoderTableAdmissibility.table_erased_of_support line 286
  27. theorem OAI.PerfectCompleteness.DecoderTableAdmissibility.table_erased_of_probability_one line 298
  28. def OAI.PerfectCompleteness.DecoderTableAdmissibility.eraseTable line 308
  29. theorem OAI.PerfectCompleteness.DecoderTableAdmissibility.eraseTable_admissible line 312
  30. theorem OAI.PerfectCompleteness.DecoderTableAdmissibility.eraseTable_eq_of_support line 320
  31. theorem OAI.PerfectCompleteness.DecoderTableAdmissibility.eraseTable_pushforward_eq line 331
  32. theorem OAI.PerfectCompleteness.DecoderTableAdmissibility.expectation_le_of_admissible line 352
  33. theorem OAI.PerfectCompleteness.DecoderTableAdmissibility.expectation_le_of_probability_one line 362
  34. theorem OAI.PerfectCompleteness.DecoderTableAdmissibility.collision_expectation_le line 371
  35. def OAI.PerfectCompleteness.UpperParameterScalars.h line 390
  36. def OAI.PerfectCompleteness.UpperParameterScalars.g line 392
  37. def OAI.PerfectCompleteness.UpperParameterScalars.q line 394
  38. def OAI.PerfectCompleteness.UpperParameterScalars.rhoPred line 396
  39. def OAI.PerfectCompleteness.UpperParameterScalars.b line 398
  40. def OAI.PerfectCompleteness.UpperParameterScalars.tau line 400
  41. def OAI.PerfectCompleteness.UpperParameterScalars.gamma line 402
  42. theorem OAI.PerfectCompleteness.UpperParameterScalars.h_pos line 405
  43. theorem OAI.PerfectCompleteness.UpperParameterScalars.g_pos line 407
  44. theorem OAI.PerfectCompleteness.UpperParameterScalars.q_pos line 411
  45. theorem OAI.PerfectCompleteness.UpperParameterScalars.rhoPred_pos line 414
  46. theorem OAI.PerfectCompleteness.UpperParameterScalars.b_pos line 418
  47. theorem OAI.PerfectCompleteness.UpperParameterScalars.tau_pos line 422
  48. theorem OAI.PerfectCompleteness.UpperParameterScalars.gamma_pos line 427
  49. theorem OAI.PerfectCompleteness.UpperParameterScalars.all_pos line 434
  50. theorem OAI.PerfectCompleteness.UpperParameterScalars.reciprocal_pow_eq_zpow line 441
  51. theorem OAI.PerfectCompleteness.UpperParameterScalars.gamma_eq_neg_zpow line 445
  52. theorem OAI.PerfectCompleteness.UpperParameterScalars.reciprocal_power_sub_antitone line 453
  53. theorem OAI.PerfectCompleteness.UpperParameterScalars.exists_rows_upward line 459
  54. theorem OAI.PerfectCompleteness.UpperParameterScalars.exists_rows line 473
  55. theorem OAI.PerfectCompleteness.UpperParameterScalars.exists_rows_rhoPred line 479
  56. theorem OAI.PerfectCompleteness.UpperParameterScalars.exists_repeats_upward line 485
  57. theorem OAI.PerfectCompleteness.UpperParameterScalars.exists_repeats line 497
  58. theorem OAI.PerfectCompleteness.UpperParameterScalars.exists_upper_repeats line 502
  59. theorem OAI.PerfectCompleteness.UpperParameterScalars.exists_upper_choices line 508