OAI/Probability/SKGap/Stability/ImplicitLinear.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.ImplicitLinear.lower_norm_of_quadratic line 13
2. lemma OAI.SKGap.ImplicitLinear.quadratic_perturbation line 21
3. lemma OAI.SKGap.ImplicitLinear.injective_of_lower_norm line 33
4. theorem OAI.SKGap.ImplicitLinear.exists_bounded_inverse line 44
5. lemma OAI.SKGap.ImplicitLinear.jacobson_left line 70
6. lemma OAI.SKGap.ImplicitLinear.jacobson_right line 76
7. theorem OAI.SKGap.ImplicitLinear.unnormalized_inverse line 89
8. lemma OAI.SKGap.ImplicitLinear.unique_solution_of_inverse line 110
9. def OAI.SKGap.ImplicitSystem.rank line 130
10. lemma OAI.SKGap.ImplicitSystem.rank_apply line 132
11. lemma OAI.SKGap.ImplicitSystem.rank_add_right line 134
12. lemma OAI.SKGap.ImplicitSystem.rank_add_left line 137
13. lemma OAI.SKGap.ImplicitSystem.rank_sub_left line 140
14. lemma OAI.SKGap.ImplicitSystem.rank_smul_left line 143
15. lemma OAI.SKGap.ImplicitSystem.rank_norm_le line 146
16. lemma OAI.SKGap.ImplicitSystem.rank_perturbation line 154
17. lemma OAI.SKGap.ImplicitSystem.rank_perturbation_bound line 159
18. def OAI.SKGap.ImplicitSystem.L₂ line 169
19. def OAI.SKGap.ImplicitSystem.stableMatrix line 172
20. lemma OAI.SKGap.ImplicitSystem.normalized_difference line 175
21. lemma OAI.SKGap.ImplicitSystem.normalized_difference_bound line 182
22. def OAI.SKGap.ImplicitSystem.Equations line 198
23. lemma OAI.SKGap.ImplicitSystem.eliminated_equation line 201
24. theorem OAI.SKGap.ImplicitSystem.unique_implicit_solution line 211