OAI/Analysis/IrrationalRotation/Product/ProductIdealCylinderLimit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.IdealSampling.mem_frontier_preimage_of_continuousAt line 13
2. theorem OAI.Invariant233.ProductModel.IdealSampling.null_frontier_preimage_of_ae_continuousAt line 22
3. theorem OAI.Invariant233.ProductModel.IdealSampling.triangularLaw_coordinate_singleton line 31
4. theorem OAI.Invariant233.ProductModel.IdealSampling.triangularLaw_cutCoordinate_singleton line 55
5. theorem OAI.Invariant233.ProductModel.IdealSampling.triangularLaw_ae_continuousAt_cutCoordinate line 64
6. theorem OAI.Invariant233.ProductModel.IdealSampling.triangularLaw_null_frontier_interval line 77
7. theorem OAI.Invariant233.ProductModel.IdealSampling.triangularLaw_null_frontier_endpointCylinder line 94
8. theorem OAI.Invariant233.ProductModel.IdealSampling.finiteMeasure_tendsto_apply_of_null_frontier line 112
9. theorem OAI.Invariant233.ProductModel.IdealSampling.cylinder_real_tendsto_of_weaklyConverges line 138
10. theorem OAI.Invariant233.ProductModel.IdealSampling.law_cylinder_real_tendsto_of_productScaleLaws line 156