OAI/Analysis/IrrationalRotation/Sampling/ProductSamplingJointMeasurable.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.continuous_rotationIterate_joint line 12
2. theorem OAI.Invariant233.ProductModel.measurable_rotationIterate_joint line 17
3. theorem OAI.Invariant233.ProductModel.SamplingWeights.measurable_orbitWeight_inverse_joint line 23
4. theorem OAI.Invariant233.ProductModel.SamplingWeights.measurable_orbitTestWeight_joint line 32
5. theorem OAI.Invariant233.ProductModel.SamplingWeights.measurable_orbitTestWeight_inverse_joint line 41
6. theorem OAI.Invariant233.ProductModel.SamplingWeights.measurable_firstTestAverage_joint line 51
7. theorem OAI.Invariant233.ProductModel.SamplingWeights.measurable_secondTestAverage_joint line 59
8. theorem OAI.Invariant233.ProductModel.SamplingWeights.measurable_spatialSquaredError line 67