Some finite probability theory

class ProbabilityTheory.FinitelyAdditive (A : Type u_1) [BooleanAlgebra A] : Type u_1

• prob : A → ℝ
• prob_top : prob ⊤ = 1
• prob_nonneg (E : A) : 0 ≤ prob E
• prob_disj_sup {E F : A} (hEF : Disjoint E F) : prob (E ⊔ F) = prob E + prob F

instance ProbabilityTheory.FinitelyAdditive.instFunLike (A : Type u_1) [BooleanAlgebra A] : FunLike (FinitelyAdditive A) A ℝ

Equations

• ProbabilityTheory.FinitelyAdditive.instFunLike A = { coe := fun (ℙ : ProbabilityTheory.FinitelyAdditive A) => ProbabilityTheory.FinitelyAdditive.prob, coe_injective' := ⋯ }

@[simp]

theorem ProbabilityTheory.FinitelyAdditive.top {A : Type u_1} [BooleanAlgebra A] (ℙ : FinitelyAdditive A) : ℙ ⊤ = 1

theorem ProbabilityTheory.FinitelyAdditive.nonneg {A : Type u_1} [BooleanAlgebra A] (ℙ : FinitelyAdditive A) (E : A) : 0 ≤ ℙ E

theorem ProbabilityTheory.FinitelyAdditive.disj_sup {A : Type u_1} [BooleanAlgebra A] (ℙ : FinitelyAdditive A) {E F : A} (hEF : Disjoint E F) : ℙ (E ⊔ F) = ℙ E + ℙ F

@[simp]

theorem ProbabilityTheory.FinitelyAdditive.bot {A : Type u_1} [BooleanAlgebra A] (ℙ : FinitelyAdditive A) : ℙ ⊥ = 0

@[simp]

theorem ProbabilityTheory.FinitelyAdditive.compl {A : Type u_1} [BooleanAlgebra A] (ℙ : FinitelyAdditive A) (E : A) : ℙ Eᶜ = 1 - ℙ E

theorem ProbabilityTheory.FinitelyAdditive.le_one {A : Type u_1} [BooleanAlgebra A] (ℙ : FinitelyAdditive A) (E : A) : ℙ E ≤ 1

theorem ProbabilityTheory.FinitelyAdditive.ge_eq_add_diff {A : Type u_1} [BooleanAlgebra A] (ℙ : FinitelyAdditive A) {E F : A} (hEF : E ≤ F) : ℙ F = ℙ (F \ E) + ℙ E

theorem ProbabilityTheory.FinitelyAdditive.mono {A : Type u_1} [BooleanAlgebra A] (ℙ : FinitelyAdditive A) {E F : A} (hEF : E ≤ F) : ℙ E ≤ ℙ F

theorem ProbabilityTheory.FinitelyAdditive.sup_add_inf {A : Type u_1} [BooleanAlgebra A] (ℙ : FinitelyAdditive A) (E F : A) : ℙ (E ⊔ F) + ℙ (E ⊓ F) = ℙ E + ℙ F

theorem ProbabilityTheory.FinitelyAdditive.sup_le_add {A : Type u_1} [BooleanAlgebra A] (ℙ : FinitelyAdditive A) (E F : A) : ℙ (E ⊔ F) ≤ ℙ E + ℙ F

def BoundedLatticeHom.preserves {A : Type u_1} [BooleanAlgebra A] (ℙ : ProbabilityTheory.FinitelyAdditive A) {A' : Type u_2} [BooleanAlgebra A'] (ℙ' : ProbabilityTheory.FinitelyAdditive A') (f : BoundedLatticeHom A A') : Prop

Equations

• BoundedLatticeHom.preserves ℙ ℙ' f = ∀ (E : A), ℙ' (f E) = ℙ E

@[simp]

theorem BoundedLatticeHom.preserves.map {A : Type u_1} [BooleanAlgebra A] (ℙ : ProbabilityTheory.FinitelyAdditive A) {A' : Type u_2} [BooleanAlgebra A'] (ℙ' : ProbabilityTheory.FinitelyAdditive A') {f : BoundedLatticeHom A A'} (hf : preserves ℙ ℙ' f) (E : A) : ℙ' (f E) = ℙ E

class ProbabilityTheory.FinitelyAdditive.ExampleProb {A : Type u_3} [BooleanAlgebra A] (ℙ : FinitelyAdditive A) : Type u_3

• E : A
• F : A
• G : A
• prob_E : ℙ (E ℙ) = 0.5
• prob_EF : ℙ (E ℙ ⊔ F ℙ) = 0.75
• prob_EF' : ℙ (E ℙ ⊓ F ℙ) = 0.25
• prob_EG : ℙ (E ℙ \ G ℙ) = 0.4
• prob_G : ℙ (G ℙ)ᶜ = 0.3

def ProbabilityTheory.FinitelyAdditive.ExampleProb.map {A : Type u_1} [BooleanAlgebra A] (ℙ : FinitelyAdditive A) {A' : Type u_2} [BooleanAlgebra A'] (ℙ' : FinitelyAdditive A') {Ω : ℙ.ExampleProb} {f : BoundedLatticeHom A A'} (hf : BoundedLatticeHom.preserves ℙ ℙ' f) : ℙ'.ExampleProb

Equations

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