OAI/Probability/GaussianInformation/Dyadic/ProjectionTests.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RepeatedLocalization.weightedProjectionMoment line 19
2. lemma OAI.RepeatedLocalization.weightedProjectionMoment_ne_top line 23
3. lemma OAI.RepeatedLocalization.actual_smoothedProjection_moment line 29
4. lemma OAI.RepeatedLocalization.actual_projection_borel_test line 52