OAI/Analysis/IrrationalRotation/Sampling/ProductSamplingTestIntegrability.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Invariant233.ProductModel.SamplingWeights.testedProduct line 12
2. def OAI.Invariant233.ProductModel.SamplingWeights.testedIdeal line 17
3. theorem OAI.Invariant233.ProductModel.SamplingWeights.measurable_scalarProduct_pair line 23
4. theorem OAI.Invariant233.ProductModel.SamplingWeights.measurable_testedProduct_pair line 36
5. theorem OAI.Invariant233.ProductModel.SamplingWeights.testedProduct_bounds line 45
6. theorem OAI.Invariant233.ProductModel.SamplingWeights.memLp_testedProduct_pair line 59
7. theorem OAI.Invariant233.ProductModel.SamplingWeights.stronglyMeasurable_testedAverage line 72
8. theorem OAI.Invariant233.ProductModel.SamplingWeights.norm_testedAverage_le line 80
9. theorem OAI.Invariant233.ProductModel.SamplingWeights.memLp_testedIdeal line 91
10. theorem OAI.Invariant233.ProductModel.SamplingWeights.memLp_testedAverageError_pair line 111
11. theorem OAI.Invariant233.ProductModel.SamplingWeights.integrable_testedAverageError_sq line 122