OAI/Computability/VertexCover/PCP/LazySmoothing.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.PCP.LazySmoothing.bitCount line 9
  2. def OAI.UniqueGames.Foundations.PCP.LazySmoothing.binomialMean line 12
  3. def OAI.UniqueGames.Foundations.PCP.LazySmoothing.splitTape line 15
  4. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.bitCount_succ line 23
  5. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.mean_congr line 27
  6. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.mean_const line 32
  7. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.mean_add line 35
  8. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.mean_sub line 39
  9. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.mean_mul line 43
  10. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.mean_zero line 47
  11. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.expect_bool line 50
  12. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.mean_succ line 54
  13. def OAI.UniqueGames.Foundations.PCP.LazySmoothing.score line 65
  14. def OAI.UniqueGames.Foundations.PCP.LazySmoothing.scoreMean line 67
  15. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.scoreMean_zero line 70
  16. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.scoreMean_succ line 73
  17. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.score_identity line 92
  18. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.score_mean_zero line 102
  19. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.score_second_moment line 109
  20. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.score_difference line 128
  21. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.adjacent_difference_sq line 134
  22. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.adjacent_difference_le line 168
  23. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.mean_shift_le line 181
  24. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.mean_ordered_difference_le line 200
  25. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.mean_window_le line 206
  26. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.square_window_le line 228
  27. theorem OAI.UniqueGames.Foundations.PCP.LazySmoothing.modal_transfer line 254