def indicator (cond : Bool) : ℚ

Boolean indicator function

Equations

• indicator cond = Bool.rec 0 1 cond

@[reducible, inline]

abbrev 𝕀 : Bool → ℚ

Equations

• 𝕀 = indicator

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

Indicator is 0 or 1

@[reducible, inline]

abbrev Prob (p : ℚ) : Prop

states that p is a valid probability value

Equations

• Prob p = (0 ≤ p ∧ p ≤ 1)

@[simp]

theorem Prob.of_complement {p : ℚ} (hp : Prob p) : Prob (1 - p)

@[simp]

theorem Prob.complement_inv_nneg {p : ℚ} (hp : Prob p) : 0 ≤ (1 - p)⁻¹

theorem Prob.lower_bound_fst {p x y : ℚ} (hp : Prob p) (h : x ≤ y) : x ≤ p * x + (1 - p) * y

theorem Prob.lower_bound_snd {p x y : ℚ} (hp : Prob p) (h : y ≤ x) : y ≤ p * x + (1 - p) * y

theorem Prob.upper_bound_fst {p x y : ℚ} (hp : Prob p) (h : y ≤ x) : p * x + (1 - p) * y ≤ x

theorem Prob.upper_bound_snd {p x y : ℚ} (hp : Prob p) (h : x ≤ y) : p * x + (1 - p) * y ≤ y

def List.scale (L : List ℚ) (c : ℚ) : List ℚ

Equations

• L.scale c = List.map (fun (x : ℚ) => x * c) L

@[simp]

theorem List.scale_sum {L : List ℚ} {c : ℚ} : (L.scale c).sum = c * L.sum

@[simp]

theorem List.scale_length {L : List ℚ} {c : ℚ} : (L.scale c).length = L.length

theorem List.scale_nneg_of_nneg {L : List ℚ} {c : ℚ} (h : ∀ l ∈ L, 0 ≤ l) (h1 : 0 ≤ c) (l : ℚ) : l ∈ L.scale c → 0 ≤ l

theorem List.append_nneg_of_nneg {L : List ℚ} {p : ℚ} (h : ∀ l ∈ L, 0 ≤ l) (h1 : 0 ≤ p) (l : ℚ) : l ∈ p :: L → 0 ≤ l

def List.grow (L : List ℚ) (p : ℚ) : List ℚ

adds a new probability to a list and renormalizes the rest -

Equations

• L.grow p = p :: L.scale (1 - p)

theorem List.grow_sum {L : List ℚ} {p : ℚ} : (L.grow p).sum = L.sum * (1 - p) + p

def List.shrink : List ℚ → List ℚ

Removes head and rescales

Equations

• [].shrink = []
• (head :: tail).shrink = tail.scale (1 - head)⁻¹

@[simp]

theorem List.shrink_length {L : List ℚ} : L.shrink.length = L.tail.length

theorem List.shrink_length_less_one {L : List ℚ} : L.shrink.length = L.length - 1

@[simp]

theorem List.shrink_sum {L : List ℚ} (npt : L ≠ []) (h : L.head npt < 1) : L.shrink.sum = L.tail.sum / (1 - L.head npt)

theorem List.shrink_ge0 {L : List ℚ} (h1 : ∀ l ∈ L, Prob l) (l : ℚ) : l ∈ L.shrink → 0 ≤ l

structure LSimplex (L : List ℚ) : Prop

Self-normalizing list of probabilities -

• nneg (p : ℚ) : p ∈ L → 0 ≤ p
• normalized : L.sum = 1

def LSimplex.singleton : LSimplex [1]

Equations

• LSimplex.singleton = ⋯

@[simp]

theorem LSimplex.nonempty {L : List ℚ} (S : LSimplex L) : L ≠ []

cannot define a simplex on an empty set

@[simp, reducible, inline]

abbrev LSimplex.npt {L : List ℚ} : LSimplex L → L ≠ []

Equations

• ⋯ = ⋯

def LSimplex.phead {L : List ℚ} (h : LSimplex L) : ℚ

Equations

• h.phead = L.head ⋯

def LSimplex.degenerate {L : List ℚ} (S : LSimplex L) : Bool

all probability in the head element

Equations

• S.degenerate = (S.phead == 1)

@[reducible]

def LSimplex.supported {L : List ℚ} (S : LSimplex L) : Bool

Equations

• S.supported = decide ¬S.degenerate = true

