OAI/Analysis/IrrationalRotation/Sampling/ProductSamplingCylinderWeights.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Invariant233.ProductModel.SamplingWeights.cylinderSupport line 15
2. def OAI.Invariant233.ProductModel.SamplingWeights.cylinderCoordinateSet line 18
3. theorem OAI.Invariant233.ProductModel.SamplingWeights.cylinderCoordinateSet_empty line 21
4. theorem OAI.Invariant233.ProductModel.SamplingWeights.cylinderCoordinateSet_eq_univ_of_not_mem line 26
5. theorem OAI.Invariant233.ProductModel.SamplingWeights.measurableSet_cylinderCoordinateSet line 35
6. theorem OAI.Invariant233.ProductModel.SamplingWeights.cylinderCoordinateSet_normal_form line 47
7. theorem OAI.Invariant233.ProductModel.SamplingWeights.endpointCylinder_eq_rectangle line 73
8. theorem OAI.Invariant233.ProductModel.SamplingWeights.cylinder_orbitTestWeight_eq_first_product line 96
9. theorem OAI.Invariant233.ProductModel.SamplingWeights.cylinder_orbitTestWeight_eq_second_product line 106
10. theorem OAI.Invariant233.ProductModel.SamplingWeights.cylinderTestAverage_eq_product_average line 117
11. theorem OAI.Invariant233.ProductModel.SamplingWeights.eventually_cylinderSupport_subset_sourcePrefix line 127