OAI/Analysis/IrrationalRotation/Couplings/ProductDensityLimit.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductDensity.inner_toLp_eq_integral_mul line 14
2. def OAI.Invariant233.ProductDensity.partialDensityLp line 23
3. theorem OAI.Invariant233.ProductDensity.partialDensityLp_inner line 31
4. theorem OAI.Invariant233.ProductDensity.exists_partialDensityLp_limit line 51
5. theorem OAI.Invariant233.ProductDensity.tendsto_eLpNorm_one_partialDensity_sub line 75
6. theorem OAI.Invariant233.ProductDensity.partialDensityLp_limit_nonneg line 99
7. theorem OAI.Invariant233.ProductDensity.partialDensityLp_limit_integral line 116
8. theorem OAI.Invariant233.ProductDensity.partialDensityLp_limit_setIntegral_pi line 135
9. theorem OAI.Invariant233.ProductDensity.isProbabilityMeasure_withDensity_ofReal line 159
10. theorem OAI.Invariant233.ProductDensity.partialDensityLp_limit_withDensity line 169
11. theorem OAI.Invariant233.ProductDensity.exists_product_density line 198
12. theorem OAI.Invariant233.ProductDensity.norm_toLp_sq_eq_integral_sq line 221
13. theorem OAI.Invariant233.ProductDensity.centered_eLpNorm_sq_eq_integral line 230
14. theorem OAI.Invariant233.ProductDensity.exists_product_density_of_norm line 239
15. theorem OAI.Invariant233.ProductDensity.exists_hybrid_product_density line 259