OAI/Analysis/IrrationalRotation/Sampling/PrefixPatternDomination.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.PrefixPatterns.measurable_replacement line 13
2. theorem OAI.Invariant233.ProductModel.PrefixPatterns.measurable_rectangleDensity line 21
3. theorem OAI.Invariant233.ProductModel.PrefixPatterns.lintegral_rectangleDensity line 26
4. theorem OAI.Invariant233.ProductModel.PrefixPatterns.ordered_cut_intervals line 34
5. theorem OAI.Invariant233.ProductModel.PrefixPatterns.measurable_patternDensity line 40
6. theorem OAI.Invariant233.ProductModel.PrefixPatterns.patternDensity_replacement line 51
7. theorem OAI.Invariant233.ProductModel.PrefixPatterns.measurableSet_triangularEvent line 60
8. theorem OAI.Invariant233.ProductModel.PrefixPatterns.patternDensity_zero_off_triangle line 69
9. theorem OAI.Invariant233.ProductModel.PrefixPatterns.map_withDensity_comp line 87
10. theorem OAI.Invariant233.ProductModel.PrefixPatterns.patternLaw_eq_withDensity line 96
11. theorem OAI.Invariant233.ProductModel.PrefixPatterns.patternLaw_absolutelyContinuous_of_order line 122
12. theorem OAI.Invariant233.ProductModel.PrefixPatterns.patternLaw_absolutelyContinuous line 138
13. theorem OAI.Invariant233.ProductModel.PrefixPatterns.map_withDensity_comp_ae line 147
14. theorem OAI.Invariant233.ProductModel.PrefixPatterns.aemeasurable_patternDensity line 160
15. theorem OAI.Invariant233.ProductModel.PrefixPatterns.patternLaw_eq_withDensity_ae line 176
16. theorem OAI.Invariant233.ProductModel.PrefixPatterns.triangularLaw_absolutelyContinuous_prefix_sum line 203
17. theorem OAI.Invariant233.ProductModel.PrefixPatterns.mixtureLaw_absolutelyContinuous_prefix_sum line 209
18. theorem OAI.Invariant233.ProductModel.PrefixPatterns.ae_mixtureLaw_of_ae_triangularLaw line 238