OAI/Probability/SKValue/Equations/PolynomialObservable.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SKValue.BoundedJoint line 10
2. lemma OAI.SKValue.BoundedJoint.const line 14
3. lemma OAI.SKValue.BoundedJoint.add line 17
4. lemma OAI.SKValue.BoundedJoint.mul line 29
5. lemma OAI.SKValue.BoundedJoint.continuous line 44
6. lemma OAI.SKValue.BoundedJoint.spatial line 55
7. def OAI.SKValue.JetExpr.spatial line 63
8. def OAI.SKValue.JetExpr.spatialIter line 64
9. def OAI.SKValue.polyJet line 68
10. lemma OAI.SKValue.SmoothEvolution.polyJet_joint line 70
11. lemma OAI.SKValue.SmoothEvolution.polyJet_smooth line 79
12. lemma OAI.SKValue.SmoothEvolution.polyJet_hasDeriv line 87
13. lemma OAI.SKValue.SmoothEvolution.polyJet_iterated line 94
14. lemma OAI.SKValue.BoundedSmoothFamily.at_continuous line 113
15. def OAI.SKValue.weightedFamilyIntegral line 118
16. lemma OAI.SKValue.BoundedSmoothFamily.weightedFamilyIntegral_hasDerivAt line 121