Theory Basic_Method

(* Theory: Basic_Method
   Author: Chelsea Edmonds
*)

section ‹The Basic Probabilistic Method Framework›
text ‹This theory includes all aspects of step (3) and (4) of the basic method framework, 
which are purely probabilistic ›

theory Basic_Method imports Indep_Events
begin

subsection ‹More Set and Multiset lemmas ›
lemma card_size_set_mset: "card (set_mset A) ≤ size A"
  using size_multiset_overloaded_eq
  by (metis card_eq_sum count_greater_eq_one_iff sum_mono) 
  
lemma Union_exists: "{a ∈ A . ∃ b ∈ B . P a b} = (⋃b ∈ B . {a ∈ A . P a b})"
  by blast

lemma Inter_forall:  "B ≠ {} ⟹ {a ∈ A . ∀ b ∈ B . P a b} = (⋂b ∈ B . {a ∈ A . P a b})"
  by auto

lemma function_map_multi_filter_size:
  assumes "image_mset F (mset_set A) = B" and "finite A"
  shows "card {a ∈ A . P (F a)} = size {# b ∈# B . P b #}"
using assms(2) assms(1) proof (induct A arbitrary: B rule: finite_induct)
  case empty
  then show ?case by simp
next
  case (insert x C)
  then have beq: "B= image_mset F (mset_set C) + {#F x#}" by auto
  then show ?case proof (cases "P (F x)")
    case True
    then have "filter_mset P B = filter_mset P (image_mset F (mset_set C)) + {#F x#}"
      by (simp add: True beq) 
    then have s: "size (filter_mset P B) = size (filter_mset P (image_mset F (mset_set C))) + 1"
      using size_single size_union by auto
    have "{a ∈ insert x C. P (F a)} = insert x {a ∈ C. P (F a)}" using True by auto
    moreover have "x ∉ {a ∈ C. P (F a)}" using insert.hyps(2) by simp
    ultimately have "card {a ∈ insert x C. P (F a)} = card {a ∈ C. P (F a)} + 1" 
      using card_insert_disjoint insert.hyps(1) by auto
    then show ?thesis using s insert.hyps(3) by simp
  next
    case False
    then have "filter_mset P B = filter_mset P (image_mset F (mset_set C))" using beq by simp
    moreover have "{a ∈ insert x C. P (F a)} = {a ∈ C. P (F a)}" using False by auto
    ultimately show ?thesis using insert.hyps(3) by simp
  qed
qed

lemma bij_mset_obtain_set_elem:
  assumes "image_mset F (mset_set A) = B"
  assumes "b ∈# B"
  obtains a where "a ∈ A" and "F a = b"
  using assms set_image_mset
  by (metis finite_set_mset_mset_set image_iff mem_simps(2) mset_set.infinite  set_mset_empty) 

lemma bij_mset_obtain_mset_elem: 
  assumes "finite A"
  assumes "image_mset F (mset_set A) = B"
  assumes "a ∈ A"
  obtains b where "b ∈# B" and "F a = b"
  using assms by fastforce

lemma prod_fn_le1: 
  fixes f :: "'c ⇒ ('d :: {comm_monoid_mult, linordered_semidom})"
  assumes "finite A"
  assumes "A ≠ {}"
  assumes "⋀ y. y ∈ A ⟹ f y ≥ 0 ∧ f y < 1"
  shows "(∏x∈ A. f x) < 1"
using assms(1) assms(2) assms(3) proof (induct A rule: finite_ne_induct)
  case (singleton x)
  then show ?case by auto
next
  case (insert x F)
  then show ?case
  proof (cases "x ∈ F")
    case True
    then show ?thesis using insert.hyps by auto
  next
    case False
    then have "prod f (insert x F) = f x * prod f F" by (simp add: local.insert(1))
    moreover have "prod f F < 1" using insert.hyps insert.prems by auto
    moreover have "f x < 1" "f x ≥ 0" using insert.prems by auto
    ultimately show ?thesis
      by (metis basic_trans_rules(20) basic_trans_rules(23) more_arith_simps(6) 
          mult_left_less_imp_less verit_comp_simplify1(3)) 
  qed
qed

context prob_space
begin

subsection ‹Existence Lemmas ›

lemma prob_lt_one_obtain: 
  assumes "{e ∈ space M . Q e} ∈ events"
  assumes "prob {e ∈ space M . Q e} < 1"
  obtains e where "e ∈ space M" and "¬ Q e"
