OAI/Combinatorics/IndependentSets/Fourier/EmptyContext.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Hastad.mapEquation line 11
  2. theorem OAI.IndependentSetsGames.Foundations.Hastad.satisfied_mapEquation line 18
  3. abbrev OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.Address line 26
  4. def OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.storedAssignment line 28
  5. def OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.equation line 31
  6. theorem OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.equation_second_eq_third line 37
  7. theorem OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.equation_satisfied line 40
  8. theorem OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.equation_storedAssignment_satisfied line 48
  9. theorem OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.equation_flip_first line 53
  10. theorem OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.equation_flip_rhs line 58
  11. theorem OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.equation_satisfied_flip line 61
  12. def OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.pairedEquations line 67
  13. theorem OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.pairedEquations_length line 70
  14. theorem OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.pairedEquations_ne_nil line 73
  15. theorem OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.pairedEquations_acceptedCount line 76
  16. theorem OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.pairedEquations_failureCount line 82
  17. def OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.equationAcceptance line 92
  18. def OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.equationBias line 95
  19. theorem OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.foldedMean_eq_zero line 98
  20. theorem OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.equation_indicator line 103
  21. theorem OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.equationAcceptance_eq_half line 109
  22. theorem OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.equationBias_eq_zero line 116
  23. theorem OAI.IndependentSetsGames.Foundations.Hastad.EmptyContext.mapped_equationAcceptance_eq_half line 127