OAI/Combinatorics/Progressions/Linear/AllocatedJointAmbientKernel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.coefficientJointAmbientKernel line 19
2. theorem OAI.Erdos3.VectorPolynomial.coefficientJointAmbientKernel_support line 25
3. theorem OAI.Erdos3.VectorPolynomial.coefficientJointAmbientKernel_bounds line 32
4. def OAI.Erdos3.VectorPolynomial.allocatedCoefficientJointAmbientKernel line 86
5. theorem OAI.Erdos3.VectorPolynomial.allocatedAmbientKernelFactor_bounds line 92
6. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientJointAmbientKernel_bounds line 127
7. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientJointAmbientKernel_support line 140