OAI/Probability/SKValue/Equations/JetAlgebra.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.SKValue.JetExpr line 11
2. def OAI.SKValue.JetExpr.eval line 18
3. def OAI.SKValue.JetExpr.D line 24
4. lemma OAI.SKValue.JetExpr.hasDerivAt_eval line 30
5. lemma OAI.SKValue.JetExpr.continuous_eval line 39
6. lemma OAI.SKValue.JetExpr.uniform_bound line 48
7. def OAI.SKValue.JetExpr.σx line 64
8. def OAI.SKValue.JetExpr.σh line 67
9. def OAI.SKValue.JetExpr.logGradientJet line 70
10. lemma OAI.SKValue.JetExpr.eval_σx line 74
11. lemma OAI.SKValue.JetExpr.eval_σh line 76
12. lemma OAI.SKValue.JetExpr.iteratedDeriv_logGradientJet line 79