OAI/Analysis/IrrationalRotation/Sampling/SamplingMeanSquare.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.SamplingAsymptotics.integral_coordinate_product_sub_one_sq line 12
2. theorem OAI.Invariant233.SamplingAsymptotics.integral_ideal_product_sub_one_sq_le line 42
3. theorem OAI.Invariant233.SamplingAsymptotics.integral_sub_one_sq_le_split line 61
4. theorem OAI.Invariant233.SamplingAsymptotics.integral_sample_mean_square_le line 80
5. theorem OAI.Invariant233.SamplingAsymptotics.lintegral_sample_mean_square_eq_ofReal line 127
6. theorem OAI.Invariant233.SamplingAsymptotics.tendsto_ofReal_meanSquareBound line 147
7. theorem OAI.Invariant233.SamplingAsymptotics.tendsto_zero_of_meanSquareBound line 151