Theory Miscellaneous_Lemmas
section‹Miscellaneous technical lemmas›
theory Miscellaneous_Lemmas
imports
"HOL-Library.Indicator_Function"
"HOL-Analysis.Convex"
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"
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)
qed
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"
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]"
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
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