OAI/Analysis/MatrixSigning/Arithmetic/ScalarPsi.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.Scalar.psi line 11
2. def OAI.CurrentKS.Scalar.psi₁ line 12
3. def OAI.CurrentKS.Scalar.kappa line 13
4. lemma OAI.CurrentKS.Scalar.base_pos line 15
5. lemma OAI.CurrentKS.Scalar.psi_pos line 19
6. lemma OAI.CurrentKS.Scalar.psi_cube line 22
7. lemma OAI.CurrentKS.Scalar.psi_sq line 26
8. lemma OAI.CurrentKS.Scalar.psi_le_one line 30
9. lemma OAI.CurrentKS.Scalar.hasDerivAt_psi line 35
10. lemma OAI.CurrentKS.Scalar.contDiffAt_psi line 45
11. lemma OAI.CurrentKS.Scalar.hasDerivAt_psi₁ line 49
12. lemma OAI.CurrentKS.Scalar.kappa_pos line 61
13. lemma OAI.CurrentKS.Scalar.derivative_ratio line 66
14. lemma OAI.CurrentKS.Scalar.derivative_ratio_le line 74
15. lemma OAI.CurrentKS.Scalar.psi₁_eq_base line 82