From 34222ab156aa8598ff8dca6689369599ced7ff4b Mon Sep 17 00:00:00 2001 From: ebunle Date: Tue, 2 Dec 2025 10:10:28 -0500 Subject: [PATCH 1/6] Blueprint Prroof of Non-Degenracy --- blueprint/src/content.tex | 48 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index e312163..c2c38e0 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -573,6 +573,54 @@ \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},P)$ 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 P(\{\omega\in\Omega:X(\omega)=0\})=1. +\] +\end{theorem} + +\begin{proof} +\textit{Proof of ($\Leftarrow$):} Assume $P(X=0)=1$. +If $P(X=0)=1$, then $P(X\neq0)=0$. +In discrete terms: $p_i=0$ for all $\omega_i$ such that $X_i\neq0$. +Now compute $E[|X|]$: +\[ +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: +\[ +P(X\neq0)=\sum_{\omega_i\in N} p_i =\sum_{\omega_i\in N} 0=0. +\] +Thus $P(X=0)=1-P(X\neq0)=1$. Hence, we conclude that +\[ +E[|X|]=0 \Longleftrightarrow P(X=0)=1. +\] +\end{proof} + + + + \section{Formal Decision Framework} \subsection{Markov Decision Process} From 680b4ebf7b58a9f479517ce42cfab38bb687e40c Mon Sep 17 00:00:00 2001 From: ebunle Date: Tue, 2 Dec 2025 10:12:35 -0500 Subject: [PATCH 2/6] Blueprint Prroof of Non-Degeneracy --- blueprint/src/content.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index c2c38e0..aa48560 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -575,7 +575,7 @@ \subsection{Total Expectation and Probability} -%% Non Degeneracy +%% -- Non-Degeneracy \subsection{Non-Degeneracy} \begin{theorem}[Non-degeneracy of $L_1$-norm] \label{thm:non-degeneracy} Let $(\Omega,\mathcal{F},P)$ 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 From b1b68d2ae17d2fdcc30b2a122e999850db3d3fd4 Mon Sep 17 00:00:00 2001 From: ebunle Date: Tue, 2 Dec 2025 18:21:00 -0500 Subject: [PATCH 3/6] Blueprint Proof of Non-Degeneracy --- blueprint/src/content.tex | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index aa48560..668ecf9 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -588,11 +588,12 @@ \subsection{Non-Degeneracy} \textit{Proof of ($\Leftarrow$):} Assume $P(X=0)=1$. If $P(X=0)=1$, then $P(X\neq0)=0$. In discrete terms: $p_i=0$ for all $\omega_i$ such that $X_i\neq0$. -Now compute $E[|X|]$: +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 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$. From af639c982058e81f8b044877afb11f1f0e5a8bdf Mon Sep 17 00:00:00 2001 From: ebunle Date: Tue, 2 Dec 2025 18:44:00 -0500 Subject: [PATCH 4/6] Blueprint Proof of Non-Degeneracy --- blueprint/src/content.tex | 54 +++++++++++++++++++++++++++++---------- 1 file changed, 41 insertions(+), 13 deletions(-) diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index 668ecf9..ea7a687 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -578,29 +578,29 @@ \subsection{Total Expectation and Probability} %% -- Non-Degeneracy \subsection{Non-Degeneracy} \begin{theorem}[Non-degeneracy of $L_1$-norm] \label{thm:non-degeneracy} -Let $(\Omega,\mathcal{F},P)$ 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 +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 P(\{\omega\in\Omega:X(\omega)=0\})=1. +\E[|X|]=0 \Longleftrightarrow \PP(\{\omega\in\Omega:X(\omega)=0\})=1. \] \end{theorem} \begin{proof} -\textit{Proof of ($\Leftarrow$):} Assume $P(X=0)=1$. -If $P(X=0)=1$, then $P(X\neq0)=0$. -In discrete terms: $p_i=0$ for all $\omega_i$ such that $X_i\neq0$. -Now compute $E[|X|]$ such that +\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. +\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$. +Every term is zero, so $\E[|X|]=0$. -\textit{Proof of ($\Rightarrow$):} Assume $E[|X|]=0$. +\textit{Proof of ($\Rightarrow$):} Assume $\E[|X|]=0$. We have \[ -E[|X|]=\sum_i |X_i| \cdot p_i=0, +\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 \[ @@ -611,17 +611,45 @@ \subsection{Non-Degeneracy} 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: \[ -P(X\neq0)=\sum_{\omega_i\in N} p_i =\sum_{\omega_i\in N} 0=0. +\PP(X\neq0)=\sum_{\omega_i\in N} p_i =\sum_{\omega_i\in N} 0=0. \] -Thus $P(X=0)=1-P(X\neq0)=1$. Hence, we conclude that +Thus $\P(X=0)=1-\PP(X\neq0)=1$. Hence, we conclude that \[ -E[|X|]=0 \Longleftrightarrow P(X=0)=1. +\E[|X|]=0 \Longleftrightarrow \PP(X=0)=1. \] \end{proof} + + + + + + + + + + + + + + + + + + + + + + + + + + + + \section{Formal Decision Framework} \subsection{Markov Decision Process} From e24e508a05b1d98ece7007e8b668f204f78db8c6 Mon Sep 17 00:00:00 2001 From: ebunle Date: Tue, 2 Dec 2025 18:45:04 -0500 Subject: [PATCH 5/6] Blueprint Proof of Non-Degeneracy --- blueprint/src/content.tex | 31 ------------------------------- 1 file changed, 31 deletions(-) diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index ea7a687..c21c688 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -574,7 +574,6 @@ \subsection{Total Expectation and Probability} \end{proof} - %% -- Non-Degeneracy \subsection{Non-Degeneracy} \begin{theorem}[Non-degeneracy of $L_1$-norm] \label{thm:non-degeneracy} @@ -620,36 +619,6 @@ \subsection{Non-Degeneracy} \end{proof} - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - \section{Formal Decision Framework} \subsection{Markov Decision Process} From 01004c04a6d5b1a12631aacd9bdd16940c84fae9 Mon Sep 17 00:00:00 2001 From: ebunle Date: Thu, 4 Dec 2025 10:31:21 -0500 Subject: [PATCH 6/6] Absolute value for random variables --- Probability/Probability/Basic.lean | 64 +++++++++++++++++++----------- 1 file changed, 41 insertions(+), 23 deletions(-) diff --git a/Probability/Probability/Basic.lean b/Probability/Probability/Basic.lean index 62ed81e..e0d991b 100644 --- a/Probability/Probability/Basic.lean +++ b/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