OAI/Analysis/MatrixSigning/Arithmetic/Alpha.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Scalar.psi_even line 11
2. lemma OAI.CurrentKS.Scalar.psi₁_odd line 12
3. lemma OAI.CurrentKS.Scalar.kappa_even line 13
4. lemma OAI.CurrentKS.Scalar.psi_ge_base line 15
5. lemma OAI.CurrentKS.Scalar.abs_derivative_ratio line 22
6. lemma OAI.CurrentKS.Scalar.abs_derivative_ratio_le line 35
7. lemma OAI.CurrentKS.Scalar.weighted_kappa_lower line 45
8. def OAI.CurrentKS.Scalar.alpha line 57
9. def OAI.CurrentKS.Scalar.beta line 58
10. lemma OAI.CurrentKS.Scalar.alpha_neg line 60
11. lemma OAI.CurrentKS.Scalar.beta_neg line 62
12. lemma OAI.CurrentKS.Scalar.coefficient_bounds_nonneg line 65
13. lemma OAI.CurrentKS.Scalar.product_bounds line 96
14. lemma OAI.CurrentKS.Scalar.kappa_product_bounds line 119
15. lemma OAI.CurrentKS.Scalar.light_squares_nonneg line 141
16. lemma OAI.CurrentKS.Scalar.light_squares line 168