OAI/Analysis/IrrationalRotation/Sampling/ProductSamplingWeakConvergence.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Invariant233.ProductModel.SamplingWeak.EndpointCoordinate line 15
2. abbrev OAI.Invariant233.ProductModel.SamplingWeak.RectangleTest line 16
3. abbrev OAI.Invariant233.ProductModel.SamplingWeak.representative line 18
4. abbrev OAI.Invariant233.ProductModel.SamplingWeak.quotient line 21
5. theorem OAI.Invariant233.ProductModel.SamplingWeak.measurable_representative line 24
6. theorem OAI.Invariant233.ProductModel.SamplingWeak.continuous_quotient line 27
7. theorem OAI.Invariant233.ProductModel.SamplingWeak.quotient_representative line 30
8. def OAI.Invariant233.ProductModel.SamplingWeak.rectangle line 34
9. theorem OAI.Invariant233.ProductModel.SamplingWeak.measurableSet_rectangle line 37
10. theorem OAI.Invariant233.ProductModel.SamplingWeak.rectangle_empty line 41
11. theorem OAI.Invariant233.ProductModel.SamplingWeak.map_quotient_representative line 44
12. theorem OAI.Invariant233.ProductModel.SamplingWeak.tendsto_finiteMeasure_of_rectangles line 48
13. theorem OAI.Invariant233.ProductModel.SamplingWeak.weaklyConverges_of_rectangle_real line 56
14. theorem OAI.Invariant233.ProductModel.SamplingWeak.weaklyConverges_of_rectangles line 64
15. theorem OAI.Invariant233.ProductModel.SamplingWeak.ae_weaklyConverges_of_ae_rectangle_real line 72
16. theorem OAI.Invariant233.ProductModel.SamplingWeak.countable_rectangles line 82
17. theorem OAI.Invariant233.ProductModel.SamplingWeak.ae_all_weaklyConverges_of_ae_rectangle_real line 85
18. def OAI.Invariant233.ProductModel.SamplingWeak.box line 95
19. theorem OAI.Invariant233.ProductModel.SamplingWeak.rectangle_eq_box line 98
20. theorem OAI.Invariant233.ProductModel.SamplingWeak.weaklyConverges_of_box_real line 107
21. theorem OAI.Invariant233.ProductModel.SamplingWeak.ae_all_weaklyConverges_of_ae_box_real line 118