OAI/Analysis/IrrationalRotation/Sampling/DigitAveraging.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.DigitAveraging.sq_integral_le_mass_mul_integral_sq line 14
2. theorem OAI.Invariant233.DigitAveraging.sum_integral_fibers line 44
3. theorem OAI.Invariant233.DigitAveraging.digit_averaging_energy_le line 62
4. theorem OAI.Invariant233.DigitAveraging.digit_average_nonneg line 103
5. theorem OAI.Invariant233.DigitAveraging.digit_average_mean line 110
6. theorem OAI.Invariant233.DigitAveraging.digit_average_le line 120
7. theorem OAI.Invariant233.DigitAveraging.map_withDensity_eq_digit_density line 138
8. theorem OAI.Invariant233.DigitAveraging.integral_map_eq_uniform_sum line 164
9. theorem OAI.Invariant233.DigitAveraging.integral_digit_energy_le line 181