tweaks

Author: marekpetrik

Probability/MDP/Risk.lean

@@ -150,12 +150,6 @@ end Risk
 
 section Risk2
 
-#check Set.preimage
-#synth SupSet EReal
-#synth SupSet (WithTop ℝ)
-#check instSupSetEReal
-#check WithTop.instSupSet
-
 variable {n : ℕ} {P : Findist n} {X Y : FinRV n ℚ} {t : ℚ}
 
 --TODO: can we use isLUB
@@ -164,7 +158,7 @@ theorem rv_le_compl_gt : (X ≤ᵣ t) + (X >ᵣ t) = 1 := by
   ext ω
   unfold FinRV.leq FinRV.gt
   simp
-  grind
+  exact le_or_gt (X ω) t
 
 theorem prob_le_compl_gt : ℙ[X ≤ᵣ t // P] + ℙ[X >ᵣ t // P] = 1 := by
   rw [prob_eq_exp_ind, prob_eq_exp_ind, ← exp_additive_two]
@@ -180,15 +174,13 @@ theorem prob_le_compl_gt : ℙ[X ≤ᵣ t // P] + ℙ[X >ᵣ t // P] = 1 := by
   rw [h]
   exact exp_one
 
-
 theorem prob_gt_of_le : ℙ[X >ᵣ t // P] = 1 -  ℙ[X ≤ᵣ t // P] := by
   rw [← prob_le_compl_gt]
-  linarith
+  ring
 
 theorem prob_le_of_gt :  ℙ[X ≤ᵣ t // P] = 1 - ℙ[X >ᵣ t // P] := by
   rw [← prob_le_compl_gt]
-  linarith
-
+  ring
 
 theorem prob_lt_compl_ge : ℙ[X <ᵣ t // P] + ℙ[X ≥ᵣ t // P] = 1 := by
   rw [prob_eq_exp_ind, prob_eq_exp_ind, ← exp_additive_two]
@@ -206,11 +198,11 @@ theorem prob_lt_compl_ge : ℙ[X <ᵣ t // P] + ℙ[X ≥ᵣ t // P] = 1 := by
 
 theorem prob_ge_of_lt : ℙ[X ≥ᵣ t // P] = 1 -  ℙ[X <ᵣ t // P] := by
   rw [← prob_lt_compl_ge]
-  linarith
+  ring 
 
 theorem prob_lt_of_ge :  ℙ[X <ᵣ t // P] = 1 - ℙ[X ≥ᵣ t // P] := by
   rw [← prob_lt_compl_ge]
-  linarith
+  ring 
 
 variable {n : ℕ} (P : Findist n) (X Y : FinRV n ℚ) (α : ℚ) (q v : ℚ)