Theory 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 "∀x∈B. 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