OAI/Combinatorics/Progressions/Lattices/EarlyAllocatedAffineCoveredSourceWithCutoff.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineCoefficient_from_reference_l1_withCutoff line 22
2. def OAI.Erdos3.VectorPolynomial.AllocatedAffineCoefficientComparisonWithCutoff line 139
3. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineCoefficientComparison_of_reference_withCutoff line 208
4. theorem OAI.Erdos3.VectorPolynomial.exists_early_allocated_affine_coefficient_source_withCutoff line 232
5. def OAI.Erdos3.VectorPolynomial.AllocatedAffineCoveredComparisonWithCutoff line 272
6. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineCoveredComparison_of_coefficient_withCutoff line 353
7. theorem OAI.Erdos3.VectorPolynomial.exists_early_allocated_affine_covered_source_withCutoff line 380