(* Title: HOL/Real_Vector_Spaces.thy Author: Brian Huffman Author: Johannes Hölzl
*)
section \<open>Vector Spaces and Algebras over the Reals\<close>
theory Real_Vector_Spaces imports Real Topological_Spaces Vector_Spaces begin
subsection \<open>Real vector spaces\<close>
class scaleR = fixes scaleR :: "real \ 'a \ 'a" (infixr \*\<^sub>R\ 75) begin
abbreviation divideR :: "'a \ real \ 'a" (infixl \'/\<^sub>R\ 70) where"x /\<^sub>R r \ inverse r *\<^sub>R x"
end
class real_vector = scaleR + ab_group_add + assumes scaleR_add_right: "a *\<^sub>R (x + y) = a *\<^sub>R x + a *\<^sub>R y" and scaleR_add_left: "(a + b) *\<^sub>R x = a *\<^sub>R x + b *\<^sub>R x" and scaleR_scaleR: "a *\<^sub>R b *\<^sub>R x = (a * b) *\<^sub>R x" and scaleR_one: "1 *\<^sub>R x = x"
class real_algebra = real_vector + ring + assumes mult_scaleR_left [simp]: "a *\<^sub>R x * y = a *\<^sub>R (x * y)" and mult_scaleR_right [simp]: "x * a *\<^sub>R y = a *\<^sub>R (x * y)"
class real_algebra_1 = real_algebra + ring_1
class real_div_algebra = real_algebra_1 + division_ring
class real_field = real_div_algebra + field
instantiation real :: real_field begin
definition real_scaleR_def [simp]: "scaleR a x = a * x"
instance by standard (simp_all add: algebra_simps)
end
locale linear = Vector_Spaces.linear "scaleR::_\_\'a::real_vector" "scaleR::_\_\'b::real_vector" begin
lemmas scaleR = scale
end
global_interpretation real_vector?: vector_space "scaleR :: real \ 'a \ 'a :: real_vector"
rewrites "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear" and"Vector_Spaces.linear (*) (*\<^sub>R) = linear" defines dependent_raw_def: dependent = real_vector.dependent and representation_raw_def: representation = real_vector.representation and subspace_raw_def: subspace = real_vector.subspace and span_raw_def: span = real_vector.span and extend_basis_raw_def: extend_basis = real_vector.extend_basis and dim_raw_def: dim = real_vector.dim proof unfold_locales show"Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear" "Vector_Spaces.linear (*) (*\<^sub>R) = linear" by (force simp: linear_def real_scaleR_def[abs_def])+ qed (use scaleR_add_right scaleR_add_left scaleR_scaleR scaleR_one in auto)
lemma [field_simps]: "c \ 0 \ a = b /\<^sub>R c \ c *\<^sub>R a = b" "c \ 0 \ b /\<^sub>R c = a \ b = c *\<^sub>R a" "c \ 0 \ a + b /\<^sub>R c = (c *\<^sub>R a + b) /\<^sub>R c" "c \ 0 \ a /\<^sub>R c + b = (a + c *\<^sub>R b) /\<^sub>R c" "c \ 0 \ a - b /\<^sub>R c = (c *\<^sub>R a - b) /\<^sub>R c" "c \ 0 \ a /\<^sub>R c - b = (a - c *\<^sub>R b) /\<^sub>R c" "c \ 0 \ - (a /\<^sub>R c) + b = (- a + c *\<^sub>R b) /\<^sub>R c" "c \ 0 \ - (a /\<^sub>R c) - b = (- a - c *\<^sub>R b) /\<^sub>R c" for a b :: "'a :: real_vector" by (auto simp add: scaleR_add_right scaleR_add_left scaleR_diff_right scaleR_diff_left)
lemmas linear_injective_0 = linear_inj_iff_eq_0 and linear_injective_on_subspace_0 = linear_inj_on_iff_eq_0 and linear_cmul = linear_scale and linear_scaleR = linear_scale_self and subspace_mul = subspace_scale and span_linear_image = linear_span_image and span_0 = span_zero and span_mul = span_scale and injective_scaleR = injective_scale
lemma scaleR_minus1_left [simp]: "scaleR (-1) x = - x" for x :: "'a::real_vector" by simp
lemma scaleR_2: fixes x :: "'a::real_vector" shows"scaleR 2 x = x + x" unfolding one_add_one [symmetric] scaleR_left_distrib by simp
lemma scaleR_half_double [simp]: fixes a :: "'a::real_vector" shows"(1 / 2) *\<^sub>R (a + a) = a" proof - have"\r. r *\<^sub>R (a + a) = (r * 2) *\<^sub>R a" by (metis scaleR_2 scaleR_scaleR) thenshow ?thesis by simp qed
lemma shift_zero_ident [simp]: fixes f :: "'a \ 'b::real_vector" shows"(+)0 \ f = f" by force
lemma linear_scale_real: fixes r::real shows"linear f \ f (r * b) = r * f b" using linear_scale by fastforce
interpretation scaleR_left: additive "(\a. scaleR a x :: 'a::real_vector)" by standard (rule scaleR_left_distrib)
interpretation scaleR_right: additive "(\x. scaleR a x :: 'a::real_vector)" by standard (rule scaleR_right_distrib)
lemma nonzero_inverse_scaleR_distrib: "a \ 0 \ x \ 0 \ inverse (scaleR a x) = scaleR (inverse a) (inverse x)" for x :: "'a::real_div_algebra" by (rule inverse_unique) simp
lemma inverse_scaleR_distrib: "inverse (scaleR a x) = scaleR (inverse a) (inverse x)" for x :: "'a::{real_div_algebra,division_ring}" by (metis inverse_zero nonzero_inverse_scaleR_distrib scale_eq_0_iff)
named_theorems vector_add_divide_simps "to simplify sums of scaled vectors"
lemma [vector_add_divide_simps]: "v + (b / z) *\<^sub>R w = (if z = 0 then v else (z *\<^sub>R v + b *\<^sub>R w) /\<^sub>R z)" "a *\<^sub>R v + (b / z) *\<^sub>R w = (if z = 0 then a *\<^sub>R v else ((a * z) *\<^sub>R v + b *\<^sub>R w) /\<^sub>R z)" "(a / z) *\<^sub>R v + w = (if z = 0 then w else (a *\<^sub>R v + z *\<^sub>R w) /\<^sub>R z)" "(a / z) *\<^sub>R v + b *\<^sub>R w = (if z = 0 then b *\<^sub>R w else (a *\<^sub>R v + (b * z) *\<^sub>R w) /\<^sub>R z)" "v - (b / z) *\<^sub>R w = (if z = 0 then v else (z *\<^sub>R v - b *\<^sub>R w) /\<^sub>R z)" "a *\<^sub>R v - (b / z) *\<^sub>R w = (if z = 0 then a *\<^sub>R v else ((a * z) *\<^sub>R v - b *\<^sub>R w) /\<^sub>R z)" "(a / z) *\<^sub>R v - w = (if z = 0 then -w else (a *\<^sub>R v - z *\<^sub>R w) /\<^sub>R z)" "(a / z) *\<^sub>R v - b *\<^sub>R w = (if z = 0 then -b *\<^sub>R w else (a *\<^sub>R v - (b * z) *\<^sub>R w) /\<^sub>R z)" for v :: "'a :: real_vector" by (simp_all add: divide_inverse_commute scaleR_add_right scaleR_diff_right)
lemma eq_vector_fraction_iff [vector_add_divide_simps]: fixes x :: "'a :: real_vector" shows"(x = (u / v) *\<^sub>R a) \ (if v=0 then x = 0 else v *\<^sub>R x = u *\<^sub>R a)" by auto (metis (no_types) divide_eq_1_iff divide_inverse_commute scaleR_one scaleR_scaleR)
lemma vector_fraction_eq_iff [vector_add_divide_simps]: fixes x :: "'a :: real_vector" shows"((u / v) *\<^sub>R a = x) \ (if v=0 then x = 0 else u *\<^sub>R a = v *\<^sub>R x)" by (metis eq_vector_fraction_iff)
lemma real_vector_affinity_eq: fixes x :: "'a :: real_vector" assumes m0: "m \ 0" shows"m *\<^sub>R x + c = y \ x = inverse m *\<^sub>R y - (inverse m *\<^sub>R c)"
(is"?lhs \ ?rhs") proof assume ?lhs thenhave"m *\<^sub>R x = y - c" by (simp add: field_simps) thenhave"inverse m *\<^sub>R (m *\<^sub>R x) = inverse m *\<^sub>R (y - c)" by simp thenshow"x = inverse m *\<^sub>R y - (inverse m *\<^sub>R c)" using m0 by (simp add: scaleR_diff_right) next assume ?rhs with m0 show"m *\<^sub>R x + c = y" by (simp add: scaleR_diff_right) qed
lemma real_vector_eq_affinity: "m \ 0 \ y = m *\<^sub>R x + c \ inverse m *\<^sub>R y - (inverse m *\<^sub>R c) = x" for x :: "'a::real_vector" using real_vector_affinity_eq[where m=m and x=x and y=y and c=c] by metis
lemma scaleR_eq_iff [simp]: "b + u *\<^sub>R a = a + u *\<^sub>R b \ a = b \ u = 1" for a :: "'a::real_vector" proof (cases "u = 1") case True thenshow ?thesis by auto next case False have"a = b"if"b + u *\<^sub>R a = a + u *\<^sub>R b" proof - from that have"(u - 1) *\<^sub>R a = (u - 1) *\<^sub>R b" by (simp add: algebra_simps) with False show ?thesis by auto qed thenshow ?thesis by auto qed
lemma scaleR_collapse [simp]: "(1 - u) *\<^sub>R a + u *\<^sub>R a = a" for a :: "'a::real_vector" by (simp add: algebra_simps)
subsection \<open>Embedding of the Reals into any \<open>real_algebra_1\<close>: \<open>of_real\<close>\<close>
definition of_real :: "real \ 'a::real_algebra_1" where"of_real r = scaleR r 1"
lemma scaleR_conv_of_real: "scaleR r x = of_real r * x" by (simp add: of_real_def)
lemma of_real_diff [simp]: "of_real (x - y) = of_real x - of_real y" by (simp add: of_real_def scaleR_left_diff_distrib)
lemma of_real_mult [simp]: "of_real (x * y) = of_real x * of_real y" by (simp add: of_real_def)
lemma of_real_sum[simp]: "of_real (sum f s) = (\x\s. of_real (f x))" by (induct s rule: infinite_finite_induct) auto
lemma of_real_prod[simp]: "of_real (prod f s) = (\x\s. of_real (f x))" by (induct s rule: infinite_finite_induct) auto
lemma sum_list_of_real: "sum_list (map of_real xs) = of_real (sum_list xs)" by (induction xs) auto
lemma nonzero_of_real_inverse: "x \ 0 \ of_real (inverse x) = inverse (of_real x :: 'a::real_div_algebra)" by (simp add: of_real_def nonzero_inverse_scaleR_distrib)
lemma of_real_inverse [simp]: "of_real (inverse x) = inverse (of_real x :: 'a::{real_div_algebra,division_ring})" by (simp add: of_real_def inverse_scaleR_distrib)
lemma nonzero_of_real_divide: "y \ 0 \ of_real (x / y) = (of_real x / of_real y :: 'a::real_field)" by (simp add: divide_inverse nonzero_of_real_inverse)
lemma of_real_divide [simp]: "of_real (x / y) = (of_real x / of_real y :: 'a::real_div_algebra)" by (simp add: divide_inverse)
lemma of_real_power [simp]: "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1}) ^ n" by (induct n) simp_all
lemma of_real_power_int [simp]: "of_real (power_int x n) = power_int (of_real x :: 'a :: {real_div_algebra,division_ring}) n" by (auto simp: power_int_def)
lemma of_real_eq_iff [simp]: "of_real x = of_real y \ x = y" by (simp add: of_real_def)
lemma inj_of_real: "inj of_real" by (auto intro: injI)
lemma minus_of_real_eq_of_real_iff [simp]: "-of_real x = of_real y \ -x = y" using of_real_eq_iff[of "-x" y] by (simp only: of_real_minus)
lemma of_real_eq_minus_of_real_iff [simp]: "of_real x = -of_real y \ x = -y" using of_real_eq_iff[of x "-y"] by (simp only: of_real_minus)
lemma of_real_eq_id [simp]: "of_real = (id :: real \ real)" by (rule ext) (simp add: of_real_def)
text\<open>Collapse nested embeddings.\<close> lemma of_real_of_nat_eq [simp]: "of_real (of_nat n) = of_nat n" by (induct n) auto
lemma of_real_of_int_eq [simp]: "of_real (of_int z) = of_int z" by (cases z rule: int_diff_cases) simp
lemma of_real_numeral [simp]: "of_real (numeral w) = numeral w" using of_real_of_int_eq [of "numeral w"] by simp
lemma of_real_neg_numeral [simp]: "of_real (- numeral w) = - numeral w" using of_real_of_int_eq [of "- numeral w"] by simp
lemma numeral_power_int_eq_of_real_cancel_iff [simp]: "power_int (numeral x) n = (of_real y :: 'a :: {real_div_algebra, division_ring}) \
power_int (numeral x) n = y" proof - have"power_int (numeral x) n = (of_real (power_int (numeral x) n) :: 'a)" by simp alsohave"\ = of_real y \ power_int (numeral x) n = y" by (subst of_real_eq_iff) auto finallyshow ?thesis . qed
lemma of_real_eq_numeral_power_int_cancel_iff [simp]: "(of_real y :: 'a :: {real_div_algebra, division_ring}) = power_int (numeral x) n \
y = power_int (numeral x) n" by (subst (1 2) eq_commute) simp
lemma of_real_eq_of_real_power_int_cancel_iff [simp]: "power_int (of_real b :: 'a :: {real_div_algebra, division_ring}) w = of_real x \
power_int b w = x" by (metis of_real_power_int of_real_eq_iff)
lemma of_real_in_Ints_iff [simp]: "of_real x \ \ \ x \ \" proof safe fix x assume"(of_real x :: 'a) \ \" thenobtain n where"(of_real x :: 'a) = of_int n" by (auto simp: Ints_def) alsohave"of_int n = of_real (real_of_int n)" by simp finallyhave"x = real_of_int n" by (subst (asm) of_real_eq_iff) thus"x \ \" by auto qed (auto simp: Ints_def)
lemma Ints_of_real [intro]: "x \ \ \ of_real x \ \" by simp
text\<open>Every real algebra has characteristic zero.\<close> instance real_algebra_1 < ring_char_0 proof from inj_of_real inj_of_nat have"inj (of_real \ of_nat)" by (rule inj_compose) thenshow"inj (of_nat :: nat \ 'a)" by (simp add: comp_def) qed
lemma fraction_scaleR_times [simp]: fixes a :: "'a::real_algebra_1" shows"(numeral u / numeral v) *\<^sub>R (numeral w * a) = (numeral u * numeral w / numeral v) *\<^sub>R a" by (metis (no_types, lifting) of_real_numeral scaleR_conv_of_real scaleR_scaleR times_divide_eq_left)
lemma inverse_scaleR_times [simp]: fixes a :: "'a::real_algebra_1" shows"(1 / numeral v) *\<^sub>R (numeral w * a) = (numeral w / numeral v) *\<^sub>R a" by (metis divide_inverse_commute inverse_eq_divide of_real_numeral scaleR_conv_of_real scaleR_scaleR)
lemma scaleR_times [simp]: fixes a :: "'a::real_algebra_1" shows"(numeral u) *\<^sub>R (numeral w * a) = (numeral u * numeral w) *\<^sub>R a" by (simp add: scaleR_conv_of_real)
instance real_field < field_char_0 ..
subsection \<open>The Set of Real Numbers\<close>
definition Reals :: "'a::real_algebra_1 set" (\<open>\<real>\<close>) where"\ = range of_real"
lemma Reals_of_real [simp]: "of_real r \ \" by (simp add: Reals_def)
lemma Reals_of_int [simp]: "of_int z \ \" by (subst of_real_of_int_eq [symmetric], rule Reals_of_real)
lemma Reals_of_nat [simp]: "of_nat n \ \" by (subst of_real_of_nat_eq [symmetric], rule Reals_of_real)
lemma Reals_numeral [simp]: "numeral w \ \" by (subst of_real_numeral [symmetric], rule Reals_of_real)
lemma Reals_0 [simp]: "0 \ \" and Reals_1 [simp]: "1 \ \" by (simp_all add: Reals_def)
lemma Reals_add [simp]: "a \ \ \ b \ \ \ a + b \ \" by (metis (no_types, opaque_lifting) Reals_def Reals_of_real imageE of_real_add)
lemma Reals_minus [simp]: "a \ \ \ - a \ \" by (auto simp: Reals_def)
lemma Reals_minus_iff [simp]: "- a \ \ \ a \ \" using Reals_minus by fastforce
lemma Reals_diff [simp]: "a \ \ \ b \ \ \ a - b \ \" by (metis Reals_add Reals_minus_iff add_uminus_conv_diff)
lemma Reals_mult [simp]: "a \ \ \ b \ \ \ a * b \ \" by (metis (no_types, lifting) Reals_def Reals_of_real imageE of_real_mult)
lemma nonzero_Reals_inverse: "a \ \ \ a \ 0 \ inverse a \ \" for a :: "'a::real_div_algebra" by (metis Reals_def Reals_of_real imageE of_real_inverse)
lemma Reals_inverse: "a \ \ \ inverse a \ \" for a :: "'a::{real_div_algebra,division_ring}" using nonzero_Reals_inverse by fastforce
lemma Reals_inverse_iff [simp]: "inverse x \ \ \ x \ \" for x :: "'a::{real_div_algebra,division_ring}" by (metis Reals_inverse inverse_inverse_eq)
lemma nonzero_Reals_divide: "a \ \ \ b \ \ \ b \ 0 \ a / b \ \" for a b :: "'a::real_field" by (simp add: divide_inverse)
lemma Reals_divide [simp]: "a \ \ \ b \ \ \ a / b \ \" for a b :: "'a::{real_field,field}" using nonzero_Reals_divide by fastforce
lemma Reals_power [simp]: "a \ \ \ a ^ n \ \" for a :: "'a::real_algebra_1" by (metis Reals_def Reals_of_real imageE of_real_power)
lemma Reals_cases [cases set: Reals]: assumes"q \ \" obtains (of_real) r where"q = of_real r" unfolding Reals_def proof - from\<open>q \<in> \<real>\<close> have "q \<in> range of_real" unfolding Reals_def . thenobtain r where"q = of_real r" .. thenshow thesis .. qed
lemma sum_in_Reals [intro,simp]: "(\i. i \ s \ f i \ \) \ sum f s \ \" proof (induct s rule: infinite_finite_induct) case infinite thenshow ?caseby (metis Reals_0 sum.infinite) qed simp_all
lemma prod_in_Reals [intro,simp]: "(\i. i \ s \ f i \ \) \ prod f s \ \" proof (induct s rule: infinite_finite_induct) case infinite thenshow ?caseby (metis Reals_1 prod.infinite) qed simp_all
lemma Reals_induct [case_names of_real, induct set: Reals]: "q \ \ \ (\r. P (of_real r)) \ P q" by (rule Reals_cases) auto
subsection \<open>Ordered real vector spaces\<close>
class ordered_real_vector = real_vector + ordered_ab_group_add + assumes scaleR_left_mono: "x \ y \ 0 \ a \ a *\<^sub>R x \ a *\<^sub>R y" and scaleR_right_mono: "a \ b \ 0 \ x \ a *\<^sub>R x \ b *\<^sub>R x" begin
lemma scaleR_mono: "a \ b \ x \ y \ 0 \ b \ 0 \ x \ a *\<^sub>R x \ b *\<^sub>R y" by (meson order_trans scaleR_left_mono scaleR_right_mono)
lemma scaleR_mono': "a \ b \ c \ d \ 0 \ a \ 0 \ c \ a *\<^sub>R c \ b *\<^sub>R d" by (rule scaleR_mono) (auto intro: order.trans)
lemma pos_le_divideR_eq [field_simps]: "a \ b /\<^sub>R c \ c *\<^sub>R a \ b" (is "?P \ ?Q") if "0 < c" proof assume ?P with scaleR_left_mono that have"c *\<^sub>R a \ c *\<^sub>R (b /\<^sub>R c)" by simp with that show ?Q by (simp add: scaleR_one scaleR_scaleR inverse_eq_divide) next assume ?Q with scaleR_left_mono that have"c *\<^sub>R a /\<^sub>R c \ b /\<^sub>R c" by simp with that show ?P by (simp add: scaleR_one scaleR_scaleR inverse_eq_divide) qed
lemma pos_less_divideR_eq [field_simps]: "a < b /\<^sub>R c \ c *\<^sub>R a < b" if "c > 0" using that pos_le_divideR_eq [of c a b] by (auto simp add: le_less scaleR_scaleR scaleR_one)
lemma pos_divideR_le_eq [field_simps]: "b /\<^sub>R c \ a \ b \ c *\<^sub>R a" if "c > 0" using that pos_le_divideR_eq [of "inverse c" b a] by simp
lemma pos_divideR_less_eq [field_simps]: "b /\<^sub>R c < a \ b < c *\<^sub>R a" if "c > 0" using that pos_less_divideR_eq [of "inverse c" b a] by simp
lemma pos_le_minus_divideR_eq [field_simps]: "a \ - (b /\<^sub>R c) \ c *\<^sub>R a \ - b" if "c > 0" using that by (metis add_minus_cancel diff_0 left_minus minus_minus neg_le_iff_le
scaleR_add_right uminus_add_conv_diff pos_le_divideR_eq)
lemma pos_less_minus_divideR_eq [field_simps]: "a < - (b /\<^sub>R c) \ c *\<^sub>R a < - b" if "c > 0" using that by (metis le_less less_le_not_le pos_divideR_le_eq
pos_divideR_less_eq pos_le_minus_divideR_eq)
lemma pos_minus_divideR_le_eq [field_simps]: "- (b /\<^sub>R c) \ a \ - b \ c *\<^sub>R a" if "c > 0" using that by (metis pos_divideR_le_eq pos_le_minus_divideR_eq that
inverse_positive_iff_positive le_imp_neg_le minus_minus)
lemma pos_minus_divideR_less_eq [field_simps]: "- (b /\<^sub>R c) < a \ - b < c *\<^sub>R a" if "c > 0" using that by (simp add: less_le_not_le pos_le_minus_divideR_eq pos_minus_divideR_le_eq)
lemma neg_le_divideR_eq [field_simps]: "a \ b /\<^sub>R c \ b \ c *\<^sub>R a" (is "?P \ ?Q") if "c < 0" for a b :: "'a :: ordered_real_vector" using that pos_le_divideR_eq [of "- c" a "- b"] by simp
lemma neg_less_divideR_eq [field_simps]: "a < b /\<^sub>R c \ b < c *\<^sub>R a" if "c < 0" for a b :: "'a :: ordered_real_vector" using that neg_le_divideR_eq [of c a b] by (auto simp add: le_less)
lemma neg_divideR_le_eq [field_simps]: "b /\<^sub>R c \ a \ c *\<^sub>R a \ b" if "c < 0" for a b :: "'a :: ordered_real_vector" using that pos_divideR_le_eq [of "- c""- b" a] by simp
lemma neg_divideR_less_eq [field_simps]: "b /\<^sub>R c < a \ c *\<^sub>R a < b" if "c < 0" for a b :: "'a :: ordered_real_vector" using that neg_divideR_le_eq [of c b a] by (auto simp add: le_less)
lemma neg_le_minus_divideR_eq [field_simps]: "a \ - (b /\<^sub>R c) \ - b \ c *\<^sub>R a" if "c < 0" for a b :: "'a :: ordered_real_vector" using that pos_le_minus_divideR_eq [of "- c" a "- b"] by (simp add: minus_le_iff)
lemma neg_less_minus_divideR_eq [field_simps]: "a < - (b /\<^sub>R c) \ - b < c *\<^sub>R a" if "c < 0" for a b :: "'a :: ordered_real_vector" proof - have *: "- b = c *\<^sub>R a \ b = - (c *\<^sub>R a)" by (metis add.inverse_inverse) from that neg_le_minus_divideR_eq [of c a b] show ?thesis by (auto simp add: le_less *) qed
lemma neg_minus_divideR_le_eq [field_simps]: "- (b /\<^sub>R c) \ a \ c *\<^sub>R a \ - b" if "c < 0" for a b :: "'a :: ordered_real_vector" using that pos_minus_divideR_le_eq [of "- c""- b" a] by (simp add: le_minus_iff)
lemma neg_minus_divideR_less_eq [field_simps]: "- (b /\<^sub>R c) < a \ c *\<^sub>R a < - b" if "c < 0" for a b :: "'a :: ordered_real_vector" using that by (simp add: less_le_not_le neg_le_minus_divideR_eq neg_minus_divideR_le_eq)
lemma [field_split_simps]: "a = b /\<^sub>R c \ (if c = 0 then a = 0 else c *\<^sub>R a = b)" "b /\<^sub>R c = a \ (if c = 0 then a = 0 else b = c *\<^sub>R a)" "a + b /\<^sub>R c = (if c = 0 then a else (c *\<^sub>R a + b) /\<^sub>R c)" "a /\<^sub>R c + b = (if c = 0 then b else (a + c *\<^sub>R b) /\<^sub>R c)" "a - b /\<^sub>R c = (if c = 0 then a else (c *\<^sub>R a - b) /\<^sub>R c)" "a /\<^sub>R c - b = (if c = 0 then - b else (a - c *\<^sub>R b) /\<^sub>R c)" "- (a /\<^sub>R c) + b = (if c = 0 then b else (- a + c *\<^sub>R b) /\<^sub>R c)" "- (a /\<^sub>R c) - b = (if c = 0 then - b else (- a - c *\<^sub>R b) /\<^sub>R c)" for a b :: "'a :: real_vector" by (auto simp add: field_simps)
lemma [field_split_simps]: "0 < c \ a \ b /\<^sub>R c \ (if c > 0 then c *\<^sub>R a \ b else if c < 0 then b \ c *\<^sub>R a else a \ 0)" "0 < c \ a < b /\<^sub>R c \ (if c > 0 then c *\<^sub>R a < b else if c < 0 then b < c *\<^sub>R a else a < 0)" "0 < c \ b /\<^sub>R c \ a \ (if c > 0 then b \ c *\<^sub>R a else if c < 0 then c *\<^sub>R a \ b else a \ 0)" "0 < c \ b /\<^sub>R c < a \ (if c > 0 then b < c *\<^sub>R a else if c < 0 then c *\<^sub>R a < b else a > 0)" "0 < c \ a \ - (b /\<^sub>R c) \ (if c > 0 then c *\<^sub>R a \ - b else if c < 0 then - b \ c *\<^sub>R a else a \ 0)" "0 < c \ a < - (b /\<^sub>R c) \ (if c > 0 then c *\<^sub>R a < - b else if c < 0 then - b < c *\<^sub>R a else a < 0)" "0 < c \ - (b /\<^sub>R c) \ a \ (if c > 0 then - b \ c *\<^sub>R a else if c < 0 then c *\<^sub>R a \ - b else a \0)" "0 < c \ - (b /\<^sub>R c) < a \ (if c > 0 then - b < c *\<^sub>R a else if c < 0 then c *\<^sub>R a < - b else a > 0)" for a b :: "'a :: ordered_real_vector" by (clarsimp intro!: field_simps)+
lemma scaleR_nonneg_nonneg: "0 \ a \ 0 \ x \ 0 \ a *\<^sub>R x" for x :: "'a::ordered_real_vector" using scaleR_left_mono [of 0 x a] by simp
lemma scaleR_nonneg_nonpos: "0 \ a \ x \ 0 \ a *\<^sub>R x \ 0" for x :: "'a::ordered_real_vector" using scaleR_left_mono [of x 0 a] by simp
lemma scaleR_nonpos_nonneg: "a \ 0 \ 0 \ x \ a *\<^sub>R x \ 0" for x :: "'a::ordered_real_vector" using scaleR_right_mono [of a 0 x] by simp
lemma split_scaleR_neg_le: "(0 \ a \ x \ 0) \ (a \ 0 \ 0 \ x) \ a *\<^sub>R x \ 0" for x :: "'a::ordered_real_vector" by (auto simp: scaleR_nonneg_nonpos scaleR_nonpos_nonneg)
lemma le_add_iff1: "a *\<^sub>R e + c \ b *\<^sub>R e + d \ (a - b) *\<^sub>R e + c \ d" for c d e :: "'a::ordered_real_vector" by (simp add: algebra_simps)
lemma le_add_iff2: "a *\<^sub>R e + c \ b *\<^sub>R e + d \ c \ (b - a) *\<^sub>R e + d" for c d e :: "'a::ordered_real_vector" by (simp add: algebra_simps)
lemma scaleR_left_mono_neg: "b \ a \ c \ 0 \ c *\<^sub>R a \ c *\<^sub>R b" for a b :: "'a::ordered_real_vector" by (drule scaleR_left_mono [of _ _ "- c"], simp_all)
lemma scaleR_right_mono_neg: "b \ a \ c \ 0 \ a *\<^sub>R c \ b *\<^sub>R c" for c :: "'a::ordered_real_vector" by (drule scaleR_right_mono [of _ _ "- c"], simp_all)
lemma scaleR_nonpos_nonpos: "a \ 0 \ b \ 0 \ 0 \ a *\<^sub>R b" for b :: "'a::ordered_real_vector" using scaleR_right_mono_neg [of a 0 b] by simp
lemma split_scaleR_pos_le: "(0 \ a \ 0 \ b) \ (a \ 0 \ b \ 0) \ 0 \ a *\<^sub>R b" for b :: "'a::ordered_real_vector" by (auto simp: scaleR_nonneg_nonneg scaleR_nonpos_nonpos)
lemma zero_le_scaleR_iff: fixes b :: "'a::ordered_real_vector" shows"0 \ a *\<^sub>R b \ 0 < a \ 0 \ b \ a < 0 \ b \ 0 \ a = 0"
(is"?lhs = ?rhs") proof (cases "a = 0") case True thenshow ?thesis by simp next case False show ?thesis proof assume ?lhs from\<open>a \<noteq> 0\<close> consider "a > 0" | "a < 0" by arith thenshow ?rhs proof cases case 1 with\<open>?lhs\<close> have "inverse a *\<^sub>R 0 \<le> inverse a *\<^sub>R (a *\<^sub>R b)" by (intro scaleR_mono) auto with 1 show ?thesis by simp next case 2 with\<open>?lhs\<close> have "- inverse a *\<^sub>R 0 \<le> - inverse a *\<^sub>R (a *\<^sub>R b)" by (intro scaleR_mono) auto with 2 show ?thesis by simp qed next assume ?rhs thenshow ?lhs by (auto simp: not_le \<open>a \<noteq> 0\<close> intro!: split_scaleR_pos_le) qed qed
lemma scaleR_le_0_iff: "a *\<^sub>R b \ 0 \ 0 < a \ b \ 0 \ a < 0 \ 0 \ b \ a = 0" for b::"'a::ordered_real_vector" by (insert zero_le_scaleR_iff [of "-a" b]) force
lemma scaleR_le_cancel_left: "c *\<^sub>R a \ c *\<^sub>R b \ (0 < c \ a \ b) \ (c < 0 \ b \ a)" for b :: "'a::ordered_real_vector" by (auto simp: neq_iff scaleR_left_mono scaleR_left_mono_neg
dest: scaleR_left_mono[where a="inverse c"] scaleR_left_mono_neg[where c="inverse c"])
lemma scaleR_le_cancel_left_pos: "0 < c \ c *\<^sub>R a \ c *\<^sub>R b \ a \ b" for b :: "'a::ordered_real_vector" by (auto simp: scaleR_le_cancel_left)
lemma scaleR_le_cancel_left_neg: "c < 0 \ c *\<^sub>R a \ c *\<^sub>R b \ b \ a" for b :: "'a::ordered_real_vector" by (auto simp: scaleR_le_cancel_left)
lemma scaleR_left_le_one_le: "0 \ x \ a \ 1 \ a *\<^sub>R x \ x" for x :: "'a::ordered_real_vector"and a :: real using scaleR_right_mono[of a 1 x] by simp
class sgn_div_norm = scaleR + norm + sgn + assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x"
class dist_norm = dist + norm + minus + assumes dist_norm: "dist x y = norm (x - y)"
class uniformity_dist = dist + uniformity + assumes uniformity_dist: "uniformity = (INF e\{0 <..}. principal {(x, y). dist x y < e})" begin
lemma eventually_uniformity_metric: "eventually P uniformity \ (\e>0. \x y. dist x y < e \ P (x, y))" unfolding uniformity_dist by (subst eventually_INF_base)
(auto simp: eventually_principal subset_eq intro: bexI[of _ "min _ _"])
end
class real_normed_vector = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity + assumes norm_eq_zero [simp]: "norm x = 0 \ x = 0" and norm_triangle_ineq: "norm (x + y) \ norm x + norm y" and norm_scaleR [simp]: "norm (scaleR a x) = \a\ * norm x" begin
lemma norm_ge_zero [simp]: "0 \ norm x" proof - have"0 = norm (x + -1 *\<^sub>R x)" using scaleR_add_left[of 1 "-1" x] norm_scaleR[of 0 x] by (simp add: scaleR_one) alsohave"\ \ norm x + norm (-1 *\<^sub>R x)" by (rule norm_triangle_ineq) finallyshow ?thesis by simp qed
lemma bdd_below_norm_image: "bdd_below (norm ` A)" by (meson bdd_belowI2 norm_ge_zero)
end
class real_normed_algebra = real_algebra + real_normed_vector + assumes norm_mult_ineq: "norm (x * y) \ norm x * norm y"
lemma (in real_normed_algebra_1) scaleR_power [simp]: "(scaleR x y) ^ n = scaleR (x^n) (y^n)" by (induct n) (simp_all add: scaleR_one scaleR_scaleR mult_ac)
class real_normed_div_algebra = real_div_algebra + real_normed_vector + assumes norm_mult: "norm (x * y) = norm x * norm y"
lemma divideR_right: fixes x y :: "'a::real_normed_vector" shows"r \ 0 \ y = x /\<^sub>R r \ r *\<^sub>R y = x" by auto
class real_normed_field = real_field + real_normed_div_algebra
lemma dist_mult_left: "dist (a * b) (a * c :: 'a :: real_normed_field) = norm a * dist b c" unfolding dist_norm right_diff_distrib [symmetric] norm_mult by simp
lemma dist_mult_right: "dist (b * a) (c * a :: 'a :: real_normed_field) = norm a * dist b c" using dist_mult_left[of a b c] by (simp add: mult_ac)
instance real_normed_div_algebra < real_normed_algebra_1 proof show"norm (x * y) \ norm x * norm y" for x y :: 'a by (simp add: norm_mult) next have"norm (1 * 1::'a) = norm (1::'a) * norm (1::'a)" by (rule norm_mult) thenshow"norm (1::'a) = 1"by simp qed
context real_normed_vector begin
lemma norm_zero [simp]: "norm (0::'a) = 0" by simp
lemma zero_less_norm_iff [simp]: "norm x > 0 \ x \ 0" by (simp add: order_less_le)
lemma norm_not_less_zero [simp]: "\ norm x < 0" by (simp add: linorder_not_less)
lemma norm_le_zero_iff [simp]: "norm x \ 0 \ x = 0" by (simp add: order_le_less)
lemma norm_minus_cancel [simp]: "norm (- x) = norm x" proof - have"- 1 *\<^sub>R x = - (1 *\<^sub>R x)" unfolding add_eq_0_iff2[symmetric] scaleR_add_left[symmetric] using norm_eq_zero by fastforce thenhave"norm (- x) = norm (scaleR (- 1) x)" by (simp only: scaleR_one) alsohave"\ = \- 1\ * norm x" by (rule norm_scaleR) finallyshow ?thesis by simp qed
lemma norm_minus_commute: "norm (a - b) = norm (b - a)" proof - have"norm (- (b - a)) = norm (b - a)" by (rule norm_minus_cancel) thenshow ?thesis by simp qed
lemma dist_add_cancel [simp]: "dist (a + b) (a + c) = dist b c" by (simp add: dist_norm)
lemma dist_add_cancel2 [simp]: "dist (b + a) (c + a) = dist b c" by (simp add: dist_norm)
lemma norm_uminus_minus: "norm (- x - y) = norm (x + y)" by (subst (2) norm_minus_cancel[symmetric], subst minus_add_distrib) simp
lemma norm_triangle_ineq2: "norm a - norm b \ norm (a - b)" proof - have"norm (a - b + b) \ norm (a - b) + norm b" by (rule norm_triangle_ineq) thenshow ?thesis by simp qed
lemma norm_triangle_ineq3: "\norm a - norm b\ \ norm (a - b)" proof - have"norm a - norm b \ norm (a - b)" by (simp add: norm_triangle_ineq2) moreoverhave"norm b - norm a \ norm (a - b)" by (metis norm_minus_commute norm_triangle_ineq2) ultimatelyshow ?thesis by (simp add: abs_le_iff) qed
lemma norm_triangle_ineq4: "norm (a - b) \ norm a + norm b" proof - have"norm (a + - b) \ norm a + norm (- b)" by (rule norm_triangle_ineq) thenshow ?thesis by simp qed
lemma norm_triangle_le_diff: "norm x + norm y \ e \ norm (x - y) \ e" by (meson norm_triangle_ineq4 order_trans)
lemma norm_diff_ineq: "norm a - norm b \ norm (a + b)" proof - have"norm a - norm (- b) \ norm (a - - b)" by (rule norm_triangle_ineq2) thenshow ?thesis by simp qed
lemma norm_triangle_sub: "norm x \ norm y + norm (x - y)" using norm_triangle_ineq[of "y""x - y"] by (simp add: field_simps)
lemma norm_triangle_le: "norm x + norm y \ e \ norm (x + y) \ e" by (rule norm_triangle_ineq [THEN order_trans])
lemma norm_triangle_lt: "norm x + norm y < e \ norm (x + y) < e" by (rule norm_triangle_ineq [THEN le_less_trans])
lemma norm_add_leD: "norm (a + b) \ c \ norm b \ norm a + c" by (metis ab_semigroup_add_class.add.commute add_commute diff_le_eq norm_diff_ineq order_trans)
lemma norm_diff_triangle_ineq: "norm ((a + b) - (c + d)) \ norm (a - c) + norm (b - d)" proof - have"norm ((a + b) - (c + d)) = norm ((a - c) + (b - d))" by (simp add: algebra_simps) alsohave"\ \ norm (a - c) + norm (b - d)" by (rule norm_triangle_ineq) finallyshow ?thesis . qed
lemma norm_diff_triangle_le: "norm (x - z) \ e1 + e2" if"norm (x - y) \ e1" "norm (y - z) \ e2" proof - have"norm (x - (y + z - y)) \ norm (x - y) + norm (y - z)" using norm_diff_triangle_ineq that diff_diff_eq2 by presburger with that show ?thesis by simp qed
lemma norm_diff_triangle_less: "norm (x - z) < e1 + e2" if"norm (x - y) < e1""norm (y - z) < e2" proof - have"norm (x - z) \ norm (x - y) + norm (y - z)" by (metis norm_diff_triangle_ineq add_diff_cancel_left' diff_diff_eq2) with that show ?thesis by auto qed
lemma norm_triangle_mono: "norm a \ r \ norm b \ s \ norm (a + b) \ r + s" by (metis (mono_tags) add_mono_thms_linordered_semiring(1) norm_triangle_ineq order.trans)
lemma norm_sum: "norm (sum f A) \ (\i\A. norm (f i))" for f::"'b \ 'a" by (induct A rule: infinite_finite_induct) (auto intro: norm_triangle_mono)
lemma sum_norm_le: "norm (sum f S) \ sum g S" if"\x. x \ S \ norm (f x) \ g x" for f::"'b \ 'a" by (rule order_trans [OF norm_sum sum_mono]) (simp add: that)
lemma sum_norm_bound: "norm (sum f S) \ of_nat (card S)*K" if"\x. x \ S \ norm (f x) \ K" for f :: "'b \ 'a" using sum_norm_le[OF that] sum_constant[symmetric] by simp
lemma norm_add_less: "norm x < r \ norm y < s \ norm (x + y) < r + s" by (rule order_le_less_trans [OF norm_triangle_ineq add_strict_mono])
end
lemma dist_sum_le: fixes f :: "'a \ 'b :: real_normed_vector" shows"dist (\x\A. f x) (\x\A. g x) \ (\x\A. dist (f x) (g x))" proof - have"dist (\x\A. f x) (\x\A. g x) = norm (\x\A. f x - g x)" by (simp add: dist_norm sum_subtractf) alsohave"\ \ (\x\A. norm (f x - g x))" by (rule norm_sum) finallyshow ?thesis by (simp add: dist_norm) qed
lemma dist_scaleR [simp]: "dist (x *\<^sub>R a) (y *\<^sub>R a) = \x - y\ * norm a" for a :: "'a::real_normed_vector" by (metis dist_norm norm_scaleR scaleR_left.diff)
lemma norm_mult_less: "norm x < r \ norm y < s \ norm (x * y) < r * s" for x y :: "'a::real_normed_algebra" by (rule order_le_less_trans [OF norm_mult_ineq]) (simp add: mult_strict_mono')
lemma norm_of_real [simp]: "norm (of_real r :: 'a::real_normed_algebra_1) = \r\" by (simp add: of_real_def)
lemma nonzero_norm_inverse: "a \ 0 \ norm (inverse a) = inverse (norm a)" for a :: "'a::real_normed_div_algebra" by (metis inverse_unique norm_mult norm_one right_inverse)
lemma norm_inverse: "norm (inverse a) = inverse (norm a)" for a :: "'a::{real_normed_div_algebra,division_ring}" by (metis inverse_zero nonzero_norm_inverse norm_zero)
lemma nonzero_norm_divide: "b \ 0 \ norm (a / b) = norm a / norm b" for a b :: "'a::real_normed_field" by (simp add: divide_inverse norm_mult nonzero_norm_inverse)
lemma norm_divide: "norm (a / b) = norm a / norm b" for a b :: "'a::{real_normed_field,field}" by (simp add: divide_inverse norm_mult norm_inverse)
lemma dist_divide_right: "dist (a/c) (b/c) = dist a b / norm c"for c :: "'a :: real_normed_field" by (metis diff_divide_distrib dist_norm norm_divide)
lemma norm_inverse_le_norm: fixes x :: "'a::real_normed_div_algebra" shows"r \ norm x \ 0 < r \ norm (inverse x) \ inverse r" by (simp add: le_imp_inverse_le norm_inverse)
lemma norm_power_ineq: "norm (x ^ n) \ norm x ^ n" for x :: "'a::real_normed_algebra_1" proof (induct n) case 0 show"norm (x ^ 0) \ norm x ^ 0" by simp next case (Suc n) have"norm (x * x ^ n) \ norm x * norm (x ^ n)" by (rule norm_mult_ineq) alsofrom Suc have"\ \ norm x * norm x ^ n" using norm_ge_zero by (rule mult_left_mono) finallyshow"norm (x ^ Suc n) \ norm x ^ Suc n" by simp qed
lemma norm_power: "norm (x ^ n) = norm x ^ n" for x :: "'a::real_normed_div_algebra" by (induct n) (simp_all add: norm_mult)
lemma norm_power_int: "norm (power_int x n) = power_int (norm x) n" for x :: "'a::real_normed_div_algebra" by (cases n rule: int_cases4) (auto simp: norm_power power_int_minus norm_inverse)
lemma power_eq_imp_eq_norm: fixes w :: "'a::real_normed_div_algebra" assumes eq: "w ^ n = z ^ n"and"n > 0" shows"norm w = norm z" proof - have"norm w ^ n = norm z ^ n" by (metis (no_types) eq norm_power) thenshow ?thesis using assms by (force intro: power_eq_imp_eq_base) qed
lemma power_eq_1_iff: fixes w :: "'a::real_normed_div_algebra" shows"w ^ n = 1 \ norm w = 1 \ n = 0" by (metis norm_one power_0_left power_eq_0_iff power_eq_imp_eq_norm power_one)
lemma norm_mult_numeral1 [simp]: "norm (numeral w * a) = numeral w * norm a" for a b :: "'a::{real_normed_field,field}" by (simp add: norm_mult)
lemma norm_mult_numeral2 [simp]: "norm (a * numeral w) = norm a * numeral w" for a b :: "'a::{real_normed_field,field}" by (simp add: norm_mult)
lemma norm_divide_numeral [simp]: "norm (a / numeral w) = norm a / numeral w" for a b :: "'a::{real_normed_field,field}" by (simp add: norm_divide)
lemma norm_of_real_diff [simp]: "norm (of_real b - of_real a :: 'a::real_normed_algebra_1) \ \b - a\" by (metis norm_of_real of_real_diff order_refl)
text\<open>Despite a superficial resemblance, \<open>norm_eq_1\<close> is not relevant.\<close> lemma square_norm_one: fixes x :: "'a::real_normed_div_algebra" assumes"x\<^sup>2 = 1" shows"norm x = 1" by (metis assms norm_minus_cancel norm_one power2_eq_1_iff)
lemma norm_less_p1: "norm x < norm (of_real (norm x) + 1 :: 'a)" for x :: "'a::real_normed_algebra_1" proof - have"norm x < norm (of_real (norm x + 1) :: 'a)" by (simp add: of_real_def) thenshow ?thesis by simp qed
lemma prod_norm: "prod (\x. norm (f x)) A = norm (prod f A)" for f :: "'a \ 'b::{comm_semiring_1,real_normed_div_algebra}" by (induct A rule: infinite_finite_induct) (auto simp: norm_mult)
lemma norm_prod_le: "norm (prod f A) \ (\a\A. norm (f a :: 'a :: {real_normed_algebra_1,comm_monoid_mult}))" proof (induct A rule: infinite_finite_induct) case empty thenshow ?caseby simp next case (insert a A) thenhave"norm (prod f (insert a A)) \ norm (f a) * norm (prod f A)" by (simp add: norm_mult_ineq) alsohave"norm (prod f A) \ (\a\A. norm (f a))" by (rule insert) finallyshow ?case by (simp add: insert mult_left_mono) next case infinite thenshow ?caseby simp qed
lemma norm_prod_diff: fixes z w :: "'i \ 'a::{real_normed_algebra_1, comm_monoid_mult}" shows"(\i. i \ I \ norm (z i) \ 1) \ (\i. i \ I \ norm (w i) \ 1) \
norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) \<le> (\<Sum>i\<in>I. norm (z i - w i))" proof (induction I rule: infinite_finite_induct) case empty thenshow ?caseby simp next case (insert i I) note insert.hyps[simp]
have"norm ((\i\insert i I. z i) - (\i\insert i I. w i)) =
norm ((\<Prod>i\<in>I. z i) * (z i - w i) + ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) * w i)"
(is"_ = norm (?t1 + ?t2)") by (auto simp: field_simps) alsohave"\ \ norm ?t1 + norm ?t2" by (rule norm_triangle_ineq) alsohave"norm ?t1 \ norm (\i\I. z i) * norm (z i - w i)" by (rule norm_mult_ineq) alsohave"\ \ (\i\I. norm (z i)) * norm(z i - w i)" by (rule mult_right_mono) (auto intro: norm_prod_le) alsohave"(\i\I. norm (z i)) \ (\i\I. 1)" by (intro prod_mono) (auto intro!: insert) alsohave"norm ?t2 \ norm ((\i\I. z i) - (\i\I. w i)) * norm (w i)" by (rule norm_mult_ineq) alsohave"norm (w i) \ 1" by (auto intro: insert) alsohave"norm ((\i\I. z i) - (\i\I. w i)) \ (\i\I. norm (z i - w i))" using insert by auto finallyshow ?case by (auto simp: ac_simps mult_right_mono mult_left_mono) next case infinite thenshow ?caseby simp qed
lemma norm_power_diff: fixes z w :: "'a::{real_normed_algebra_1, comm_monoid_mult}" assumes"norm z \ 1" "norm w \ 1" shows"norm (z^m - w^m) \ m * norm (z - w)" proof - have"norm (z^m - w^m) = norm ((\ i < m. z) - (\ i < m. w))" by simp alsohave"\ \ (\i by (intro norm_prod_diff) (auto simp: assms) alsohave"\ = m * norm (z - w)" by simp finallyshow ?thesis . qed
subsection \<open>Metric spaces\<close>
class metric_space = uniformity_dist + open_uniformity + assumes dist_eq_0_iff [simp]: "dist x y = 0 \ x = y" and dist_triangle2: "dist x y \ dist x z + dist y z" begin
lemma dist_self [simp]: "dist x x = 0" by simp
lemma zero_le_dist [simp]: "0 \ dist x y" using dist_triangle2 [of x x y] by simp
lemma zero_less_dist_iff: "0 < dist x y \ x \ y" by (simp add: less_le)
lemma dist_not_less_zero [simp]: "\ dist x y < 0" by (simp add: not_less)
lemma dist_le_zero_iff [simp]: "dist x y \ 0 \ x = y" by (simp add: le_less)
lemma dist_commute: "dist x y = dist y x" proof (rule order_antisym) show"dist x y \ dist y x" using dist_triangle2 [of x y x] by simp show"dist y x \ dist x y" using dist_triangle2 [of y x y] by simp qed
lemma dist_commute_lessI: "dist y x < e \ dist x y < e" by (simp add: dist_commute)
lemma dist_triangle: "dist x z \ dist x y + dist y z" using dist_triangle2 [of x z y] by (simp add: dist_commute)
lemma dist_triangle3: "dist x y \ dist a x + dist a y" using dist_triangle2 [of x y a] by (simp add: dist_commute)
lemma abs_dist_diff_le: "\dist a b - dist b c\ \ dist a c" using dist_triangle3[of b c a] dist_triangle2[of a b c] by simp
lemma dist_pos_lt: "x \ y \ 0 < dist x y" by (simp add: zero_less_dist_iff)
lemma dist_nz: "x \ y \ 0 < dist x y" by (simp add: zero_less_dist_iff)
declare dist_nz [symmetric, simp]
lemma dist_triangle_le: "dist x z + dist y z \ e \ dist x y \ e" by (rule order_trans [OF dist_triangle2])
lemma dist_triangle_lt: "dist x z + dist y z < e \ dist x y < e" by (rule le_less_trans [OF dist_triangle2])
lemma dist_triangle_less_add: "dist x1 y < e1 \ dist x2 y < e2 \ dist x1 x2 < e1 + e2" by (rule dist_triangle_lt [where z=y]) simp
lemma dist_triangle_half_l: "dist x1 y < e / 2 \ dist x2 y < e / 2 \ dist x1 x2 < e" by (rule dist_triangle_lt [where z=y]) simp
lemma dist_triangle_half_r: "dist y x1 < e / 2 \ dist y x2 < e / 2 \ dist x1 x2 < e" by (rule dist_triangle_half_l) (simp_all add: dist_commute)
subclass uniform_space proof fix E x assume"eventually E uniformity" thenobtain e where E: "0 < e""\x y. dist x y < e \ E (x, y)" by (auto simp: eventually_uniformity_metric) thenshow"E (x, x)""\\<^sub>F (x, y) in uniformity. E (y, x)" by (auto simp: eventually_uniformity_metric dist_commute) show"\D. eventually D uniformity \ (\x y z. D (x, y) \ D (y, z) \ E (x, z))" using E dist_triangle_half_l[where e=e] unfolding eventually_uniformity_metric by (intro exI[of _ "\(x, y). dist x y < e / 2"] exI[of _ "e/2"] conjI)
(auto simp: dist_commute) qed
lemma open_dist: "open S \ (\x\S. \e>0. \y. dist y x < e \ y \ S)" by (simp add: dist_commute open_uniformity eventually_uniformity_metric)
lemma open_ball: "open {y. dist x y < d}" unfolding open_dist proof (intro ballI) fix y assume *: "y \ {y. dist x y < d}" thenshow"\e>0. \z. dist z y < e \ z \ {y. dist x y < d}" by (auto intro!: exI[of _ "d - dist x y"] simp: field_simps dist_triangle_lt) qed
subclass first_countable_topology proof fix x show"\A::nat \ 'a set. (\i. x \ A i \ open (A i)) \ (\S. open S \ x \ S \ (\i. A i \ S))" proof (safe intro!: exI[of _ "\n. {y. dist x y < inverse (Suc n)}"]) fix S assume"open S""x \ S" thenobtain e where e: "0 < e"and"{y. dist x y < e} \ S" by (auto simp: open_dist subset_eq dist_commute) moreover from e obtain i where"inverse (Suc i) < e" by (auto dest!: reals_Archimedean) thenhave"{y. dist x y < inverse (Suc i)} \ {y. dist x y < e}" by auto ultimatelyshow"\i. {y. dist x y < inverse (Suc i)} \ S" by blast qed (auto intro: open_ball) qed
end
instance metric_space \<subseteq> t2_space proof fix x y :: "'a::metric_space" assume xy: "x \ y" let ?U = "{y'. dist x y' < dist x y / 2}" let ?V = "{x'. dist y x' < dist x y / 2}" have *: "d x z \ d x y + d y z \ d y z = d z y \ \ (d x y * 2 < d x z \ d z y * 2 < d x z)" for d :: "'a \ 'a \ real" and x y z :: 'a by arith have"open ?U \ open ?V \ x \ ?U \ y \ ?V \ ?U \ ?V = {}" using dist_pos_lt[OF xy] *[of dist, OF dist_triangle dist_commute] using open_ball[of _ "dist x y / 2"] by auto thenshow"\U V. open U \ open V \ x \ U \ y \ V \ U \ V = {}" by blast qed
text\<open>Every normed vector space is a metric space.\<close> instance real_normed_vector < metric_space proof fix x y z :: 'a show"dist x y = 0 \ x = y" by (simp add: dist_norm) show"dist x y \ dist x z + dist y z" using norm_triangle_ineq4 [of "x - z""y - z"] by (simp add: dist_norm) qed
subsection \<open>Class instances for real numbers\<close>
instantiation real :: real_normed_field begin
definition dist_real_def: "dist x y = \x - y\"
definition uniformity_real_def [code del]: "(uniformity :: (real \ real) filter) = (INF e\{0 <..}. principal {(x, y). dist x y < e})"
definition open_real_def [code del]: "open (U :: real set) \ (\x\U. eventually (\(x', y). x' = x \ y \ U) uniformity)"
definition real_norm_def [simp]: "norm r = \r\"
instance by intro_classes (auto simp: abs_mult open_real_def dist_real_def sgn_real_def uniformity_real_def)
end
declare uniformity_Abort[where'a=real, code]
lemma dist_of_real [simp]: "dist (of_real x :: 'a) (of_real y) = dist x y" for a :: "'a::real_normed_div_algebra" by (metis dist_norm norm_of_real of_real_diff real_norm_def)
declare [[code abort: "open :: real set \ bool"]]
instance real :: linorder_topology proof show"(open :: real set \ bool) = generate_topology (range lessThan \ range greaterThan)" proof (rule ext, safe) fix S :: "real set" assume"open S" thenobtain f where"\x\S. 0 < f x \ (\y. dist y x < f x \ y \ S)" unfolding open_dist bchoice_iff .. thenhave *: "(\x\S. {x - f x <..} \ {..< x + f x}) = S" (is "?S = S") by (fastforce simp: dist_real_def) moreoverhave"generate_topology (range lessThan \ range greaterThan) ?S" by (force intro: generate_topology.Basis generate_topology_Union generate_topology.Int) ultimatelyshow"generate_topology (range lessThan \ range greaterThan) S" by simp next fix S :: "real set" assume"generate_topology (range lessThan \ range greaterThan) S" moreoverhave"\a::real. open {.. unfolding open_dist dist_real_def proof clarify fix x a :: real assume"x < a" thenhave"0 < a - x \ (\y. \y - x\ < a - x \ y \ {.. thenshow"\e>0. \y. \y - x\ < e \ y \ {.. qed moreoverhave"\a::real. open {a <..}" unfolding open_dist dist_real_def proof clarify fix x a :: real assume"a < x" thenhave"0 < x - a \ (\y. \y - x\ < x - a \ y \ {a<..})" by auto thenshow"\e>0. \y. \y - x\ < e \ y \ {a<..}" .. qed ultimatelyshow"open S" by induct auto qed qed
instance real :: ordered_real_vector by standard (auto intro: mult_left_mono mult_right_mono)
subsection \<open>Extra type constraints\<close>
text\<open>Only allow \<^term>\<open>open\<close> in class \<open>topological_space\<close>.\<close> setup\<open>Sign.add_const_constraint
(\<^const_name>\<open>open\<close>, SOME \<^typ>\<open>'a::topological_space set \<Rightarrow> bool\<close>)\<close>
text\<open>Only allow \<^term>\<open>uniformity\<close> in class \<open>uniform_space\<close>.\<close> setup\<open>Sign.add_const_constraint
(\<^const_name>\<open>uniformity\<close>, SOME \<^typ>\<open>('a::uniformity \<times> 'a) filter\<close>)\<close>
text\<open>Only allow \<^term>\<open>dist\<close> in class \<open>metric_space\<close>.\<close> setup\<open>Sign.add_const_constraint
(\<^const_name>\<open>dist\<close>, SOME \<^typ>\<open>'a::metric_space \<Rightarrow> 'a \<Rightarrow> real\<close>)\<close>
text\<open>Only allow \<^term>\<open>norm\<close> in class \<open>real_normed_vector\<close>.\<close> setup\<open>Sign.add_const_constraint
(\<^const_name>\<open>norm\<close>, SOME \<^typ>\<open>'a::real_normed_vector \<Rightarrow> real\<close>)\<close>
subsection \<open>Sign function\<close>
lemma norm_sgn: "norm (sgn x) = (if x = 0 then 0 else 1)" for x :: "'a::real_normed_vector" by (simp add: sgn_div_norm)
lemma sgn_of_real: "sgn (of_real r :: 'a::real_normed_algebra_1) = of_real (sgn r)" unfolding of_real_def by (simp only: sgn_scaleR sgn_one)
lemma sgn_mult: "sgn (x * y) = sgn x * sgn y" for x y :: "'a::real_normed_div_algebra" by (simp add: sgn_div_norm norm_mult)
hide_fact (open) sgn_mult
lemma real_sgn_eq: "sgn x = x / \x\" for x :: real by (simp add: sgn_div_norm divide_inverse)
lemma zero_le_sgn_iff [simp]: "0 \ sgn x \ 0 \ x" for x :: real by (cases "0::real" x rule: linorder_cases) simp_all
lemma sgn_le_0_iff [simp]: "sgn x \ 0 \ x \ 0" for x :: real by (cases "0::real" x rule: linorder_cases) simp_all
lemma norm_conv_dist: "norm x = dist x 0" unfolding dist_norm by simp
declare norm_conv_dist [symmetric, simp]
lemma dist_0_norm [simp]: "dist 0 x = norm x" for x :: "'a::real_normed_vector" by (simp add: dist_norm)
lemma dist_diff [simp]: "dist a (a - b) = norm b""dist (a - b) a = norm b" by (simp_all add: dist_norm)
lemma dist_of_int: "dist (of_int m) (of_int n :: 'a :: real_normed_algebra_1) = of_int \m - n\" proof - have"dist (of_int m) (of_int n :: 'a) = dist (of_int m :: 'a) (of_int m - (of_int (m - n)))" by simp alsohave"\ = of_int \m - n\" by (subst dist_diff, subst norm_of_int) simp finallyshow ?thesis . qed
lemma dist_of_nat: "dist (of_nat m) (of_nat n :: 'a :: real_normed_algebra_1) = of_int \int m - int n\" by (subst (1 2) of_int_of_nat_eq [symmetric]) (rule dist_of_int)
subsection \<open>Bounded Linear and Bilinear Operators\<close>
lemma linearI: "linear f" if"\b1 b2. f (b1 + b2) = f b1 + f b2" "\r b. f (r *\<^sub>R b) = r *\<^sub>R f b" using that by unfold_locales (auto simp: algebra_simps)
lemma linear_iff: "linear f \ (\x y. f (x + y) = f x + f y) \ (\c x. f (c *\<^sub>R x) = c *\<^sub>R f x)"
(is"linear f \ ?rhs") proof assume"linear f" theninterpret f: linear f . show"?rhs"by (simp add: f.add f.scale) next assume"?rhs" thenshow"linear f"by (intro linearI) auto qed
lemma linear_of_real [simp]: "linear of_real" by (simp add: linear_iff scaleR_conv_of_real)
corollary real_linearD: fixes f :: "real \ real" assumes"linear f"obtains c where"f = (*) c" by (rule linear_imp_scaleR [OF assms]) (force simp: scaleR_conv_of_real)
lemma linear_times_of_real: "linear (\x. a * of_real x)" by (auto intro!: linearI simp: distrib_left)
(metis mult_scaleR_right scaleR_conv_of_real)
locale bounded_linear = linear f for f :: "'a::real_normed_vector \ 'b::real_normed_vector" + assumes bounded: "\K. \x. norm (f x) \ norm x * K" begin
lemma pos_bounded: "\K>0. \x. norm (f x) \ norm x * K" proof - obtain K where K: "\x. norm (f x) \ norm x * K" using bounded by blast show ?thesis proof (intro exI impI conjI allI) show"0 < max 1 K" by (rule order_less_le_trans [OF zero_less_one max.cobounded1]) next fix x have"norm (f x) \ norm x * K" using K . alsohave"\ \ norm x * max 1 K" by (rule mult_left_mono [OF max.cobounded2 norm_ge_zero]) finallyshow"norm (f x) \ norm x * max 1 K" . qed qed
lemma nonneg_bounded: "\K\0. \x. norm (f x) \ norm x * K" using pos_bounded by (auto intro: order_less_imp_le)
lemma linear: "linear f" by (fact local.linear_axioms)
end
lemma bounded_linear_intro: assumes"\x y. f (x + y) = f x + f y" and"\r x. f (scaleR r x) = scaleR r (f x)" and"\x. norm (f x) \ norm x * K" shows"bounded_linear f" by standard (blast intro: assms)+
locale bounded_bilinear = fixes prod :: "'a::real_normed_vector \ 'b::real_normed_vector \ 'c::real_normed_vector"
(infixl\<open>**\<close> 70) assumes add_left: "prod (a + a') b = prod a b + prod a' b" and add_right: "prod a (b + b') = prod a b + prod a b'" and scaleR_left: "prod (scaleR r a) b = scaleR r (prod a b)" and scaleR_right: "prod a (scaleR r b) = scaleR r (prod a b)" and bounded: "\K. \a b. norm (prod a b) \ norm a * norm b * K" begin
lemma pos_bounded: "\K>0. \a b. norm (a ** b) \ norm a * norm b * K" proof - obtain K where"\a b. norm (a ** b) \ norm a * norm b * K" using bounded by blast thenhave"norm (a ** b) \ norm a * norm b * (max 1 K)" for a b by (rule order.trans) (simp add: mult_left_mono) thenshow ?thesis by force qed
lemma nonneg_bounded: "\K\0. \a b. norm (a ** b) \ norm a * norm b * K" using pos_bounded by (auto intro: order_less_imp_le)
lemma additive_right: "additive (\b. prod a b)" by (rule additive.intro, rule add_right)
lemma additive_left: "additive (\a. prod a b)" by (rule additive.intro, rule add_left)
lemma zero_left: "prod 0 b = 0" by (rule additive.zero [OF additive_left])
lemma zero_right: "prod a 0 = 0" by (rule additive.zero [OF additive_right])
lemma minus_left: "prod (- a) b = - prod a b" by (rule additive.minus [OF additive_left])
lemma minus_right: "prod a (- b) = - prod a b" by (rule additive.minus [OF additive_right])
lemma diff_left: "prod (a - a') b = prod a b - prod a' b" by (rule additive.diff [OF additive_left])
lemma diff_right: "prod a (b - b') = prod a b - prod a b'" by (rule additive.diff [OF additive_right])
lemma sum_left: "prod (sum g S) x = sum ((\i. prod (g i) x)) S" by (rule additive.sum [OF additive_left])
lemma sum_right: "prod x (sum g S) = sum ((\i. (prod x (g i)))) S" by (rule additive.sum [OF additive_right])
lemma bounded_linear_left: "bounded_linear (\a. a ** b)" proof - obtain K where"\a b. norm (a ** b) \ norm a * norm b * K" using pos_bounded by blast thenshow ?thesis by (rule_tac K="norm b * K"in bounded_linear_intro) (auto simp: algebra_simps scaleR_left add_left) qed
lemma bounded_linear_right: "bounded_linear (\b. a ** b)" proof - obtain K where"\a b. norm (a ** b) \ norm a * norm b * K" using pos_bounded by blast thenshow ?thesis by (rule_tac K="norm a * K"in bounded_linear_intro) (auto simp: algebra_simps scaleR_right add_right) qed
lemma prod_diff_prod: "(x ** y - a ** b) = (x - a) ** (y - b) + (x - a) ** b + a ** (y - b)" by (simp add: diff_left diff_right)
lemma flip: "bounded_bilinear (\x y. y ** x)" proof
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
