OAI/Probability/GaussianInformation/Dyadic/Tubes.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.RepeatedLocalization.exists_affine_tube_coverline 13 - lemma
OAI.RepeatedLocalization.measure_affine_tube_le_of_gridline 60