Theory L1_norm_list
theory L1_norm_list
imports "HOL-Analysis.Abstract_Metric_Spaces"
"HOL-Library.Extended_Real"
begin
section‹ L1-norm on Lists with fixed length ›
lemma list_sum_dist_Cons:
fixes a b xs ys n assumes xn: "length xs = n" and yn: "length ys = n"
shows "(∑i = 1..Suc n. d ((a # xs) ! (i - 1)) ((b # ys) ! (i - 1))) = d a b + (∑i = 1..n. d (xs ! (i - 1)) (ys ! (i - 1)))"
proof-
have 0: "{ 0.. n} = {0}∪ {1.. n}"
by auto
show "(∑i = 1..(Suc n). d ((a # xs) ! (i - 1)) ((b # ys) ! (i - 1))) = d a b + (∑i = 1.. n. d (xs ! (i - 1)) (ys ! (i - 1)))"
by(subst sum.reindex_bij_witness[of _ Suc "λi. i - 1" "{0..n}"],auto simp: 0)
qed
subsection‹ A locale for L1-norm of Lists ›
locale L1_norm_list = Metric_space +
fixes n::nat
begin
definition space_L1_norm_list ::"('a list) set" where
"space_L1_norm_list = {xs. xs∈ lists M ∧ length xs = n}"
lemma in_space_L1_norm_list_iff:
shows "x ∈ space_L1_norm_list ⟷(x∈ lists M ∧ length x = n) "
unfolding space_L1_norm_list_def by auto
definition dist_L1_norm_list ::"('a list) ⇒ ('a list) ⇒ real" where
"dist_L1_norm_list xs ys = (∑ i∈{1..n}. d (nth xs (i-1)) (nth ys (i-1)))"
lemma dist_L1_norm_list_nonneg:
shows "⋀ x y. 0 ≤ dist_L1_norm_list x y "
unfolding dist_L1_norm_list_def by(auto intro!: sum_nonneg)
lemma dist_L1_norm_list_commute:
shows "⋀ x y. dist_L1_norm_list x y = dist_L1_norm_list y x "
unfolding dist_L1_norm_list_def using commute by presburger
lemma dist_L1_norm_list_zero:
shows "⋀ x y. length x = n ⟹ length y = n ⟹ x ∈ lists M ⟹ y ∈ lists M ⟹ (dist_L1_norm_list x y = 0 = (x = y))"
proof-
fix x y::"'a list" assume xm: "length x = n" and x: "x ∈ lists M" and ym: "length y = n" and y: "y ∈ lists M"
show "(dist_L1_norm_list x y = 0) = (x = y)"
using xm ym x y
proof(intro iffI)
show "length x = n ⟹ length y = n ⟹ x ∈ lists M ⟹ y ∈ lists M ⟹ x = y ⟹ dist_L1_norm_list x y = 0"
unfolding dist_L1_norm_list_def
proof(induction x arbitrary: n y)
case Nil
then show ?case by auto
next
case (Cons a x2)
then obtain m where n: "n = Suc m" and y: "y = (a # x2)" and x2m: "length x2 = m" and x2M: "x2 ∈ lists M" and aM: "a ∈ M"
by fastforce
have *: "(∑i = 1..n. d ((a # x2) ! (i - 1)) (y ! (i - 1))) = (d a a) + (∑i = 1..m. d ( x2 ! (i-1)) (x2 ! (i-1)))"
unfolding n y using list_sum_dist_Cons[OF x2m x2m] by blast
then show ?case
using Cons.IH[of m x2, OF x2m x2m x2M x2M] aM by auto
qed
next
show " length x = n ⟹ length y = n ⟹ x ∈ lists M ⟹ y ∈ lists M ⟹ dist_L1_norm_list x y = 0 ⟹ x = y"
unfolding dist_L1_norm_list_def
proof(induction x arbitrary: n y)
case Nil
then show ?case by auto
next
case (Cons a x2)
then obtain m b y2 where n: "n = Suc m" and y: "y = (b # y2)" and x2m: "length x2 = m" and y2m: "length y2 = m" and aM: "a ∈ M" and bM: "b ∈ M" and x2M: "x2 ∈ lists M" and y2M:"y2 ∈lists M"
by (metis (no_types, opaque_lifting) Cons_in_lists_iff Suc_length_conv)
have "0 ≤ (∑i = 1..n. d ((a # x2) ! (i - 1)) (y ! (i - 1)))" and 1: "0 ≤ (∑i = 1..m. d (x2 ! (i - 1)) (y2 ! (i - 1))) "
by(rule sum_nonneg,auto)+
hence 0: "(∑i = 1..n. d ((a # x2) ! (i - 1)) (y ! (i - 1))) = 0"
using Cons.prems(5) by blast
have *: "(∑i = 1..n. d ((a # x2) ! (i - 1)) (y ! (i - 1))) = (d a b) + (∑i = 1..m. d ( x2 ! (i-1)) (y2 ! (i-1)))"
unfolding y n using list_sum_dist_Cons[of x2 m y2 d a b , OF x2m y2m ] by blast
have 2: " (∑i = 1..m. d (x2 ! (i - 1)) (y2 ! (i - 1))) ≤ 0"
using nonneg[of a b] Cons.prems(5) unfolding * by linarith
with 1 have 3: "(∑i = 1..m. d (x2 ! (i - 1)) (y2 ! (i - 1))) = 0"
by auto
have "a = b" and "y2 = x2"
unfolding y using 0 * nonneg[of a b] zero[of a b,OF aM bM] Cons.IH[of m y2,OF x2m y2m x2M y2M] 3 by auto
thus ?case by(auto simp: y)
qed
qed
qed
lemma dist_L1_norm_list_trans:
shows"⋀ x y z. length x = n ⟹ length y = n ⟹ length z = n⟹ x ∈ lists M ⟹ y ∈ lists M ⟹ z ∈ lists M ⟹ (dist_L1_norm_list x z ≤ dist_L1_norm_list x y + dist_L1_norm_list y z)"
proof-
fix x y z::"'a list" assume xm: "length x = n" and x: "x ∈ lists M" and ym: "length y = n" and y: "y ∈ lists M" and zm: "length z = n" and z: "z ∈ lists M"
show "dist_L1_norm_list x z ≤ dist_L1_norm_list x y + dist_L1_norm_list y z"
using xm ym zm x y z triangle unfolding dist_L1_norm_list_def
proof(induction n arbitrary:x y z)
case 0
then show ?case by auto
next
case (Suc n)
then obtain a b c::'a and xs ys zs::"'a list" where x: "x = a#xs" and y: "y = b#ys" and z:"z = c#zs"
and xn: "length xs = n" and yn: "length ys = n" and zn: "length zs = n"
using Suc_length_conv[of n x] Suc_length_conv[of n y] Suc_length_conv[of n z] by auto
hence aM: "a ∈ M" and bM: "b ∈ M" and cM: "c ∈ M" and xsM: "xs ∈ lists M" and ysM: "ys ∈ lists M" and zsM: "zs ∈ lists M"
using listsE Suc.prems(4,5,6) unfolding x y z by auto
have " (∑i = 1..Suc n. d (x ! (i - 1)) (z ! (i - 1))) = d a c + (∑i = 1..n. d (xs ! (i - 1)) (zs ! (i - 1)))"
unfolding x z using list_sum_dist_Cons[of xs n zs d a c, OF xn zn] by blast
also have "... ≤ (d a b + d b c) + ( (∑i = 1.. n. d (xs ! (i - 1)) (ys ! (i - 1))) + (∑i = 1.. n. d (ys ! (i - 1)) (zs ! (i - 1))))"
using Suc.IH[of xs ys zs, OF xn yn zn xsM ysM zsM] Suc.prems(7)
triangle[of a b c, OF aM bM cM] by auto
also have "... ≤ (d a b + (∑i = 1.. n. d (xs ! (i - 1)) (ys ! (i - 1)))) + ( d b c + (∑i = 1.. n. d (ys ! (i - 1)) (zs ! (i - 1))))"
by auto
also have "... = (∑i = 1..Suc n. d (x ! (i - 1)) (y ! (i - 1))) + (∑i = 1..Suc n. d (y ! (i - 1)) (z ! (i - 1)))"
unfolding x y z using list_sum_dist_Cons[of ys n zs d b c, OF yn zn,THEN sym] list_sum_dist_Cons[of xs n ys d a b, OF xn yn,THEN sym] by presburger
finally show ?case.
qed
qed
lemma Metric_L1_norm_list : "Metric_space space_L1_norm_list dist_L1_norm_list"
by (simp add: Metric_space_def dist_L1_norm_list_commute dist_L1_norm_list_nonneg dist_L1_norm_list_trans dist_L1_norm_list_zero in_space_L1_norm_list_iff)
end
sublocale L1_norm_list ⊆ MetL1: Metric_space "space_L1_norm_list" "dist_L1_norm_list"
by (simp add: Metric_L1_norm_list)
subsection‹ Lemmas on L1-norm on lists of natural numbers ›
lemma L1_dist_k:
fixes x y k::nat
assumes "real_of_int ¦int x - int y¦ ≤ k"
shows "(x,y) ∈ {(x,y) | x y. ¦int x - int y¦ ≤ 1} ^^ k"
using assms proof(induction k arbitrary: x y)
case 0
then have " x = y"
by auto
then show ?case
by auto
next
case (Suc k)
then show ?case
proof(cases "real_of_int ¦int x - int y¦ ≤ k" )
case True
then have "(x,y) ∈ {(x,y) | x y. ¦int x - int y¦ ≤ 1} ^^ k"
using Suc.IH[of x y] by auto
thus ?thesis
by auto
next
case False
hence "¦int x - int y¦ > k"
by auto
moreover have " ¦int x - int y¦ ≤ Suc k"
using Suc.prems by linarith
ultimately have absSuck: "¦ int x - int y¦ = Suc k"
unfolding Int.zabs_def using int_ops(4) of_int_of_nat_eq of_nat_less_of_int_iff by linarith
have "∃z::nat. ¦ int x - int z¦ = k ∧ ¦ int z - int y¦ = 1"
proof(cases "x ≤ y")
case True
thus ?thesis
using absSuck by(intro exI[of _ "x + k"],auto)
next
case False
thus ?thesis
using absSuck by(intro exI[of _ "y + 1"],auto)
qed
then obtain z::nat where a: "¦ int x - int z¦ = k" and b: "¦ int z - int y¦ = 1"
by blast
then have "(x,z) ∈ {(x,y) | x y. ¦int x - int y¦ ≤ 1} ^^ k" and "(z,y) ∈ {(x,y) | x y. ¦int x - int y¦ ≤ 1} ^^ 1"
using Suc.IH[of x z] by auto
thus ?thesis
by auto
qed
qed
context
fixes n::nat
begin
interpretation L11nat: L1_norm_list "(UNIV::nat set)" "(λx y. ¦int x - int y¦)" n
by(unfold_locales,auto)
interpretation L11nat2: L1_norm_list "(UNIV::nat set)" "(λx y. ¦int x - int y¦)" "Suc n"
by(unfold_locales,auto)
abbreviation "adj_L11nat ≡ {(xs, ys) |xs ys. xs ∈ L11nat.space_L1_norm_list ∧ ys ∈ L11nat.space_L1_norm_list ∧ L11nat.dist_L1_norm_list xs ys ≤ 1}"
abbreviation "adj_L11nat2 ≡ {(xs, ys) |xs ys. xs ∈ L11nat2.space_L1_norm_list ∧ ys ∈ L11nat2.space_L1_norm_list ∧ L11nat2.dist_L1_norm_list xs ys ≤ 1}"
lemma L1_adj_iterate_Cons1:
assumes "xs ∈ L11nat.space_L1_norm_list"
and "ys ∈ L11nat.space_L1_norm_list"
and "(xs, ys) ∈ adj_L11nat ^^ k"
shows "(x#xs, x#ys) ∈ adj_L11nat2 ^^ k"
using assms
proof(induction k arbitrary: xs ys)
case 0
then have 1: "x # xs = x # ys" and "x # xs ∈ L11nat2.space_L1_norm_list"
by (auto simp: L11nat.space_L1_norm_list_def L11nat2.space_L1_norm_list_def)
then show ?case
by auto
next
case (Suc k)
then obtain zs where k: "(xs , zs) ∈ adj_L11nat ^^ k" and 1: "(zs , ys) ∈ adj_L11nat" and zs: "zs ∈ L11nat.space_L1_norm_list"
by auto
have A: "(x # xs , x # zs) ∈ adj_L11nat2 ^^ k"
by(rule Suc.IH [of xs zs,OF Suc(2) zs, OF k])
have "x # zs ∈ L11nat2.space_L1_norm_list " and "x # ys ∈ L11nat2.space_L1_norm_list "
using Suc(3) zs by(auto simp: L11nat2.space_L1_norm_list_def L11nat.space_L1_norm_list_def )
moreover have "L11nat2.dist_L1_norm_list (x # zs)(x # ys) ≤ 1"
using 1 L1_norm_list.list_sum_dist_Cons[of zs n ys "(λx y. real_of_int ¦int x - int y¦)" x x] Suc(3) zs L11nat.space_L1_norm_list_def
L11nat2.dist_L1_norm_list_def L11nat.dist_L1_norm_list_def
by auto
ultimately show ?case
using A by auto
qed
lemma L1_adj_Cons1:
assumes "xs ∈ L11nat.space_L1_norm_list"
and "real_of_int ¦int x - int y¦ ≤ 1"
shows "(x # xs, y # xs) ∈ adj_L11nat2"
using L1_norm_list.list_sum_dist_Cons[of xs n xs "(λx y. real_of_int ¦int x - int y¦)" x y] assms
unfolding L11nat.dist_L1_norm_list_def L11nat2.space_L1_norm_list_def L11nat2.dist_L1_norm_list_def L11nat.space_L1_norm_list_def lists_UNIV by auto
lemma L1_adj_iterate_Cons2:
assumes "xs ∈ L11nat.space_L1_norm_list" and "real_of_int ¦int x - int y¦ ≤ k"
shows "(x # xs, y # xs) ∈ adj_L11nat2 ^^ k"
proof-
have "(x,y) ∈ {(x,y) | x y. ¦int x - int y¦ ≤ 1} ^^ k"
using L1_dist_k[of x y k] assms(2) by auto
thus ?thesis
proof(induction k arbitrary: x y)
case 0
then have "x = y"
by auto
then show ?case
by auto
next
case (Suc k)
then obtain z where k: "(x, z) ∈ {(x, y) |x y. ¦int x - int y¦ ≤ 1} ^^ k" and "(z, y) ∈ {(x, y) |x y. ¦int x - int y¦ ≤ 1}"
using L1_dist_k[of x y k] by auto
then have "(x#xs, z#xs) ∈ adj_L11nat2 ^^ k" and "(z#xs, y#xs) ∈ adj_L11nat2"
using Suc.IH[of x z, OF k] L1_adj_Cons1[of xs z y, OF assms(1)]
by auto
then show ?case
by auto
qed
qed
lemma L1_adj_iterate:
fixes k::nat
assumes "xs ∈ L11nat.space_L1_norm_list"
and "ys ∈ L11nat.space_L1_norm_list"
and " L11nat.dist_L1_norm_list xs ys ≤ k"
shows "(xs,ys) ∈ adj_L11nat ^^ k"
using assms
proof(induction n arbitrary: xs ys k)
case 0
interpret L1_norm_list "UNIV::nat set" "(λx y. real_of_int ¦int x - int y¦)" 0
by(unfold_locales,auto)
let ?R = "{(xs, ys) |xs ys. xs ∈ space_L1_norm_list ∧ ys ∈ space_L1_norm_list ∧ dist_L1_norm_list xs ys ≤ 1}"
from 0 have 1: "xs = []" and 2: "ys = []"
by (auto simp: space_L1_norm_list_def)
then show ?case
proof(induction k)
case 0
then show ?case
by auto
next
case (Suc k)
then have 1: "(xs, ys) ∈ ?R ^^ k"
by auto
moreover from Suc have "dist_L1_norm_list ys ys = 0"
by(subst MetL1.mdist_zero,auto simp: space_L1_norm_list_def)
moreover hence 2: "(ys, ys) ∈ ?R"
using space_L1_norm_list_def 2 unfolding lists_UNIV by auto
ultimately show ?case
by auto
qed
next
case (Suc n)
interpret sp: L1_norm_list "UNIV::nat set" "(λx y. real_of_int ¦int x - int y¦)" n
by(unfold_locales,auto)
interpret sp2: L1_norm_list "UNIV::nat set" "(λx y. real_of_int ¦int x - int y¦)" "Suc n"
by(unfold_locales,auto)
let ?R = "{(xs, ys) |xs ys. xs ∈ sp.space_L1_norm_list ∧ ys ∈ sp.space_L1_norm_list ∧ sp.dist_L1_norm_list xs ys ≤ 1}"
let ?R2 = "{(xs, ys) |xs ys. xs ∈ sp2.space_L1_norm_list ∧ ys ∈ sp2.space_L1_norm_list ∧ sp2.dist_L1_norm_list xs ys ≤ 1}"
show ?case
using Suc proof(induction k)
case 0
from 0(2,3,4) have "sp2.dist_L1_norm_list xs ys = 0"
using sp2.MetL1.mdist_pos_eq sp2.MetL1.mdist_zero by fastforce
moreover have "sp2.dist_L1_norm_list xs ys ≥ 0"
by(rule sp2.MetL1.nonneg)
ultimately have "sp2.dist_L1_norm_list xs ys = 0"
by auto
hence "xs = ys"
using sp2.MetL1.zero[of xs ys] 0(2,3) by auto
then show ?case by auto
next
case (Suc k)
then obtain x y xs2 ys2 where xs: "xs = x # xs2" and ys: "ys = y # ys2" and xs2: "xs2 ∈ sp.space_L1_norm_list" and ys2: "ys2 ∈ sp.space_L1_norm_list"
using Suc.prems(1) Suc.prems(2) length_Suc_conv[of xs n] length_Suc_conv[of ys n] sp.space_L1_norm_list_def sp2.space_L1_norm_list_def by auto
hence *: " ¦int x - int y¦ + sp.dist_L1_norm_list xs2 ys2 = sp2.dist_L1_norm_list xs ys"
using L1_norm_list.list_sum_dist_Cons[of xs2 n ys2 "(λx y. real_of_int ¦int x - int y¦)" x y] xs2 ys2
unfolding sp.dist_L1_norm_list_def sp2.dist_L1_norm_list_def xs ys sp.space_L1_norm_list_def lists_UNIV by auto
show ?case
proof(cases "x = y")
case True
hence "sp.dist_L1_norm_list xs2 ys2 ≤ (Suc k)"
using Suc(5) * by auto
with Suc.prems(1)[of xs2 ys2 "Suc k"] xs2 ys2 have "(xs2, ys2) ∈ ?R ^^ Suc k"
by auto
thus ?thesis
unfolding True xs ys
using L1_norm_list.L1_adj_iterate_Cons1[of xs2 n ys2 "Suc k" y,OF xs2 ys2] by blast
next
case False
then obtain k2::nat where k2: "¦int x - int y¦ = k2"
by (meson abs_ge_zero nonneg_int_cases)
moreover then have en: "sp.dist_L1_norm_list xs2 ys2 ≤ Suc k - k2"
using * Suc.prems(4) by auto
moreover have "0 ≤ sp.dist_L1_norm_list xs2 ys2"
by(rule sp.MetL1.nonneg)
ultimately have plus: "Suc k ≥ k2"
using * Suc.prems(4) by linarith
have p: "k2 ≥ 1"
using * False k2 by auto
then obtain k3::nat where k3: "k2 = Suc k3"
using not0_implies_Suc by force
with plus en have en: "k ≥ k3" and "sp.dist_L1_norm_list xs2 ys2 ≤ k - k3"
by auto
hence "(xs2, ys2) ∈ ?R ^^ (k - k3)"
using Suc.prems(1)[of xs2 ys2 "k - k3" ] xs2 ys2 by auto
hence A: "(y # xs2, y # ys2) ∈ ?R2 ^^ (k - k3)"
using L1_norm_list.L1_adj_iterate_Cons1[of xs2 n ys2 " (k - k3)" y ] xs2 ys2 by blast
have "¦int x - int y¦ = (Suc k3)"
by(auto simp: k2 k3)
then have B: "(x # xs2, y # xs2) ∈ ?R2 ^^ Suc k3"
by(intro L1_norm_list.L1_adj_iterate_Cons2 xs2,auto)
have "(x # xs2, y # ys2) ∈ ?R2 ^^ (Suc k3 + (k - k3))"
by(intro relpow_trans[of _ "y#xs2"] A B )
thus "(xs, ys) ∈ ?R2 ^^ (Suc k)"
unfolding xs ys using en k3 by auto
qed
qed
qed
end
hide_fact (open) list_sum_dist_Cons
end