expectation probability cleanup

marekpetrik · Dec 28, 2024 · 1c90249 · 1c90249
1 parent 478aa67
commit 1c90249
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/LeanMDPs/FinPr.lean b/LeanMDPs/FinPr.lean
@@ -109,14 +109,14 @@ def expect_cnd_rv (X : Finrv P ρ) (Y : Finrv P V) : Finrv P ρ :=
 notation "𝔼[" X "|ᵥ" Y "]" => expect_cnd_rv X Y
 
 
-/- ------------ Law of total expectation ----------/
+/- ------------ Law of the unconscious statistician ----------/
 
+/-- Conditional version of the Law of the unconscious statistician -/
 theorem unconscious_statistician_cnd (X : Finrv P ρ) (Y : Finrv P V) :
   ∀ ω ∈ P.Ω, Finrv.val 𝔼[X |ᵥ Y ] ω =  ∑ y ∈ V, ℙ[ Y ᵣ== (Y.val ω) ]* 𝔼[X | Y ᵣ== (Y.val ω) ]  :=
     sorry
 
 
-
 /- ------------ Law of total expectation ----------/
 
 theorem total_expectation (X : Finrv P ρ) (Y : Finrv P V) :