OAI/Computability/DirectedFeedback/Encoding/RawPrivateTable.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Soundness.RawPrivateTable.Extension line 19
  2. def OAI.DFVSGames.Soundness.RawPrivateTable.displayed line 21
  3. theorem OAI.DFVSGames.Soundness.RawPrivateTable.full_occurrence_eq_of_displayed_eq line 27
  4. theorem OAI.DFVSGames.Soundness.RawPrivateTable.single_name_eq_of_displayed_eq line 34
  5. theorem OAI.DFVSGames.Soundness.RawPrivateTable.displayed_eq_iff line 43
  6. def OAI.DFVSGames.Soundness.RawPrivateTable.SupportedV line 59
  7. def OAI.DFVSGames.Soundness.RawPrivateTable.representative line 63
  8. theorem OAI.DFVSGames.Soundness.RawPrivateTable.representative_display line 66
  9. def OAI.DFVSGames.Soundness.RawPrivateTable.supported line 71
  10. def OAI.DFVSGames.Soundness.RawPrivateTable.projection line 80
  11. def OAI.DFVSGames.Soundness.RawPrivateTable.merge line 84
  12. theorem OAI.DFVSGames.Soundness.RawPrivateTable.merge_comp line 89
  13. def OAI.DFVSGames.Soundness.RawPrivateTable.sourceTable line 94
  14. def OAI.DFVSGames.Soundness.RawPrivateTable.privateTable line 99
  15. theorem OAI.DFVSGames.Soundness.RawPrivateTable.canonical_same_display line 106
  16. theorem OAI.DFVSGames.Soundness.RawPrivateTable.privateTable_pullback line 117
  17. def OAI.DFVSGames.Decoder.TableKeys.slope line 148
  18. theorem OAI.DFVSGames.Decoder.TableKeys.slope_apply line 153
  19. theorem OAI.DFVSGames.Decoder.TableKeys.slope_zero_iff line 157
  20. theorem OAI.DFVSGames.Decoder.TableKeys.slope_injective line 170
  21. def OAI.DFVSGames.Decoder.TableKeys.freeTriple line 190
  22. def OAI.DFVSGames.Decoder.TableKeys.reduceBlock line 192
  23. theorem OAI.DFVSGames.Decoder.TableKeys.reduceBlock_zero line 197
  24. theorem OAI.DFVSGames.Decoder.TableKeys.reduceBlock_first line 201
  25. theorem OAI.DFVSGames.Decoder.TableKeys.reduceBlock_second line 206
  26. theorem OAI.DFVSGames.Decoder.TableKeys.reduceBlock_third line 212
  27. theorem OAI.DFVSGames.Decoder.TableKeys.reduceBlock_full line 217
  28. theorem OAI.DFVSGames.Decoder.TableKeys.third_intercept_cancels line 227
  29. theorem OAI.DFVSGames.Decoder.TableKeys.third_key_cancels line 231
  30. theorem OAI.DFVSGames.Decoder.TableKeys.full_record_occurrence_injective line 240
  31. abbrev OAI.DFVSGames.Decoder.TableKeys.Key line 252
  32. def OAI.DFVSGames.Decoder.TableKeys.key line 254
  33. theorem OAI.DFVSGames.Decoder.TableKeys.key_data_ext_iff line 260
  34. theorem OAI.DFVSGames.Decoder.TableKeys.key_shift line 268
  35. theorem OAI.DFVSGames.Decoder.TableKeys.key_shift_free line 274
  36. theorem OAI.DFVSGames.Decoder.TableKeys.projected_key_sharing line 284
  37. def OAI.DFVSGames.Decoder.TableKeys.projectedKey line 294
  38. theorem OAI.DFVSGames.Decoder.TableKeys.projectedKey_pullback line 301
  39. def OAI.DFVSGames.Decoder.TableKeys.visibleTau line 323
  40. theorem OAI.DFVSGames.Decoder.TableKeys.projection_surjective line 326
  41. theorem OAI.DFVSGames.Decoder.TableKeys.projection_preserves_homogeneous line 334
  42. theorem OAI.DFVSGames.Decoder.TableKeys.visible_table_unique line 341
  43. theorem OAI.DFVSGames.Decoder.TableKeys.pullback_shift line 351
  44. theorem OAI.DFVSGames.Decoder.TableKeys.projectedKey_shift line 366
  45. structure OAI.DFVSGames.Decoder.AdviceExperiment.FullAdvice line 390
  46. structure OAI.DFVSGames.Decoder.AdviceExperiment.Draw line 396
  47. structure OAI.DFVSGames.Decoder.AdviceExperiment.ProjectedAdvice line 408
  48. def OAI.DFVSGames.Decoder.AdviceExperiment.projection line 416
  49. def OAI.DFVSGames.Decoder.AdviceExperiment.leftObservation line 420
  50. def OAI.DFVSGames.Decoder.AdviceExperiment.rightObservation line 426
  51. def OAI.DFVSGames.Decoder.AdviceExperiment.paddedMatrix line 434
  52. def OAI.DFVSGames.Decoder.AdviceExperiment.paddedComplement line 437
  53. theorem OAI.DFVSGames.Decoder.AdviceExperiment.left_rows_eq line 440
  54. theorem OAI.DFVSGames.Decoder.AdviceExperiment.left_rows_attainable line 443
  55. theorem OAI.DFVSGames.Decoder.AdviceExperiment.right_rows_attainable line 448
  56. def OAI.DFVSGames.Decoder.AdviceExperiment.changeHidden line 453
  57. theorem OAI.DFVSGames.Decoder.AdviceExperiment.leftObservation_changeHidden line 457
  58. theorem OAI.DFVSGames.Decoder.AdviceExperiment.rightObservation_changeHidden line 462
  59. theorem OAI.DFVSGames.Decoder.AdviceExperiment.selectedWitness_changeHidden line 467
  60. theorem OAI.DFVSGames.Decoder.AdviceExperiment.projection_actual_answer line 473
  61. def OAI.DFVSGames.Clean.AdviceImageLaw.rangePoint line 497
  62. def OAI.DFVSGames.Clean.AdviceImageLaw.selectedLift line 500
  63. theorem OAI.DFVSGames.Clean.AdviceImageLaw.selectedLift_spec line 503
  64. theorem OAI.DFVSGames.Clean.AdviceImageLaw.rangePoint_lift_add_kernel line 507
  65. def OAI.DFVSGames.Clean.AdviceImageLaw.imageKernelEquiv line 513
  66. def OAI.DFVSGames.Clean.AdviceImageLaw.columnImage line 532
  67. def OAI.DFVSGames.Clean.AdviceImageLaw.columnSplitEquiv line 535
  68. def OAI.DFVSGames.Clean.AdviceImageLaw.visibleCoefficients line 539
  69. def OAI.DFVSGames.Clean.AdviceImageLaw.coefficientsSplitEquiv line 543
  70. instance OAI.DFVSGames.Clean.AdviceImageLaw.rangeFintype line 548
  71. instance OAI.DFVSGames.Clean.AdviceImageLaw.kernelFintype line 551
  72. theorem OAI.DFVSGames.Clean.AdviceImageLaw.uniform_visible_coefficients line 554
  73. theorem OAI.DFVSGames.Clean.AdviceImageLaw.uniform_coordinate_product line 568
  74. theorem OAI.DFVSGames.Clean.AdviceImageLaw.visible_coefficient_product line 576
  75. theorem OAI.DFVSGames.Clean.AdviceImageLaw.uniform_pushforward_of_expect line 584
  76. theorem OAI.DFVSGames.Clean.AdviceImageLaw.visible_coefficients_pushforward line 602
  77. theorem OAI.DFVSGames.Clean.AdviceImageLaw.visible_card_le line 608
  78. theorem OAI.DFVSGames.Clean.AdviceImageLaw.visible_card_binary_le line 614
  79. abbrev OAI.DFVSGames.Clean.AdviceImageLaw.PartnerSpace line 628
  80. theorem OAI.DFVSGames.Clean.AdviceImageLaw.coefficients_comp line 630
  81. def OAI.DFVSGames.Clean.AdviceImageLaw.actualVisibleCoefficients line 635
  82. theorem OAI.DFVSGames.Clean.AdviceImageLaw.actualVisibleCoefficients_second line 640
  83. def OAI.DFVSGames.Clean.AdviceImageLaw.actualMapPairEquiv line 648
  84. theorem OAI.DFVSGames.Clean.AdviceImageLaw.actual_maps_visible_uniform line 654
  85. theorem OAI.DFVSGames.Clean.AdviceImageLaw.actual_maps_visible_product line 666
  86. theorem OAI.DFVSGames.Clean.AdviceImageLaw.actual_maps_visible_pushforward line 674