OAI/Analysis/IrrationalRotation/Sampling/ProductIdealSamplingLimit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Invariant233.ProductModel.IdealSampling.sourceMeasure_finite line 14
2. instance OAI.Invariant233.ProductModel.IdealSampling.uncutLaw_finite line 18
3. instance OAI.Invariant233.ProductModel.IdealSampling.law_finite line 22
4. theorem OAI.Invariant233.ProductModel.IdealSampling.endpointMap_measurable line 27
5. theorem OAI.Invariant233.ProductModel.IdealSampling.cutoffEvent_measurable line 50
6. theorem OAI.Invariant233.ProductModel.IdealSampling.endpointMap_tendsto line 62
7. theorem OAI.Invariant233.ProductModel.IdealSampling.uncutLaw_weaklyConverges line 84
8. theorem OAI.Invariant233.ProductModel.IdealSampling.circle_cutoff_loss_le line 96
9. theorem OAI.Invariant233.ProductModel.IdealSampling.cutoff_loss_le line 125
10. theorem OAI.Invariant233.ProductModel.IdealSampling.cutoff_loss_tendsto_zero line 158
11. theorem OAI.Invariant233.ProductModel.IdealSampling.law_weaklyConverges line 173
12. theorem OAI.Invariant233.ProductModel.IdealSampling.law_weaklyConverges_of_linear_dimension line 194