(* Title: HOL/Probability/Probability_Mass_Function.thy Author: Johannes Hölzl, TU München Author: Andreas Lochbihler, ETH Zurich Author: Manuel Eberl, TU München *) section ‹ Probability mass function › theory Probability_Mass_Function imports Giry_Monad "HOL-Library.Multiset" begin text ‹Conflicting notation from \<^theory>‹HOL-Analysis.Infinite_Sum›› no_notation Infinite_Sum.abs_summable_on (infixr "abs'_summable'_on" 46) lemma AE_emeasure_singleton: assumes x: "emeasure M {x} ≠ 0" and ae: "AE x in M. P x" shows "P x" proof - from x have x_M: "{x} ∈ sets M" by (auto intro: emeasure_notin_sets) from ae obtain N where N: "{x∈space M. ¬ P x} ⊆ N" "emeasure M N = 0" "N ∈ sets M" by (auto elim: AE_E) { assume "¬ P x" with x_M[THEN sets.sets_into_space] N have "emeasure M {x} ≤ emeasure M N" by (intro emeasure_mono) auto with x N have False by (auto simp:) } then show "P x" by auto qed lemma AE_measure_singleton: "measure M {x} ≠ 0 ⟹ AE x in M. P x ⟹ P x" by (metis AE_emeasure_singleton measure_def emeasure_empty measure_empty) lemma (in finite_measure) AE_support_countable: assumes [simp]: "sets M = UNIV" shows "(AE x in M. measure M {x} ≠ 0) ⟷ (∃S. countable S ∧ (AE x in M. x ∈ S))" proof assume "∃S. countable S ∧ (AE x in M. x ∈ S)" then obtain S where S[intro]: "countable S" and ae: "AE x in M. x ∈ S" by auto then have "emeasure M (⋃x∈{x∈S. emeasure M {x} ≠ 0}. {x}) = (∫⇧^{+}x. emeasure M {x} * indicator {x∈S. emeasure M {x} ≠ 0} x ∂count_space UNIV)" by (subst emeasure_UN_countable) (auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space) also have "… = (∫⇧^{+}x. emeasure M {x} * indicator S x ∂count_space UNIV)" by (auto intro!: nn_integral_cong split: split_indicator) also have "… = emeasure M (⋃x∈S. {x})" by (subst emeasure_UN_countable) (auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space) also have "… = emeasure M (space M)" using ae by (intro emeasure_eq_AE) auto finally have "emeasure M {x ∈ space M. x∈S ∧ emeasure M {x} ≠ 0} = emeasure M (space M)" by (simp add: emeasure_single_in_space cong: rev_conj_cong) with finite_measure_compl[of "{x ∈ space M. x∈S ∧ emeasure M {x} ≠ 0}"] have "AE x in M. x ∈ S ∧ emeasure M {x} ≠ 0" by (intro AE_I[OF order_refl]) (auto simp: emeasure_eq_measure measure_nonneg set_diff_eq cong: conj_cong) then show "AE x in M. measure M {x} ≠ 0" by (auto simp: emeasure_eq_measure) qed (auto intro!: exI[of _ "{x. measure M {x} ≠ 0}"] countable_support) subsection ‹ PMF as measure › typedef 'a pmf = "{M :: 'a measure. prob_space M ∧ sets M = UNIV ∧ (AE x in M. measure M {x} ≠ 0)}" morphisms measure_pmf Abs_pmf by (intro exI[of _ "uniform_measure (count_space UNIV) {undefined}"]) (auto intro!: prob_space_uniform_measure AE_uniform_measureI) declare [[coercion measure_pmf]] lemma prob_space_measure_pmf: "prob_space (measure_pmf p)" using pmf.measure_pmf[of p] by auto