(* Title: Multivariate_Analysis/Vec1.thy
Author: Amine Chaieb, University of Cambridge
Author: Robert Himmelmann, TU Muenchen
*)
header {* Vectors of size 1, 2, or 3 *}
theory Vec1
imports Topology_Euclidean_Space
begin
text{* Some common special cases.*}
lemma forall_1[simp]: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"
by (metis num1_eq_iff)
lemma ex_1[simp]: "(\<exists>x::1. P x) \<longleftrightarrow> P 1"
by auto (metis num1_eq_iff)
lemma exhaust_2:
fixes x :: 2 shows "x = 1 \<or> x = 2"
proof (induct x)
case (of_int z)
then have "0 <= z" and "z < 2" by simp_all
then have "z = 0 | z = 1" by arith
then show ?case by auto
qed
lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2"
by (metis exhaust_2)
lemma exhaust_3:
fixes x :: 3 shows "x = 1 \<or> x = 2 \<or> x = 3"
proof (induct x)
case (of_int z)
then have "0 <= z" and "z < 3" by simp_all
then have "z = 0 \<or> z = 1 \<or> z = 2" by arith
then show ?case by auto
qed
lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"
by (metis exhaust_3)
lemma UNIV_1 [simp]: "UNIV = {1::1}"
by (auto simp add: num1_eq_iff)
lemma UNIV_2: "UNIV = {1::2, 2::2}"
using exhaust_2 by auto
lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"
using exhaust_3 by auto
lemma setsum_1: "setsum f (UNIV::1 set) = f 1"
unfolding UNIV_1 by simp
lemma setsum_2: "setsum f (UNIV::2 set) = f 1 + f 2"
unfolding UNIV_2 by simp
lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3"
unfolding UNIV_3 by (simp add: add_ac)
instantiation num1 :: cart_one begin
instance proof
show "CARD(1) = Suc 0" by auto
qed end
(* "lift" from 'a to 'a^1 and "drop" from 'a^1 to 'a -- FIXME: potential use of transfer *)
abbreviation vec1:: "'a \<Rightarrow> 'a ^ 1" where "vec1 x \<equiv> vec x"
abbreviation dest_vec1:: "'a ^1 \<Rightarrow> 'a"
where "dest_vec1 x \<equiv> (x$1)"
lemma vec1_component[simp]: "(vec1 x)$1 = x"
by simp
lemma vec1_dest_vec1: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"
by (simp_all add: Cart_eq)
declare vec1_dest_vec1(1) [simp]
lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))"
by (metis vec1_dest_vec1(1))
lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))"
by (metis vec1_dest_vec1(1))
lemma vec1_eq[simp]: "vec1 x = vec1 y \<longleftrightarrow> x = y"
by (metis vec1_dest_vec1(2))
lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \<longleftrightarrow> x = y"
by (metis vec1_dest_vec1(1))
subsection{* The collapse of the general concepts to dimension one. *}
lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
by (simp add: Cart_eq)
lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"
apply auto
apply (erule_tac x= "x$1" in allE)
apply (simp only: vector_one[symmetric])
done
lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
by (simp add: norm_vector_def)
lemma norm_real: "norm(x::real ^ 1) = abs(x$1)"
by (simp add: norm_vector_1)
lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))"
by (auto simp add: norm_real dist_norm)
subsection{* Explicit vector construction from lists. *}
primrec from_nat :: "nat \<Rightarrow> 'a::{monoid_add,one}"
where "from_nat 0 = 0" | "from_nat (Suc n) = 1 + from_nat n"
lemma from_nat [simp]: "from_nat = of_nat"
by (rule ext, induct_tac x, simp_all)
primrec
list_fun :: "nat \<Rightarrow> _ list \<Rightarrow> _ \<Rightarrow> _"
where
"list_fun n [] = (\<lambda>x. 0)"
| "list_fun n (x # xs) = fun_upd (list_fun (Suc n) xs) (from_nat n) x"
definition "vector l = (\<chi> i. list_fun 1 l i)"
(*definition "vector l = (\<chi> i. if i <= length l then l ! (i - 1) else 0)"*)
lemma vector_1: "(vector[x]) $1 = x"
unfolding vector_def by simp
lemma vector_2:
"(vector[x,y]) $1 = x"
"(vector[x,y] :: 'a^2)$2 = (y::'a::zero)"
unfolding vector_def by simp_all
lemma vector_3:
"(vector [x,y,z] ::('a::zero)^3)$1 = x"
"(vector [x,y,z] ::('a::zero)^3)$2 = y"
"(vector [x,y,z] ::('a::zero)^3)$3 = z"
unfolding vector_def by simp_all
lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))"
apply auto
apply (erule_tac x="v$1" in allE)
apply (subgoal_tac "vector [v$1] = v")
apply simp
apply (vector vector_def)
apply simp
done
lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
apply auto
apply (erule_tac x="v$1" in allE)
apply (erule_tac x="v$2" in allE)
apply (subgoal_tac "vector [v$1, v$2] = v")
apply simp
apply (vector vector_def)
apply (simp add: forall_2)
done
lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))"
apply auto
apply (erule_tac x="v$1" in allE)
apply (erule_tac x="v$2" in allE)
apply (erule_tac x="v$3" in allE)
apply (subgoal_tac "vector [v$1, v$2, v$3] = v")
apply simp
apply (vector vector_def)
apply (simp add: forall_3)
done
lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_ext,rule) unfolding image_iff defer
apply(rule_tac x="dest_vec1 x" in bexI) by auto
lemma dest_vec1_lambda: "dest_vec1(\<chi> i. x i) = x 1"
by (simp)
lemma dest_vec1_vec: "dest_vec1(vec x) = x"
by (simp)
lemma dest_vec1_sum: assumes fS: "finite S"
shows "dest_vec1(setsum f S) = setsum (dest_vec1 o f) S"
apply (induct rule: finite_induct[OF fS])
apply simp
apply auto
done
lemma norm_vec1 [simp]: "norm(vec1 x) = abs(x)"
by (simp add: vec_def norm_real)
lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)"
by (simp only: dist_real vec1_component)
lemma abs_dest_vec1: "norm x = \<bar>dest_vec1 x\<bar>"
by (metis vec1_dest_vec1(1) norm_vec1)
lemmas vec1_dest_vec1_simps = forall_vec1 vec_add[THEN sym] dist_vec1 vec_sub[THEN sym] vec1_dest_vec1 norm_vec1 vector_smult_component
vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def
lemma bounded_linear_vec1:"bounded_linear (vec1::real\<Rightarrow>real^1)"
unfolding bounded_linear_def additive_def bounded_linear_axioms_def
unfolding smult_conv_scaleR[THEN sym] unfolding vec1_dest_vec1_simps
apply(rule conjI) defer apply(rule conjI) defer apply(rule_tac x=1 in exI) by auto
lemma linear_vmul_dest_vec1:
fixes f:: "real^_ \<Rightarrow> real^1"
shows "linear f \<Longrightarrow> linear (\<lambda>x. dest_vec1(f x) *s v)"
unfolding smult_conv_scaleR
by (rule linear_vmul_component)
lemma linear_from_scalars:
assumes lf: "linear (f::real^1 \<Rightarrow> real^_)"
shows "f = (\<lambda>x. dest_vec1 x *s column 1 (matrix f))"
unfolding smult_conv_scaleR
apply (rule ext)
apply (subst matrix_works[OF lf, symmetric])
apply (auto simp add: Cart_eq matrix_vector_mult_def column_def mult_commute)
done
lemma linear_to_scalars: assumes lf: "linear (f::real ^'n \<Rightarrow> real^1)"
shows "f = (\<lambda>x. vec1(row 1 (matrix f) \<bullet> x))"
apply (rule ext)
apply (subst matrix_works[OF lf, symmetric])
apply (simp add: Cart_eq matrix_vector_mult_def row_def inner_vector_def mult_commute)
done
lemma dest_vec1_eq_0: "dest_vec1 x = 0 \<longleftrightarrow> x = 0"
by (simp add: dest_vec1_eq[symmetric])
lemma setsum_scalars: assumes fS: "finite S"
shows "setsum f S = vec1 (setsum (dest_vec1 o f) S)"
unfolding vec_setsum[OF fS] by simp
lemma dest_vec1_wlog_le: "(\<And>(x::'a::linorder ^ 1) y. P x y \<longleftrightarrow> P y x) \<Longrightarrow> (\<And>x y. dest_vec1 x <= dest_vec1 y ==> P x y) \<Longrightarrow> P x y"
apply (cases "dest_vec1 x \<le> dest_vec1 y")
apply simp
apply (subgoal_tac "dest_vec1 y \<le> dest_vec1 x")
apply (auto)
done
text{* Lifting and dropping *}
lemma continuous_on_o_dest_vec1: fixes f::"real \<Rightarrow> 'a::real_normed_vector"
assumes "continuous_on {a..b::real} f" shows "continuous_on {vec1 a..vec1 b} (f o dest_vec1)"
using assms unfolding continuous_on_iff apply safe
apply(erule_tac x="x$1" in ballE,erule_tac x=e in allE) apply safe
apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real
apply(erule_tac x="dest_vec1 x'" in ballE) by(auto simp add:vector_le_def)
lemma continuous_on_o_vec1: fixes f::"real^1 \<Rightarrow> 'a::real_normed_vector"
assumes "continuous_on {a..b} f" shows "continuous_on {dest_vec1 a..dest_vec1 b} (f o vec1)"
using assms unfolding continuous_on_iff apply safe
apply(erule_tac x="vec x" in ballE,erule_tac x=e in allE) apply safe
apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real
apply(erule_tac x="vec1 x'" in ballE) by(auto simp add:vector_le_def)
lemma continuous_on_vec1:"continuous_on A (vec1::real\<Rightarrow>real^1)"
by(rule linear_continuous_on[OF bounded_linear_vec1])
lemma mem_interval_1: fixes x :: "real^1" shows
"(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
"(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
by(simp_all add: Cart_eq vector_less_def vector_le_def)
lemma vec1_interval:fixes a::"real" shows
"vec1 ` {a .. b} = {vec1 a .. vec1 b}"
"vec1 ` {a<..<b} = {vec1 a<..<vec1 b}"
apply(rule_tac[!] set_ext) unfolding image_iff vector_less_def unfolding mem_interval
unfolding forall_1 unfolding vec1_dest_vec1_simps
apply rule defer apply(rule_tac x="dest_vec1 x" in bexI) prefer 3 apply rule defer
apply(rule_tac x="dest_vec1 x" in bexI) by auto
(* Some special cases for intervals in R^1. *)
lemma interval_cases_1: fixes x :: "real^1" shows
"x \<in> {a .. b} ==> x \<in> {a<..<b} \<or> (x = a) \<or> (x = b)"
unfolding Cart_eq vector_less_def vector_le_def mem_interval by(auto simp del:dest_vec1_eq)
lemma in_interval_1: fixes x :: "real^1" shows
"(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b) \<and>
(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
unfolding Cart_eq vector_less_def vector_le_def mem_interval by(auto simp del:dest_vec1_eq)
lemma interval_eq_empty_1: fixes a :: "real^1" shows
"{a .. b} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a"
"{a<..<b} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a"
unfolding interval_eq_empty and ex_1 by auto
lemma subset_interval_1: fixes a :: "real^1" shows
"({a .. b} \<subseteq> {c .. d} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or>
dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a \<le> dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
"({a .. b} \<subseteq> {c<..<d} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or>
dest_vec1 c < dest_vec1 a \<and> dest_vec1 a \<le> dest_vec1 b \<and> dest_vec1 b < dest_vec1 d)"
"({a<..<b} \<subseteq> {c .. d} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or>
dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
"({a<..<b} \<subseteq> {c<..<d} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or>
dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
unfolding subset_interval[of a b c d] unfolding forall_1 by auto
lemma eq_interval_1: fixes a :: "real^1" shows
"{a .. b} = {c .. d} \<longleftrightarrow>
dest_vec1 b < dest_vec1 a \<and> dest_vec1 d < dest_vec1 c \<or>
dest_vec1 a = dest_vec1 c \<and> dest_vec1 b = dest_vec1 d"
unfolding set_eq_subset[of "{a .. b}" "{c .. d}"]
unfolding subset_interval_1(1)[of a b c d]
unfolding subset_interval_1(1)[of c d a b]
by auto
lemma disjoint_interval_1: fixes a :: "real^1" shows
"{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d < dest_vec1 c \<or> dest_vec1 b < dest_vec1 c \<or> dest_vec1 d < dest_vec1 a"
"{a .. b} \<inter> {c<..<d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d \<le> dest_vec1 c \<or> dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
"{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or> dest_vec1 d < dest_vec1 c \<or> dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
"{a<..<b} \<inter> {c<..<d} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or> dest_vec1 d \<le> dest_vec1 c \<or> dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
unfolding disjoint_interval and ex_1 by auto
lemma open_closed_interval_1: fixes a :: "real^1" shows
"{a<..<b} = {a .. b} - {a, b}"
unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
lemma closed_open_interval_1: "dest_vec1 (a::real^1) \<le> dest_vec1 b ==> {a .. b} = {a<..<b} \<union> {a,b}"
unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
lemma Lim_drop_le: fixes f :: "'a \<Rightarrow> real^1" shows
"(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. dest_vec1 (f x) \<le> b) net ==> dest_vec1 l \<le> b"
using Lim_component_le[of f l net 1 b] by auto
lemma Lim_drop_ge: fixes f :: "'a \<Rightarrow> real^1" shows
"(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. b \<le> dest_vec1 (f x)) net ==> b \<le> dest_vec1 l"
using Lim_component_ge[of f l net b 1] by auto
text{* Also more convenient formulations of monotone convergence. *}
lemma bounded_increasing_convergent: fixes s::"nat \<Rightarrow> real^1"
assumes "bounded {s n| n::nat. True}" "\<forall>n. dest_vec1(s n) \<le> dest_vec1(s(Suc n))"
shows "\<exists>l. (s ---> l) sequentially"
proof-
obtain a where a:"\<forall>n. \<bar>dest_vec1 (s n)\<bar> \<le> a" using assms(1)[unfolded bounded_iff abs_dest_vec1] by auto
{ fix m::nat
have "\<And> n. n\<ge>m \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)"
apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE) by(auto simp add: not_less_eq_eq) }
hence "\<forall>m n. m \<le> n \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)" by auto
then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar>dest_vec1 (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a] unfolding monoseq_def by auto
thus ?thesis unfolding Lim_sequentially apply(rule_tac x="vec1 l" in exI)
unfolding dist_norm unfolding abs_dest_vec1 by auto
qed
lemma dest_vec1_simps[simp]: fixes a::"real^1"
shows "a$1 = 0 \<longleftrightarrow> a = 0" (*"a \<le> 1 \<longleftrightarrow> dest_vec1 a \<le> 1" "0 \<le> a \<longleftrightarrow> 0 \<le> dest_vec1 a"*)
"a \<le> b \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 b" "dest_vec1 (1::real^1) = 1"
by(auto simp add: vector_le_def Cart_eq)
lemma dest_vec1_inverval:
"dest_vec1 ` {a .. b} = {dest_vec1 a .. dest_vec1 b}"
"dest_vec1 ` {a<.. b} = {dest_vec1 a<.. dest_vec1 b}"
"dest_vec1 ` {a ..<b} = {dest_vec1 a ..<dest_vec1 b}"
"dest_vec1 ` {a<..<b} = {dest_vec1 a<..<dest_vec1 b}"
apply(rule_tac [!] equalityI)
unfolding subset_eq Ball_def Bex_def mem_interval_1 image_iff
apply(rule_tac [!] allI)apply(rule_tac [!] impI)
apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI)
apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI)
by (auto simp add: vector_less_def vector_le_def)
lemma dest_vec1_setsum: assumes "finite S"
shows " dest_vec1 (setsum f S) = setsum (\<lambda>x. dest_vec1 (f x)) S"
using dest_vec1_sum[OF assms] by auto
lemma open_dest_vec1_vimage: "open S \<Longrightarrow> open (dest_vec1 -` S)"
unfolding open_vector_def forall_1 by auto
lemma tendsto_dest_vec1 [tendsto_intros]:
"(f ---> l) net \<Longrightarrow> ((\<lambda>x. dest_vec1 (f x)) ---> dest_vec1 l) net"
by(rule tendsto_Cart_nth)
lemma continuous_dest_vec1: "continuous net f \<Longrightarrow> continuous net (\<lambda>x. dest_vec1 (f x))"
unfolding continuous_def by (rule tendsto_dest_vec1)
lemma forall_dest_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P(dest_vec1 x))"
apply safe defer apply(erule_tac x="vec1 x" in allE) by auto
lemma forall_of_dest_vec1: "(\<forall>v. P (\<lambda>x. dest_vec1 (v x))) \<longleftrightarrow> (\<forall>x. P x)"
apply rule apply rule apply(erule_tac x="(vec1 \<circ> x)" in allE) unfolding o_def vec1_dest_vec1 by auto
lemma forall_of_dest_vec1': "(\<forall>v. P (dest_vec1 v)) \<longleftrightarrow> (\<forall>x. P x)"
apply rule apply rule apply(erule_tac x="(vec1 x)" in allE) defer apply rule
apply(erule_tac x="dest_vec1 v" in allE) unfolding o_def vec1_dest_vec1 by auto
lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding dist_norm by auto
lemma bounded_linear_vec1_dest_vec1: fixes f::"real \<Rightarrow> real"
shows "linear (vec1 \<circ> f \<circ> dest_vec1) = bounded_linear f" (is "?l = ?r") proof-
{ assume ?l guess K using linear_bounded[OF `?l`] ..
hence "\<exists>K. \<forall>x. \<bar>f x\<bar> \<le> \<bar>x\<bar> * K" apply(rule_tac x=K in exI)
unfolding vec1_dest_vec1_simps by (auto simp add:field_simps) }
thus ?thesis unfolding linear_def bounded_linear_def additive_def bounded_linear_axioms_def o_def
unfolding vec1_dest_vec1_simps by auto qed
lemma vec1_le[simp]:fixes a::real shows "vec1 a \<le> vec1 b \<longleftrightarrow> a \<le> b"
unfolding vector_le_def by auto
lemma vec1_less[simp]:fixes a::real shows "vec1 a < vec1 b \<longleftrightarrow> a < b"
unfolding vector_less_def by auto
end