OAI/Analysis/IrrationalRotation/Sampling/SamplingCylinderError.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.SamplingCylinderWeak.weaklyConverges_of_real_cylinders line 13
2. theorem OAI.Invariant233.SamplingCylinderWeak.abs_integral_sub_le_eLpNorm_two line 26
3. theorem OAI.Invariant233.SamplingCylinderWeak.tendsto_integral_of_eLpNorm_sub_tendsto_zero line 43
4. theorem OAI.Invariant233.SamplingCylinderWeak.real_mass_eq_integral_of_tested_first_marginal line 61
5. theorem OAI.Invariant233.SamplingCylinderWeak.weaklyConverges_of_tested_first_marginal_L2 line 74
6. theorem OAI.Invariant233.SamplingCylinderWeak.ae_all_triangular_weaklyConverges_of_tested_L2 line 95