OAI/Analysis/IrrationalRotation/Sampling/ProductSamplingUniformL2.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductSampling.exists_uniform_norm_bound_of_error_tendsto line 12
2. theorem OAI.Invariant233.ProductSampling.sqrt_integral_sq_eq_toLp_norm line 24
3. theorem OAI.Invariant233.ProductSampling.tendsto_norm_toLp_sub_of_integral_sq line 35
4. theorem OAI.Invariant233.ProductSampling.exists_uniform_toLp_norm_bound_of_energy line 48
5. theorem OAI.Invariant233.ProductModel.hasUniformL2Marginals_of_energy_convergence line 66
6. theorem OAI.Invariant233.ProductModel.ae_hasUniformL2Marginals_of_summable_expected_errors line 107