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 - (iA. prob (F i))" 
    using indep_events_prod_all assms by simp
  moreover have "(iA. 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)) = (iA. 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 "(iA. 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