OAI/Combinatorics/Progressions/Estimates/AllocatedSlicedNormalizedNativeModel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.AllocatedModelPhysicalExpansionIdentity.common_cover line 64
2. theorem OAI.Erdos3.VectorPolynomial.AllocatedModelPhysicalExpansionIdentity.exists_large_source_term line 168
3. theorem OAI.Erdos3.VectorPolynomial.AllocatedModelPhysicalExpansionIdentity.exists_common_cover_source line 283
4. def OAI.Erdos3.VectorPolynomial.allocatedRecenteredFiniteModelSource line 418
5. theorem OAI.Erdos3.VectorPolynomial.AllocatedModelPhysicalExpansionIdentity.exists_twisted_common_cover_source line 428
6. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedRecenteredFactor_normalization line 507
7. theorem OAI.Erdos3.VectorPolynomial.AllocatedModelPhysicalExpansionIdentity.exists_native_source line 650
8. theorem OAI.Erdos3.VectorPolynomial.AllocatedModelPhysicalExpansionIdentity.exists_native_source_of_transfer line 822
9. theorem OAI.Erdos3.VectorPolynomial.AllocatedModelPhysicalExpansionIdentity.exists_normalized_native_source_of_transfer line 973
10. theorem OAI.Erdos3.VectorPolynomial.AllocatedModelPhysicalExpansionIdentity.exists_normalized_native_model_of_transfer line 1151
11. theorem OAI.Erdos3.VectorPolynomial.AllocatedModelPhysicalExpansionIdentity.exists_canonical_normalized_native_model_of_transfer line 1239
12. theorem OAI.Erdos3.VectorPolynomial.AllocatedModelPhysicalExpansionIdentity.exists_uniform_canonical_normalized_native_model_of_transfer line 1325