small namespace and proof cleanup

Author: marekpetrik

Probability/Probability/Basic.lean

@@ -8,23 +8,23 @@ import Mathlib.Data.Fintype.BigOperators
   # Basic properties for probability spaces and expectations
 
   The main results:
-  - Arithmetic manipulations of random variables
-  - The law of total probabilities
+  - LOTUS: The law of the unconscious statistician 
   - The law of total expectations
+  - The law of total probabilities
 -/
 
 namespace Findist
 
 variable {n : ℕ} {P : Findist n} {B : FinRV n Bool}
 
 theorem ge_zero : 0 ≤ ℙ[B // P] := 
-    by rw [Ex.prob_eq_exp_ind]
+    by rw [prob_eq_exp_ind]
        calc 0 = 𝔼[0 // P] := exp_const.symm 
             _ ≤ 𝔼[𝕀 ∘ B//P] := exp_monotone ind_nneg
 
 
 theorem le_one : ℙ[B // P] ≤ 1 := 
-    by rw [Ex.prob_eq_exp_ind]
+    by rw [prob_eq_exp_ind]
        calc 𝔼[𝕀 ∘ B//P] ≤ 𝔼[1 // P] := exp_monotone ind_le_one 
             _ = 1 := exp_const 
 
@@ -34,33 +34,16 @@ end Findist
 
 ------------------------------ Probability ---------------------------
 
-namespace Pr
-
 variable {n : ℕ} {P : Findist n} {B C : FinRV n Bool}
 
 theorem prob_compl_sums_to_one : ℙ[B // P] + ℙ[¬ᵣB // P] = 1 := 
-    by rw [Ex.prob_eq_exp_ind, Ex.prob_eq_exp_ind, ←exp_dists_add, one_of_ind_bool_or_not]
+    by rw [prob_eq_exp_ind, prob_eq_exp_ind, ←exp_dists_add, one_of_ind_bool_or_not]
        exact exp_one 
 
-
 theorem prob_compl_one_minus : ℙ[¬ᵣB // P] = 1 - ℙ[B // P] :=
     by rw [←prob_compl_sums_to_one (P:=P) (B:=B)]; ring 
 
 
------------------------------- Expectation ---------------------------
-
-namespace PMF
-
-variable {n : ℕ} {k : ℕ}  {L : FinRV n (Fin k)}
-variable {pmf : Fin k → ℚ} {P : Findist n}
-
-theorem pmf_rv_k_ge_1 (h : PMF pmf P L)  : 0 < k :=
-  match k with  
-  | Nat.zero =>   Fin.pos <| L ⟨0,P.nonempty⟩
-  | Nat.succ k₂ => Nat.zero_lt_succ k₂
-
-end PMF
-
 ------------------------------ Expectation ---------------------------
 
 namespace Ex
@@ -69,8 +52,8 @@ variable {n : ℕ} {P : Findist n}
 variable {k : ℕ} {X : FinRV n ℚ} {B : FinRV n Bool} {L : FinRV n (Fin k)}
 variable  (g : Fin k → ℚ)
 
-/-- LOTUS: the law of the unconscious statistician (or similar) -/
-theorem LOTUS (g : Fin k → ℚ) : 𝔼[g ∘ L // P ] = ∑ i, ℙ[L =ᵣ i // P] * (g i) :=
+/-- LOTUS: The law of the unconscious statistician (or similar) -/
+theorem LOTUS : 𝔼[g ∘ L // P ] = ∑ i, ℙ[L =ᵣ i // P] * (g i) :=
   by rewrite [exp_decompose (X := g ∘ L) (L := L) ]
      apply Fintype.sum_congr
      intro i
@@ -93,52 +76,16 @@ theorem law_total_exp : 𝔼[𝔼[X |ᵣ L // P] // P] = 𝔼[X // P] :=
 
 end Ex
 
-
-
--- TODO: I think that we can show the following results from the law of total expectations
-
---TODO: theorem law_of_total_probs_bool : ℙ[B // P] = ℙ[B * C // P] + ℙ[B * (¬ᵣC) // P] :=
-/-  by
-    unfold probability
-    have h : ∀ i : Fin n, (𝕀 (B i)) = (𝕀 (B i * C i)) + (𝕀 (B i * (¬ᵣ C) i)) :=
-      by
-        intro i
-        by_cases hB : B i
-        · by_cases hC : C i
-          · simp [hB, hC, FinRV.not, indicator]
-          · simp [hB, hC, FinRV.not, indicator]
-        · by_cases hC : C i
-          · simp [hB, hC, FinRV.not, indicator]
-          · simp [hB, hC, FinRV.not, indicator]
-    sorry ---I tried to do this proof but got stuck, feel free to delete my work
--/
-
---TODO: theorem conditional_total (h : 0 < ℙ[C // P]) : ℙ[B * C // P] =  ℙ[B | C // P] * ℙ[C // P] :=
-  -- by simp [probability_cnd] at ⊢ h
-  --    have : P.ℙ.iprodb C * (P.ℙ.iprodb C)⁻¹ = 1 :=
-  --           Rat.mul_inv_cancel (P.ℙ.iprodb C) (Ne.symm (ne_of_lt h))
-  --    calc
-  --       P.ℙ.iprodb (B ∧ᵣC) = P.ℙ.iprodb (B ∧ᵣC) * 1 := by ring
-  --       _ = P.ℙ.iprodb (B ∧ᵣC) * (P.ℙ.iprodb C * (P.ℙ.iprodb C)⁻¹) := by rw [←this]
-  --       _ = P.ℙ.iprodb (B ∧ᵣ C) / P.ℙ.iprodb C * P.ℙ.iprodb C := by ring
-
-
---TODO: theorem law_total_prbs_cnd  (h1 : 0 < ℙ[C // P]) (h2 : ℙ[C // P] < 1)
---: ℙ[B // P] = ℙ[B | C // P] * ℙ[ C // P] + ℙ[B | ¬ᵣC // P] * ℙ[¬ᵣC // P] :=
---        by have h2' : 0 < ℙ[¬ᵣC // P] := by rw [prob_compl_one_minus]; linarith
---           rw [←conditional_total P B C h1]
---           rw [←conditional_total P B (¬ᵣC) h2']
---           exact law_of_total_probs_bool P B C
+namespace Pr
 
 variable {k : ℕ}  {L : FinRV n (Fin k)}
 
-
 /-- The law of total probabilities -/
 theorem law_of_total_probs : ℙ[B // P] =  ∑ i, ℙ[B * (L =ᵣ i) // P]  := 
-  by rewrite [Ex.prob_eq_exp_ind, rv_decompose (𝕀∘B) L, exp_additive]
+  by rewrite [prob_eq_exp_ind, rv_decompose (𝕀∘B) L, exp_additive]
      apply Fintype.sum_congr
      intro i 
-     rewrite [Ex.prob_eq_exp_ind] 
+     rewrite [prob_eq_exp_ind] 
      apply exp_congr
      ext ω
      by_cases h1 : L ω = i 

Probability/Probability/Defs.lean

@@ -157,10 +157,9 @@ variable {k : ℕ} {L : FinRV n (Fin k)}
 theorem indi_eq_indr : ∀i : Fin k, (𝕀 ∘ (L =ᵣ i)) = (L =ᵢ i) := by
   intro i; unfold FinRV.eq FinRV.eqi 𝕀 indicator; ext ω; by_cases h: L ω = i; repeat simp [h]
 
-
 variable {B : FinRV n Bool}
 /-- Indicator is 0 or 1 -/
-theorem ind_zero_one  :  ∀ ω, (𝕀∘B) ω = 1 ∨ (𝕀∘B) ω = 0 := by
+theorem ind_zero_one : ∀ ω, (𝕀∘B) ω = 1 ∨ (𝕀∘B) ω = 0 := by
     intro ω
     by_cases h : B ω
     · left; simp only [Function.comp_apply, h, indicator]
@@ -190,14 +189,12 @@ theorem one_of_ind_bool_or_not : (𝕀∘B) + (𝕀∘(¬ᵣ B)) = (1 : FinRV n
        · simp [h]
        · simp [h]
 
-variable {X Y: FinRV n ℚ}
+variable {X Y: FinRV n ℚ} {Xs : Fin k → FinRV n ℚ}
 
 theorem rv_le_abs : X ≤ abs ∘ X := by intro i; simp [le_abs_self (X i)]
 
-theorem rv_prod_sum_additive {Xs : Fin k → FinRV n ℚ} : ∑ i, Y * (Xs i) = Y * (∑ i, Xs i) :=
-    by ext ω
-       simp
-       rw [Finset.mul_sum]
+theorem rv_prod_sum_additive  : ∑ i, Y * (Xs i) = Y * (∑ i, Xs i) :=
+    by ext ω; simp [Finset.mul_sum]
 
 variable {g : Fin k → ℚ}
 
@@ -221,9 +218,6 @@ notation "ℙ[" B "//" P "]" => probability P B
 -- helps to refold is when needed
 lemma probability_def : P.p ⬝ᵥ (𝕀 ∘ B) = ℙ[B // P] := rfl
 
--- TODO: the sorry in the definition has to do with the decidability of the membership
---theorem prob_iprod_eq_def : ℙ[B // P] = P.measure (B.preimage true) sorry := sorry
-
 /-- Conditional probability of B -/
 def probability_cnd : ℚ := ℙ[B * C // P] / ℙ[ C // P ]
 
@@ -234,8 +228,7 @@ notation "ℙ[" B "|" C "//" P "]" => probability_cnd P B C
 
 theorem prob_one_of_true : ℙ[1 // P] = 1 :=
     by unfold probability
-       rw[one_of_true]
-       rw [dotProduct_comm]
+       rewrite [one_of_true, dotProduct_comm]
        exact P.prob
 
 example {a b : ℚ} (h : 0 ≤ a) (h2 : 0 ≤ b) : 0 ≤ a * b :=  Rat.mul_nonneg h h2
@@ -245,7 +238,6 @@ variable {P : Findist n} {B : FinRV n Bool}
 theorem prod_zero_of_prob_zero : ℙ[B // P] = 0 → (P.p * (𝕀∘B) = 0) := by
     intro h; exact prod_eq_zero_of_nneg_dp_zero P.nneg ind_nneg h
 
-
 ------------------------------ PMF ---------------------------
 
 /-- Proof that p is a the PMF of X on probability space P -/
@@ -254,6 +246,15 @@ def PMF {K : ℕ} (pmf : Fin K → ℚ) (P : Findist n) (L : FinRV n (Fin K)) :=
 
 namespace PMF
 
+variable {n : ℕ} {k : ℕ}  {L : FinRV n (Fin k)}
+variable {pmf : Fin k → ℚ} {P : Findist n}
+
+theorem pmf_rv_k_ge_1 (h : PMF pmf P L)  : 0 < k :=
+  match k with  
+  | Nat.zero => Fin.pos <| L ⟨0,P.nonempty⟩
+  | Nat.succ k₂ => Nat.zero_lt_succ k₂
+
+
 
 end PMF
 
@@ -270,7 +271,6 @@ Main results
 -/
 
 
-namespace Ex
 
 
 variable {n : ℕ} (P : Findist n) (X Y Z: FinRV n ℚ) (B : FinRV n Bool)
@@ -302,15 +302,15 @@ def expect_cnd_rv : Fin n → ℚ := fun i ↦ 𝔼[ X | L =ᵣ (L i) // P ]
 
 notation "𝔼[" X "|ᵣ" L "//" P "]" => expect_cnd_rv P X L
 
-end Ex
+
 --- some basic properties
 
 section Expectation_properties
 variable {P : Findist n} {X Y Z: FinRV n ℚ} {B : FinRV n Bool}
 
 theorem exp_congr : (X = Y) → 𝔼[X // P] = 𝔼[Y // P] :=
   by intro h
-     unfold Ex.expect dotProduct
+     unfold expect dotProduct
      apply Fintype.sum_congr
      simp_all
 
@@ -320,40 +320,40 @@ theorem exp_mul_comm : 𝔼[X * Y // P] = 𝔼[Y * X // P] := exp_congr (CommMon
 variable {c : ℚ} {p : Fin n → ℚ}
 
 theorem exp_const : 𝔼[(fun _ ↦ c) // P] = c :=
-    by unfold Ex.expect
-       rw [rv_const_fun_to_one]
-       simp only [dotProduct_smul, smul_eq_mul]
-       rw [dotProduct_comm, P.prob]
-       simp
+  by unfold expect
+     rw [rv_const_fun_to_one]
+     simp only [dotProduct_smul, smul_eq_mul]
+     rw [dotProduct_comm, P.prob]
+     simp
 
 theorem exp_one : 𝔼[ 1 // P] = 1  := exp_const
 
 theorem exp_cond_eq_def  : 𝔼[X | B // P] * ℙ[B // P] = 𝔼[X * (𝕀 ∘ B) // P] :=
-    by unfold Ex.expect_cnd 
-       by_cases h: ℙ[B//P] = 0
-       · rw [h, Rat.mul_zero]
-         unfold Ex.expect 
-         rw [dotProd_hadProd_comm, dotProd_hadProd_rotate, prod_zero_of_prob_zero h]
-         exact (dotProduct_zero X).symm 
-       · simp_all 
+  by unfold expect_cnd 
+     by_cases h: ℙ[B//P] = 0
+     · rw [h, Rat.mul_zero]
+       unfold expect 
+       rw [dotProd_hadProd_comm, dotProd_hadProd_rotate, prod_zero_of_prob_zero h]
+       exact (dotProduct_zero X).symm 
+     · simp_all 
 
 
 lemma constant_mul_eq_smul : (fun ω ↦ c * X ω) = c • X := rfl
 
 theorem exp_prod_const_fun : 𝔼[(λ _ ↦ c) * X // P] = c * 𝔼[X // P] :=
-  by simp only [Ex.expect, Pi.mul_def, constant_mul_eq_smul, dotProduct_smul, smul_eq_mul]
+  by simp only [expect, Pi.mul_def, constant_mul_eq_smul, dotProduct_smul, smul_eq_mul]
 
 theorem exp_indi_eq_exp_indr : ∀i : Fin k, 𝔼[L =ᵢ i // P] = 𝔼[𝕀 ∘ (L =ᵣ i) // P] := by
   intro i; rw [indi_eq_indr]
 
 /-- Expectation is homogeneous under product -/
-theorem exp_homogenous : 𝔼[c • X // P] = c * 𝔼[X // P] := by simp only [Ex.expect, dotProduct_smul, smul_eq_mul]
+theorem exp_homogenous : 𝔼[c • X // P] = c * 𝔼[X // P] := by simp only [expect, dotProduct_smul, smul_eq_mul]
 
-theorem exp_dists_add : 𝔼[X + Y // P] = 𝔼[X // P] + 𝔼[Y // P] := by simp [Ex.expect]
+theorem exp_dists_add : 𝔼[X + Y // P] = 𝔼[X // P] + 𝔼[Y // P] := by simp [expect]
 
 /-- Additivity of expectation --/
 theorem exp_additive {m : ℕ} (Xs : Fin m → FinRV n ℚ) : 𝔼[∑ i : Fin m, Xs i // P] = ∑ i : Fin m, 𝔼[Xs i // P] := 
-  by unfold Ex.expect; exact dotProduct_sum P.p Finset.univ Xs
+  by unfold expect; exact dotProduct_sum P.p Finset.univ Xs
 
 /-- Expectation is monotone  -/
 theorem exp_monotone (h: X ≤ Y)  : 𝔼[X // P] ≤ 𝔼[Y // P] :=  dotProduct_le_dotProduct_of_nonneg_left h P.nneg
@@ -371,9 +371,9 @@ theorem exp_decompose : 𝔼[X // P] = ∑ i, 𝔼[X * (L =ᵢ i) // P] :=
 /-- Expectation of a conditional constant. Only when probability is positive.  -/
 theorem exp_cond_const : ∀ i, ℙ[L =ᵣ i //   P] ≠ 0 → 𝔼[g ∘ L | L =ᵣ i // P] = g i := 
     by intro i h 
-       unfold Ex.expect_cnd
+       unfold expect_cnd
        rw [indi_eq_indr, rv_prod_const i, exp_homogenous]
-       rw [←indi_eq_indr, ←Ex.prob_eq_exp_ind]
+       rw [←indi_eq_indr, ←prob_eq_exp_ind]
        simp only [h, ne_eq, isUnit_iff_ne_zero, not_false_eq_true, IsUnit.mul_div_cancel_right]
 
 end Expectation_properties