OAI/Combinatorics/Progressions/Geometry/WeightedTranslationBufferedCoordinates.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.PolynomialTranslationLie.weightedShearEmbedding_coordinate_row line 13
2. theorem OAI.Erdos3.realificationLieHom_repr_zero line 77
3. theorem OAI.Erdos3.realificationLieHom_repr_coordinate line 84
4. theorem OAI.Erdos3.PolynomialTranslationLie.realShearEmbedding_repr line 107
5. theorem OAI.Erdos3.PolynomialTranslationLie.realShearEmbedding_coordinate_row line 115
6. theorem OAI.Erdos3.PolynomialTranslationLie.realShearEmbedding_coordinate_abs_le line 134
7. theorem OAI.Erdos3.PolynomialTranslationLie.realShearEmbedding_coefficient_abs_le line 146
8. theorem OAI.Erdos3.PolynomialTranslationLie.bchRealTranslation_inverse_action_X line 173
9. theorem OAI.Erdos3.PolynomialTranslationLie.bchRealTranslation_bounds_of_shear_coordinates line 189
10. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_real_log_coordinates_bound line 241
11. def OAI.Erdos3.PolynomialTranslationLie.weightedTranslationDisplacementConstant line 275
12. theorem OAI.Erdos3.PolynomialTranslationLie.weightedTranslationDisplacementConstant_pos line 279
13. theorem OAI.Erdos3.PolynomialTranslationLie.bchRealTranslation_bounds_near_one line 284
14. theorem OAI.Erdos3.PolynomialTranslationLie.buffered_translation_term_of_shear_coordinates line 347