OAI/Analysis/IrrationalRotation/Sampling/ProductIdealSamplingOrder.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.IdealSampling.displacement_bounds line 12
2. theorem OAI.Invariant233.ProductModel.IdealSampling.representative_displaced line 32
3. theorem OAI.Invariant233.ProductModel.IdealSampling.endpoint_ordered line 59
4. theorem OAI.Invariant233.ProductModel.IdealSampling.uncutLaw_ordered line 71
5. theorem OAI.Invariant233.ProductModel.IdealSampling.law_le_uncutLaw line 78
6. theorem OAI.Invariant233.ProductModel.IdealSampling.law_ordered line 81
7. theorem OAI.Invariant233.ProductModel.IdealSampling.uncutLaw_mass line 85