OAI/Combinatorics/Progressions/Estimates/PreparedEnlargedModularAllocation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.preparedInitialRankSpatialEmbedding line 16
2. def OAI.Erdos3.VectorPolynomial.preparedInitialRankKernelEmbedding line 21
3. def OAI.Erdos3.VectorPolynomial.preparedInitialRankPrincipalEmbedding line 26
4. theorem OAI.Erdos3.VectorPolynomial.preparedInitialRank_layer_card line 47
5. theorem OAI.Erdos3.VectorPolynomial.preparedInitialRank_dimension_le line 52
6. theorem OAI.Erdos3.VectorPolynomial.preparedInitialRank_output_dimension_le line 64
7. theorem OAI.Erdos3.VectorPolynomial.preparedInitialRank_parameters line 73
8. theorem OAI.Erdos3.VectorPolynomial.preparedInitialRank_smooth_card_le line 85