OAI/Computability/DirectedFeedback/Analysis/PrivateFourier.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Decoder.PrivateFourier.sign line 20
  2. theorem OAI.DFVSGames.Decoder.PrivateFourier.sign_zero line 22
  3. theorem OAI.DFVSGames.Decoder.PrivateFourier.sign_one line 23
  4. theorem OAI.DFVSGames.Decoder.PrivateFourier.sign_sq line 25
  5. theorem OAI.DFVSGames.Decoder.PrivateFourier.sign_abs line 28
  6. theorem OAI.DFVSGames.Decoder.PrivateFourier.sign_add line 31
  7. theorem OAI.DFVSGames.Decoder.PrivateFourier.sign_add_one line 34
  8. theorem OAI.DFVSGames.Decoder.PrivateFourier.binary_neg_eq_self line 45
  9. theorem OAI.DFVSGames.Decoder.PrivateFourier.binary_add_eq_zero_iff line 51
  10. theorem OAI.DFVSGames.Decoder.PrivateFourier.average_sign_dual line 54
  11. theorem OAI.DFVSGames.Decoder.PrivateFourier.average_sign_primal line 60
  12. theorem OAI.DFVSGames.Decoder.PrivateFourier.average_sign_equality line 66
  13. theorem OAI.DFVSGames.Decoder.PrivateFourier.trivial_restriction_probability line 72
  14. theorem OAI.DFVSGames.Decoder.PrivateFourier.trivial_restriction_probability_pow line 93
  15. def OAI.DFVSGames.Decoder.PrivateFourier.tableSign line 115
  16. def OAI.DFVSGames.Decoder.PrivateFourier.frequencyWeight line 118
  17. theorem OAI.DFVSGames.Decoder.PrivateFourier.frequencyWeight_nonneg line 122
  18. theorem OAI.DFVSGames.Decoder.PrivateFourier.tableSign_frequencyWeight_sum line 125
  19. theorem OAI.DFVSGames.Decoder.PrivateFourier.tableSign_antifold line 132
  20. theorem OAI.DFVSGames.Decoder.PrivateFourier.linearCoeff_translate line 142
  21. theorem OAI.DFVSGames.Decoder.PrivateFourier.positive_frequency_first_bit line 159
  22. def OAI.DFVSGames.Decoder.PrivateFourier.frequencyCoset line 191
  23. def OAI.DFVSGames.Decoder.PrivateFourier.sliceCorrelation line 194
  24. theorem OAI.DFVSGames.Decoder.PrivateFourier.traceCharacter_re_mul line 200
  25. theorem OAI.DFVSGames.Decoder.PrivateFourier.sliceCorrelation_eq_coset line 206
  26. theorem OAI.DFVSGames.Decoder.PrivateFourier.sliceCorrelation_sq_le_coset_mass line 231
  27. theorem OAI.DFVSGames.Decoder.PrivateFourier.target_character line 259
  28. theorem OAI.DFVSGames.Decoder.PrivateFourier.affine_equality_character_expansion line 269
  29. theorem OAI.DFVSGames.Decoder.PrivateFourier.sliceCorrelation_tableSign_abs_le_one line 298
  30. theorem OAI.DFVSGames.Decoder.PrivateFourier.agreement_le_average_abs_correlation line 315
  31. theorem OAI.DFVSGames.Decoder.PrivateFourier.frequencyCoset_card line 339
  32. theorem OAI.DFVSGames.Decoder.PrivateFourier.frequencyCoset_card_le line 353
  33. theorem OAI.DFVSGames.Decoder.PrivateFourier.remove_bad_characters line 368
  34. theorem OAI.DFVSGames.Decoder.PrivateFourier.average_coset_mass_lower line 385
  35. theorem OAI.DFVSGames.Decoder.PrivateFourier.contraction_mem_target_coset line 414
  36. theorem OAI.DFVSGames.Decoder.PrivateFourier.uniform_preimage_probability line 437
  37. theorem OAI.DFVSGames.Decoder.PrivateFourier.independent_agreement_lower line 451
  38. def OAI.DFVSGames.Decoder.PrivateStrategy.candidates line 495
  39. theorem OAI.DFVSGames.Decoder.PrivateStrategy.mem_candidates line 498
  40. theorem OAI.DFVSGames.Decoder.PrivateStrategy.candidates_nonempty line 501
  41. theorem OAI.DFVSGames.Decoder.PrivateStrategy.candidates_card_le line 505
  42. theorem OAI.DFVSGames.Decoder.PrivateStrategy.candidates_card_le_pow line 517
  43. theorem OAI.DFVSGames.Decoder.PrivateStrategy.candidate_preimage line 529
  44. theorem OAI.DFVSGames.Decoder.PrivateStrategy.exists_unit line 553
  45. def OAI.DFVSGames.Decoder.PrivateStrategy.chooseUnit line 563
  46. theorem OAI.DFVSGames.Decoder.PrivateStrategy.chooseUnit_spec line 567
  47. abbrev OAI.DFVSGames.Decoder.PrivateStrategy.ActualAnswer line 570
  48. def OAI.DFVSGames.Decoder.PrivateStrategy.privateSeedLaw line 572
  49. theorem OAI.DFVSGames.Decoder.PrivateStrategy.privateSeedLaw_expectation line 582
  50. def OAI.DFVSGames.Decoder.PrivateStrategy.privateOutput line 591
  51. theorem OAI.DFVSGames.Decoder.PrivateStrategy.privateOutput_eq_contraction line 599
  52. def OAI.DFVSGames.Decoder.PrivateStrategy.privateLaw line 612
  53. theorem OAI.DFVSGames.Decoder.PrivateStrategy.privateLaw_expectation line 617
  54. def OAI.DFVSGames.Decoder.PrivateStrategy.candidateLaw line 631
  55. theorem OAI.DFVSGames.Decoder.PrivateStrategy.candidateLaw_expectation line 638
  56. def OAI.DFVSGames.Decoder.PrivateStrategy.conditionalAgreement line 662
  57. theorem OAI.DFVSGames.Decoder.PrivateStrategy.conditionalAgreement_eq_sum line 669
  58. def OAI.DFVSGames.Decoder.PrivateStrategy.goodCosetMass line 697
  59. theorem OAI.DFVSGames.Decoder.PrivateStrategy.goodCosetMass_nonneg line 705
  60. theorem OAI.DFVSGames.Decoder.PrivateStrategy.good_frequency_preimage line 717
  61. theorem OAI.DFVSGames.Decoder.PrivateStrategy.conditionalAgreement_ge_mass_div_card line 736
  62. theorem OAI.DFVSGames.Decoder.PrivateStrategy.goodCosetMass_lower_from_slice line 773
  63. theorem OAI.DFVSGames.Decoder.PrivateStrategy.conditionalAgreement_from_slice line 842