OAI/Analysis/IrrationalRotation/Sampling/ProductSourceSamplingL2.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.SamplingWeights.memLp_orientedAverage line 14
2. theorem OAI.Invariant233.ProductModel.SamplingWeights.sourceTestedError_univ_eq line 34
3. theorem OAI.Invariant233.ProductModel.SamplingWeights.source_orientedAverage_uniform_bound line 43
4. theorem OAI.Invariant233.ProductModel.SamplingWeights.source_hasUniformL2Marginals_of_energy_convergence line 96