Theory Probability_Ext

```section ‹Probability Spaces›

theory Probability_Ext
imports
"HOL-Probability.Stream_Space"
Concentration_Inequalities.Bienaymes_Identity
Universal_Hash_Families.Carter_Wegman_Hash_Family
Frequency_Moments_Preliminary_Results
begin

context prob_space
begin

lemma pmf_mono:
assumes "M = measure_pmf p"
assumes "⋀x. x ∈ P ⟹ x ∈ set_pmf p ⟹ x ∈ Q"
shows "prob P ≤ prob Q"
proof -
have "prob P = prob (P ∩ (set_pmf p))"
by (rule  measure_pmf_eq[OF assms(1)], blast)
also have "... ≤ prob Q"
using assms by (intro finite_measure.finite_measure_mono, auto)
finally show ?thesis by simp
qed

assumes "M = measure_pmf p"
assumes  "⋀x. x ∈ P ⟹ x ∈ set_pmf p ⟹ x ∈ Q ∨ x ∈ R"
shows "prob P ≤ prob Q + prob R"
proof -
have [simp]:"events = UNIV" by (subst assms(1), simp)
have "prob P ≤ prob (Q ∪ R)"
using assms by (intro pmf_mono[OF assms(1)], blast)
also have "... ≤ prob Q + prob R"
finally show ?thesis by simp
qed

assumes "M = measure_pmf p"
assumes "prob {ω. P ω} ≤ r1"
assumes "prob {ω. Q ω} ≤ r2"
shows "prob {ω. P ω ∨ Q ω} ≤ r1 + r2" (is "?lhs ≤ ?rhs")
proof -
have "?lhs ≤ prob {ω. P ω} + prob {ω. Q ω}"