major refactor: name change and updated libraries

Author: marekpetrik

MDPLib.lean

@@ -0,0 +1,11 @@
+-- This module serves as the root of the `MDPLib` library.
+-- Import modules here that should be built as part of the library.
+
+import MDPLib.Probability.Prelude
+import MDPLib.Probability.Defs
+import MDPLib.Probability.Basic
+import MDPLib.Probability.Quantile
+
+import MDPLib.Risk.VaR
+
+import MDPLib.MDP.Histories

Probability/Expected.lean MDPLib/Expected.leanProbability/Expected.lean renamed to MDPLib/Expected.lean

@@ -16,7 +16,7 @@ import Mathlib.Data.NNReal.Basic
 import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Finset.Image
 
-import Probability.Probability.Basic
+import MDPLib.Probability.Basic
 
 namespace MDPs
 
@@ -388,10 +388,9 @@ theorem hist_horiz_exact (t : ℕ) (h : Hist M) (hh : h ∈ M.HistoriesHorizon t
 
 def MDP.HistoriesHorizonT (M : MDP) (t : ℕ) : Finset (M.HistT t) := 
     let H := M.HistoriesHorizon t 
-    let f : {h : Hist M // h ∈ H} → M.HistT t := 
-          fun hh => ⟨hh.1, hist_horiz_exact t hh.1 hh.2⟩
-    have finj : Injective f := 
-          by unfold Injective f; intro h₁ h₂ steq; rewrite [Subtype.eq_iff] at steq; simpa using steq 
+    let f : {h : Hist M // h ∈ H} → M.HistT t := fun hh => ⟨hh.1, hist_horiz_exact t hh.1 hh.2⟩
+    have finj : Injective f := by unfold Injective f;  intro h₁ h₂ steq; grind only 
+        -- TODO: this used to work instead of grind: rw [Subtype.ext_iff] at steq; simpa using steq 
     H.attach.map ⟨f, finj⟩
 
 theorem hist_horiz_complete_t (t : ℕ) (h : M.HistT t) : h ∈ M.HistoriesHorizonT t := by 

Probability/Finprob.lean MDPLib/Finprob.leanProbability/Finprob.lean renamed to MDPLib/Finprob.lean

@@ -1,4 +1,4 @@
-import Probability.Probability.Defs
+import MDPLib.Probability.Defs
 
 import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Algebra.BigOperators.Group.Finset.Basic

Probability/Histories.lean MDPLib/Histories.leanProbability/Histories.lean renamed to MDPLib/Histories.lean

@@ -1,4 +1,4 @@
-import Probability.Probability.Prelude
+import MDPLib.Probability.Prelude
 
 import Mathlib.Data.Matrix.Mul  -- dot product definitions and results
 import Mathlib.Algebra.Notation.Pi.Defs -- operations on functions
@@ -155,13 +155,19 @@ infix:50 "≥ᵣ" => FinRV.geq
 /-- Boolean random variable represening Y > y inequality -/
 infix:50 ">ᵣ" => FinRV.gt
 
+example (a b : ℕ) (h : a ≤ b +1) : (a ≤ b) ∨ (a = b + 1) := by exact Nat.le_or_eq_of_le_succ h
+
+lemma exclusion {a b : ℕ} (h : a > b + 1) : (a > b) ∧ ¬(a = b + 1) := 
+  ⟨ Nat.lt_of_succ_lt h, Ne.symm (Nat.ne_of_lt h) ⟩
+
 /-- Equivalence when extending the random variable to another element. -/
 theorem le_of_le_eq (D : FinRV n ℕ) (m : ℕ) : ((D ≤ᵣ m) + (D =ᵣ m.succ)) = (D ≤ᵣ m.succ) := by
   funext x --extensionality principle for functions
   unfold FinRV.leq FinRV.eq instHAdd Add.add Pi.instAdd
-  simp [instBoolAdd]
-  have := Nat.lt_trichotomy (D x) (m+1)
-  grind only [cases Or]
+  rw [Pi.add_apply, bool_sum_or]
+  by_cases h : D x ≤ m.succ
+  · simp [h, Nat.le_or_eq_of_le_succ]
+  · simp [h, exclusion (Nat.not_le.mp h) ] 
 
 /-- Defines a preimage of an RV. This is a set with a decidable membership. -/
 def preimage (f : FinRV n ρ) : ρ → Set (Fin n) :=

Probability/MDP/Histories.lean MDPLib/MDP/Histories.leanProbability/MDP/Histories.lean renamed to MDPLib/MDP/Histories.lean

@@ -1,4 +1,4 @@
-import Probability.Probability.Prelude
+import MDPLib.Probability.Prelude
 
 import Probability.Probability.Defs
 import Mathlib.Data.Matrix.Mul

Probability/Probability/Basic.lean MDPLib/Probability/Basic.leanProbability/Probability/Basic.lean renamed to MDPLib/Probability/Basic.lean

@@ -1,4 +1,4 @@
-import Probability.Probability.Basic
+import MDPLib.Probability.Basic
 import Mathlib.Data.EReal.Basic
 import Mathlib.Data.Set.Operations
 import Mathlib.Data.Fin.VecNotation