structure Findist {τ : Type} (Ω : Finset τ) : Type

Finite probability distribution

• p : τ → NNReal
• sumsto : ∑ ω ∈ Ω, self.p ω = 1

@[reducible, inline]

abbrev Delta {τ : Type} : Finset τ → Type

Equations

• Delta = Findist

@[reducible, inline]

abbrev Δ {τ : Type} : Finset τ → Type

Equations

• Δ = Delta

structure Finprob (τ : Type) : Type

Finite probability space

• Ω : Finset τ
• prob : Findist self.Ω

structure Finrv {τ : Type} (P : Finprob τ) (ρ : Type) : Type

Random variable defined on a finite probability space

• val : τ → ρ

@[reducible]

def Finprob.p {τ : Type} (P : Finprob τ) (ω : τ) : NNReal

Probability measure

Equations

• P.p ω = P.prob.p ω

noncomputable def Finprob.filter_zero {τ : Type} (P : Finprob τ) : Finprob τ

Removes elements of Ω that have zero probability

Equations

• P.filter_zero = { Ω := Finset.filter (fun (ω : τ) => P.p ω ≠ 0) P.Ω, prob := { p := P.prob.p, sumsto := ⋯ } }

theorem prob_filtered_positive {τ : Type} {P Q : Finprob τ} (flrtd : Q = P.filter_zero) (ω : τ) : ω ∈ Q.Ω → Q.p ω > 0

noncomputable def Finrv.filter_zero {τ : Type} {P : Finprob τ} {ε : Type} (X : Finrv P ε) : Finrv P.filter_zero ε

Equations

• X.filter_zero = { val := X.val }

def Finprob.supp {τ : Type} (P : Finprob τ) (ω : τ) : Prop

Equations

• P.supp ω = (0 < P.p ω)

@[reducible]

def Finprob.indicator (cond : Bool) : NNReal

Boolean indicator function

Equations

• Finprob.indicator cond = Bool.rec 0 1 cond

@[reducible, inline]

abbrev Finprob.𝕀 : Bool → NNReal

Equations

• Finprob.𝕀 = Finprob.indicator

theorem Finprob.ind_zero_one {τ : Type} (cond : τ → Bool) (ω : τ) : (Finprob.𝕀 ∘ cond) ω = 1 ∨ (Finprob.𝕀 ∘ cond) ω = 0

Indicator is 0 or 1

theorem Finprob.ind_ge_zero {τ : Type} (cond : τ → Bool) (ω : τ) : 0 ≤ (Finprob.𝕀 ∘ cond) ω

def Finprob.expect {τ : Type} {P : Finprob τ} (X : Finrv P ℝ) : ℝ

Expectation of X

Equations

• 𝔼[X] = ∑ ω ∈ P.Ω, ↑(P.p ω) * X.val ω

