OAI/Probability/SKGap/Localization/RealPart.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.RealComplex.realPart line 46
2. lemma OAI.SKGap.RealComplex.norm_realPart_le line 48
3. lemma OAI.SKGap.RealComplex.realPart_sub line 59
4. lemma OAI.SKGap.RealComplex.realPart_liftMatrix line 62
5. lemma OAI.SKGap.RealComplex.realPart_lipschitz line 65
6. lemma OAI.SKGap.RealComplex.reVec_norm_le line 71
7. lemma OAI.SKGap.RealComplex.realPart_operator line 75
8. lemma OAI.SKGap.RealComplex.operator_realPart_le line 81
9. lemma OAI.SKGap.RealComplex.liftMatrix_inverse line 87
10. lemma OAI.SKGap.RealComplex.liftMatrix_isUnit_iff line 100
11. def OAI.SKGap.RealComplex.realPartCLM line 107
12. def OAI.SKGap.RealComplex.realTruncatedK line 113
13. lemma OAI.SKGap.RealComplex.realTruncatedK_sub_norm line 118
14. lemma OAI.SKGap.RealComplex.realTruncatedK_opNorm line 132
15. lemma OAI.SKGap.RealComplex.realTruncatedK_eq_inverse line 141
16. lemma OAI.SKGap.RealComplex.real_matrix_hasDerivAt_inverse line 182
17. lemma OAI.SKGap.RealComplex.continuous_realOpNorm line 194
18. lemma OAI.SKGap.RealComplex.realTruncatedK_eventually_inverse line 200
19. lemma OAI.SKGap.RealComplex.realTruncatedK_derivative line 225