OAI/Analysis/MatrixSigning/Arithmetic/Alpha2.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.Scalar.Alpha line 11
2. def OAI.CurrentKS.Scalar.Beta line 12
3. def OAI.CurrentKS.Scalar.scaleT line 13
4. def OAI.CurrentKS.Scalar.scaleL line 14
5. def OAI.CurrentKS.Scalar.scaleM line 15
6. lemma OAI.CurrentKS.Scalar.Alpha_eq line 17
7. lemma OAI.CurrentKS.Scalar.Beta_eq line 22
8. lemma OAI.CurrentKS.Scalar.light_rescaling_pos line 27
9. lemma OAI.CurrentKS.Scalar.scaleT_sq line 37
10. lemma OAI.CurrentKS.Scalar.scaleL_mul_scaleM line 43
11. lemma OAI.CurrentKS.Scalar.rescaled_product_bound line 50
12. lemma OAI.CurrentKS.Scalar.rescaled_square_bounds line 72
13. lemma OAI.CurrentKS.Scalar.rescaled_kappa_bounds line 99
14. lemma OAI.CurrentKS.Scalar.rescaled_sum_identity line 118
15. lemma OAI.CurrentKS.Scalar.rescaled_drift_bounds line 127