OAI/Computability/MaxCut/Gadgets/Polynomial.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.OptimalMaxCut.BooleanFourthMoment.sum_cube_succ line 11
  2. theorem OAI.OptimalMaxCut.BooleanFourthMoment.expect_cube_succ line 16
  3. theorem OAI.OptimalMaxCut.BooleanFourthMoment.expect_bool line 23
  4. def OAI.OptimalMaxCut.BooleanFourthMoment.polynomial line 27
  5. def OAI.OptimalMaxCut.BooleanFourthMoment.energy line 30
  6. theorem OAI.OptimalMaxCut.BooleanFourthMoment.energy_nonneg line 34
  7. theorem OAI.OptimalMaxCut.BooleanFourthMoment.walsh_cons line 43
  8. theorem OAI.OptimalMaxCut.BooleanFourthMoment.polynomial_cons line 47
  9. theorem OAI.OptimalMaxCut.BooleanFourthMoment.energy_cons line 59
  10. theorem OAI.OptimalMaxCut.BooleanFourthMoment.fourth_moment_cons line 69
  11. theorem OAI.OptimalMaxCut.BooleanFourthMoment.fourth_moment_bound line 82
  12. theorem OAI.OptimalMaxCut.BooleanFourthMoment.weight_eq_degree line 111
  13. theorem OAI.OptimalMaxCut.BooleanFourthMoment.energy_truncated line 115
  14. theorem OAI.OptimalMaxCut.BooleanFourthMoment.coefficient_polynomial line 127
  15. theorem OAI.OptimalMaxCut.BooleanFourthMoment.polynomial_second_moment line 135
  16. theorem OAI.OptimalMaxCut.BooleanFourthMoment.degree_fourth_moment_bound line 140
  17. theorem OAI.OptimalMaxCut.BooleanFourthMoment.degree_third_moment_bound line 147
  18. theorem OAI.OptimalMaxCut.BooleanFourthMoment.walsh_flip line 169
  19. def OAI.OptimalMaxCut.BooleanFourthMoment.discreteDiff line 181
  20. theorem OAI.OptimalMaxCut.BooleanFourthMoment.polynomial_diff line 184
  21. theorem OAI.OptimalMaxCut.BooleanFourthMoment.total_diff_second line 193
  22. theorem OAI.OptimalMaxCut.BooleanFourthMoment.total_diff_second_truncated line 205
  23. theorem OAI.OptimalMaxCut.BooleanFourthMoment.total_diff_third_truncated line 216