OAI/Probability/SKRatio/Certificates/CertifiedJet.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SKRatio.Certificate.Jet line 11
  2. def OAI.SKRatio.Certificate.Jet.rat line 20
  3. def OAI.SKRatio.Certificate.Jet.var line 21
  4. def OAI.SKRatio.Certificate.Jet.add line 22
  5. def OAI.SKRatio.Certificate.Jet.neg line 23
  6. def OAI.SKRatio.Certificate.Jet.mul line 24
  7. def OAI.SKRatio.Certificate.Jet.sq line 28
  8. def OAI.SKRatio.Certificate.Jet.inv line 30
  9. def OAI.SKRatio.Certificate.Jet.exp line 34
  10. def OAI.SKRatio.Certificate.Jet.tanhBox line 38
  11. def OAI.SKRatio.Certificate.Jet.tanh line 43
  12. lemma OAI.SKRatio.Certificate.Jet.tanh_formula line 49
  13. lemma OAI.SKRatio.Certificate.Jet.mem_tanhBox line 56
  14. inductive OAI.SKRatio.Certificate.Expr line 66
  15. def OAI.SKRatio.Certificate.Expr.val line 80
  16. def OAI.SKRatio.Certificate.Expr.der line 91
  17. def OAI.SKRatio.Certificate.Expr.sec line 102
  18. def OAI.SKRatio.Certificate.Expr.compute line 114
  19. def OAI.SKRatio.Certificate.Expr.Regular line 125
  20. lemma OAI.SKRatio.Certificate.Expr.derivatives line 131
  21. lemma OAI.SKRatio.Certificate.Expr.compute_sound line 180