@[simp]

theorem LSimplex.mem_prob {L : List ℚ} (S : LSimplex L) (p : ℚ) : p ∈ L → Prob p

theorem LSimplex.phead_inpr {L : List ℚ} (S : LSimplex L) : S.phead ∈ L

@[simp]

theorem LSimplex.phead_prob {L : List ℚ} (S : LSimplex L) : Prob S.phead

theorem LSimplex.phead_supp {L : List ℚ} (S : LSimplex L) (supp : S.supported = true) : S.phead < 1

theorem LSimplex.supported_head_lt_one {L : List ℚ} (S : LSimplex L) (supp : S.supported = true) : L.head ⋯ < 1

@[simp]

theorem LSimplex.List.grow_ge0 {p : ℚ} {L : List ℚ} (h1 : ∀ l ∈ L, 0 ≤ l) (h2 : Prob p) (l : ℚ) : l ∈ L.grow p → 0 ≤ l

@[simp]

theorem LSimplex.grow {L : List ℚ} (S : LSimplex L) {p : ℚ} (prob : Prob p) : LSimplex (L.grow p)

theorem LSimplex.false_of_p_comp1_zero_p_less_one {p : ℚ} (h1 : 1 - p = 0) (h2 : p < 1) : False

@[simp]

theorem LSimplex.tail_sum {L : List ℚ} (S : LSimplex L) : L.tail.sum = 1 - L.head ⋯

theorem LSimplex.degenerate_tail_zero {L : List ℚ} (S : LSimplex L) (degen : S.degenerate = true) (p : ℚ) : p ∈ L.tail → p = 0

theorem LSimplex.shrink {L : List ℚ} (S : LSimplex L) (supp : S.supported = true) : LSimplex L.shrink

theorem LSimplex.grow_of_shrink_list {L : List ℚ} (S : LSimplex L) (supp : S.supported = true) : L = L.shrink.grow S.phead

theorem LSimplex.grow_of_shrink {L : List ℚ} (S : LSimplex L) (supp : S.supported = true) : S = ⋯

structure Findist (N : ℕ) : Type

Finite probability distribution on a set-like list (non-duplicates)

• ℙ : List ℚ
• simplex : LSimplex self.ℙ
• lmatch : self.ℙ.length = N

@[reducible, inline]

abbrev Findist.Delta : ℕ → Type

Equations

• Findist.Delta = Findist

@[reducible, inline]

abbrev Findist.Δ : ℕ → Type

Equations

• Findist.Δ = Findist.Delta

@[reducible, inline]

abbrev Findist.degenerate {N : ℕ} (F : Findist N) : Bool

Equations

• F.degenerate = ⋯.degenerate

@[reducible, inline]

abbrev Findist.supported {N : ℕ} (F : Findist N) : Bool

Equations

• F.supported = ⋯.supported

theorem Findist.supp_not_degen {N : ℕ} (F : Findist N) (supp : F.supported = true) : ¬F.degenerate = true

@[simp]

theorem Findist.nonempty {N : ℕ} (F : Findist N) : N ≥ 1

@[simp]

theorem Findist.nonempty_P {N : ℕ} (F : Findist N) : F.ℙ ≠ []

def Findist.grow {N : ℕ} (F : Findist N) {p : ℚ} (prob : Prob p) : Findist (N + 1)

add a new head

Equations

• F.grow prob = { ℙ := F.ℙ.grow p, simplex := ⋯, lmatch := ⋯ }

def Findist.shrink {N : ℕ} (F : Findist N) (supp : F.supported = true) : Findist (N - 1)

if nondegenenrate then construct a tail distribution

Equations

• F.shrink supp = { ℙ := F.ℙ.shrink, simplex := ⋯, lmatch := ⋯ }

def Findist.singleton : Findist 1

Equations

• Findist.singleton = { ℙ := [1], simplex := LSimplex.singleton, lmatch := Findist.singleton._proof_1 }

@[reducible, inline]

abbrev Findist.phead {N : ℕ} (F : Findist N) : ℚ

Equations

• F.phead = ⋯.phead

@[simp]

theorem Findist.phead_inpr {N : ℕ} (F : Findist N) : F.phead ∈ F.ℙ

@[simp]

theorem Findist.phead_prob {N : ℕ} (F : Findist N) : Prob F.phead

theorem Findist.nondegenerate_head {N : ℕ} (F : Findist N) (supp : F.supported = true) : F.phead < 1

