# 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
imports

begin

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"
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
qed

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

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"
proof-
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
qed

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)
next
assume "¬ finite A"
thus ?thesis using assms by auto
qed

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]"
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
qed

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
real_sqrt_le_0_iff)

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))

end