OAI/Combinatorics/Progressions/Estimates/SmoothPairErrorLogBounds.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.uniform_pair_sum line 13
2. theorem OAI.Erdos3.uniform_joint_residual_bound line 23
3. theorem OAI.Erdos3.smoothSource_pair_kernel_reduction line 102
4. theorem OAI.Erdos3.fullSmoothPairError_nonneg line 160
5. theorem OAI.Erdos3.canonical_smooth_pair_correlation line 170
6. def OAI.Erdos3.smoothPairErrorCoefficient line 246
7. theorem OAI.Erdos3.smoothPairErrorCoefficient_nonneg line 249
8. theorem OAI.Erdos3.smoothPairProbabilityError_mul line 253
9. theorem OAI.Erdos3.fullSmoothPairError_le_linear line 258
10. theorem OAI.Erdos3.smoothPairRowLipschitz_le_exp line 286
11. theorem OAI.Erdos3.smoothPairScaleRatio_le_exp line 302
12. theorem OAI.Erdos3.smoothPairQuadraticFactor_le_exp line 311
13. theorem OAI.Erdos3.smoothPairProbabilityCap_le_exp line 321
14. theorem OAI.Erdos3.smoothPairKernelBaseCap_le_exp line 336
15. theorem OAI.Erdos3.smoothPairKernelBaseLip_le_exp line 346
16. theorem OAI.Erdos3.smoothPairKernelCap_le_exp line 358
17. theorem OAI.Erdos3.smoothPairKernelLip_le_exp line 366
18. theorem OAI.Erdos3.smoothPair_pivot_card line 389
19. theorem OAI.Erdos3.smoothPairRowLipschitz_pivot line 392
20. theorem OAI.Erdos3.smoothPairProbabilityError_pivot line 395
21. theorem OAI.Erdos3.smoothPairProbabilityCap_pivot line 399
22. theorem OAI.Erdos3.fullSmoothPairError_pivot line 403
23. theorem OAI.Erdos3.smoothPairKernelCap_pivot line 407
24. theorem OAI.Erdos3.smoothPairKernelLip_pivot line 411
25. def OAI.Erdos3.smoothPairRowErrorLog line 426
26. theorem OAI.Erdos3.smoothPairRowErrorLog_nonneg line 429
27. theorem OAI.Erdos3.smoothPairProbabilityError_one_le_exp line 434
28. def OAI.Erdos3.smoothPairErrorLog line 458
29. theorem OAI.Erdos3.smoothPairErrorLog_nonneg line 461
30. theorem OAI.Erdos3.smoothPairErrorCoefficient_le_exp line 467
31. theorem OAI.Erdos3.smoothPairMeshCoefficient_le_exp line 497