OAI/Computability/BinPacking/Information/EmptyContext.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.Address line 15
  2. def OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.storedAssignment line 17
  3. def OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.rhsCorrection line 21
  4. theorem OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.correction_eq line 24
  5. def OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.equation line 31
  6. theorem OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.xor_corrections line 38
  7. theorem OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.equation_satisfied line 43
  8. theorem OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.equation_satisfied_iff line 54
  9. theorem OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.equation_indicator line 63
  10. theorem OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.satisfied_repeated_right line 74
  11. theorem OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.equation_repeated_right line 81
  12. theorem OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.restrict_thirdQuery line 90
  13. def OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.conditionedEquation line 96
  14. theorem OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.conditionedEquation_rhs line 101
  15. theorem OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.conditionedEquation_satisfied line 106
  16. theorem OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.conditionedEquation_satisfied_iff line 117
  17. theorem OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.conditionedEquation_indicator line 127
  18. theorem OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.conditionedEquation_repeated_right line 139
  19. def OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.equationAcceptance line 152
  20. theorem OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.equationAcceptance_eq line 158
  21. def OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.conditionedEquationAcceptance line 165
  22. theorem OAI.BinPackingGames.Foundations.Hastad.FoldedEquation.conditionedEquationAcceptance_eq line 172
  23. def OAI.BinPackingGames.Foundations.Hastad.mapEquation line 188
  24. theorem OAI.BinPackingGames.Foundations.Hastad.satisfied_mapEquation line 195
  25. abbrev OAI.BinPackingGames.Foundations.Hastad.EmptyContext.Address line 203
  26. def OAI.BinPackingGames.Foundations.Hastad.EmptyContext.storedAssignment line 205
  27. def OAI.BinPackingGames.Foundations.Hastad.EmptyContext.equation line 208
  28. theorem OAI.BinPackingGames.Foundations.Hastad.EmptyContext.equation_second_eq_third line 214
  29. theorem OAI.BinPackingGames.Foundations.Hastad.EmptyContext.equation_satisfied line 217
  30. theorem OAI.BinPackingGames.Foundations.Hastad.EmptyContext.equation_storedAssignment_satisfied line 225
  31. theorem OAI.BinPackingGames.Foundations.Hastad.EmptyContext.equation_flip_first line 230
  32. theorem OAI.BinPackingGames.Foundations.Hastad.EmptyContext.equation_flip_rhs line 235
  33. theorem OAI.BinPackingGames.Foundations.Hastad.EmptyContext.equation_satisfied_flip line 238
  34. def OAI.BinPackingGames.Foundations.Hastad.EmptyContext.pairedEquations line 244
  35. theorem OAI.BinPackingGames.Foundations.Hastad.EmptyContext.pairedEquations_length line 247
  36. theorem OAI.BinPackingGames.Foundations.Hastad.EmptyContext.pairedEquations_ne_nil line 250
  37. theorem OAI.BinPackingGames.Foundations.Hastad.EmptyContext.pairedEquations_acceptedCount line 253
  38. theorem OAI.BinPackingGames.Foundations.Hastad.EmptyContext.pairedEquations_failureCount line 259
  39. def OAI.BinPackingGames.Foundations.Hastad.EmptyContext.equationAcceptance line 267
  40. def OAI.BinPackingGames.Foundations.Hastad.EmptyContext.equationBias line 270
  41. theorem OAI.BinPackingGames.Foundations.Hastad.EmptyContext.foldedMean_eq_zero line 273
  42. theorem OAI.BinPackingGames.Foundations.Hastad.EmptyContext.equation_indicator line 278
  43. theorem OAI.BinPackingGames.Foundations.Hastad.EmptyContext.equationAcceptance_eq_half line 284
  44. theorem OAI.BinPackingGames.Foundations.Hastad.EmptyContext.equationBias_eq_zero line 291
  45. theorem OAI.BinPackingGames.Foundations.Hastad.EmptyContext.mapped_equationAcceptance_eq_half line 302