OAI/Combinatorics/Progressions/Geometry/MultilinearBoxInverse.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.stridedMatrixPoint line 12
2. def OAI.Erdos3.stridedMatrixSliceBase line 16
3. theorem OAI.Erdos3.stridedMatrixPoint_update line 20
4. theorem OAI.Erdos3.multilinear_box_biased_slice line 43
5. theorem OAI.Erdos3.multilinear_box_coordinate_approximation line 83
6. theorem OAI.Erdos3.paired_multilinear_box_coordinate_approximation line 101