proof -
  have sin: "{e ∈ space M . ¬ Q e} ∈ events" using assms(1)
    using sets.sets_Collect_neg by blast
  have "prob {e ∈ space M . ¬ Q e} = 1 - prob {e ∈ space M . Q e}" using prob_neg assms by auto
  then have "prob {e∈ space M . ¬ Q e} > 0" using assms(2) by auto
  then show ?thesis using that
    by (smt (verit, best) empty_Collect_eq measure_empty) 
qed

lemma prob_gt_zero_obtain: 
  assumes "{e ∈ space M . Q e} ∈ events"
  assumes "prob {e ∈ space M . Q e} > 0"
  obtains e where "e ∈ space M" and "Q e"
  using assms by (smt (verit) empty_Collect_eq inf.strict_order_iff measure_empty)

lemma inter_gt0_event: 
  assumes "F ` I ⊆ events"
  assumes "prob (⋂ i ∈ I . (space M - (F i))) > 0"
  shows "(⋂ i ∈ I . (space M - (F i))) ∈ events" and "(⋂ i ∈ I . (space M - (F i))) ≠ {}"
  using assms using  measure_notin_sets by (smt (verit), fastforce)

lemma obtain_intersection:
  assumes "F ` I ⊆ events"
  assumes "prob (⋂ i ∈ I . (space M - (F i)))> 0"
  obtains e where "e ∈ space M" and "⋀ i. i ∈ I ⟹ e ∉ F i"
proof -
  have ine: "(⋂ i ∈ I . (space M - (F i))) ≠ {}" using inter_gt0_event[of F I] assms by fast
  then obtain e where "⋀ i. i ∈ I ⟹  e ∈ space M - F i"  by blast
  then show ?thesis
    by (metis Diff_iff ex_in_conv subprob_not_empty that) 
qed

lemma obtain_intersection_prop:
  assumes "F ` I ⊆ events"
  assumes "⋀ i. i ∈ I ⟹ F i = {e ∈ space M . P e i}"
  assumes "prob (⋂ i ∈ I . (space M - (F i)))> 0"
  obtains e where "e ∈ space M" and "⋀ i. i ∈ I ⟹ ¬ P e i"
proof -
  obtain e where ein: "e ∈ space M" and "⋀ i. i ∈ I ⟹ e ∉ F i"
    using obtain_intersection assms(1) assms(3) by auto
  then have "⋀ i. i ∈ I ⟹ e ∈ {e ∈ space M . ¬ P e i}" using assms(2) by simp
  then show ?thesis using ein that by simp
qed
   
lemma not_in_big_union:
  assumes "⋀ i . i ∈ A ⟹ e ∉ i"
  shows "e ∉ (⋃A)"
  using assms by (induct A rule: infinite_finite_induct) auto

lemma not_in_big_union_fn:
  assumes "⋀ i . i ∈ A ⟹ e ∉ F i"
  shows "e ∉ (⋃i ∈ A . F i)"
  using assms by (induct A rule: infinite_finite_induct) auto

lemma obtain_intersection_union:
  assumes "F ` I ⊆ events"
  assumes "prob (⋂ i ∈ I . (space M - (F i)))> 0"
  obtains e where "e ∈ space M" and "e ∉ (⋃i ∈ I. F i)"
proof -
  obtain e where "e ∈ space M" and cond: "⋀ i. i ∈ I ⟹  e  ∉  F i"  
  using obtain_intersection[of F I] assms  by blast
  then show ?thesis using not_in_big_union_fn[of I e F] that by blast
qed

subsection ‹Basic Bounds ›

text ‹Lemmas on the Complete Independence and Union bound ›

lemma complete_indep_bound1: 
  assumes "finite A"
  assumes "A ≠ {}"
  assumes "A ⊆ events"
  assumes "indep_events_set A"
  assumes "⋀ a . a ∈ A ⟹ prob a < 1"
  shows "prob (space M - (⋂A)) > 0"
proof -
  have "⋂A ∈ events" using assms(1) assms(2) assms(3) Inter_event_ss by simp
  then have "prob (space M - (⋂A)) = 1 - prob (⋂A)"
    by (simp add: prob_compl) 
  then have 1: "prob (space M - (⋂A)) = 1 - prod prob A" 
    using indep_events_set_prod_all assms by simp
  moreover have "prod prob A < 1" using assms(5) assms(1) assms(2) assms(4) indep_events_set_events
    by (metis Inf_lower ‹prob (space M - ⋂ A) = 1 - prob (⋂ A)› 
        basic_trans_rules(21) 1 diff_gt_0_iff_gt finite_has_maximal finite_measure_mono )
  ultimately show ?thesis by simp 
