OAI/Probability/SKGap/Localization/ConditionalTolerance.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.augmentedToleranceConstant line 13
2. lemma OAI.SKGap.augmentedToleranceConstant_pos line 16
3. lemma OAI.SKGap.augmentedGramTolerance_bound line 19
4. lemma OAI.SKGap.conditionalMeanData_hermitian line 39
5. lemma OAI.SKGap.conditionalScalarData_hermitian line 42
6. lemma OAI.SKGap.diagonal_mass_margin line 55
7. lemma OAI.SKGap.empirical_moment_vector_bound line 70
8. lemma OAI.SKGap.empirical_cutoff_gram_small line 83
9. lemma OAI.SKGap.gram_close_by_quarters line 103
10. def OAI.SKGap.conditionalEmpiricalCore line 107
11. theorem OAI.SKGap.conditional_empirical_fixed_tail line 118