OAI/Computability/DirectedFeedback/Games/Decoder.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.Hastad.parityProjection line 15
  2. theorem OAI.DFVSGames.Foundations.Hastad.walsh_support line 18
  3. theorem OAI.DFVSGames.Foundations.Hastad.sign_power_parity line 26
  4. theorem OAI.DFVSGames.Foundations.Hastad.walsh_pullback line 36
  5. theorem OAI.DFVSGames.Foundations.Hastad.projectedCoefficient_eq line 46
  6. theorem OAI.DFVSGames.Foundations.Hastad.projection_has_preimage line 51
  7. theorem OAI.DFVSGames.Foundations.Hastad.scaled_geometric_power_le_one line 63
  8. theorem OAI.DFVSGames.Foundations.Hastad.noise_decay_bound line 77
  9. def OAI.DFVSGames.Foundations.Hastad.zeroMask line 90
  10. theorem OAI.DFVSGames.Foundations.Hastad.support_eq_empty_iff line 93
  11. theorem OAI.DFVSGames.Foundations.Hastad.parityProjection_zero line 105
  12. def OAI.DFVSGames.Foundations.Hastad.agreementProbability line 110
  13. theorem OAI.DFVSGames.Foundations.Hastad.agreementProbability_nonneg line 115
  14. theorem OAI.DFVSGames.Foundations.Hastad.agreementProbability_projection line 123
  15. def OAI.DFVSGames.Foundations.Hastad.decoderSuccess line 149
  16. def OAI.DFVSGames.Foundations.Hastad.decodingEnergy line 153
  17. theorem OAI.DFVSGames.Foundations.Hastad.decodingEnergy_le_success line 156
  18. theorem OAI.DFVSGames.Foundations.Hastad.bias_sq_le_weighted_energy line 190
  19. theorem OAI.DFVSGames.Foundations.Hastad.decoder_four_epsilon_bias_sq line 207
  20. theorem OAI.DFVSGames.Foundations.Hastad.folded_decoder_bound line 233
  21. def OAI.DFVSGames.Foundations.Hastad.validAgreementProbability line 241
  22. theorem OAI.DFVSGames.Foundations.Hastad.validAgreementProbability_eq line 248
  23. def OAI.DFVSGames.Foundations.Hastad.validDecoderSuccess line 261
  24. theorem OAI.DFVSGames.Foundations.Hastad.conditioned_validDecoderSuccess line 267
  25. theorem OAI.DFVSGames.Foundations.Hastad.conditioned_folded_decoder_bound line 285
  26. def OAI.DFVSGames.Foundations.Hastad.supportResponse line 311
  27. theorem OAI.DFVSGames.Foundations.Hastad.supportResponse_expectation line 324
  28. def OAI.DFVSGames.Foundations.Hastad.fourierResponse line 335
  29. theorem OAI.DFVSGames.Foundations.Hastad.fourierResponse_expectation line 345
  30. theorem OAI.DFVSGames.Foundations.Hastad.response_expectation_nonnegative line 360
  31. def OAI.DFVSGames.Foundations.Hastad.responseAgreement line 365
  32. def OAI.DFVSGames.Foundations.Hastad.validResponseAgreement line 370
  33. theorem OAI.DFVSGames.Foundations.Hastad.supportResponse_validAgreement line 377
  34. theorem OAI.DFVSGames.Foundations.Hastad.validAgreement_le_supportResponses line 391
  35. theorem OAI.DFVSGames.Foundations.Hastad.validDecoderSuccess_le_response line 417
  36. theorem OAI.DFVSGames.Foundations.Hastad.conditioned_folded_response_bound line 434
  37. theorem OAI.DFVSGames.Foundations.Hastad.distribution_sq_expectation_le line 455
  38. def OAI.DFVSGames.Foundations.Hastad.projectionGame line 485
  39. def OAI.DFVSGames.Foundations.Hastad.questionBias line 490
  40. def OAI.DFVSGames.Foundations.Hastad.questionAcceptance line 494
  41. theorem OAI.DFVSGames.Foundations.Hastad.questionAcceptance_eq line 499
  42. inductive OAI.DFVSGames.Foundations.Hastad.ConditionedOracle line 510
  43. def OAI.DFVSGames.Foundations.Hastad.ConditionedOracle.answer line 514
  44. def OAI.DFVSGames.Foundations.Hastad.ConditionedOracle.fallback line 518
  45. theorem OAI.DFVSGames.Foundations.Hastad.testBias_constant_right line 524
  46. theorem OAI.DFVSGames.Foundations.Hastad.empty_conditioned_bias line 531
  47. theorem OAI.DFVSGames.Foundations.Hastad.conditionedOracle_response_bound line 541
  48. theorem OAI.DFVSGames.Foundations.Hastad.folded_game_decoder_bound line 561
  49. theorem OAI.DFVSGames.Foundations.Hastad.conditionedOracle_game_decoder_bound line 599
  50. theorem OAI.DFVSGames.Foundations.Hastad.conditionedOracle_acceptance_bound line 635
  51. def OAI.DFVSGames.Foundations.Games.FiniteDistribution.reindexEquiv line 663
  52. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.pushforward_equiv line 669
  53. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.table_const_reindex line 687
  54. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.iid_reindex line 700
  55. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_reindex_of_weight line 711
  56. def OAI.DFVSGames.Foundations.Games.Game.questionReindexEquiv line 730
  57. def OAI.DFVSGames.Foundations.Games.Game.reindexStrategy line 735
  58. theorem OAI.DFVSGames.Foundations.Games.Game.repetition_question_weight_reindex line 741
  59. theorem OAI.DFVSGames.Foundations.Games.Game.repetition_questions_reindex line 752
  60. theorem OAI.DFVSGames.Foundations.Games.Game.coordinateWin_reindex line 765
  61. theorem OAI.DFVSGames.Foundations.Games.Game.selectedWins_reindex line 783
  62. theorem OAI.DFVSGames.Foundations.Games.Game.selectedSuccess_reindex line 803
  63. theorem OAI.DFVSGames.Foundations.Games.Game.repetition_success_reindex line 818