OAI/Computability/DirectedFeedback/Games/RowErasureSliceQuotient.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Inverse.RowErasureSliceQuotient.direction line 15
  2. theorem OAI.DFVSGames.Inverse.RowErasureSliceQuotient.direction_apply line 19
  3. theorem OAI.DFVSGames.Inverse.RowErasureSliceQuotient.exists_direction_of_row_and_column line 23
  4. theorem OAI.DFVSGames.Inverse.RowErasureSliceQuotient.direction_injective line 39
  5. def OAI.DFVSGames.Inverse.RowErasureSliceQuotient.AffineSlice line 48
  6. def OAI.DFVSGames.Inverse.RowErasureSliceQuotient.ofQuotient line 51
  7. theorem OAI.DFVSGames.Inverse.RowErasureSliceQuotient.ofQuotient_val line 63
  8. theorem OAI.DFVSGames.Inverse.RowErasureSliceQuotient.ofQuotient_bijective line 67
  9. def OAI.DFVSGames.Inverse.RowErasureSliceQuotient.equiv line 90
  10. theorem OAI.DFVSGames.Inverse.RowErasureSliceQuotient.equiv_apply line 94
  11. theorem OAI.DFVSGames.Inverse.RowErasureSliceQuotient.equiv_affine_target line 98
  12. theorem OAI.DFVSGames.Inverse.RowErasureSliceQuotient.expect_equiv line 105
  13. theorem OAI.DFVSGames.Decoder.TransferredDecoding.indicator_congr line 134
  14. def OAI.DFVSGames.Decoder.TransferredDecoding.privateOrigin line 145
  15. theorem OAI.DFVSGames.Decoder.TransferredDecoding.assemble_privateOrigin line 150
  16. def OAI.DFVSGames.Decoder.TransferredDecoding.visibleFallback line 170
  17. theorem OAI.DFVSGames.Decoder.TransferredDecoding.actual_slice_agreement_eq_private line 173
  18. theorem OAI.DFVSGames.Decoder.TransferredDecoding.actual_transferred_decoding line 207
  19. structure OAI.DFVSGames.Decoder.VisiblePolicies.ResponseWitness line 286
  20. def OAI.DFVSGames.Decoder.VisiblePolicies.defaultWitness line 291
  21. abbrev OAI.DFVSGames.Decoder.VisiblePolicies.LeftInput line 296
  22. abbrev OAI.DFVSGames.Decoder.VisiblePolicies.RightInput line 300
  23. def OAI.DFVSGames.Decoder.VisiblePolicies.chosenWitness line 305
  24. theorem OAI.DFVSGames.Decoder.VisiblePolicies.chosenWitness_spec line 310
  25. def OAI.DFVSGames.Decoder.VisiblePolicies.leftPolicy line 317
  26. def OAI.DFVSGames.Decoder.VisiblePolicies.pointLaw line 323
  27. def OAI.DFVSGames.Decoder.VisiblePolicies.rightPolicy line 328
  28. theorem OAI.DFVSGames.Decoder.VisiblePolicies.rightPolicy_on_attainable line 339
  29. theorem OAI.DFVSGames.Decoder.VisiblePolicies.leftPolicy_changeHidden line 350
  30. theorem OAI.DFVSGames.Decoder.VisiblePolicies.rightPolicy_on_draw line 359
  31. def OAI.DFVSGames.Decoder.VisiblePolicies.observedAgreement line 376
  32. theorem OAI.DFVSGames.Decoder.VisiblePolicies.observedAgreement_eq_private line 386
  33. def OAI.DFVSGames.Clean.IncidenceGap.slotLaw line 424
  34. theorem OAI.DFVSGames.Clean.IncidenceGap.slotLaw_weight line 427
  35. def OAI.DFVSGames.Clean.IncidenceGap.incidenceLaw line 431
  36. def OAI.DFVSGames.Clean.IncidenceGap.game line 435
  37. theorem OAI.DFVSGames.Clean.IncidenceGap.game_accepts_iff line 440
  38. theorem OAI.DFVSGames.Clean.IncidenceGap.game_isProjection line 446
  39. def OAI.DFVSGames.Clean.IncidenceGap.paritySuccess line 456
  40. def OAI.DFVSGames.Clean.IncidenceGap.parityValue line 459
  41. theorem OAI.DFVSGames.Clean.IncidenceGap.paritySuccess_le_parityValue line 463
  42. theorem OAI.DFVSGames.Clean.IncidenceGap.local_count_bound line 468
  43. theorem OAI.DFVSGames.Clean.IncidenceGap.game_success_eq_slot_average line 481
  44. theorem OAI.DFVSGames.Clean.IncidenceGap.game_success_honest_eq_paritySuccess line 501
  45. theorem OAI.DFVSGames.Clean.IncidenceGap.parityValue_le_game_value line 514
  46. theorem OAI.DFVSGames.Clean.IncidenceGap.game_success_le_two_add_parity_third line 525
  47. theorem OAI.DFVSGames.Clean.IncidenceGap.game_value_le_one_sub_third line 546
  48. theorem OAI.DFVSGames.Clean.IncidenceGap.game_value_le_one_sub_gap_third line 556
  49. theorem OAI.DFVSGames.Clean.IncidenceGap.game_value_le_fourteen_fifteenths line 566
  50. def OAI.DFVSGames.Clean.IncidenceGap.satisfyingTriple line 574
  51. theorem OAI.DFVSGames.Clean.IncidenceGap.satisfyingTriple_valid line 577
  52. theorem OAI.DFVSGames.Clean.IncidenceGap.satisfyingTriple_of_valid line 582
  53. def OAI.DFVSGames.Clean.IncidenceGap.fourAnswerGame line 593
  54. theorem OAI.DFVSGames.Clean.IncidenceGap.four_answer_card line 598
  55. theorem OAI.DFVSGames.Clean.IncidenceGap.fourAnswerGame_isProjection line 600
  56. theorem OAI.DFVSGames.Clean.IncidenceGap.fourAnswerGame_accepts_encode line 607
  57. theorem OAI.DFVSGames.Clean.IncidenceGap.fourAnswerGame_value_eq line 619
  58. theorem OAI.DFVSGames.Clean.IncidenceGap.fourAnswerGame_value_le_one_sub_third line 637
  59. theorem OAI.DFVSGames.Clean.IncidenceGap.fourAnswerGame_value_le_fourteen_fifteenths line 644
  60. theorem OAI.DFVSGames.Clean.Bound.repeated_incidence_value_le line 669
  61. theorem OAI.DFVSGames.Clean.Bound.clean_success_le line 680
  62. theorem OAI.DFVSGames.Clean.Bound.clean_success_le_dimension line 693
  63. theorem OAI.DFVSGames.Clean.Bound.native_clean_success_le_dimension line 710
  64. theorem OAI.DFVSGames.Clean.ActualAdviceBound.deterministic_success_le_dimension line 737
  65. theorem OAI.DFVSGames.Clean.ActualAdviceBound.stochastic_success_le_dimension line 752
  66. theorem OAI.DFVSGames.Clean.ActualAdviceBound.stochastic_success_le_dimension_finite line 768