theorem Findist.grow_shrink_type {N : ℕ} (F : Findist N) : F.supported = true → Findist (N - 1 + 1) = Findist N

def Findist.growshrink {N : ℕ} (F : Findist N) (supp : F.supported = true) : Findist (N - 1 + 1)

Equations

• F.growshrink supp = (F.shrink supp).grow ⋯

theorem Findist.grow_of_shrink_2 {N : ℕ} (F : Findist N) (supp : F.supported = true) : F.growshrink supp = ⋯.mpr F

structure Finprob : Type

Finite probability space. See Finsample for the definition of the sample space.

• ℙ : List ℚ
• prob : LSimplex self.ℙ

theorem List.unique_head_notin_tail {τ : Type} (L : List τ) (ne : L ≠ []) (nodup : L.Nodup) : L.head ne ∉ L.tail

def Finprob.length (P : Finprob) : ℕ

Equations

• P.length = P.ℙ.length

def Finprob.singleton : Finprob

Equations

• Finprob.singleton = { ℙ := [1], prob := LSimplex.singleton }

def Finprob.grow (P : Finprob) {p : ℚ} (prob : Prob p) : Finprob

Equations

• P.grow prob = { ℙ := P.ℙ.grow p, prob := ⋯ }

@[reducible, inline]

abbrev Finprob.degenerate (P : Finprob) : Bool

all probability in the head

Equations

• P.degenerate = ⋯.degenerate

@[reducible, inline]

abbrev Finprob.supported (P : Finprob) : Bool

Equations

• P.supported = ⋯.supported

theorem Finprob.not_degen_supp (P : Finprob) (supp : ¬P.degenerate = true) : P.supported = true

theorem Finprob.degen_of_not_supp (P : Finprob) (notsupp : ¬P.supported = true) : P.degenerate = true

def Finprob.shrink (P : Finprob) (supp : P.supported = true) : Finprob

Equations

• P.shrink supp = { ℙ := P.ℙ.shrink, prob := ⋯ }

theorem Finprob.nonempty (P : Finprob) : ¬P.ℙ.isEmpty = true

theorem Finprob.length_gt_zero (P : Finprob) : P.length ≥ 1

theorem Finprob.shrink_length (P : Finprob) (supp : P.supported = true) : (P.shrink supp).length = P.length - 1

theorem Finprob.shrink_length_lt (P : Finprob) (supp : P.supported = true) : (P.shrink supp).length < P.length

theorem Finprob.nonempty_P (P : Finprob) : P.ℙ ≠ []

def Finprob.phead (P : Finprob) : ℚ

Equations

• P.phead = P.ℙ.head ⋯

def Finprob.ωhead (P : Finprob) : ℕ

Equations

• P.ωhead = P.length - 1

theorem Finprob.phead_inpr (P : Finprob) : P.phead ∈ P.ℙ

theorem Finprob.phead_prob (P : Finprob) : Prob P.phead

theorem Finprob.phead_supp_ne_one (P : Finprob) (supp : P.supported = true) : P.phead ≠ 1

theorem Finprob.len_ge_one (P : Finprob) : P.length ≥ 1

theorem Finprob.shrink_shorter (P : Finprob) (supp : P.supported = true) : (P.shrink supp).length = P.length - 1

theorem Finprob.grow_of_shrink (P : Finprob) (supp : P.supported = true) : P = (P.shrink supp).grow ⋯

Shows that growing an shrink probability will create the same probability space

@[irreducible]

def Finprob.induction {motive : Finprob → Prop} (degenerate : ∀ {fp : Finprob}, fp.degenerate = true → motive fp) (composite : ∀ (tail : Finprob) {p : ℚ} (inP : Prob p), motive tail → motive (tail.grow inP)) (P : Finprob) : motive P

induction principle for finite probabilities. Works as "induction P"

Equations

• ⋯ = ⋯

def FinRV (ρ : Type) : Type

Random variable defined on a finite probability space (bijection to ℕ)

Equations

• FinRV ρ = (ℕ → ρ)

def FinRV.and (B C : FinRV Bool) : FinRV Bool

Equations

• (B ∧ᵣ C) ω = (B ω && C ω)

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

Equations

• FinRV.«term_∧ᵣ_» = Lean.ParserDescr.trailingNode `FinRV.«term_∧ᵣ_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∧ᵣ ") (Lean.ParserDescr.cat `term 36))