qed

lemma complete_indep_bound1_index: 
  assumes "finite A"
  assumes "A ≠ {}"
  assumes "F ` A ⊆ events"
  assumes "indep_events F A"
  assumes "⋀ a . a ∈ A ⟹ prob (F a) < 1"
  shows "prob (space M - (⋂(F` A))) > 0"
proof -
  have pos: "⋀ a. a ∈ A ⟹ prob (F a) ≥ 0" using assms(3) by auto
  have "⋂(F ` A) ∈ events" using assms(1) assms(2) assms(3) Inter_event_ss by simp
  then have eq: "prob (space M - (⋂(F ` A))) = 1 - prob (⋂(F ` A))"
    by (simp add: prob_compl) 
  then have "prob (space M - (⋂(F ` A))) = 1 - (∏i∈A. prob (F i))" 
    using indep_events_prod_all assms by simp
  moreover have "(∏i∈A. prob (F i)) < 1" 
    using assms(5) eq assms(2) assms(1) prod_fn_le1[of A "λ i. prob (F i)"] by auto 
  ultimately show ?thesis by simp 
qed

lemma complete_indep_bound2: 
  assumes "finite A"
  assumes "A ⊆ events"
  assumes "indep_events_set A"
  assumes "⋀ a . a ∈ A ⟹ prob a < 1"
  shows "prob (space M - (⋃A)) > 0"
proof (cases "A = {}")
  case True
  then show ?thesis by (simp add: True prob_space) 
next
  case False
  then have "prob (space M - ⋃A) = prob (⋂a ∈ A . (space M - a))"  by simp
  moreover have "indep_events_set ((λ a. space M - a) ` A)" 
    using assms(1) assms(3) indep_events_set_compl by auto
  moreover have "finite ((λ a. space M - a) ` A)" using assms(1) by auto
  moreover have "((λ a. space M - a) ` A) ≠ {}" using False by auto
  ultimately have eq: "prob (space M - ⋃A) = prod prob ((λ a. space M - a) ` A)" 
    using indep_events_set_prod_all[of "((λ a. space M - a) ` A)"] by linarith
  have "⋀ a. a ∈ ((λ a. space M - a) ` A) ⟹ prob a > 0"
  proof -
    fix a assume "a ∈ ((λ a. space M - a) ` A)"
    then obtain a' where "a = space M - a'" and ain: "a' ∈ A" by blast
    then have "prob a = 1 - prob a'" using prob_compl assms(2) by auto
    moreover have "prob a' < 1" using assms(4) ain by simp
    ultimately show "prob a > 0" by simp
  qed
  then have "prod prob ((λ a. space M - a) ` A) > 0" by (meson prod_pos) 
  then show ?thesis using eq by simp
qed

lemma complete_indep_bound2_index: 
  assumes "finite A"
  assumes "F ` A ⊆ events"
  assumes "indep_events F A"
  assumes "⋀ a . a ∈ A ⟹ prob (F a) < 1"
  shows "prob (space M - (⋃(F ` A))) > 0"
proof (cases "A = {}")
  case True
  then show ?thesis by (simp add: True prob_space) 
next
  case False
  then have "prob (space M - ⋃(F `A)) = prob (⋂a ∈ A . (space M - F a))"  by simp
  moreover have "indep_events (λ a. space M - F a) A" 
    using assms(1) assms(3) indep_events_compl by auto
  ultimately have eq: "prob (space M - ⋃(F ` A)) = (∏i∈A. prob ((λ a. space M - F a) i))" 
    using indep_events_prod_all[of "(λ a. space M - F a)" A] assms(1) False by linarith
  have "⋀ a. a ∈ A ⟹ prob (space M - F a) > 0"
    using prob_compl assms(2) assms(4) by auto
  then have "(∏i∈A. prob ((λ a. space M - F a) i)) > 0" by (meson prod_pos) 
  then show ?thesis using eq by simp
qed

lemma complete_indep_bound3: 
  assumes "finite A"
  assumes "A ≠ {}"
  assumes "F ` A ⊆ events"
  assumes "indep_events F A"
  assumes "⋀ a . a ∈ A ⟹ prob (F a) < 1"
  shows "prob (⋂a ∈ A. space M - F a) > 0"
  using complete_indep_bound2_index compl_Union_fn assms by auto 

