Theory Random_Graph_Subgraph_Threshold.Ugraph_Misc

section‹Miscellaneous and contributed lemmas›

theory Ugraph_Misc
imports
  "HOL-Probability.Probability"
  Girth_Chromatic.Girth_Chromatic_Misc
begin

lemma sum_square:
  fixes a :: "'i  'a :: {monoid_mult, semiring_0}"
  shows "(i  I. a i)^2 = (i  I. j  I. a i * a j)"
  by (simp only: sum_product power2_eq_square)

lemma sum_split:
  "finite I 
  (i  I. if p i then f i else g i) = (i | i  I  p i. f i) + (i | i  I  ¬p i. g i)"
  by (simp add: sum.If_cases Int_def)

lemma sum_split2:
  assumes "finite I"
  shows "(i | i  I  P i. if Q i then f i else g i) = (i | i  I  P i  Q i. f i) + (i | i  I  P i  ¬Q i. g i)"
proof (subst sum.If_cases)
  show "finite {i  I. P i}"
    using assms by simp

  have "{i  I. P i}  Collect Q = {i  I. P i  Q i}" "{i  I. P i}  - Collect Q =  {i  I. P i  ¬ Q i}"
    by auto
  thus "sum f ({i  I. P i}  Collect Q) + sum g ({i  I. P i}  - Collect Q) = sum f {i  I. P i  Q i} + sum g {i  I. P i  ¬ Q i}"
    by presburger
qed

lemma sum_upper:
  fixes f :: "'i  'a :: ordered_comm_monoid_add"
  assumes "finite I" "i. i  I  0  f i"
  shows "(i | i  I  P i. f i)  sum f I"
proof -
  have "sum f I = (i  I. if P i then f i else f i)"
    by simp
  hence "sum f I = (i | i  I  P i. f i) + (i | i  I  ¬P i. f i)"
    by (simp only: sum_split[OF finite I])
  moreover have "0  (i | i  I  ¬P i. f i)"
    by (rule sum_nonneg) (simp add: assms)
  ultimately show ?thesis
    by (metis (full_types) add.comm_neutral add_left_mono)
qed

lemma sum_lower:
  fixes f :: "'i  'a :: ordered_comm_monoid_add"
  assumes "finite I" "i  I" "i. i  I  0  f i" "x < f i"
  shows "x < sum f I"
proof -
  have "x < f i" by fact
  also have "  sum f I"
    using sum_mono2[OF finite I, of "{i}" f] assms by auto
  finally show ?thesis .
qed

lemma sum_lower_or_eq:
  fixes f :: "'i  'a :: ordered_comm_monoid_add"
  assumes "finite I" "i  I" "i. i  I  0  f i" "x  f i"
  shows "x  sum f I"
proof -
  have "x  f i" by fact
  also have "  sum f I"
    using sum_mono2[OF finite I, of "{i}" f] assms by auto
  finally show ?thesis .
qed

lemma sum_left_div_distrib:
  fixes f :: "'i  real"
  shows "(i  I. f i / x) = sum f I / x"
proof -
  have "(i  I. f i / x) = (i  I. f i * (1 / x))"
    by simp
  also have " = sum f I * (1 / x)"
    by (rule sum_distrib_right[symmetric])
  also have " = sum f I / x"
    by simp
  finally show ?thesis
    .
qed

lemma powr_mono3:
  fixes x::real
  assumes "0 < x" "x < 1" "b  a"
  shows "x powr a  x powr b"
proof -
  have "x powr a = 1 / x powr -a"
    by (simp add: powr_minus_divide)
  also have " = (1 / x) powr -a"
    using assms by (simp add: powr_divide)
  also have "  (1 / x) powr -b"
    using assms by (simp add: powr_mono)
  also have " = 1 / x powr -b"
    using assms by (simp add: powr_divide)
  also have " = x powr b"
    by (simp add: powr_minus_divide)
  finally show ?thesis
    .
qed

