OAI/Analysis/MatrixSigning/Calculus/JetBound.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.Calculus.JetBound line 17
2. lemma OAI.CurrentKS.Calculus.JetBound.nonneg line 20
3. lemma OAI.CurrentKS.Calculus.JetBound.value line 23
4. lemma OAI.CurrentKS.Calculus.JetBound.mono line 26
5. lemma OAI.CurrentKS.Calculus.JetBound.add line 29
6. lemma OAI.CurrentKS.Calculus.JetBound.neg line 36
7. lemma OAI.CurrentKS.Calculus.JetBound.sub line 43
8. lemma OAI.CurrentKS.Calculus.JetBound.linear_comp line 48
9. lemma OAI.CurrentKS.Calculus.JetBound.comp_linear line 55
10. lemma OAI.CurrentKS.Calculus.JetBound.prod line 61
11. lemma OAI.CurrentKS.Calculus.JetBound.const line 70
12. lemma OAI.CurrentKS.Calculus.JetBound.linear line 76
13. lemma OAI.CurrentKS.Calculus.JetBound.sum line 87
14. lemma OAI.CurrentKS.Calculus.JetBound.bilinear line 94