OAI/Probability/SKRatio/Certificates/CertifiedFunctions.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.SKRatio.Certificate.Expr.(instance at line 14) line 14
2. instance OAI.SKRatio.Certificate.Expr.(instance at line 15) line 15
3. instance OAI.SKRatio.Certificate.Expr.(instance at line 16) line 16
4. instance OAI.SKRatio.Certificate.Expr.(instance at line 17) line 17
5. instance OAI.SKRatio.Certificate.Expr.(instance at line 18) line 18
6. instance OAI.SKRatio.Certificate.Expr.(instance at line 19) line 19
7. lemma OAI.SKRatio.Certificate.Expr.val_add line 20
8. lemma OAI.SKRatio.Certificate.Expr.val_sub line 21
9. lemma OAI.SKRatio.Certificate.Expr.val_mul line 22
10. lemma OAI.SKRatio.Certificate.Expr.val_div line 23
11. lemma OAI.SKRatio.Certificate.Expr.val_ofNat line 24
12. def OAI.SKRatio.Certificate.approxF line 29
13. def OAI.SKRatio.Certificate.scalarFunction line 32
14. def OAI.SKRatio.Certificate.scalarExpr line 47
15. def OAI.SKRatio.Certificate.integrandExpr line 70
16. lemma OAI.SKRatio.Certificate.scalarExpr_val line 74
17. lemma OAI.SKRatio.Certificate.integrandExpr_val line 83
18. lemma OAI.SKRatio.Certificate.continuous_approxF line 93
19. lemma OAI.SKRatio.Certificate.continuous_scalarFunction line 100