def FinRV.or (B C : FinRV Bool) : FinRV Bool

Equations

• (B ∨ᵣ C) ω = (B ω || C ω)

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

Equations

• FinRV.«term_∨ᵣ_» = Lean.ParserDescr.trailingNode `FinRV.«term_∨ᵣ_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∨ᵣ ") (Lean.ParserDescr.cat `term 31))

def FinRV.not (B : FinRV Bool) : FinRV Bool

Equations

• (¬ᵣB) ω = !B ω

def FinRV.«term¬ᵣ_» : Lean.ParserDescr

Equations

• FinRV.«term¬ᵣ_» = Lean.ParserDescr.node `FinRV.«term¬ᵣ_» 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "¬ᵣ") (Lean.ParserDescr.cat `term 40))

def FinRV.eq {η : Type} [DecidableEq η] (Y : FinRV η) (y : η) : FinRV Bool

Equations

• (Y=ᵣy) ω = decide (Y ω = y)

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

Equations

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

def FinRV.leq {η : Type} [LE η] [DecidableLE η] (Y : FinRV η) (y : η) : FinRV Bool

Equations

• (Y≤ᵣy) ω = decide (Y ω ≤ y)

def FinRV.«term_≤ᵣ_» : Lean.TrailingParserDescr

Equations

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

theorem FinRV.le_of_le_eq (D : FinRV ℕ) (n : ℕ) : (D≤ᵣn ∨ᵣ D=ᵣn.succ) = (D≤ᵣn.succ)

Shows equivalence when extending the random variable to another element.

def List.iprodb (ℙ : List ℚ) (B : FinRV Bool) : ℚ

Probability of a random variable. Does not enforce normalization

Equations

• [].iprodb B = 0
• (head :: tail).iprodb B = Bool.rec 0 head (B tail.length) + tail.iprodb B

theorem List.scale_innerprod (B : FinRV Bool) (L : List ℚ) (x : ℚ) : (L.scale x).iprodb B = x * L.iprodb B

theorem List.decompose_supp (B : FinRV Bool) (L : List ℚ) (h : L ≠ []) (ne1 : L.head h ≠ 1) : L.iprodb B = Bool.rec 0 (L.head h) (B (L.length - 1)) + (1 - L.head h) * L.shrink.iprodb B

theorem List.iprod_eq_zero_of_zeros (B : FinRV Bool) (L : List ℚ) (hz : ∀ p ∈ L, p = 0) : L.iprodb B = 0

theorem List.iprod_first_of_tail_zero (B : FinRV Bool) (L : List ℚ) (hn : L ≠ []) (hz : ∀ p ∈ L.tail, p = 0) : L.iprodb B = Bool.rec 0 (L.head hn) (B L.tail.length)

theorem List.iprodb_true_sum (L : List ℚ) : (L.iprodb fun (x : ℕ) => true) = L.sum

def probability (P : Finprob) (B : FinRV Bool) : ℚ

Probability of B

Equations

