OAI/Computability/BinPacking/Expanders/LazySmoothing.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.PCP.LazySmoothing.bitCount line 18
2. def OAI.BinPackingGames.Foundations.PCP.LazySmoothing.binomialMean line 21
3. def OAI.BinPackingGames.Foundations.PCP.LazySmoothing.splitTape line 24
4. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.bitCount_succ line 32
5. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.mean_congr line 36
6. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.mean_const line 41
7. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.mean_add line 44
8. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.mean_sub line 48
9. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.mean_mul line 52
10. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.mean_zero line 56
11. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.expect_bool line 59
12. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.mean_succ line 63
13. def OAI.BinPackingGames.Foundations.PCP.LazySmoothing.score line 74
14. def OAI.BinPackingGames.Foundations.PCP.LazySmoothing.scoreMean line 76
15. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.scoreMean_zero line 79
16. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.scoreMean_succ line 82
17. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.score_identity line 101
18. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.score_mean_zero line 111
19. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.score_second_moment line 118
20. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.score_difference line 137
21. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.adjacent_difference_sq line 143
22. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.adjacent_difference_le line 177
23. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.mean_shift_le line 190
24. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.mean_ordered_difference_le line 209
25. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.mean_window_le line 215
26. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.square_window_le line 237
27. theorem OAI.BinPackingGames.Foundations.PCP.LazySmoothing.modal_transfer line 263