Theory Miscellaneous_Lemmas

section‹Miscellaneous technical lemmas›

  Title:   Miscellaneous_Lemmas.thy
  Authors: Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds
  Affiliation: University of Cambridge
  Date: August 2022.

theory Miscellaneous_Lemmas

lemma set_pairs_filter_subset: "A  B  {p . p  A × A  P p}  {p. p  B × B  P p}"
  by (intro subsetI) blast

lemma card_set_ss_indicator: 
  assumes "A  B"
  assumes "finite B"
  shows "card A = ( p  B. indicator A p)"
proof -
  obtain C where ceq: "C = B - A" by blast
  then have beq: "B = A  C" using assms by blast
  have bint: "A  C = {}" using ceq by blast
  have finite: "finite A" using assms finite_subset by auto 
  have zero: " p. p  C  indicator (A) p = 0"
    by (simp add: ceq) 
  then have "card A = ( p  A . indicator (A) p)"
    by simp 
  also have "... = ( p  A . indicator A p) + ( p  C . indicator A p)" 
    using zero by (metis add_cancel_left_right sum.neutral) 
  finally show "card A = ( p  B. indicator A p)" using beq bint assms
    by (metis add.commute ceq sum.subset_diff) 

lemma card_cartesian_prod_square: "finite X  card (X × X) = (card X)^2" 
  using card_cartesian_product by (simp add: power2_eq_square) 

lemma (in ordered_ab_group_add) diff_strict1_mono: 
  assumes "a > a'" "b  b'"
  shows "a - b > a' - b'"
  using diff_strict_mono assms
  by (metis local.diff_strict_right_mono local.dual_order.not_eq_order_implies_strict) 

lemma card_cartesian_product_6: "card (A × A × A × A × A × A) = (card A) ^ 6"
  have "card (A × A × A × A × A × A) = 
    card A * card A * card A * card A * card A * card A" 
    using card_cartesian_product mult.commute by metis
  then show ?thesis by algebra

lemma card_cartesian_product3: "card (X × Y × Z) = card X * card Y * card Z"
  using card_cartesian_product  by (metis mult.commute mult.left_commute)  

lemma card_le_image_div:
  fixes A:: "'a set" and B:: "'b set" and f:: "'a  'b set" and r:: real
  assumes "finite B" and "pairwise (λ s t. disjnt (f s) (f t)) A" and " d  A. (card (f d))  r" 
  and " d  A. f d  B" and "r > 0"
  shows "card A  card B / r"

proof (cases "finite A")
  assume hA: "finite A"
  have hpair_disj: "pairwise disjnt (f ` A)" using assms by (metis pairwiseD pairwise_imageI)
  have "r * card A = ( d  A. r)" by simp
  also have "...  ( d  A. card (f d))" using assms sum_mono by fastforce
  also have "... = sum card (f ` A)" using assms hA by (simp add: sum_card_image)
  also have "... = card ( d  A. f d)" using assms hA hpair_disj
    by (metis Sup_upper card_Union_disjoint finite_UN_I rev_finite_subset)
  also have "...  card B" using assms card_mono
    by (metis UN_subset_iff of_nat_le_iff)
  finally have "r * card A  card B" by linarith
  thus ?thesis using divide_le_eq assms by (simp add: mult_imp_le_div_pos mult_of_nat_commute)
  assume "¬ finite A"
  thus ?thesis using assms by auto

lemma list_middle_eq: 
  "length xs = length ys  hd xs = hd ys  last xs = last ys 
     butlast (tl xs) = butlast (tl ys)  xs = ys"
  apply (induct xs ys rule: list_induct2, simp)
  by (metis append_butlast_last_id butlast.simps(1) butlast.simps(2) butlast_tl hd_Cons_tl 
      impossible_Cons le_refl list.sel(3) neq_Nil_conv)

lemma list2_middle_singleton: 
  assumes "length xs = 3"
  shows "butlast (tl xs) = [xs ! 1]"
proof (simp add: list_eq_iff_nth_eq assms)
  have l: "length (butlast (tl xs)) = 1" using length_butlast length_tl assms by simp 
  then have " butlast (tl xs) ! 0 = (tl xs) ! 0" using nth_butlast[of 0 "tl xs"] by simp
  then show "butlast (tl xs) ! 0 = xs ! Suc 0" using nth_tl[of 0 xs]  l by simp

lemma le_powr_half_mult:
  fixes x y z:: real
  assumes "x ^ 2  y * z" and "0  y" and "0  z"
  shows "x  y powr(1/2) * z powr (1/2)"
  using assms power2_eq_square
  by (metis dual_order.trans linorder_linear powr_ge_pzero powr_half_sqrt powr_mult real_le_rsqrt 

lemma Cauchy_Schwarz_ineq_sum2:
  fixes f g:: "'a  real" and A:: "'a set"
  shows "( d  A. f d * g d)  
    ( d  A. (f d)^2) powr (1/2) * ( d  A. (g d)^2) powr (1/2)"
  using Convex.Cauchy_Schwarz_ineq_sum[of "f" "g" "A"] le_powr_half_mult sum_nonneg zero_le_power2
  by (metis (mono_tags, lifting))