OAI/Probability/GaussianInformation/Dyadic/ConditionalMoments.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RepeatedLocalization.tubeWeightConstant line 14
2. lemma OAI.RepeatedLocalization.tubeWeightConstant_ne_top line 17
3. lemma OAI.RepeatedLocalization.weighted_dyadic_tube_tail line 20
4. lemma OAI.RepeatedLocalization.weighted_affine_inverseMoment line 47
5. lemma OAI.RepeatedLocalization.weighted_affine_zero_null line 65
6. lemma OAI.RepeatedLocalization.weighted_affine_inverseMoment_ennreal line 77