OAI/Combinatorics/Progressions/Linear/AllocatedKernelReplacementWithCutoff.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.allocatedKernelLogWithCutoff line 11
2. theorem OAI.Erdos3.allocatedKernelLogWithCutoff_bounds line 16
3. theorem OAI.Erdos3.allocatedKernelLogWithCutoff_allowances line 36
4. def OAI.Erdos3.VectorPolynomial.allocatedKernelReplacementLogWithCutoff line 62
5. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelReplacementLogWithCutoff_front_le line 68
6. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedKernel_replacement_withCutoff line 105
7. theorem OAI.Erdos3.VectorPolynomial.allocatedGoodKernel_replacement_withCutoff line 181