text ‹Combining complete independence with existence step ›
lemma complete_indep_bound_obtain: 
  assumes "finite A"
  assumes "A ⊆ events"
  assumes "indep_events_set A"
  assumes "⋀ a . a ∈ A ⟹ prob a < 1"
  obtains e where "e ∈ space M" and "e ∉ ⋃A"
proof -
  have "prob (space M - (⋃A)) > 0" using complete_indep_bound2 assms by auto
  then show ?thesis
    by (metis Diff_eq_empty_iff less_numeral_extra(3) measure_empty subsetI that)
qed

lemma Union_bound_events: 
  assumes "finite A"
  assumes "A ⊆ events"
  shows "prob (⋃A) ≤ (∑a ∈ A. prob a)"
  using finite_measure_subadditive_finite[of A "λ x. x"]  assms by auto

lemma Union_bound_events_fun: 
  assumes "finite A"
  assumes "f ` A ⊆ events"
  shows "prob (⋃(f ` A)) ≤ (∑ a ∈ A. prob (f a))"
  by (simp add: assms(1) assms(2) finite_measure_subadditive_finite) 


lemma Union_bound_avoid: 
  assumes "finite A"
  assumes "(∑a ∈ A. prob a) < 1"
  assumes "A ⊆ events"
  shows "prob (space M - ⋃A) > 0"
proof -
  have "⋃A ∈ events"
    by (simp add: assms(1) assms(3) sets.finite_Union) 
  then have "prob (space M - ⋃A) = 1 - prob (⋃A)"
    using prob_compl by simp
  moreover have "prob (⋃A) < 1" using assms Union_bound_events
    by fastforce 
  ultimately show ?thesis by simp
qed

lemma Union_bound_avoid_fun: 
  assumes "finite A"
  assumes "(∑a ∈ A. prob (f a)) < 1"
  assumes "f`A ⊆ events"
  shows "prob (space M - ⋃(f ` A)) > 0"
proof -
  have "⋃(f ` A) ∈ events"
    by (simp add: assms(1) assms(3) sets.finite_Union) 
  then have "prob (space M - ⋃(f ` A)) = 1 - prob (⋃(f ` A))"
    using prob_compl by simp
  moreover have "prob (⋃(f ` A)) < 1" using assms Union_bound_events_fun
    by (smt (verit, ccfv_SIG) sum.cong) 
  ultimately show ?thesis by simp
qed

text ‹Combining union bound with existance step ›
lemma Union_bound_obtain:
  assumes "finite A"
  assumes "(∑a ∈ A. prob a) < 1"
  assumes "A ⊆ events"
  obtains e where "e ∈ space M" and "e ∉ ⋃A"
proof -
  have "prob (space M - ⋃A) > 0" using Union_bound_avoid assms by simp
  then show ?thesis using that prob_gt_zero_obtain
    by (metis Diff_eq_empty_iff less_numeral_extra(3) measure_empty subsetI) 
qed

lemma Union_bound_obtain_fun:
  assumes "finite A"
  assumes "(∑a ∈ A. prob (f a)) < 1"
  assumes "f ` A ⊆ events"
  obtains e where "e ∈ space M" and "e ∉ ⋃( f` A)"
proof -
  have "prob (space M - ⋃( f` A)) > 0" using Union_bound_avoid_fun assms by simp
  then show ?thesis using that prob_gt_zero_obtain
    by (metis Diff_eq_empty_iff less_numeral_extra(3) measure_empty subsetI) 
qed

lemma Union_bound_obtain_compl:
  assumes "finite A"
  assumes "(∑a ∈ A. prob a) < 1"
  assumes "A ⊆ events"
  obtains e where "e ∈ (space M - ⋃A)"
proof -
  have "prob (space M - ⋃A) > 0" using Union_bound_avoid assms by simp
  then show ?thesis using that prob_gt_zero_obtain
    by (metis all_not_in_conv measure_empty verit_comp_simplify(2) verit_comp_simplify1(3))
qed

lemma Union_bound_obtain_compl_fun:
  assumes "finite A"
  assumes "(∑a ∈ A. prob (f a)) < 1"
  assumes "f ` A ⊆ events"
  obtains e where "e ∈ (space M - ⋃( f` A))"
proof -
  obtain e where "e ∈ space M" and "e ∉ ⋃(f` A)"
    using assms Union_bound_obtain_fun by blast
  then have "e ∈ space M - ⋃ (f ` A)" by simp
  then show ?thesis by fact
qed

end

end