# Theory Probability_Ext

section ‹Probability Spaces›
text ‹Some additional results about probability spaces in addition to "HOL-Probability".›
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
lemma pmf_add:
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"
by (rule measure_subadditive, auto)
finally show ?thesis by simp
qed
lemma pmf_add_2:
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 ω}"
by (intro pmf_add[OF assms(1)], auto)
also have "... ≤ ?rhs"
by (intro add_mono assms(2-3))
finally show ?thesis
by simp
qed
end
end