OAI/Analysis/IrrationalRotation/Sampling/ScalarSamplingPairMoments.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Invariant233.ScalarSampling.scalarUnitLaw line 14
2. def OAI.Invariant233.ScalarSampling.scalarPairLaw line 16
3. instance OAI.Invariant233.ScalarSampling.scalarUnitLaw_probability line 19
4. lemma OAI.Invariant233.ScalarSampling.scalarPairLaw_probability line 23
5. lemma OAI.Invariant233.ScalarSampling.integral_scalarUnitLaw line 29
6. lemma OAI.Invariant233.ScalarSampling.measurable_kernel_mean line 34
7. lemma OAI.Invariant233.ScalarSampling.integrable_kernel_mean line 40
8. lemma OAI.Invariant233.ScalarSampling.integrable_kernel_mean_square line 49
9. lemma OAI.Invariant233.ScalarSampling.integrable_sampled_product line 59
10. lemma OAI.Invariant233.ScalarSampling.integrable_sampled_cross line 77
11. lemma OAI.Invariant233.ScalarSampling.scalarPair_error_transfer line 97
12. theorem OAI.Invariant233.ScalarSampling.scalarPair_cross_error line 110
13. theorem OAI.Invariant233.ScalarSampling.scalarPair_offdiag_error line 124
14. lemma OAI.Invariant233.ScalarSampling.integrable_haar_kernel_square line 137
15. theorem OAI.Invariant233.ScalarSampling.scalarPair_diagonal_le line 149
16. theorem OAI.Invariant233.ScalarSampling.scalarPair_offdiag_error_fifty line 167
17. theorem OAI.Invariant233.ScalarSampling.scalarPair_diagonal_rate line 178