OAI/Combinatorics/IndependentSets/Fourier/Decoder.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Hastad.parityProjection line 15
  2. theorem OAI.IndependentSetsGames.Foundations.Hastad.walsh_support line 18
  3. theorem OAI.IndependentSetsGames.Foundations.Hastad.sign_power_parity line 26
  4. theorem OAI.IndependentSetsGames.Foundations.Hastad.walsh_pullback line 36
  5. theorem OAI.IndependentSetsGames.Foundations.Hastad.projectedCoefficient_eq line 46
  6. theorem OAI.IndependentSetsGames.Foundations.Hastad.projection_has_preimage line 51
  7. theorem OAI.IndependentSetsGames.Foundations.Hastad.scaled_geometric_power_le_one line 63
  8. theorem OAI.IndependentSetsGames.Foundations.Hastad.noise_decay_bound line 77
  9. def OAI.IndependentSetsGames.Foundations.Hastad.zeroMask line 90
  10. theorem OAI.IndependentSetsGames.Foundations.Hastad.support_eq_empty_iff line 93
  11. theorem OAI.IndependentSetsGames.Foundations.Hastad.parityProjection_zero line 105
  12. def OAI.IndependentSetsGames.Foundations.Hastad.agreementProbability line 110
  13. theorem OAI.IndependentSetsGames.Foundations.Hastad.agreementProbability_nonneg line 115
  14. theorem OAI.IndependentSetsGames.Foundations.Hastad.agreementProbability_projection line 123
  15. def OAI.IndependentSetsGames.Foundations.Hastad.decoderSuccess line 149
  16. def OAI.IndependentSetsGames.Foundations.Hastad.decodingEnergy line 153
  17. theorem OAI.IndependentSetsGames.Foundations.Hastad.decodingEnergy_le_success line 156
  18. theorem OAI.IndependentSetsGames.Foundations.Hastad.bias_sq_le_weighted_energy line 190
  19. theorem OAI.IndependentSetsGames.Foundations.Hastad.decoder_four_epsilon_bias_sq line 207
  20. theorem OAI.IndependentSetsGames.Foundations.Hastad.folded_decoder_bound line 233
  21. def OAI.IndependentSetsGames.Foundations.Hastad.validAgreementProbability line 241
  22. theorem OAI.IndependentSetsGames.Foundations.Hastad.validAgreementProbability_eq line 248
  23. def OAI.IndependentSetsGames.Foundations.Hastad.validDecoderSuccess line 261
  24. theorem OAI.IndependentSetsGames.Foundations.Hastad.conditioned_validDecoderSuccess line 267
  25. theorem OAI.IndependentSetsGames.Foundations.Hastad.conditioned_folded_decoder_bound line 285