OAI/Analysis/MatrixSigning/Calculus/IteratedNormCompLinear.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Calculus.iterated_norm_comp_linear line 21
2. lemma OAI.CurrentKS.Calculus.iterated_norm_comp_contraction line 34
3. lemma OAI.CurrentKS.Calculus.iterated_norm_linear_ge_two line 40
4. lemma OAI.CurrentKS.Calculus.bilinear_one line 47
5. lemma OAI.CurrentKS.Calculus.bilinear_two line 59
6. lemma OAI.CurrentKS.Calculus.bilinear_three line 73
7. lemma OAI.CurrentKS.Calculus.iterated_norm_linear_comp line 95
8. lemma OAI.CurrentKS.Calculus.inverse_linear_first_three line 102
9. theorem OAI.CurrentKS.Calculus.inverse_sandwich_first_three line 117