OAI/Probability/SKGap/Localization/ProjectedReal.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.signConjugate_mul line 17
2. def OAI.SKGap.realProject line 29
3. lemma OAI.SKGap.realProject_opNorm line 32
4. lemma OAI.SKGap.realProject_sub_norm line 36
5. lemma OAI.SKGap.realProject_eq_self line 44
6. lemma OAI.SKGap.realProject_sign line 52
7. lemma OAI.SKGap.realProject_lipschitz line 57
8. lemma OAI.SKGap.realProjectedProduct_opNorm line 63
9. lemma OAI.SKGap.realProjectedProduct_sub_norm line 69
10. lemma OAI.SKGap.projected_product_expectation_error line 97
11. def OAI.SKGap.projectedErrorConstant line 157
12. lemma OAI.SKGap.projected_error_absorption line 160