OAI/Analysis/IrrationalRotation/Product/ProductConvolutionIdentity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.ae_antitone_cocycleVersion line 13
2. theorem OAI.Invariant233.ProductModel.ae_convolution_two_ratio_bounds line 32
3. theorem OAI.Invariant233.ProductModel.coefficients_absolute_and_zero_of_pair line 57
4. theorem OAI.Invariant233.ProductModel.ae_coefficients_absolute_and_zero line 97
5. theorem OAI.Invariant233.ProductModel.ae_coefficients_absolute_sum_le line 125