OAI/Computability/MinUncut/Encoding/Decoder.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Hastad.parityProjection line 16
  2. theorem OAI.MinUncutGames.Foundations.Hastad.walsh_support line 19
  3. theorem OAI.MinUncutGames.Foundations.Hastad.sign_power_parity line 27
  4. theorem OAI.MinUncutGames.Foundations.Hastad.walsh_pullback line 37
  5. theorem OAI.MinUncutGames.Foundations.Hastad.projectedCoefficient_eq line 47
  6. theorem OAI.MinUncutGames.Foundations.Hastad.projection_has_preimage line 52
  7. theorem OAI.MinUncutGames.Foundations.Hastad.scaled_geometric_power_le_one line 64
  8. theorem OAI.MinUncutGames.Foundations.Hastad.noise_decay_bound line 78
  9. def OAI.MinUncutGames.Foundations.Hastad.zeroMask line 91
  10. theorem OAI.MinUncutGames.Foundations.Hastad.support_eq_empty_iff line 94
  11. theorem OAI.MinUncutGames.Foundations.Hastad.parityProjection_zero line 106
  12. def OAI.MinUncutGames.Foundations.Hastad.agreementProbability line 111
  13. theorem OAI.MinUncutGames.Foundations.Hastad.agreementProbability_nonneg line 116
  14. theorem OAI.MinUncutGames.Foundations.Hastad.agreementProbability_projection line 124
  15. def OAI.MinUncutGames.Foundations.Hastad.decoderSuccess line 150
  16. def OAI.MinUncutGames.Foundations.Hastad.decodingEnergy line 154
  17. theorem OAI.MinUncutGames.Foundations.Hastad.decodingEnergy_le_success line 157
  18. theorem OAI.MinUncutGames.Foundations.Hastad.bias_sq_le_weighted_energy line 191
  19. theorem OAI.MinUncutGames.Foundations.Hastad.decoder_four_epsilon_bias_sq line 208
  20. theorem OAI.MinUncutGames.Foundations.Hastad.folded_decoder_bound line 234
  21. def OAI.MinUncutGames.Foundations.Hastad.validAgreementProbability line 242
  22. theorem OAI.MinUncutGames.Foundations.Hastad.validAgreementProbability_eq line 249
  23. def OAI.MinUncutGames.Foundations.Hastad.validDecoderSuccess line 262
  24. theorem OAI.MinUncutGames.Foundations.Hastad.conditioned_validDecoderSuccess line 268
  25. theorem OAI.MinUncutGames.Foundations.Hastad.conditioned_folded_decoder_bound line 286