OAI/Combinatorics/Progressions/Estimates/ShiftedSmoothSelectedMarginal.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.pmf_map_finite_sum line 14
2. theorem OAI.Erdos3.pmf_image_finite_expectation line 21
3. theorem OAI.Erdos3.pmf_image_finite_test_error line 42
4. theorem OAI.Erdos3.pmf_image_finite_real_mean line 73
5. theorem OAI.Erdos3.pmf_image_energy_of_point_cap line 91
6. theorem OAI.Erdos3.pmf_map_add_right line 121
7. theorem OAI.Erdos3.pmf_map_image_add_right line 126
8. theorem OAI.Erdos3.pmf_image_shifted_finite_expectation line 132
9. theorem OAI.Erdos3.pmf_image_shifted_finite_test_error line 140
10. theorem OAI.Erdos3.shiftedSmoothProductMass_coordinate_pos line 160
11. theorem OAI.Erdos3.shiftedSmoothProductPMF_eq_independent line 171
12. theorem OAI.Erdos3.shiftedSmoothProductPMF_base_cap line 183
13. theorem OAI.Erdos3.smoothProbabilityProfile_inner_lower line 206
14. theorem OAI.Erdos3.shiftedSmoothCoefficientPMF_inner_lower line 218
15. theorem OAI.Erdos3.shiftedSmoothProductPMF_inner_lower line 232
16. theorem OAI.Erdos3.shiftedSmoothProductPMF_inner_mass line 245
17. theorem OAI.Erdos3.smoothProductPMF_eq_independent line 267
18. theorem OAI.Erdos3.smoothProductPMF_rows line 274
19. theorem OAI.Erdos3.shiftedSmoothProductMass_restrict_pos line 290
20. theorem OAI.Erdos3.shiftedSmoothProductPMF_selected_factorization line 297
21. def OAI.Erdos3.smoothInputSplit line 328
22. def OAI.Erdos3.smoothInputJoin line 331
23. theorem OAI.Erdos3.smoothInputSplit_join line 334
24. theorem OAI.Erdos3.smoothInputJoin_split line 338
25. theorem OAI.Erdos3.smoothInputSplit_injective line 344
26. theorem OAI.Erdos3.smoothInputSplit_law line 350
27. theorem OAI.Erdos3.pmf_map_finite_expectation line 380
28. theorem OAI.Erdos3.shiftedSmoothProductPMF_selected_marginal line 397
29. theorem OAI.Erdos3.shiftedSmoothProductPMF_selected_map line 407
30. theorem OAI.Erdos3.shiftedSmoothProductPMF_selected_expectation line 417