OAI/Combinatorics/Progressions/Probability/PivotDensitySupport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.splitPivotDensity_formula line 14
2. theorem OAI.Erdos3.splitPivotDensity_displacement line 35
3. def OAI.Erdos3.spatialKernelErrorConstant line 89
4. theorem OAI.Erdos3.spatialKernelErrorConstant_nonneg line 92
5. theorem OAI.Erdos3.supported_column_displacement line 97
6. theorem OAI.Erdos3.normalizedSplitDensity_displacement line 106
7. theorem OAI.Erdos3.pivotOutputDensity_zero_outside line 138
8. theorem OAI.Erdos3.splitPivotDensity_zero_outside line 162