OAI/Analysis/IrrationalRotation/Operators/BlockedProjectionWindow.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.BlockedProductCoupling.measurable_sourceEvent line 14
2. theorem OAI.Invariant233.BlockedProductCoupling.ae_sourceEvent_coefficient_properties line 51
3. theorem OAI.Invariant233.BlockedProductCoupling.measurable_sourceCoefficientA line 104
4. theorem OAI.Invariant233.BlockedProductCoupling.measurable_sourceCoefficientB line 114
5. theorem OAI.Invariant233.BlockedProductCoupling.source_polynomial_sum_lower line 131
6. theorem OAI.Invariant233.BlockedProductCoupling.sourceEvent_integral_lower line 143
7. theorem OAI.Invariant233.BlockedProductCoupling.eventually_sourceEvent_and_integral_lower line 167