Changes before changing laptop

binghe · Oct 3, 2024 · 81750a6 · 81750a6
1 parent f8c3ff1
commit 81750a6
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/examples/probability/distributionScript.sml b/examples/probability/distributionScript.sml
@@ -223,6 +223,13 @@ Definition normal_rv_def :
                                  distribution p X s = normal_measure mu sig s
 End
 
+(* TODO *)
+Theorem extreal_exp_alt :
+    ∀x :extreal. exp x = ext_suminf (λn. inv (&FACT n) * x pow n)
+Proof
+    cheat
+QED
+
 val _ = export_theory ();
 val _ = html_theory "distribution";