lemma card_union: "finite A  finite B  card (A  B) = card A + card B - card (A  B)"
by (metis card_Un_Int[symmetric] diff_add_inverse2)

lemma card_1_element:
  assumes "card E = 1"
  shows "a. E = {a}"
proof -
  from assms obtain a where "a  E"
    by force
  let ?E' = "E - {a}"

  have "finite ?E'"
    using assms card_ge_0_finite by force
  hence "card (insert a ?E') = 1 + card ?E'"
    using card.insert_remove by fastforce
  moreover have "E = insert a ?E'"
    using a  E by blast
  ultimately have "card E = 1 + card ?E'"
    by simp
  hence "card ?E' = 0"
    using assms by simp
  hence "?E' = {}"
    using finite ?E' by simp
  thus ?thesis
    using a  E by blast
qed

lemma card_2_elements:
  assumes "card E = 2"
  shows "a b. E = {a, b}  a  b"
proof -
  from assms obtain a where "a  E"
    by force
  let ?E' = "E - {a}"

  have "finite ?E'"
    using assms card_ge_0_finite by force
  hence "card (insert a ?E') = 1 + card ?E'"
    using card.insert_remove by fastforce
  moreover have "E = insert a ?E'"
    using a  E by blast
  ultimately have "card E = 1 + card ?E'"
    by simp
  hence "card ?E' = 1"
    using assms by simp
  then obtain b where "?E' = {b}"
    using card_1_element by blast
  hence "E = {a, b}"
    using a  E by blast
  moreover have "a  b"
    using ?E' = {b} by blast
  ultimately show ?thesis
    by blast
qed

lemma bij_lift:
  assumes "bij_betw f A B"
  shows "bij_betw (λe. f ` e) (Pow A) (Pow B)"
proof -
  have f: "inj_on f A" "f ` A = B"
    using assms unfolding bij_betw_def by simp_all
  have "inj_on (λe. f ` e) (Pow A)"
    unfolding inj_on_def by clarify (metis f(1) inv_into_image_cancel)
  moreover have "(λe. f ` e) ` (Pow A) = (Pow B)"
    by (metis f(2) image_Pow_surj)
  ultimately show ?thesis
    unfolding bij_betw_def by simp
qed

lemma card_inj_subs: "inj_on f A  B  A  card (f ` B) = card B"
by (metis card_image subset_inj_on)

lemma image_comp_cong: "(a. a  A  f a = f (g a))  f ` A = f ` (g ` A)"
  by auto

abbreviation less_fun :: "(nat  real)  (nat  real)  bool" (infix "" 50) where
"f  g  (λn. f n / g n)  0"

context
  fixes f :: "nat  real"
begin

  lemma LIMSEQ_power_zero: "f  0  0 < n   (λx. f x ^ n :: real)  0"
  by (metis power_eq_0_iff tendsto_power)

  lemma LIMSEQ_cong:
    assumes "f  x" "n. f n = g n"
    shows "g  x"
  by (rule real_tendsto_sandwich[where f = f and h = f, OF eventually_mono[OF assms(2)] eventually_mono[OF assms(2)]]) (auto simp: assms(1))
  print_statement Lim_transform_eventually


  lemma LIMSEQ_le_zero:
    assumes "g  0" "n. 0  f n" "n. f n  g n"
    shows "f  0"
  by (rule real_tendsto_sandwich[OF assms(2) assms(3) tendsto_const assms(1)])

  lemma LIMSEQ_const_mult:
    assumes "f  a"
    shows "(λx. c * f x)  c * a"
  by (rule tendsto_mult[OF tendsto_const[where k = c] assms])

  lemma LIMSEQ_const_div:
    assumes "f  a" "c  0"
    shows "(λx. f x / c)  a / c"
  using LIMSEQ_const_mult[where c = "1/c"] assms by simp

end

lemma quot_bounds:
  fixes x :: "'a :: linordered_field"
  assumes "x  x'" "y'  y" "0 < y" "0  x" "0 < y'"
  shows "x / y  x' / y'"
