OAI/Probability/SKGap/Localization/EmpiricalConditionalData.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.conditionalSize_bounds line 13
2. lemma OAI.SKGap.empiricalGramColumns_norm line 31
3. def OAI.SKGap.empiricalUnit line 52
4. lemma OAI.SKGap.empiricalUnit_unit line 55
5. lemma OAI.SKGap.empiricalUnit_norm line 65
6. lemma OAI.SKGap.normalized_average_l2 line 73
7. lemma OAI.SKGap.empirical_mass_close line 93