OAI/Analysis/IrrationalRotation/Product/ProductOrbitMarginals.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.TailTrimming.rotationIterate_inverse_left line 12
2. theorem OAI.Invariant233.ProductModel.TailTrimming.orbitPairMeasure_first_marginal line 17
3. theorem OAI.Invariant233.ProductModel.TailTrimming.orbitPairMeasure_second_marginal line 23
4. theorem OAI.Invariant233.ProductModel.TailTrimming.orbitAverageMeasure_first_marginal line 35
5. theorem OAI.Invariant233.ProductModel.TailTrimming.orbitAverageMeasure_second_marginal line 47
6. theorem OAI.Invariant233.ProductModel.TailTrimming.orbitPairMeasure_restrict line 66
7. theorem OAI.Invariant233.ProductModel.TailTrimming.orbitAverageMeasure_restrict line 75
8. theorem OAI.Invariant233.ProductModel.TailTrimming.orbitAverageMeasure_restrict_first_marginal line 88
9. theorem OAI.Invariant233.ProductModel.TailTrimming.orbitAverageMeasure_restrict_second_marginal line 98
10. theorem OAI.Invariant233.ProductModel.TailTrimming.ofReal_average_eq line 109
11. theorem OAI.Invariant233.ProductModel.TailTrimming.orbitAverageMeasure_first_marginal_real line 119
12. theorem OAI.Invariant233.ProductModel.TailTrimming.orbitAverageMeasure_second_marginal_real line 130