proof (rule order_trans)
  have "0  y"
    using assms by simp
  thus "x / y  x' / y"
    using assms by (simp add: divide_right_mono)
next
  have "0  x'"
    using assms by simp
  moreover have "0 < y * y'"
    using assms by simp
  ultimately show "x' / y  x' / y'"
    using assms by (simp add: divide_left_mono)
qed

lemma less_fun_bounds:
  assumes "f'  g'" "n. f n  f' n" "n. g' n  g n" "n. 0  f n" "n. 0 < g n" "n. 0 < g' n"
  shows "f  g"
proof (rule real_tendsto_sandwich)
  show "n. 0  f n / g n"
    using assms(4,5) by eventually_elim simp
next
  show "n. f n / g n  f' n / g' n"
    using assms(2-) by eventually_elim (simp only: quot_bounds)
qed (auto intro: assms(1))

lemma less_fun_const_quot:
  assumes "f  g" "c  0"
  shows "(λn. b * f n)  (λn. c * g n)"
proof -
  have "(λn. (b * (f n / g n)) / c)  (b * 0) / c"
    using assms by (rule LIMSEQ_const_div[OF LIMSEQ_const_mult])
  hence "(λn. (b * (f n / g n)) / c)  0"
    by simp
  with eventually_sequentiallyI show ?thesis
    by (fastforce intro: Lim_transform_eventually)
qed

lemma partition_set_of_intersecting_sets_by_card:
  assumes "finite A"
  shows "{B. A  B  {}} = (n  {1..card A}. {B. card (A  B) = n})"
proof (rule set_eqI, rule iffI)
  fix B
  assume "B  {B. A  B  {}}"
  hence "0 < card (A  B)"
    using assms by auto
  moreover have "card (A  B)  card A"
    using assms by (simp add: card_mono)
  ultimately have "card (A  B)  {1..card A}"
    by simp
  thus "B  (n  {1..card A}. {B. card (A  B) = n})"
    by blast
qed force

lemma card_set_of_intersecting_sets_by_card:
  assumes "A  I" "finite I" "k  n" "n  card I" "k  card A"
  shows "card {B. B  I  card B = n  card (A  B) = k} = (card A choose k) * ((card I - card A) choose (n - k))"
proof -
  note finite_A = finite_subset[OF assms(1,2)]

  have "card {B. B  I  card B = n  card (A  B) = k} = card ({K. K  A  card K = k} × {B'. B'  I - A  card B' = n - k})" (is "card ?lhs = card ?rhs")
    proof (rule bij_betw_same_card[symmetric])
      let ?f = "λ(K, B'). K  B'"
      have "inj_on ?f ?rhs"
        by (blast intro: inj_onI)
      moreover have "?f ` ?rhs = ?lhs"
        proof (rule set_eqI, rule iffI)
          fix B
          assume "B  ?f ` ?rhs"
          then obtain K B' where K: "K  A" "card K = k" "B'  I - A" "card B' = n - k" "K  B' = B"
            by blast
          show "B  ?lhs"
            proof safe
              fix x assume "x  B" thus "x  I"
                using K A  I by blast
            next
              have "card B = card K + card B' - card (K  B')"
                using K assms by (metis card_union finite_A finite_subset finite_Diff)
              moreover have "K  B' = {}"
                using K assms by blast
              ultimately show "card B = n"
                using K assms by simp
            next
              have "A  B = K"
                using K assms(1) by blast
              thus "card (A  B) = k"
                using K by simp
            qed
        next
          fix B
          assume "B  ?lhs"
          hence B: "B  I" "card B = n" "card (A  B) = k"
            by auto
          let ?K = "A  B"
          let ?B' = "B - A"
          have "?K  A" "card ?K = k" "?B'  I - A"
            using B by auto
          moreover have "card ?B' = n - k"
            using B finite_A assms(1) by (metis Int_commute card_Diff_subset_Int finite_Un inf.left_idem le_iff_inf sup_absorb2)
          ultimately have "(?K, ?B')  ?rhs"
            by blast
          moreover have "B = ?f (?K, ?B')"
            by auto
          ultimately show "B  ?f ` ?rhs"
            by blast
        qed
      ultimately show "bij_betw ?f ?rhs ?lhs"
        unfolding bij_betw_def ..
    qed
  also have " = (K | K  A  card K = k. card {B'. B'  I - A  card B' = n - k})"
    proof (rule card_SigmaI, safe)
      show "finite {K. K  A  card K = k}"
        by (blast intro: finite_subset[where B = "Pow A"] finite_A)
    next
      fix K
      assume "K  A"
      thus "finite {B'. B'  I - A  card B' = n - card K}"
        using assms by auto
    qed
  also have " = card {K. K  A  card K = k} * card {B'. B'  I - A  card B' = n - k}"
    by simp
  also have " = (card A choose k) * (card (I - A) choose (n - k))"
    by (simp only: n_subsets[OF finite_A] n_subsets[OF finite_Diff[OF assms(2)]])
  also have " = (card A choose k) * ((card I - card A) choose (n - k))"
    by (simp only: card_Diff_subset[OF finite_A assms(1)])
  finally show ?thesis
    .
