OAI/Computability/MaxCut/Encoding/BitCube.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OptimalMaxCut.GaussianBellman.BitCube line 10
  2. def OAI.OptimalMaxCut.GaussianBellman.corrAverage line 12
  3. def OAI.OptimalMaxCut.GaussianBellman.midpointSection line 17
  4. def OAI.OptimalMaxCut.GaussianBellman.slopeSection line 20
  5. theorem OAI.OptimalMaxCut.GaussianBellman.section_decomposition line 23
  6. theorem OAI.OptimalMaxCut.GaussianBellman.midpointSection_mem line 27
  7. theorem OAI.OptimalMaxCut.GaussianBellman.expect_section line 34
  8. theorem OAI.OptimalMaxCut.GaussianBellman.corrAverage_mono line 45
  9. theorem OAI.OptimalMaxCut.GaussianBellman.corrAverage_add line 59
  10. theorem OAI.OptimalMaxCut.GaussianBellman.corrAverage_mul_const line 66
  11. theorem OAI.OptimalMaxCut.GaussianBellman.corrAverage_const_mul line 73
  12. theorem OAI.OptimalMaxCut.GaussianBellman.expect_zero_cube line 77
  13. theorem OAI.OptimalMaxCut.GaussianBellman.corrAverage_fst line 81
  14. theorem OAI.OptimalMaxCut.GaussianBellman.corrAverage_snd line 93
  15. def OAI.OptimalMaxCut.GaussianBellman.cubicCost line 105
  16. theorem OAI.OptimalMaxCut.GaussianBellman.finite_bellman_tensorization line 109
  17. def OAI.OptimalMaxCut.GaussianBellman.gradient line 137
  18. theorem OAI.OptimalMaxCut.GaussianBellman.gradient_cons_zero line 140
  19. theorem OAI.OptimalMaxCut.GaussianBellman.gradient_midpoint line 144
  20. theorem OAI.OptimalMaxCut.GaussianBellman.abs_midpoint_cube_le line 149
  21. theorem OAI.OptimalMaxCut.GaussianBellman.midpoint_cubic_contract line 157
  22. theorem OAI.OptimalMaxCut.GaussianBellman.gradient_zero_cubic line 164
  23. theorem OAI.OptimalMaxCut.GaussianBellman.cubicCost_le_gradients line 171
  24. theorem OAI.OptimalMaxCut.GaussianBellman.gradient_lipschitz line 186