OAI/Computability/DirectedFeedback/Games/AdviceLaw.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Decoder.AdviceLaw.visibleMap line 36
  2. theorem OAI.DFVSGames.Decoder.AdviceLaw.visibleMap_apply line 42
  3. def OAI.DFVSGames.Decoder.AdviceLaw.rawMapPairCoefficientsEquiv line 46
  4. theorem OAI.DFVSGames.Decoder.AdviceLaw.visibleMap_raw line 53
  5. theorem OAI.DFVSGames.Decoder.AdviceLaw.uniform_visible_maps line 59
  6. theorem OAI.DFVSGames.Decoder.AdviceLaw.uniform_visible_maps_expectation line 75
  7. def OAI.DFVSGames.Decoder.AdviceLaw.actualSuccess line 86
  8. theorem OAI.DFVSGames.Decoder.AdviceLaw.actualSuccess_eq_cleanSuccess line 98
  9. def OAI.DFVSGames.Decoder.AdviceLaw.drawDistribution line 117
  10. def OAI.DFVSGames.Decoder.AdviceLaw.paddedDistribution line 131
  11. theorem OAI.DFVSGames.Decoder.AdviceLaw.paddedDistribution_totalVariation_eq_slope line 136
  12. theorem OAI.DFVSGames.Decoder.AdviceLaw.paddedDistribution_totalVariation line 145
  13. def OAI.DFVSGames.Decoder.AdviceLaw.withKernel line 158
  14. theorem OAI.DFVSGames.Decoder.AdviceLaw.withKernel_totalVariation line 167
  15. theorem OAI.DFVSGames.Decoder.AdviceLaw.withKernel_totalVariation_le line 183
  16. theorem OAI.DFVSGames.Decoder.AdviceLaw.wholeAdvice_totalVariation line 195
  17. theorem OAI.DFVSGames.Decoder.AdviceLaw.wholeAdvice_totalVariation_eq_slope line 209
  18. theorem OAI.DFVSGames.Decoder.AdviceLaw.wholeAdvice_totalVariation_le_slope line 225
  19. instance OAI.DFVSGames.Decoder.AdviceLaw.observedRowsFintype line 245
  20. theorem OAI.DFVSGames.Decoder.AdviceLaw.observed_hidden_independent line 248
  21. abbrev OAI.DFVSGames.Decoder.AdviceLaw.ProjectionSeed line 263
  22. def OAI.DFVSGames.Decoder.AdviceLaw.projectionSeedDistribution line 267
  23. def OAI.DFVSGames.Decoder.AdviceLaw.projectSeedMap line 278
  24. theorem OAI.DFVSGames.Decoder.AdviceLaw.projectionSeed_expectation line 284
  25. theorem OAI.DFVSGames.Decoder.AdviceLaw.projectionSeed_pushforward line 308
  26. def OAI.DFVSGames.Decoder.AdviceLaw.seedToActualDraw line 326
  27. theorem OAI.DFVSGames.Decoder.AdviceLaw.seed_projection line 335
  28. theorem OAI.DFVSGames.Decoder.AdviceLaw.seed_padded_pair line 341
  29. theorem OAI.DFVSGames.Decoder.AdviceLaw.seed_left_observation line 348
  30. theorem OAI.DFVSGames.Decoder.AdviceLaw.seed_right_observation line 357
  31. def OAI.DFVSGames.Decoder.AdviceLaw.choiceDistribution line 370
  32. def OAI.DFVSGames.Decoder.AdviceLaw.maskSlotChoice line 376
  33. theorem OAI.DFVSGames.Decoder.AdviceLaw.maskSlotChoice_pushforward line 379
  34. def OAI.DFVSGames.Decoder.AdviceLaw.choicesOfMaskSlots line 389
  35. theorem OAI.DFVSGames.Decoder.AdviceLaw.choices_expectation line 393
  36. theorem OAI.DFVSGames.Decoder.AdviceLaw.choices_mask line 404
  37. theorem OAI.DFVSGames.Decoder.AdviceLaw.choices_active_slot line 412
  38. theorem OAI.DFVSGames.Decoder.AdviceLaw.projectionSeed_mask_slots_expectation line 417
  39. theorem OAI.DFVSGames.Decoder.AdviceLaw.product_pushforward_withKernel line 448
  40. def OAI.DFVSGames.Decoder.AdviceLaw.fullSeedLaw line 473
  41. def OAI.DFVSGames.Decoder.AdviceLaw.fullSeedPad line 479
  42. theorem OAI.DFVSGames.Decoder.AdviceLaw.fullSeed_pad_law line 484
  43. theorem OAI.DFVSGames.Decoder.AdviceLaw.fullSeed_totalVariation line 500
  44. theorem OAI.DFVSGames.Decoder.AdviceLaw.fullSeed_totalVariation_eq_slope line 513
  45. theorem OAI.DFVSGames.Decoder.AdviceLaw.fullSeed_totalVariation_le_slope line 528
  46. abbrev OAI.DFVSGames.Decoder.AdviceLaw.FullSeed line 548
  47. abbrev OAI.DFVSGames.Decoder.AdviceLaw.CompleteData line 553
  48. abbrev OAI.DFVSGames.Decoder.AdviceLaw.PrivateMap line 561
  49. def OAI.DFVSGames.Decoder.AdviceLaw.targetObservationEquiv line 564
  50. def OAI.DFVSGames.Decoder.AdviceLaw.fullSeedCoordinatesEquiv line 573
  51. def OAI.DFVSGames.Decoder.AdviceLaw.completeObserve line 584
  52. def OAI.DFVSGames.Decoder.AdviceLaw.completeAssemble line 587
  53. theorem OAI.DFVSGames.Decoder.AdviceLaw.completeObserve_eq line 591
  54. theorem OAI.DFVSGames.Decoder.AdviceLaw.completeAssemble_eq line 596
  55. theorem OAI.DFVSGames.Decoder.AdviceLaw.completeObserve_assemble line 601
  56. def OAI.DFVSGames.Decoder.AdviceLaw.completeFiberEquiv line 605
  57. theorem OAI.DFVSGames.Decoder.AdviceLaw.completeFiberEquiv_val line 610
  58. def OAI.DFVSGames.Decoder.AdviceLaw.completeDraw line 613
  59. theorem OAI.DFVSGames.Decoder.AdviceLaw.completeDraw_seed line 622
  60. theorem OAI.DFVSGames.Decoder.AdviceLaw.completeDraw_rows line 626
  61. theorem OAI.DFVSGames.Decoder.AdviceLaw.completeDraw_left line 631
  62. theorem OAI.DFVSGames.Decoder.AdviceLaw.completeDraw_right line 641
  63. def OAI.DFVSGames.Decoder.AdviceLaw.completeWeight line 652
  64. theorem OAI.DFVSGames.Decoder.AdviceLaw.fullSeed_weight_observed line 661
  65. theorem OAI.DFVSGames.Decoder.AdviceLaw.fullSeed_weight_fiber line 668
  66. def OAI.DFVSGames.Fourier.Parity.finiteSum line 687
  67. theorem OAI.DFVSGames.Fourier.Parity.finiteSum_le line 692
  68. theorem OAI.DFVSGames.Fourier.Parity.finiteSum_split line 703
  69. theorem OAI.DFVSGames.Fourier.Parity.nonzero_sum_gt_half line 714
  70. theorem OAI.DFVSGames.Fourier.Parity.signed_le_abs line 722
  71. theorem OAI.DFVSGames.Fourier.Parity.coefficient_of_bounds line 728
  72. theorem OAI.DFVSGames.Fourier.Parity.coefficient_gt_half_div line 763
  73. theorem OAI.DFVSGames.Fourier.Parity.div_div_eq line 784
  74. theorem OAI.DFVSGames.Fourier.Parity.lemma53_arithmetic line 788