OAI/Combinatorics/Progressions/Estimates/DerivativeHorizontalLifts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Erdos3.RationalHorizontalLift line 13
2. theorem OAI.Erdos3.exists_basis_linear_lift line 46
3. theorem OAI.Erdos3.euclideanVerticalMap_norm_eq line 59
4. theorem OAI.Erdos3.graph_derivative_decomposition line 82
5. theorem OAI.Erdos3.assemble_rational_horizontal_lift line 137
6. theorem OAI.Erdos3.indexed_derivative_decomposition line 220
7. theorem OAI.Erdos3.euclideanDerivative_horizontal_norm_bound line 268
8. theorem OAI.Erdos3.euclideanDerivative_horizontal_lifts line 336