OAI/Combinatorics/Progressions/Linear/LayerOneProjectionMatrixBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.rational_horizontal_basis_transport line 15
2. theorem OAI.Erdos3.NilpotentLieFiltration.layerOne_equiv_rational_matrix line 87
3. theorem OAI.Erdos3.NilpotentLieFiltration.layerOne_rational_kernel_basis line 98
4. theorem OAI.Erdos3.NilpotentLieFiltration.derivative_system_layerOne_rational_basis line 114
5. theorem OAI.Erdos3.NilpotentLieFiltration.layerOne_projection_matrix line 159
6. theorem OAI.Erdos3.NilpotentLieFiltration.layerOne_projection_grid line 165
7. theorem OAI.Erdos3.NilpotentLieFiltration.layerOne_projection_scaled_norm line 172