OAI/Combinatorics/Progressions/Estimates/ControlledLinearSubspaceLift.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_block_subspace_defining_matrix line 13
2. theorem OAI.Erdos3.exists_controlled_weighted_linear_splitting line 53
3. theorem OAI.Erdos3.exists_controlled_constraint_section line 111
4. def OAI.Erdos3.jointMatrixImages line 198
5. theorem OAI.Erdos3.jointMatrixImages_grid line 201
6. theorem OAI.Erdos3.jointMatrixImages_equation line 223
7. theorem OAI.Erdos3.exists_joint_weighted_corrections line 239
8. theorem OAI.Erdos3.exists_controlled_block_subspace_lift line 317
9. theorem OAI.Erdos3.exists_block_subspace_corrections line 383
10. theorem OAI.Erdos3.exists_controlled_linear_subspace_lift line 454