OAI/Probability/SKGap/Localization/ConditionalHessianLaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.scalarQMoment_empirical_overlap line 14
2. lemma OAI.SKGap.empirical_columns_zero_outer line 19
3. lemma OAI.SKGap.empirical_unit_outer line 30
4. lemma OAI.SKGap.empiricalConditionalMiddle_literal line 41
5. lemma OAI.SKGap.fieldHessian_diagonalHessian line 52
6. lemma OAI.SKGap.empiricalConditionalGoe_hessian line 63
7. lemma OAI.SKGap.quadraticForm_dotProduct line 69
8. lemma OAI.SKGap.quadraticForm_margin line 75
9. lemma OAI.SKGap.measurable_conditionalGoe_map line 98
10. lemma OAI.SKGap.measurable_badField_fiber line 104
11. lemma OAI.SKGap.conditional_bad_le_freshbad line 108