Blueprint Proof of Non-Degeneracy

Probability/Probability/Basic.lean

@@ -8,7 +8,7 @@ import Mathlib.Data.Fintype.BigOperators
   # Basic properties for probability spaces and expectations
 
   The main results:
-  - LOTUS: The law of the unconscious statistician 
+  - LOTUS: The law of the unconscious statistician
   - The law of total expectations
   - The law of total probabilities
 -/
@@ -17,16 +17,16 @@ namespace Findist
 
 variable {n : ℕ} {P : Findist n} {B : FinRV n Bool}
 
-theorem ge_zero : 0 ≤ ℙ[B // P] := 
+theorem ge_zero : 0 ≤ ℙ[B // P] :=
     by rw [prob_eq_exp_ind]
-       calc 0 = 𝔼[0 // P] := exp_const.symm 
+       calc 0 = 𝔼[0 // P] := exp_const.symm
             _ ≤ 𝔼[𝕀 ∘ B//P] := exp_monotone ind_nneg
-
 
-theorem le_one : ℙ[B // P] ≤ 1 := 
+
+theorem le_one : ℙ[B // P] ≤ 1 :=
     by rw [prob_eq_exp_ind]
-       calc 𝔼[𝕀 ∘ B//P] ≤ 𝔼[1 // P] := exp_monotone ind_le_one 
-            _ = 1 := exp_const 
+       calc 𝔼[𝕀 ∘ B//P] ≤ 𝔼[1 // P] := exp_monotone ind_le_one
+            _ = 1 := exp_const
 
 theorem in_prob (P : Findist n) : Prob ℙ[B // P] := ⟨ge_zero, le_one⟩
 
@@ -36,17 +36,17 @@ end Findist
 
 variable {n : ℕ} {P : Findist n} {B C : FinRV n Bool}
 
-theorem prob_compl_sums_to_one : ℙ[B // P] + ℙ[¬ᵣB // P] = 1 := 
+theorem prob_compl_sums_to_one : ℙ[B // P] + ℙ[¬ᵣB // P] = 1 :=
     by rw [prob_eq_exp_ind, prob_eq_exp_ind, ←exp_dists_add, one_of_ind_bool_or_not]
-       exact exp_one 
+       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 
+    by rw [←prob_compl_sums_to_one (P:=P) (B:=B)]; ring
 
 
 ------------------------------ Expectation ---------------------------
 
-section Expectation 
+section Expectation
 
 variable {n : ℕ} {P : Findist n}
 variable {k : ℕ} {X : FinRV n ℚ} {B : FinRV n Bool} {L : FinRV n (Fin k)}
@@ -59,38 +59,56 @@ theorem LOTUS : 𝔼[g ∘ L // P ] = ∑ i, ℙ[L =ᵣ i // P] * (g i) :=
      intro i
      rewrite [←indi_eq_indr]
      rewrite [←exp_cond_eq_def (X := g ∘ L) ]
-     by_cases! h : ℙ[L =ᵣ i // P] = 0 
+     by_cases! h : ℙ[L =ᵣ i // P] = 0
      · rw [h];  simp only [mul_zero, zero_mul]
      · rw [exp_cond_const i h ]
-       ring 
+       ring
 
 theorem law_total_exp : 𝔼[𝔼[X |ᵣ L // P] // P] = 𝔼[X // P] :=
   let g i := 𝔼[X | L =ᵣ i // P]
   calc
     𝔼[𝔼[X |ᵣ L // P] // P ] = ∑ i , ℙ[ L =ᵣ i // P] * 𝔼[ X | L =ᵣ i // P ] := LOTUS g
-    _ =  ∑ i , 𝔼[ X | L =ᵣ i // P ] * ℙ[ L =ᵣ i // P] := by apply Fintype.sum_congr; intro i; ring 
+    _ =  ∑ i , 𝔼[ X | L =ᵣ i // P ] * ℙ[ L =ᵣ i // P] := by apply Fintype.sum_congr; intro i; ring
     _ =  ∑ i : Fin k, 𝔼[X * (𝕀 ∘ (L =ᵣ i)) // P] := by apply Fintype.sum_congr; exact fun a  ↦ exp_cond_eq_def
-    _ =  ∑ i : Fin k, 𝔼[X * (L =ᵢ i) // P] := by apply Fintype.sum_congr; intro i; apply exp_congr; rw[indi_eq_indr] 
+    _ =  ∑ i : Fin k, 𝔼[X * (L =ᵢ i) // P] := by apply Fintype.sum_congr; intro i; apply exp_congr; rw[indi_eq_indr]
     _ = 𝔼[X // P]  := by rw [←exp_decompose]
 
-end Expectation 
+end Expectation
+
+
+namespace Nondegeneracy
+
+-- Absolute value for random variables
+def abs (X : FinRV n ℚ) : FinRV n ℚ :=
+  fun i => |X i|
+
+/-- **Non-degeneracy** -/
+theorem exp_abs_eq_zero_iff_prob_one_of_zero :
+    𝔼[abs X // P] = 0 ↔ ℙ[X =ᵣ (0 : ℚ) // P] = 1 := by
+          sorry
+
+end Nondegeneracy
 
-section Probability 
+
+
+
+
+section Probability
 
 variable {k : ℕ}  {L : FinRV n (Fin k)}
 
 /-- The law of total probabilities -/
-theorem law_of_total_probs : ℙ[B // P] =  ∑ i, ℙ[B * (L =ᵣ i) // P]  := 
+theorem law_of_total_probs : ℙ[B // P] =  ∑ i, ℙ[B * (L =ᵣ i) // P]  :=
   by rewrite [prob_eq_exp_ind, rv_decompose (𝕀∘B) L, exp_additive]
      apply Fintype.sum_congr
-     intro i 
-     rewrite [prob_eq_exp_ind] 
+     intro i
+     rewrite [prob_eq_exp_ind]
      apply exp_congr
      ext ω
-     by_cases h1 : L ω = i 
+     by_cases h1 : L ω = i
      repeat by_cases h2 : B ω; repeat simp [h1, h2, 𝕀, indicator ]
 
 
-end Probability 
+end Probability
 
-#lint 
+#lint

blueprint/src/content.tex

@@ -573,6 +573,52 @@ \subsection{Total Expectation and Probability}
 \end{align*}
 \end{proof}
 
+
+%% -- Non-Degeneracy 
+\subsection{Non-Degeneracy}
+\begin{theorem}[Non-degeneracy of $L_1$-norm] \label{thm:non-degeneracy}
+Let $(\Omega,\mathcal{F},\PP)$ be a discrete probability space with $\Omega=\{\omega_1,\omega_2,\ldots\}$ countable, and let $p_i=P(\{\omega_i\})\geq0$ with $\sum_i p_i =1$. Let $X$ be a random variable with $X_i=X(\omega_i)$. Then
+\[
+\E[|X|]=0 \Longleftrightarrow \PP(\{\omega\in\Omega:X(\omega)=0\})=1.
+\]
+\end{theorem}
+
+\begin{proof}
+\textit{Proof of ($\Leftarrow$):} Assume $\PP(X=0)=1$.
+If $\PP(X=0)=1$, then $\PP(X\neq0)=0$.
+In discrete terms $p_i=0$ for all $\omega_i$ such that $X_i\neq0$.
+Now compute $\E[|X|]$ such that
+\[
+\E[|X|]=\sum_i |X_i| \cdot p_i.
+\]
+
+	Case 1: $X_i=0\Rightarrow |X_i|p_i=0\cdot p_i=0$.\\
+	Case 2: $X_i\neq0\Rightarrow p_i=0\Rightarrow |X_i|p_i=|X_i|\cdot0=0$.
+Every term is zero, so $\E[|X|]=0$.
+
+\textit{Proof of ($\Rightarrow$):} Assume $\E[|X|]=0$.
+We have
+\[
+\E[|X|]=\sum_i |X_i| \cdot p_i=0,
+\]
+where $|X_i|p_i\geq0$ for all $i$. For a sum of nonnegative terms to be zero, each term must be zero
+\[
+|X_i|p_i=0 \quad \text{for all } i.
+\]
+Thus, for each $i$, either $p_i=0$ or $|X_i|=0$ (i.e., $X_i=0$).
+Let $N=\{\omega_i:X_i\neq0\}$.
+For $\omega_i\in N$, we have $X_i\neq0\Rightarrow |X_i|\neq0\Rightarrow$ from $|X_i|p_i=0$ we must have $p_i=0$.
+Therefore:
+\[
+\PP(X\neq0)=\sum_{\omega_i\in N} p_i =\sum_{\omega_i\in N} 0=0.
+\]
+Thus $\P(X=0)=1-\PP(X\neq0)=1$. Hence, we conclude that 
+\[
+\E[|X|]=0 \Longleftrightarrow \PP(X=0)=1.
+\]
+\end{proof}
+
+
 \section{Formal Decision Framework}
 
 \subsection{Markov Decision Process}