OAI/Analysis/IrrationalRotation/Sampling/ProductSamplingTestCongruence.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.SamplingWeights.indicator_one_eq_of_mem_iff line 14
2. theorem OAI.Invariant233.ProductModel.SamplingWeights.measurePreserving_fract_add_unit line 22
3. theorem OAI.Invariant233.ProductModel.SamplingWeights.testedProduct_first_congr_ae line 38
4. theorem OAI.Invariant233.ProductModel.SamplingWeights.testedIdeal_first_congr_ae line 62
5. theorem OAI.Invariant233.ProductModel.SamplingWeights.sourceTestedError_first_congr_ae line 87
6. theorem OAI.Invariant233.ProductModel.SamplingWeights.integral_sq_sourceTestedError_first_congr line 105
7. theorem OAI.Invariant233.ProductModel.SamplingWeights.cylinderCoordinateSet_ae_Ico line 116
8. theorem OAI.Invariant233.ProductModel.SamplingWeights.exists_cylinderTest_first_error_rationalIco line 130