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