OAI/Probability/GaussianInformation/Dyadic/ProjectionMoments.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RepeatedLocalization.gaussianRows line 20
2. def OAI.RepeatedLocalization.projectVector line 23
3. lemma OAI.RepeatedLocalization.continuous_projectVector line 26
4. lemma OAI.RepeatedLocalization.projectVector_sub line 31
5. lemma OAI.RepeatedLocalization.projectVector_rowMatrix line 36
6. lemma OAI.RepeatedLocalization.boxScale_cancel line 44
7. lemma OAI.RepeatedLocalization.fixedReplica_moment_le line 53
8. def OAI.RepeatedLocalization.smoothedProjection line 107
9. lemma OAI.RepeatedLocalization.measurable_projection_kernel line 112
10. lemma OAI.RepeatedLocalization.measurable_smoothedProjection line 121
11. lemma OAI.RepeatedLocalization.measurable_replicated line 126
12. lemma OAI.RepeatedLocalization.measurable_replica_kernel line 133
13. lemma OAI.RepeatedLocalization.smoothedProjection_moment_le line 139