added a small numerical example

Author: marekpetrik

MDPLib/Probability/Basic.lean

@@ -34,7 +34,7 @@ theorem nneg_dotProd_pos_ex_pos (h1 : ∀ ω, p ω ≥ 0) (h2 : ∀ ω, x ω ≥
   | succ n ih =>
     by_cases hn : x ⟨0, Nat.zero_lt_succ n⟩ > 0 
     · exact ⟨0, hn⟩
-    · push_neg at hn 
+    · push Not at hn 
       have hvh0 : 0 = vecHead x := le_antisymm (h2 0) hn
       rewrite [dotProduct_head_tail, ←hvh0] at h 
       obtain ⟨ω, hω⟩ := ih (Fin.tail h1) (Fin.tail h2) (by simpa [vecHead, vecTail] using h) 
@@ -141,7 +141,7 @@ theorem rv_le_step_lt_max (h0 : t < (FinRV.max P X)) : ∃q > t, (X ≤ᵣ t) =
            have hxω : X ω ∉ 𝓨 := by
               by_contra! inY; exact false_of_le_gt (Finset.min'_le 𝓨 (X ω) inY) h2
            rw [Finset.mem_filter] at hxω
-           push_neg at hxω
+           push Not at hxω
            exact hxω (Finset.mem_image_of_mem X (Finset.mem_univ ω))
 
 theorem rv_le_step_lt (P : Findist n) : ∃q > t,  (X ≤ᵣ t) = (X <ᵣ q) :=

MDPLib/Risk/VaR.lean

@@ -134,7 +134,7 @@ theorem isquantilelower_le_isquantile : IsCofinalFor (QuantileLower P X α.val)
       · exfalso; exact false_of_lt_ge h2r h
 
 theorem isquantile_le_isquantilelower : IsCofinalFor (Quantile P X α.val) (QuantileLower P X α.val) :=
-    HasSubset.Subset.iscofinalfor quantile_subset_quantilelower
+    HasSubset.Subset.isCofinalFor quantile_subset_quantilelower
 
 theorem varq_eq_var : IsVaR_Q P X α v ↔ IsVaR P X α v := 
     ⟨fun h => ⟨varq_is_quantilelower h, (upperBounds_mono_of_isCofinalFor isquantilelower_le_isquantile) h.2⟩,

Main.lean

@@ -1,5 +1,17 @@
 import MDPLib
+import MDPLib.Risk.VaR
+
+theorem fancy : True := True.intro
 
 def main : IO Unit := -- main
-  IO.println s!"Hello!"
+  let x : Fin 3 → ℚ := ![1,2,3]
+  let p : Fin 3 → ℚ := ![0.1, 0.5, 0.4]
+  let P : Findist 3 := 
+    {p := p, prob := by  simp [dotProduct, p]; sorry; , nneg := by sorry }     
+  let α : Risk.RiskLevel := ⟨0.5, by unfold Risk.IsRiskLevel; constructor; linarith; linarith  ⟩
+
+  let v := Risk.FinVaR P x α
+
+  IO.println s!"VaR value: {v}" 
+
 

lake-manifest.json

@@ -1,11 +1,11 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d86a5de2ff21aa80102530624e079756b2723855",
+   "rev": "d4c205d5773673a2e8112f8c72bf33a0358e333d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "68a23ef0da7598345429a493ca8d4250fd44087f",
+   "rev": "aa4c3e4e14f5b31495b7c7238762ecceddd9f52c",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e84e3e16aea6b72cc5d311ca1bb25caad417e162",
+   "rev": "f449eabb8f7e3feef0366856c20e28a6d2c97ee3",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f207d9fcf0cef00ba79962a33ef156061914d9c7",
+   "rev": "86503d416c875fdcf3b6b6c54c22581e96c6bda7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,50 +65,50 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2e58165a9dcdca9837b666528f974299ee1a51cc",
+   "rev": "82d457fb3bdd9efadbae06608ff337d689efdddf",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.92",
+   "inputRev": "v0.0.97",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c3361708f266893de5d1769192b60d4b1831f2bb",
+   "rev": "f74c7555aaa94eadd7b7bff9170f7983f92aac21",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "221e8088e3a066b8676dc471ff10638cf1c10835",
+   "rev": "7aa86cb20b8458748dc24d55dab2d7ea01161057",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "77a5160a74772214ef37caba2847cfe9ab600285",
+   "rev": "bf597c77bf9b8e66720d724928207f5911533113",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.30.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "3de531c1135f5e3a01f3ac04830996fda476b28e",
+   "rev": "f7d0ca7c926cdde0562af20394dd25d028b839a5",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0-rc6",
+   "inputRev": "v4.30.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/kim-em/leansqlite",
@@ -125,7 +125,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d7f24379ba37ec711f3f96b7187ca8dcc98b20e3",
+   "rev": "9539e34e5cb2d52a6454d9b6218f6b6835cad071",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -152,4 +152,5 @@
    "inherited": true,
    "configFile": "lakefile.lean"}],
  "name": "mdplib",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.29.0-rc6
+leanprover/lean4:v4.30.0-rc1