OAI/Combinatorics/IndependentSets/Expansion/LazySmoothing.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.bitCount line 10
  2. def OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.binomialMean line 13
  3. def OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.splitTape line 16
  4. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.bitCount_succ line 24
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.mean_congr line 28
  6. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.mean_const line 33
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.mean_add line 36
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.mean_sub line 40
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.mean_mul line 44
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.mean_zero line 48
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.expect_bool line 51
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.mean_succ line 55
  13. def OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.score line 66
  14. def OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.scoreMean line 68
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.scoreMean_zero line 71
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.scoreMean_succ line 74
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.score_identity line 93
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.score_mean_zero line 103
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.score_second_moment line 110
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.score_difference line 129
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.adjacent_difference_sq line 135
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.adjacent_difference_le line 169
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.mean_shift_le line 182
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.mean_ordered_difference_le line 201
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.mean_window_le line 207
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.square_window_le line 229
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.LazySmoothing.modal_transfer line 255