def Finprob.«term𝔼[_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem Finprob.exp_ge_zero {τ : Type} {P : Finprob τ} {X : Finrv P ℝ} (gezero : ∀ ω ∈ P.Ω, 0 ≤ X.val ω) : 0 ≤ 𝔼[X]

def Finprob.probability {τ : Type} {P : Finprob τ} (B : Finrv P Bool) : NNReal

Probability of B

Equations

• ℙ[B] = ⟨𝔼[{ val := fun (ω : τ) => ↑(Finprob.𝕀 (B.val ω)) }], ⋯⟩

def Finprob.«termℙ[_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

noncomputable def Finprob.expect_cnd {τ : Type} {P : Finprob τ} (X : Finrv P ℝ) (B : Finrv P Bool) : ℝ

Expected value 𝔼[X|B] conditional on a Bool random variable IMPORTANT: conditional expectation for zero probability B is zero

Equations

• 𝔼[X|B] = ↑ℙ[B]⁻¹ * 𝔼[{ val := fun (ω : τ) => ↑((Finprob.𝕀 ∘ B.val) ω) * X.val ω }]

def Finprob.«term𝔼[_|_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem Finprob.exp_cnd_ge_zero {τ : Type} {P : Finprob τ} {X : Finrv P ℝ} {B : Finrv P Bool} (gezero : ∀ ω ∈ P.Ω, 0 ≤ X.val ω) : 0 ≤ 𝔼[X|B]

@[reducible]

noncomputable def Finprob.probability_cnd {τ : Type} {P : Finprob τ} (B C : Finrv P Bool) : NNReal

Conditional probability of B

Equations

• ℙ[B|C] = ⟨𝔼[{ val := fun (ω : τ) => ↑((Finprob.𝕀 ∘ B.val) ω) }|C], ⋯⟩

def Finprob.«termℙ[_|_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def Finprob.EqRV {τ : Type} {P : Finprob τ} {η : Type} [DecidableEq η] (Y : Finrv P η) (y : η) : Finrv P Bool

Random variable equality

Equations

• (Y ᵣ== y) = { val := fun (ω : τ) => Y.val ω == y }

def Finprob.«term_ᵣ==_» : Lean.TrailingParserDescr

Equations

• Finprob.«term_ᵣ==_» = Lean.ParserDescr.trailingNode `Finprob.«term_ᵣ==_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ᵣ== ") (Lean.ParserDescr.cat `term 51))

@[reducible]

def Finprob.AndRV {τ : Type} {P : Finprob τ} (B C : Finrv P Bool) : Finrv P Bool

Equations

• (B ∧ᵣ C) = { val := fun (ω : τ) => B.val ω && C.val ω }

def Finprob.«term_∧ᵣ_» : Lean.TrailingParserDescr

Equations

• Finprob.«term_∧ᵣ_» = Lean.ParserDescr.trailingNode `Finprob.«term_∧ᵣ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∧ᵣ ") (Lean.ParserDescr.cat `term 51))

@[reducible]

def Finprob.OrRV {τ : Type} {P : Finprob τ} (B C : Finrv P Bool) : Finrv P Bool

Equations

• (B ∨ᵣ C) = { val := fun (ω : τ) => B.val ω || C.val ω }

def Finprob.«term_∨ᵣ_» : Lean.TrailingParserDescr

Equations

• Finprob.«term_∨ᵣ_» = Lean.ParserDescr.trailingNode `Finprob.«term_∨ᵣ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∨ᵣ ") (Lean.ParserDescr.cat `term 51))

@[reducible]

