Theory Prob_Events_Extras
section ‹General Event Lemmas›
text ‹General lemmas for reasoning on events in probability spaces after different operations ›
theory Prob_Events_Extras
imports
"HOL-Probability.Probability"
PiE_Rel_Extras
begin
context prob_space
begin
lemma :
assumes measurable: "finite A" "A ⊆ events" "disjoint A"
shows "prob (⋃A ) = (∑e∈A. prob (e))"
proof -
obtain f where bb: "bij_betw f {0..<card A} A"
using assms(1) ex_bij_betw_nat_finite by auto
then have eq: "f ` {0..<card A} = A"
by (simp add: bij_betw_imp_surj_on)
moreover have "inj_on f {0..<card A}"
using bb bij_betw_def by blast
ultimately have "disjoint_family_on f {0..<card A}"
using disjoint_image_disjoint_family_on[of f "{0..<card A}"] assms by auto
moreover have "(∑e∈A. prob (e)) = (∑i∈{0..<card A}. prob (f i))" using sum.reindex bb
by (simp add: sum.reindex_bij_betw)
ultimately show ?thesis using finite_measure_finite_Union eq assms(1) assms(2)
by (metis bb bij_betw_finite)
qed
lemma :
assumes "finite S"
assumes "S ≠ {}"
shows "(⋀ A. A ∈ S ⟹ A ∈ events) ⟹ ⋂S ∈ events"
using assms proof (induct S rule: finite_ne_induct)
case (singleton x)
then show ?case by auto
next
case (insert x F)
then show ?case using sets.Int
by (metis complete_lattice_class.Inf_insert insertCI)
qed
lemma :
assumes "finite S"
shows "(⋀ A. A ∈ S ⟹ A ∈ events) ⟹ ⋃S ∈ events"
using assms(1) proof (induct S rule: finite_induct)
case empty
then show ?case by auto
next
case (insert x F)
then show ?case using sets.Un
by (simp add: insertI1)
qed
lemma : "A ∈ events ⟹ prob (A ∩ (⋂AS)) ≤ prob A"
by (simp add: finite_measure_mono)
lemma : "finite A ⟹ A ⊆ events ⟹ A ≠ {} ⟹ ⋂A ∈ events"
by (simp add: events_inter subset_iff)
lemma :
assumes "finite A"
assumes "A ⊆ events"
assumes "B ≠ {}"
assumes "B ⊆ A"
shows "prob (⋂A) ≤ prob (⋂B)"
proof (cases "B = A")
case True
then show ?thesis by simp
next
case False
then obtain C where "C = A - B" and "C ≠ {}"
using assms(4) by auto
then have "⋂ A = ⋂C ∩ ⋂B"
by (metis Inter_Un_distrib Un_Diff_cancel2 assms(4) sup.orderE)
moreover have "⋂B ∈ events" using assms(1) assms(3) assms(2) Inter_event_ss
by (meson assms(2) assms(4) dual_order.trans finite_subset)
ultimately show ?thesis using prob_inter_set_lt_elem
by (simp add: inf_commute)
qed
lemma :
assumes "finite A"
assumes "F ` A ⊆ events"
assumes "B ≠ {}"
assumes "B ⊆ A"
shows "prob (⋂(F ` A)) ≤ prob (⋂(F `B))"
using prob_inter_ss_lt[of "F ` A" "F ` B"] assms by auto
lemma :
assumes "S ⊆ events"
shows "((-) (space M)) ` (((-) (space M)) ` S) = S"
proof (intro subset_antisym subsetI)
fix x assume "x ∈ (-) (space M) ` (-) (space M) ` S"
then obtain x' where xeq: "x = space M - x'" and "x' ∈ (-) (space M) ` S" by blast
then obtain x'' where "x' = space M - x''" and xin: "x'' ∈ S" by blast
then have "x'' = x" using xeq assms
by (simp add: Diff_Diff_Int Set.basic_monos(7))
then show "x ∈ S" using xin by simp
next
fix x assume "x ∈ S"
then obtain x' where xeq: "x' = space M - x" and "x' ∈ (-) (space M) ` S" by simp
then have "space M - x' ∈(-) (space M) ` (-) (space M) ` S" by auto
moreover have "space M - x' = x" using xeq assms
by (simp add: Diff_Diff_Int ‹x ∈ S› subset_iff)
ultimately show "x ∈ (-) (space M) ` (-) (space M) ` S" by simp
qed
lemma :
assumes "S ⊆ events"
assumes "S' = ((-) (space M)) ` S"
shows "bij_betw ((-) (space M)) S' S"
proof (intro bij_betwI')
show "⋀x y. x ∈ S' ⟹ y ∈ S' ⟹ (space M - x = space M - y) = (x = y)"
using assms(2) by blast
next
show "⋀x. x ∈ S' ⟹ space M - x ∈ S" using space_compl_double assms by auto
next
show "⋀y. y ∈ S ⟹ ∃x∈S'. y = space M - x" using space_compl_double assms by auto
qed
lemma :
assumes "S ⊆ events"
assumes "S' = ((-) (space M)) ` S"
shows "bij_betw ((-) (space M)) S S'"
proof (intro bij_betwI')
show "⋀x y. x ∈ S ⟹ y ∈ S ⟹ (space M - x = space M - y) = (x = y)"
using assms by (metis Diff_Diff_Int sets.Int_space_eq1 subset_eq)
next
show "⋀x. x ∈ S ⟹ space M - x ∈ S'" using space_compl_double assms by auto
next
show "⋀y. y ∈ S' ⟹ ∃x∈S. y = space M - x" using space_compl_double assms by auto
qed
lemma : "A ∈ events ⟹ B ∈ events ⟹ prob A = 0 ⟹ prob (A ∩ B) = 0"
by (metis Int_lower1 finite_measure_mono measure_le_0_iff)
lemma : "A ∈ events ⟹ B ⊆ events ⟹ prob A = 0 ⟹ prob (A ∩ (⋂B)) = 0"
by (metis Int_lower1 finite_measure_mono measure_le_0_iff)
lemma : "A ∈ events ⟹ B ∈ events ⟹ prob A = 1 ⟹ prob (A ∩ B) = prob B"
by (metis inf_commute measure_space_inter prob_space)
lemma :
assumes "A ∈ events" "B ⊆ events"
assumes "prob A = 1"
assumes "B ≠ {}"
assumes "finite B"
shows "prob (A ∩ (⋂B)) = prob (⋂B)"
proof -
have "⋂B ∈ events" using Inter_event_ss assms by auto
then show ?thesis using assms prob1_basic_inter by auto
qed
lemma : "A ∈ events ⟹ space M - (space M - A) = A"
by (simp add: double_diff sets.sets_into_space)
lemma : "A ∈ events ⟹ B ∈ events ⟹
prob (A ∪ B) = prob A + prob B - prob (A ∩ B)"
by (simp add: finite_measure_Diff' finite_measure_Union' inf_commute)
lemma : "S ⊆ events ⟹ (-) (space M) ` S ⊆ events"
by auto
lemma : "A ∈ events ⟹ B ∈ events ⟹
prob (A ∩ (space M - B)) = prob A - prob (A ∩ B)"
by (simp add: Diff_Int_distrib finite_measure_Diff sets.Int)
lemma : "bij_betw f A B ⟹ (∏b∈B. prob b) = (∏a∈A. prob (f a))"
by (simp add: prod.reindex_bij_betw)
:: "'a set ⇒ 'a set" where
"event_compl A ≡ space M - A"
lemma : "A ≠ {} ⟹ space M - (⋃A) = (⋂a ∈ A . (space M - a))"
by (simp)
lemma : "A ≠ {} ⟹ space M - (⋃(F ` A)) = (⋂a ∈ A . (space M - F a))"
by (simp)
end
text ‹Reasoning on the probability of function sets ›
lemma :
assumes "finite A"
assumes "b ∈ B"
assumes "d ⊆ A"
assumes "B ≠ {}"
assumes "finite B"
shows "card {f ∈ (A →⇩E B) . (∀ v ∈ d .f v = b)}/card (A →⇩E B) = 1/((card B) powi (card d))"
(is "card {f ∈ ?C . (∀ v ∈ d .f v = b)}/card ?C = 1/((card B) powi (card d))")
proof -
have lt: "card d ≤ card A"
by (simp add: card_mono assms(1) assms(3))
then have scard: "card {f ∈ ?C . ∀ v ∈ d . f v = b} = (card B) powi ((card A) - card d)"
using assms(1) card_PiE_filter_range_set_const[of b B d A] assms(3) assms(2) by fastforce
have Ccard: "card ?C = (card B) powi (card A)" using card_funcsetE assms(2) assms(1) by auto
have bgt: "card B ≠ 0" using assms(5) assms(4) by auto
have "card {f ∈ ?C . ∀ v ∈ d . f v = b}/ (card ?C) =
((card B) powi ((card A) - card d))/((card B) powi (card A))"
using Ccard scard by simp
also have "... = (card B) powi (int (card A - card d) - int (card A))"
using bgt by (simp add: power_int_diff)
also have "... = (card B) powi (int (card A) - int (card d) - int (card A))"
using int_ops lt by simp
also have "... = (card B) powi -(card d)" using assms(1) by (simp add: of_nat_diff)
also have "... = inverse ((card B) powi (card d))"
using power_int_minus[of "card B" "(int (card d))"] by simp
finally show ?thesis by (simp add: inverse_eq_divide)
qed
lemma :
assumes "finite A"
assumes "b ∈ B"
assumes "d ∈ A"
assumes "B ≠ {}"
assumes "finite B"
shows "card {f ∈ (A →⇩E B) . f d = b}/card (A →⇩E B) = 1/(card B)"
(is "card {f ∈ ?C .f d = b}/card ?C = 1/(card B)")
proof -
have "{d} ⊆ A" using assms(3) by simp
moreover have "⋀ f . f ∈ ?C ⟹ f d = b ⟷ (∀ d' ∈ {d}. f d' = b)" by auto
ultimately have "card {f ∈ ?C .f d = b}/card ?C = 1/((card B) powi (card {d}))"
using card_PiE_val_ss_eq[of A b B "{d}"] assms by auto
also have "... = 1/((card B) powi 1)" by auto
finally show ?thesis by simp
qed
lemma :
assumes "finite A"
assumes "b ∈ B"
assumes "d ⊆ A"
assumes "B ≠ {}"
assumes "A ≠ {}"
assumes "finite B"
shows "prob_space.prob (uniform_count_measure (A →⇩E B)) {f ∈ (A →⇩E B) . (∀ v ∈ d .f v = b)} =
1/((card B) powi (card d))"
proof -
let ?C = "(A →⇩E B)"
let ?M = "uniform_count_measure ?C"
have finC: "finite ?C" using assms(2) assms(6) assms(1)
by (simp add: finite_PiE)
moreover have "?C ≠ {}" using assms(4) assms(1)
by (simp add: PiE_eq_empty_iff)
ultimately interpret P: prob_space ?M
using assms(3) by (simp add: prob_space_uniform_count_measure)
have "P.prob {f ∈ ?C . ∀ v ∈ d . f v = b} = card {f ∈ ?C . ∀ v ∈ d . f v = b}/ (card ?C)"
using measure_uniform_count_measure[of ?C "{f ∈ ?C . ∀ v ∈ d . f v = b} "] finC assms(3)
by fastforce
then show ?thesis using card_PiE_val_ss_eq assms by (simp)
qed
proposition :
fixes g :: "'a ⇒ 'b::{banach, second_countable_topology}"
shows "finite A ⟹ integrable (uniform_count_measure A) g"
unfolding uniform_count_measure_def
using integrable_point_measure_finite by fastforce
end