OAI/Combinatorics/Progressions/Linear/CanonicalKernelSlowParameter.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.canonicalKernelSlowMap line 14
2. theorem OAI.Erdos3.canonicalKernelSlowMap_measurable line 19
3. theorem OAI.Erdos3.canonicalKernelSlowMap_parameter_lipschitz line 24
4. theorem OAI.Erdos3.canonicalKernelSlowMap_eq line 61
5. def OAI.Erdos3.canonicalKernelSlowExpectation line 80
6. theorem OAI.Erdos3.canonicalKernelSlowExpectation_norm_le line 84
7. theorem OAI.Erdos3.canonicalKernelSlowExpectation_lipschitz line 92
8. theorem OAI.Erdos3.canonicalKernelSlowExpectation_eq line 115