OAI/Combinatorics/Progressions/Lattices/AllocatedSupportedAffineAccurateSource.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_global_masked_affine_ideal_approximation line 71
2. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_supported_affine_ideal_model line 215
3. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_supported_affine_source_model line 380
4. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_supported_affine_uniform_source_model line 527
5. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_supported_affine_uniform_physical_source line 733
6. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_supported_affine_good_kernel_source line 954
7. def OAI.Erdos3.VectorPolynomial.affineSourceSum line 1121
8. theorem OAI.Erdos3.VectorPolynomial.affineSource_sum_eq line 1124
9. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_supported_affine_accurate_source line 1189