Exercises from Grinstead and Snell

def exercise_1_2_4.H : Bool

Equations

• exercise_1_2_4.H = true

def exercise_1_2_4.T : Bool

Equations

• exercise_1_2_4.T = false

theorem exercise_1_2_4.part_1 : {![H, H, H], ![H, H, T], ![H, T, H], ![H, T, T]} = {x : Fin (Nat.succ 0).succ.succ → Bool | x 0 = H}

theorem exercise_1_2_4.part_2 : {![H, H, H], ![T, T, T]} = {x : Fin (Nat.succ 0).succ.succ → Bool | ∀ (i : Fin (Nat.succ 0).succ.succ), x i = x 0}

theorem exercise_1_2_4.part_3 : {![H, H, T], ![H, T, H], ![T, H, H]} = {x : Fin (Nat.succ 0).succ.succ → Bool | ∃! i : Fin (Nat.succ 0).succ.succ, x i = T}

theorem exercise_1_2_4.part_4 : {![H, H, T], ![H, T, H], ![H, T, T], ![T, H, H], ![T, H, T], ![T, T, H], ![T, T, T]} = {x : Fin (Nat.succ 0).succ.succ → Bool | ∃ (i : Fin (Nat.succ 0).succ.succ), x i = T}

theorem arithmetic_for_exercise_1_2_7 : 1 / 2 + 1 = 11 / 12 + 1 / 4 + 1 / 3

theorem exercise_1_2_7 {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [i : MeasureTheory.IsProbabilityMeasure μ] (A B : Set Ω) (hA : MeasurableSet A) (h₀ : μ (A ∩ B) = 1 / 4) (h₁ : μ Aᶜ = 1 / 3) (h₂ : μ B = 1 / 2) : μ (A ∪ B) = 11 / 12

Exercise 1.2.7: Let A and B be events such that P(A ∩ B) = 1/4, P(A˜) = 1/3, and P(B) = 1/2. What is P(A ∪ B)?

theorem exercise_1_2_6 (μ : MeasureTheory.Measure (Fin 6)) [i : MeasureTheory.IsProbabilityMeasure μ] (h : μ {2} = 2 * μ {1} ∧ μ {3} = 3 * μ {1} ∧ μ {4} = 4 * μ {1} ∧ μ {5} = 5 * μ {1} ∧ μ {6} = 6 * μ {1}) : μ {2, 4, 6} = 12 / 21