• ℙ[B//P] = P.ℙ.iprodb B

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

Equations

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

def probability_cnd (P : Finprob) (B C : FinRV Bool) : ℚ

Conditional probability of B

Equations

• ℙ[B|C//P] = ℙ[B ∧ᵣ C//P] / ℙ[C//P]

theorem Finprob.decompose_supp (P : Finprob) (B : FinRV Bool) (supp : P.supported = true) : ℙ[B//P] = Bool.rec 0 P.phead (B P.ωhead) + (1 - P.phead) * ℙ[B//P.shrink supp]

If supported then can be decomposed to the immediate probability and the remaining probability

theorem Finprob.decompose_degen (P : Finprob) (B : FinRV Bool) (degen : P.degenerate = true) : ℙ[B//P] = Bool.rec 0 P.phead (B P.ωhead)

@[irreducible]

theorem Finprob.in_prob (B : FinRV Bool) (P : Finprob) : Prob ℙ[B//P]

theorem Prob.ge_zero (P : Finprob) (B : FinRV Bool) : ℙ[B//P] ≥ 0

theorem Prob.le_one (P : Finprob) (B : FinRV Bool) : ℙ[B//P] ≤ 1

theorem Prob.true_one (P : Finprob) : ℙ[fun (x : ℕ) => true//P] = 1

theorem List.list_compl_sums_to_one (B : FinRV Bool) (L : List ℚ) : L.iprodb B + L.iprodb (¬ᵣB) = L.sum

theorem List.law_of_total_probs (B C : FinRV Bool) (L : List ℚ) : L.iprodb B = L.iprodb (B ∧ᵣ C) + L.iprodb (B ∧ᵣ ¬ᵣC)

theorem Prob.prob_compl_sums_to_one (P : Finprob) (B : FinRV Bool) : ℙ[B//P] + ℙ[¬ᵣB//P] = 1

theorem Prob.prob_compl_one_minus (P : Finprob) (B : FinRV Bool) : ℙ[¬ᵣB//P] = 1 - ℙ[B//P]

theorem Prob.law_of_total_probs (P : Finprob) (B C : FinRV Bool) : ℙ[B//P] = ℙ[B ∧ᵣ C//P] + ℙ[B ∧ᵣ ¬ᵣC//P]

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

Equations

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

theorem Prob.conditional_total (P : Finprob) (B C : FinRV Bool) (h : 0 < ℙ[C//P]) : ℙ[B ∧ᵣ C//P] = ℙ[B|C//P] * ℙ[C//P]

theorem Prob.law_of_total_probs_cnd (P : Finprob) (B C : FinRV Bool) (h1 : 0 < ℙ[C//P]) (h2 : ℙ[C//P] < 1) : ℙ[B//P] = ℙ[B|C//P] * ℙ[C//P] + ℙ[B|¬ᵣC//P] * ℙ[¬ᵣC//P]

def List.iprod (ℙ : List ℚ) (X : FinRV ℚ) : ℚ

Equations

• [].iprod X = 0
• (head :: tail).iprod X = head * X tail.length + tail.iprod X

def expect (P : Finprob) (X : FinRV ℚ) : ℚ

Equations

• 𝔼[X//P] = P.ℙ.iprod X

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

Equations

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

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

Equations

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

def expect_cnd (P : Finprob) (X : FinRV ℚ) (B : FinRV Bool) : ℚ

Equations

• 𝔼[X|B//P] = P.ℙ.iprod X / P.ℙ.iprodb B

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

Equations

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

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

Equations

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

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

Equations

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

theorem List.law_of_total_expectations (L : List ℚ) (X : FinRV ℚ) (B : FinRV Bool) : L.iprod X = (L.iprod fun (ω : ℕ) => if B ω = true then X ω else 0) + L.iprod fun (ω : ℕ) => if ¬B ω = true then X ω else 0

theorem Prob.law_of_total_expectation (P : Finprob) (X : FinRV ℚ) (B : FinRV Bool) (h1 : 0 < ℙ[B//P]) (h2 : 0 < ℙ[¬ᵣB//P]) : 𝔼[X//P] = 𝔼[X|B//P] * ℙ[B//P] + 𝔼[X|¬ᵣB//P] * ℙ[¬ᵣB//P]

def Finprob.SampleMap (P : Finprob) (m : ℕ) : Type

Represents the generator of the sample space of a Finprob. Each element is mapped to a single generator. Note that different Finsample definitions may induce equivalent sample spaces. Also there is no guarantee that there will not be a generator with zero probability.

Equations

• P.SampleMap m = (Fin P.length → Fin m)

instance instCoeOutSampleMapFinRVFin {P : Finprob} {m : ℕ} : CoeOut (P.SampleMap m) (FinRV (Fin m))

Equations

• instCoeOutSampleMapFinRVFin = { coe := fun (a : P.SampleMap m) (ω : ℕ) => if h : ω < P.length then a ⟨ω, h⟩ else a ⟨0, ⋯⟩ }

def FinRV.MeasurableRV {ρ : Type} {P : Finprob} {m : ℕ} (X Y : FinRV ρ) (ℱ : P.SampleMap m) : Prop

Defines that the random variable X is measurable with respect to a map and a reduced random variable Y

Equations

• X.MeasurableRV Y ℱ = ∀ (ω : Fin P.length), X ↑ω = Y ↑(ℱ ω)

def FinProb.MeasurableProb {P : Finprob} {L : List ℚ} (ℱ : P.SampleMap L.length) : Prop

Defines the aggregated probability in the compacted space -

Equations

• FinProb.MeasurableProb ℱ = ∀ (m : Fin L.length), ℙ[(fun (ω : ℕ) => if h : ω < P.length then ℱ ⟨ω, h⟩ else ℱ ⟨0, ⋯⟩)=ᵣm//P] = L.get m