OAI/Computability/DirectedFeedback/Games/ActualAdviceUpper.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.DFVSGames.Decoder.ActualAdviceUpper.publicMapFintype line 41
  2. def OAI.DFVSGames.Decoder.ActualAdviceUpper.sourceIncidence line 45
  3. abbrev OAI.DFVSGames.Decoder.ActualAdviceUpper.Visible line 50
  4. def OAI.DFVSGames.Decoder.ActualAdviceUpper.complementMap line 52
  5. def OAI.DFVSGames.Decoder.ActualAdviceUpper.rowMap line 57
  6. def OAI.DFVSGames.Decoder.ActualAdviceUpper.fullInput line 62
  7. def OAI.DFVSGames.Decoder.ActualAdviceUpper.projectedInput line 71
  8. def OAI.DFVSGames.Decoder.ActualAdviceUpper.policies line 80
  9. def OAI.DFVSGames.Decoder.ActualAdviceUpper.actualDraw line 89
  10. theorem OAI.DFVSGames.Decoder.ActualAdviceUpper.fullInput_actual line 102
  11. theorem OAI.DFVSGames.Decoder.ActualAdviceUpper.projectedInput_actual line 112
  12. theorem OAI.DFVSGames.Decoder.ActualAdviceUpper.policyAgreement_actual line 123
  13. theorem OAI.DFVSGames.Decoder.ActualAdviceUpper.source_projection_eq line 145
  14. theorem OAI.DFVSGames.Decoder.ActualAdviceUpper.fixed_public_map_bound line 153
  15. theorem OAI.DFVSGames.Decoder.ActualAdviceUpper.public_map_average_bound line 167
  16. theorem OAI.DFVSGames.Decoder.ActualAdviceUpper.actual_source_average_bound line 188
  17. theorem OAI.DFVSGames.Reduction.ActualCompleteness.expect_linear_eval line 221
  18. theorem OAI.DFVSGames.Reduction.ActualCompleteness.expect_independent_linear_evals line 242
  19. def OAI.DFVSGames.Reduction.ActualCompleteness.localNoiseFailure line 257
  20. theorem OAI.DFVSGames.Reduction.ActualCompleteness.localNoiseFailure_eq_half line 261
  21. theorem OAI.DFVSGames.Reduction.ActualCompleteness.localNoiseFailure_le line 290
  22. theorem OAI.DFVSGames.Reduction.ActualCompleteness.expect_function_apply line 301
  23. def OAI.DFVSGames.Reduction.ActualCompleteness.tupleFailure line 315
  24. theorem OAI.DFVSGames.Reduction.ActualCompleteness.tupleFailure_le line 319
  25. def OAI.DFVSGames.Reduction.ActualCompleteness.evalTriple line 354
  26. def OAI.DFVSGames.Reduction.ActualCompleteness.evalRecord line 357
  27. def OAI.DFVSGames.Reduction.ActualCompleteness.evaluate line 362
  28. theorem OAI.DFVSGames.Reduction.ActualCompleteness.record_eval_normalized line 365
  29. theorem OAI.DFVSGames.Reduction.ActualCompleteness.record_eval_adjustment line 383
  30. theorem OAI.DFVSGames.Reduction.ActualCompleteness.evaluate_data line 394
  31. def OAI.DFVSGames.Reduction.ActualCompleteness.honestPoint line 404
  32. theorem OAI.DFVSGames.Reduction.ActualCompleteness.honestPoint_tau line 407
  33. theorem OAI.DFVSGames.Reduction.ActualCompleteness.canonical_evaluate line 410
  34. def OAI.DFVSGames.Reduction.ActualCompleteness.honestVertexLabel line 423
  35. def OAI.DFVSGames.Reduction.ActualCompleteness.honestLabeling line 428
  36. theorem OAI.DFVSGames.Reduction.ActualCompleteness.honest_unfolded line 433
  37. def OAI.DFVSGames.Reduction.ActualCompleteness.sourcePoint line 450
  38. theorem OAI.DFVSGames.Reduction.ActualCompleteness.sourcePoint_tau line 454
  39. theorem OAI.DFVSGames.Reduction.ActualCompleteness.satisfied_parity line 457
  40. theorem OAI.DFVSGames.Reduction.ActualCompleteness.honest_unfolded_valid line 467
  41. theorem OAI.DFVSGames.Reduction.ActualCompleteness.expect_pair_inline_ActualCompleteness line 477
  42. theorem OAI.DFVSGames.Reduction.ActualCompleteness.honest_acceptance_bound line 481
  43. theorem OAI.DFVSGames.Reduction.ActualCompleteness.honest_acceptance_of_bounds line 540
  44. theorem OAI.DFVSGames.Reduction.ActualCompleteness.honest_satisfied_fraction_bound line 549
  45. theorem OAI.DFVSGames.Reduction.ActualCompleteness.actual_completeAt line 558
  46. def OAI.DFVSGames.Decoder.TableKeysCompleteness.diagonalLabeling line 590
  47. theorem OAI.DFVSGames.Decoder.TableKeysCompleteness.diagonal_unfolded line 595
  48. theorem OAI.DFVSGames.Decoder.TableKeysCompleteness.acceptanceProbability_eq_diagonal line 603
  49. def OAI.DFVSGames.Decoder.TableKeysCompleteness.honestLabeling line 610
  50. theorem OAI.DFVSGames.Decoder.TableKeysCompleteness.diagonal_honestLabeling line 614
  51. theorem OAI.DFVSGames.Decoder.TableKeysCompleteness.honest_unfolded line 621
  52. theorem OAI.DFVSGames.Decoder.TableKeysCompleteness.honest_unfolded_valid line 629
  53. theorem OAI.DFVSGames.Decoder.TableKeysCompleteness.honest_acceptance_bound line 637
  54. theorem OAI.DFVSGames.Decoder.TableKeysCompleteness.honest_acceptance_of_bounds line 644
  55. theorem OAI.DFVSGames.Decoder.TableKeysCompleteness.honest_satisfied_fraction_bound line 653
  56. theorem OAI.DFVSGames.Decoder.TableKeysCompleteness.completeAt line 662
  57. theorem OAI.DFVSGames.Decoder.TableKeysCompleteness.completeAt_withEnumeration line 676
  58. abbrev OAI.DFVSGames.Reduction.CanonicalEncoding.Ambient line 697
  59. abbrev OAI.DFVSGames.Reduction.CanonicalEncoding.Record line 698
  60. abbrev OAI.DFVSGames.Reduction.CanonicalEncoding.Body line 699
  61. def OAI.DFVSGames.Reduction.CanonicalEncoding.vectorWord line 701
  62. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.vectorWord_lt line 704
  63. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.vectorWord_injective line 707
  64. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.vectorWord_eq_iff line 713
  65. def OAI.DFVSGames.Reduction.CanonicalEncoding.recordWords line 716
  66. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.recordWords_length line 726
  67. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.recordWords_injective line 730
  68. def OAI.DFVSGames.Reduction.CanonicalEncoding.recordsWords line 765
  69. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.recordsWords_nil line 768
  70. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.recordsWords_cons line 771
  71. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.recordsWords_length line 775
  72. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.recordsWords_take_head line 781
  73. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.recordsWords_injective line 788
  74. def OAI.DFVSGames.Reduction.CanonicalEncoding.bodyWords line 816
  75. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.bodyWords_length line 819
  76. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.bodyWords_injective line 823
  77. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.bodyWords_eq_iff line 831
  78. def OAI.DFVSGames.Reduction.CanonicalEncoding.wordBound line 834
  79. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.recordWords_bounded line 836
  80. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.bodyWords_bounded line 861
  81. def OAI.DFVSGames.Reduction.CanonicalEncoding.bodyBits line 872
  82. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.bodyBits_injective line 875
  83. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.bodyBits_eq_iff line 880
  84. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.bodyBits_length_le line 883
  85. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.imageVertices_bodyWords line 888
  86. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.imageVertices_bodyBits line 896
  87. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.idxOf_map_injective line 904
  88. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.imageIndex_map_val line 916
  89. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.imageIndex_bodyWords_val line 930
  90. theorem OAI.DFVSGames.Reduction.CanonicalEncoding.imageIndex_bodyBits_val line 937