noncomputable def Finprob.expect_cnd_rv {τ : Type} {P : Finprob τ} {ν : Type} [DecidableEq ν] {V : Finset ν} (X : Finrv P ℝ) (Y : Finrv P { x : ν // x ∈ V }) : Finrv P ℝ

Expectation conditioned on a finite-valued random variable -

Equations

• 𝔼[X|ᵥY] = { val := fun (ω : τ) => 𝔼[X|Y ᵣ== Y.val ω] }

def Finprob.«term𝔼[_|ᵥ_]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

instance Finprob.instConstRV {τ : Type} {P : Finprob τ} : Coe ℝ (Finrv P ℝ)

Equations

• Finprob.instConstRV = { coe := fun (c : ℝ) => { val := fun (x : τ) => c } }

instance Finprob.instRVadd {τ : Type} {P : Finprob τ} : HAdd (Finrv P ℝ) (Finrv P ℝ) (Finrv P ℝ)

Equations

• Finprob.instRVadd = { hAdd := fun (l r : Finrv P ℝ) => { val := fun (ω : τ) => l.val ω + r.val ω } }

instance Finprob.instRVmul {τ : Type} {P : Finprob τ} [HMul ℝ ℝ ℝ] : HMul ℝ (Finrv P ℝ) (Finrv P ℝ)

Equations

• Finprob.instRVmul = { hMul := fun (l : ℝ) (r : Finrv P ℝ) => { val := fun (ω : τ) => l * r.val ω } }

def Finprob.dirac_ofsingleton {τ : Type} (t : τ) : Findist {t}

Construct a dirac distribution

Equations

• Finprob.dirac_ofsingleton t = { p := fun (x : τ) => 1, sumsto := ⋯ }

def Finprob.dirac_dist {τ : Type} [DecidableEq τ] (T : Finset τ) (t : { x : τ // x ∈ T }) : Findist T

Dirac distribution over T with P[t] = 1

Equations

• Finprob.dirac_dist T t = { p := fun (x : τ) => if x = ↑t then 1 else 0, sumsto := ⋯ }

theorem Finprob.ind_and_eq_prod_ind {τ : Type} {P : Finprob τ} {B C : Finrv P Bool} (ω : τ) : ω ∈ P.Ω → Finprob.𝕀 ((B ∧ᵣ C).val ω) = (Finprob.𝕀 ∘ B.val) ω * (Finprob.𝕀 ∘ C.val) ω

theorem Finprob.exp_zero_cond {τ : Type} {P : Finprob τ} {X : Finrv P ℝ} {C : Finrv P Bool} (zero : ℙ[C] = 0) : 𝔼[X|C] = 0

theorem Finprob.prob_zero_cond {τ : Type} {P : Finprob τ} {B C : Finrv P Bool} (zero : ℙ[C] = 0) : ℙ[B|C] = 0

theorem Finprob.prob_eq_prob_cond_prod {τ : Type} {P : Finprob τ} {B C : Finrv P Bool} : ℙ[B ∧ᵣ C] = ℙ[B|C] * ℙ[C]

theorem Finprob.prob_ge_measure {τ : Type} {P : Finprob τ} {ν : Type} [DecidableEq ν] {V : Finset ν} {Y : Finrv P { x : ν // x ∈ V }} (ω : τ) : ω ∈ P.Ω → ℙ[Y ᵣ== Y.val ω] ≥ P.p ω

theorem Finprob.exp_omit_zero {τ : Type} {P : Finprob τ} {X : Finrv P ℝ} : 𝔼[X] = 𝔼[X.filter_zero]

theorem Finprob.exp_add_rv {τ : Type} {P : Finprob τ} {X Z : Finrv P ℝ} : 𝔼[X + Z] = 𝔼[X] + 𝔼[Z]

theorem Finprob.exp_const {τ : Type} {P : Finprob τ} {c : ℝ} : 𝔼[{ val := fun (x : τ) => c }] = c

theorem Finprob.exp_add_const {τ : Type} {P : Finprob τ} {X : Finrv P ℝ} {c : ℝ} : 𝔼[{ val := fun (x : τ) => c } + X] = c + 𝔼[X]

theorem Finprob.exp_cnd_rv_add_const {τ : Type} {P : Finprob τ} {ν : Type} [DecidableEq ν] {V : Finset ν} {X : Finrv P ℝ} {Y : Finrv P { x : ν // x ∈ V }} {c : ℝ} (ω : τ) : ω ∈ P.Ω → 𝔼[{ val := fun (x : τ) => c } + X|ᵥY].val ω = c + 𝔼[X|ᵥY].val ω

theorem Finprob.exp_monotone {τ : Type} {P : Finprob τ} {X Z : Finrv P ℝ} (ge : ∀ ω ∈ P.Ω, ∀ ω ∈ P.Ω, P.prob.p ω > 0 → X.val ω ≥ Z.val ω) : 𝔼[X] ≥ 𝔼[Z]

theorem Finprob.exp_congr {τ : Type} {P : Finprob τ} {X Z : Finrv P ℝ} (rv_same : ∀ ω ∈ P.Ω, P.supp ω → X.val ω = Z.val ω) : 𝔼[X] = 𝔼[Z]

Expectations of identical rv are the same

theorem Finprob.exp_sum_val {τ : Type} {P : Finprob τ} (X : Finrv P ℝ) : 𝔼[X] = ∑ x ∈ Finset.image X.val P.Ω, ↑ℙ[X ᵣ== x] * x

Law of the unconscious statistician

theorem Finprob.exp_sum_val_cnd {τ : Type} {P : Finprob τ} (X : Finrv P ℝ) (B : Finrv P Bool) : 𝔼[X|B] = ∑ x ∈ Finset.image X.val P.Ω, ↑ℙ[X ᵣ== x|B] * x

Law of the unconscious statistician, conditional

theorem Finprob.exp_sum_val_cnd_rv {τ : Type} {P : Finprob τ} {ν : Type} [DecidableEq ν] {V : Finset ν} (X : Finrv P ℝ) (Y : Finrv P { x : ν // x ∈ V }) (ω : τ) : ω ∈ P.Ω → 𝔼[X|ᵥY].val ω = ∑ y ∈ V, ↑ℙ[Y ᵣ== Y.val ω] * 𝔼[X|Y ᵣ== Y.val ω]

Law of the unconscious statistician, conditional random variable

theorem Finprob.total_probability {τ : Type} {P : Finprob τ} {ν : Type} [DecidableEq ν] {V : Finset ν} (B : Finrv P Bool) (Y : Finrv P { x : ν // x ∈ V }) : ℙ[B] = ∑ y : { x : ν // x ∈ V }, ℙ[Y ᵣ== y] * ℙ[B|Y ᵣ== y]

theorem Finprob.total_expectation {τ : Type} {P : Finprob τ} {ν : Type} [DecidableEq ν] {V : Finset ν} (X : Finrv P ℝ) (Y : Finrv P { x : ν // x ∈ V }) : 𝔼[𝔼[X|ᵥY]] = 𝔼[X]

theorem Finprob.prob_prod_prob {τ₁ τ₂ : Type} {T₁ : Finset τ₁} {T₂ : Finset τ₂} (f : τ₁ → NNReal) (g : τ₁ → τ₂ → NNReal) (h1 : ∑ t₁ ∈ T₁, f t₁ = 1) (h2 : ∀ t₁ ∈ T₁, ∑ t₂ ∈ T₂, g t₁ t₂ = 1) : (∑ x ∈ T₁ ×ˢ T₂, match x with | (t₁, t₂) => f t₁ * g t₁ t₂) = 1

Product of a probability distribution with a dependent probability distributions is a probability distribution.

def Finprob.product_dep {τ₁ τ₂ : Type} {Ω₁ : Finset τ₁} (P₁ : Findist Ω₁) (Ω₂ : Finset τ₂) (p : τ₁ → τ₂ → NNReal) (h1 : ∀ ω₁ ∈ Ω₁, ∑ ω₂ ∈ Ω₂, p ω₁ ω₂ = 1) : Findist (Ω₁ ×ˢ Ω₂)

Probability distribution as a product of a probability distribution and a dependent probability distribution.

Equations

• Finprob.product_dep P₁ Ω₂ p h1 = { p := fun (x : τ₁ × τ₂) => match x with | (ω₁, ω₂) => P₁.p ω₁ * p ω₁ ω₂, sumsto := ⋯ }

def Finprob.product_dep_pr {τ₁ τ₂ : Type} {Ω₁ : Finset τ₁} (P₁ : Findist Ω₁) (Ω₂ : Finset τ₂) (Q : τ₁ → Findist Ω₂) : Findist (Ω₁ ×ˢ Ω₂)

Constructs a probability space as a product of a probability space and a dependent probability space.

Equations

• Finprob.product_dep_pr P₁ Ω₂ Q = { p := fun (x : τ₁ × τ₂) => match x with | (ω₁, ω₂) => P₁.p ω₁ * (Q ω₁).p ω₂, sumsto := ⋯ }

theorem Finprob.embed_preserve {τ₁ τ₂ : Type} (T₁ : Finset τ₁) (p : τ₁ → NNReal) (f : τ₁ ↪ τ₂) (f_linv : τ₂ → τ₁) (h : Function.LeftInverse f_linv ⇑f) : ∑ t₂ ∈ Finset.map f T₁, (p ∘ f_linv) t₂ = ∑ t₁ ∈ T₁, p t₁

Embedding preserves a sum

def Finprob.embed {τ₁ τ₂ : Type} {Ω₁ : Finset τ₁} (P : Findist Ω₁) (e : τ₁ ↪ τ₂) (e_linv : τ₂ → τ₁) (h : Function.LeftInverse e_linv ⇑e) : Findist (Finset.map e Ω₁)

Embed the probability in a new space using e. Needs an inverse

Equations

• Finprob.embed P e e_linv h = { p := fun (t₂ : τ₂) => (P.p ∘ e_linv) t₂, sumsto := ⋯ }