OAI/Analysis/IrrationalRotation/Sampling/ProductIdealSamplingProduct.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Invariant233.ProductModel.IdealSampling.coordinateEndpoint line 11
2. def OAI.Invariant233.ProductModel.IdealSampling.coordinateEvent line 17
3. theorem OAI.Invariant233.ProductModel.IdealSampling.coordinateEndpoint_measurable line 21
4. theorem OAI.Invariant233.ProductModel.IdealSampling.coordinateEvent_measurable line 36
5. theorem OAI.Invariant233.ProductModel.IdealSampling.mem_retained_iff line 47
6. theorem OAI.Invariant233.ProductModel.IdealSampling.retained_product_eq line 64
7. theorem OAI.Invariant233.ProductModel.IdealSampling.integral_law_product line 85
8. def OAI.Invariant233.ProductModel.IdealSampling.coordinateKernel line 121
9. theorem OAI.Invariant233.ProductModel.IdealSampling.integral_coordinate_eq_kernel line 124
10. theorem OAI.Invariant233.ProductModel.IdealSampling.integral_law_product_eq_kernels line 158