OAI/Analysis/IrrationalRotation/Sampling/ProductSamplingExpectedTransport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.SamplingWeights.testedCoordinateWeight_eq_testedKernel line 14
2. theorem OAI.Invariant233.ProductModel.SamplingWeights.testedAverage_eq_kernel_mean line 26
3. theorem OAI.Invariant233.ProductModel.SamplingWeights.measurePreserving_finite_representatives line 38
4. theorem OAI.Invariant233.ProductModel.SamplingWeights.integral_angle_circle_eq_finite_unit line 46
5. theorem OAI.Invariant233.ProductModel.SamplingWeights.testedAverageError_expected_eq line 70
6. theorem OAI.Invariant233.ProductModel.SamplingWeights.testedAverageError_expected_cond_eq line 132
7. theorem OAI.Invariant233.ProductModel.SamplingWeights.sourceTestedError_expected_eq line 148
8. theorem OAI.Invariant233.ProductModel.SamplingWeights.sourceTestedError_expected_le line 163
9. theorem OAI.Invariant233.ProductModel.SamplingWeights.sourceTestedError_expected_le_common line 187