qed

lemma card_dep_pair_set:
  assumes "finite A" "a. a  A  finite (f a)"
  shows "card {(a, b). a  A  card a = n  b  f a  card b = g a} = (a | a  A  card a = n. card (f a) choose g a)" (is "card ?S = ?C")
proof -
  have S: "?S = Sigma {a. a  A  card a = n} (λa. {b. b  f a  card b = g a})" (is "_ = Sigma ?A ?B")
    by auto

  have "card (Sigma ?A ?B) = (a  {a. a  A  card a = n}. card (?B a))"
    proof (rule card_SigmaI, safe)
      show "finite ?A"
        by (rule finite_subset[OF _ finite_Collect_subsets[OF assms(1)]]) blast
    next
      fix a
      assume "a  A"
      hence "finite (f a)"
        by (fact assms(2))
      thus "finite (?B a)"
        by (rule finite_subset[rotated, OF finite_Collect_subsets]) blast
    qed
  also have " = ?C"
    proof (rule sum.cong)
      fix a
      assume "a  {a. a  A  card a = n}"
      hence "finite (f a)"
        using assms(2) by blast
      thus "card (?B a) = card (f a) choose g a"
        by (fact n_subsets)
    qed simp
  finally have "card (Sigma ?A ?B) = ?C"
    .

  thus ?thesis
    by (subst S)
qed

lemma prod_cancel_nat:
  ― ‹Contributed by Manuel Eberl›
  fixes f::"'a  nat"
  assumes "B  A" and "finite A" and "xB. f x  0"
  shows "prod f A / prod f B = prod f (A - B)" (is "?A / ?B = ?C")
proof-
  from prod.subset_diff[OF assms(1,2)] have "?A = ?C * ?B" by auto
  moreover have "?B  0" using assms by (simp add: finite_subset)
  ultimately show ?thesis by simp
qed

lemma prod_id_cancel_nat:
  ― ‹Contributed by Manuel Eberl›
  fixes A::"nat set"
  assumes "B  A" and "finite A" and "0  B"
  shows "A / B = (A-B)"
  using assms(1-2) by (rule prod_cancel_nat) (metis assms(3))

lemma (in prob_space) integrable_squareD:
  ― ‹Contributed by Johannes Hölzl›
  fixes X :: "_  real"
  assumes "integrable M (λx. (X x)^2)" "X  borel_measurable M"
  shows "integrable M X"
proof -
  have "integrable M (λx. max 1 ((X x)^2))"
    using assms by auto
  then show "integrable M X"
  proof (rule Bochner_Integration.integrable_bound[OF _ _ always_eventually[OF allI]])
    fix x show "norm (X x)  norm (max 1 ((X x)^2))"
      using abs_le_square_iff[of 1 "X x"] power_increasing[of 1 2 "abs (X x)"]
      by (auto split: split_max)
  qed fact
qed

end