OAI/Analysis/IrrationalRotation/Sampling/ProductSamplingRestriction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.samplingMeasure_isFinite_of_uniformL2 line 11
2. theorem OAI.Invariant233.ProductModel.uniformL2Marginals_of_domination line 24
3. theorem OAI.Invariant233.ProductModel.uniformL2Marginals_restrict_with_finiteness line 49
4. theorem OAI.Invariant233.ProductModel.uniformL2Marginals_of_domination_auto line 56
5. theorem OAI.Invariant233.ProductModel.uniformL2Marginals_restrict line 62
6. theorem OAI.Invariant233.ProductModel.positiveOrderedOrbitSupport_of_domination line 68