# HG changeset patch # User hoelzl # Date 1475242537 -7200 # Node ID da89140186e2e42702e73912059d1ee0a6223b5e # Parent 3b6a3632e754da4124e052257e9f95cf2779968f HOL-Analysis: move Product_Vector and Inner_Product from Library diff -r 3b6a3632e754 -r da89140186e2 src/HOL/Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Sep 30 15:35:32 2016 +0200 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Sep 30 15:35:37 2016 +0200 @@ -11,7 +11,6 @@ theory Convex_Euclidean_Space imports Topology_Euclidean_Space - "~~/src/HOL/Library/Product_Vector" "~~/src/HOL/Library/Set_Algebras" begin diff -r 3b6a3632e754 -r da89140186e2 src/HOL/Analysis/Euclidean_Space.thy --- a/src/HOL/Analysis/Euclidean_Space.thy Fri Sep 30 15:35:32 2016 +0200 +++ b/src/HOL/Analysis/Euclidean_Space.thy Fri Sep 30 15:35:37 2016 +0200 @@ -7,9 +7,7 @@ theory Euclidean_Space imports - L2_Norm - "~~/src/HOL/Library/Inner_Product" - "~~/src/HOL/Library/Product_Vector" + L2_Norm Product_Vector begin subsection \Type class of Euclidean spaces\ diff -r 3b6a3632e754 -r da89140186e2 src/HOL/Analysis/Inner_Product.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Analysis/Inner_Product.thy Fri Sep 30 15:35:37 2016 +0200 @@ -0,0 +1,402 @@ +(* Title: HOL/Analysis/Inner_Product.thy + Author: Brian Huffman +*) + +section \Inner Product Spaces and the Gradient Derivative\ + +theory Inner_Product +imports "~~/src/HOL/Complex_Main" +begin + +subsection \Real inner product spaces\ + +text \ + Temporarily relax type constraints for @{term "open"}, @{term "uniformity"}, + @{term dist}, and @{term norm}. +\ + +setup \Sign.add_const_constraint + (@{const_name "open"}, SOME @{typ "'a::open set \ bool"})\ + +setup \Sign.add_const_constraint + (@{const_name dist}, SOME @{typ "'a::dist \ 'a \ real"})\ + +setup \Sign.add_const_constraint + (@{const_name uniformity}, SOME @{typ "('a::uniformity \ 'a) filter"})\ + +setup \Sign.add_const_constraint + (@{const_name norm}, SOME @{typ "'a::norm \ real"})\ + +class real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity + + fixes inner :: "'a \ 'a \ real" + assumes inner_commute: "inner x y = inner y x" + and inner_add_left: "inner (x + y) z = inner x z + inner y z" + and inner_scaleR_left [simp]: "inner (scaleR r x) y = r * (inner x y)" + and inner_ge_zero [simp]: "0 \ inner x x" + and inner_eq_zero_iff [simp]: "inner x x = 0 \ x = 0" + and norm_eq_sqrt_inner: "norm x = sqrt (inner x x)" +begin + +lemma inner_zero_left [simp]: "inner 0 x = 0" + using inner_add_left [of 0 0 x] by simp + +lemma inner_minus_left [simp]: "inner (- x) y = - inner x y" + using inner_add_left [of x "- x" y] by simp + +lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z" + using inner_add_left [of x "- y" z] by simp + +lemma inner_setsum_left: "inner (\x\A. f x) y = (\x\A. inner (f x) y)" + by (cases "finite A", induct set: finite, simp_all add: inner_add_left) + +text \Transfer distributivity rules to right argument.\ + +lemma inner_add_right: "inner x (y + z) = inner x y + inner x z" + using inner_add_left [of y z x] by (simp only: inner_commute) + +lemma inner_scaleR_right [simp]: "inner x (scaleR r y) = r * (inner x y)" + using inner_scaleR_left [of r y x] by (simp only: inner_commute) + +lemma inner_zero_right [simp]: "inner x 0 = 0" + using inner_zero_left [of x] by (simp only: inner_commute) + +lemma inner_minus_right [simp]: "inner x (- y) = - inner x y" + using inner_minus_left [of y x] by (simp only: inner_commute) + +lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z" + using inner_diff_left [of y z x] by (simp only: inner_commute) + +lemma inner_setsum_right: "inner x (\y\A. f y) = (\y\A. inner x (f y))" + using inner_setsum_left [of f A x] by (simp only: inner_commute) + +lemmas inner_add [algebra_simps] = inner_add_left inner_add_right +lemmas inner_diff [algebra_simps] = inner_diff_left inner_diff_right +lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right + +text \Legacy theorem names\ +lemmas inner_left_distrib = inner_add_left +lemmas inner_right_distrib = inner_add_right +lemmas inner_distrib = inner_left_distrib inner_right_distrib + +lemma inner_gt_zero_iff [simp]: "0 < inner x x \ x \ 0" + by (simp add: order_less_le) + +lemma power2_norm_eq_inner: "(norm x)\<^sup>2 = inner x x" + by (simp add: norm_eq_sqrt_inner) + +text \Identities involving real multiplication and division.\ + +lemma inner_mult_left: "inner (of_real m * a) b = m * (inner a b)" + by (metis real_inner_class.inner_scaleR_left scaleR_conv_of_real) + +lemma inner_mult_right: "inner a (of_real m * b) = m * (inner a b)" + by (metis real_inner_class.inner_scaleR_right scaleR_conv_of_real) + +lemma inner_mult_left': "inner (a * of_real m) b = m * (inner a b)" + by (simp add: of_real_def) + +lemma inner_mult_right': "inner a (b * of_real m) = (inner a b) * m" + by (simp add: of_real_def real_inner_class.inner_scaleR_right) + +lemma Cauchy_Schwarz_ineq: + "(inner x y)\<^sup>2 \ inner x x * inner y y" +proof (cases) + assume "y = 0" + thus ?thesis by simp +next + assume y: "y \ 0" + let ?r = "inner x y / inner y y" + have "0 \ inner (x - scaleR ?r y) (x - scaleR ?r y)" + by (rule inner_ge_zero) + also have "\ = inner x x - inner y x * ?r" + by (simp add: inner_diff) + also have "\ = inner x x - (inner x y)\<^sup>2 / inner y y" + by (simp add: power2_eq_square inner_commute) + finally have "0 \ inner x x - (inner x y)\<^sup>2 / inner y y" . + hence "(inner x y)\<^sup>2 / inner y y \ inner x x" + by (simp add: le_diff_eq) + thus "(inner x y)\<^sup>2 \ inner x x * inner y y" + by (simp add: pos_divide_le_eq y) +qed + +lemma Cauchy_Schwarz_ineq2: + "\inner x y\ \ norm x * norm y" +proof (rule power2_le_imp_le) + have "(inner x y)\<^sup>2 \ inner x x * inner y y" + using Cauchy_Schwarz_ineq . + thus "\inner x y\\<^sup>2 \ (norm x * norm y)\<^sup>2" + by (simp add: power_mult_distrib power2_norm_eq_inner) + show "0 \ norm x * norm y" + unfolding norm_eq_sqrt_inner + by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero) +qed + +lemma norm_cauchy_schwarz: "inner x y \ norm x * norm y" + using Cauchy_Schwarz_ineq2 [of x y] by auto + +subclass real_normed_vector +proof + fix a :: real and x y :: 'a + show "norm x = 0 \ x = 0" + unfolding norm_eq_sqrt_inner by simp + show "norm (x + y) \ norm x + norm y" + proof (rule power2_le_imp_le) + have "inner x y \ norm x * norm y" + by (rule norm_cauchy_schwarz) + thus "(norm (x + y))\<^sup>2 \ (norm x + norm y)\<^sup>2" + unfolding power2_sum power2_norm_eq_inner + by (simp add: inner_add inner_commute) + show "0 \ norm x + norm y" + unfolding norm_eq_sqrt_inner by simp + qed + have "sqrt (a\<^sup>2 * inner x x) = \a\ * sqrt (inner x x)" + by (simp add: real_sqrt_mult_distrib) + then show "norm (a *\<^sub>R x) = \a\ * norm x" + unfolding norm_eq_sqrt_inner + by (simp add: power2_eq_square mult.assoc) +qed + +end + +lemma inner_divide_left: + fixes a :: "'a :: {real_inner,real_div_algebra}" + shows "inner (a / of_real m) b = (inner a b) / m" + by (metis (no_types) divide_inverse inner_commute inner_scaleR_right mult.left_neutral mult.right_neutral mult_scaleR_right of_real_inverse scaleR_conv_of_real times_divide_eq_left) + +lemma inner_divide_right: + fixes a :: "'a :: {real_inner,real_div_algebra}" + shows "inner a (b / of_real m) = (inner a b) / m" + by (metis inner_commute inner_divide_left) + +text \ + Re-enable constraints for @{term "open"}, @{term "uniformity"}, + @{term dist}, and @{term norm}. +\ + +setup \Sign.add_const_constraint + (@{const_name "open"}, SOME @{typ "'a::topological_space set \ bool"})\ + +setup \Sign.add_const_constraint + (@{const_name uniformity}, SOME @{typ "('a::uniform_space \ 'a) filter"})\ + +setup \Sign.add_const_constraint + (@{const_name dist}, SOME @{typ "'a::metric_space \ 'a \ real"})\ + +setup \Sign.add_const_constraint + (@{const_name norm}, SOME @{typ "'a::real_normed_vector \ real"})\ + +lemma bounded_bilinear_inner: + "bounded_bilinear (inner::'a::real_inner \ 'a \ real)" +proof + fix x y z :: 'a and r :: real + show "inner (x + y) z = inner x z + inner y z" + by (rule inner_add_left) + show "inner x (y + z) = inner x y + inner x z" + by (rule inner_add_right) + show "inner (scaleR r x) y = scaleR r (inner x y)" + unfolding real_scaleR_def by (rule inner_scaleR_left) + show "inner x (scaleR r y) = scaleR r (inner x y)" + unfolding real_scaleR_def by (rule inner_scaleR_right) + show "\K. \x y::'a. norm (inner x y) \ norm x * norm y * K" + proof + show "\x y::'a. norm (inner x y) \ norm x * norm y * 1" + by (simp add: Cauchy_Schwarz_ineq2) + qed +qed + +lemmas tendsto_inner [tendsto_intros] = + bounded_bilinear.tendsto [OF bounded_bilinear_inner] + +lemmas isCont_inner [simp] = + bounded_bilinear.isCont [OF bounded_bilinear_inner] + +lemmas has_derivative_inner [derivative_intros] = + bounded_bilinear.FDERIV [OF bounded_bilinear_inner] + +lemmas bounded_linear_inner_left = + bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner] + +lemmas bounded_linear_inner_right = + bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner] + +lemmas bounded_linear_inner_left_comp = bounded_linear_inner_left[THEN bounded_linear_compose] + +lemmas bounded_linear_inner_right_comp = bounded_linear_inner_right[THEN bounded_linear_compose] + +lemmas has_derivative_inner_right [derivative_intros] = + bounded_linear.has_derivative [OF bounded_linear_inner_right] + +lemmas has_derivative_inner_left [derivative_intros] = + bounded_linear.has_derivative [OF bounded_linear_inner_left] + +lemma differentiable_inner [simp]: + "f differentiable (at x within s) \ g differentiable at x within s \ (\x. inner (f x) (g x)) differentiable at x within s" + unfolding differentiable_def by (blast intro: has_derivative_inner) + + +subsection \Class instances\ + +instantiation real :: real_inner +begin + +definition inner_real_def [simp]: "inner = op *" + +instance +proof + fix x y z r :: real + show "inner x y = inner y x" + unfolding inner_real_def by (rule mult.commute) + show "inner (x + y) z = inner x z + inner y z" + unfolding inner_real_def by (rule distrib_right) + show "inner (scaleR r x) y = r * inner x y" + unfolding inner_real_def real_scaleR_def by (rule mult.assoc) + show "0 \ inner x x" + unfolding inner_real_def by simp + show "inner x x = 0 \ x = 0" + unfolding inner_real_def by simp + show "norm x = sqrt (inner x x)" + unfolding inner_real_def by simp +qed + +end + +lemma + shows real_inner_1_left[simp]: "inner 1 x = x" + and real_inner_1_right[simp]: "inner x 1 = x" + by simp_all + +instantiation complex :: real_inner +begin + +definition inner_complex_def: + "inner x y = Re x * Re y + Im x * Im y" + +instance +proof + fix x y z :: complex and r :: real + show "inner x y = inner y x" + unfolding inner_complex_def by (simp add: mult.commute) + show "inner (x + y) z = inner x z + inner y z" + unfolding inner_complex_def by (simp add: distrib_right) + show "inner (scaleR r x) y = r * inner x y" + unfolding inner_complex_def by (simp add: distrib_left) + show "0 \ inner x x" + unfolding inner_complex_def by simp + show "inner x x = 0 \ x = 0" + unfolding inner_complex_def + by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff) + show "norm x = sqrt (inner x x)" + unfolding inner_complex_def complex_norm_def + by (simp add: power2_eq_square) +qed + +end + +lemma complex_inner_1 [simp]: "inner 1 x = Re x" + unfolding inner_complex_def by simp + +lemma complex_inner_1_right [simp]: "inner x 1 = Re x" + unfolding inner_complex_def by simp + +lemma complex_inner_ii_left [simp]: "inner \ x = Im x" + unfolding inner_complex_def by simp + +lemma complex_inner_ii_right [simp]: "inner x \ = Im x" + unfolding inner_complex_def by simp + + +subsection \Gradient derivative\ + +definition + gderiv :: + "['a::real_inner \ real, 'a, 'a] \ bool" + ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) +where + "GDERIV f x :> D \ FDERIV f x :> (\h. inner h D)" + +lemma gderiv_deriv [simp]: "GDERIV f x :> D \ DERIV f x :> D" + by (simp only: gderiv_def has_field_derivative_def inner_real_def mult_commute_abs) + +lemma GDERIV_DERIV_compose: + "\GDERIV f x :> df; DERIV g (f x) :> dg\ + \ GDERIV (\x. g (f x)) x :> scaleR dg df" + unfolding gderiv_def has_field_derivative_def + apply (drule (1) has_derivative_compose) + apply (simp add: ac_simps) + done + +lemma has_derivative_subst: "\FDERIV f x :> df; df = d\ \ FDERIV f x :> d" + by simp + +lemma GDERIV_subst: "\GDERIV f x :> df; df = d\ \ GDERIV f x :> d" + by simp + +lemma GDERIV_const: "GDERIV (\x. k) x :> 0" + unfolding gderiv_def inner_zero_right by (rule has_derivative_const) + +lemma GDERIV_add: + "\GDERIV f x :> df; GDERIV g x :> dg\ + \ GDERIV (\x. f x + g x) x :> df + dg" + unfolding gderiv_def inner_add_right by (rule has_derivative_add) + +lemma GDERIV_minus: + "GDERIV f x :> df \ GDERIV (\x. - f x) x :> - df" + unfolding gderiv_def inner_minus_right by (rule has_derivative_minus) + +lemma GDERIV_diff: + "\GDERIV f x :> df; GDERIV g x :> dg\ + \ GDERIV (\x. f x - g x) x :> df - dg" + unfolding gderiv_def inner_diff_right by (rule has_derivative_diff) + +lemma GDERIV_scaleR: + "\DERIV f x :> df; GDERIV g x :> dg\ + \ GDERIV (\x. scaleR (f x) (g x)) x + :> (scaleR (f x) dg + scaleR df (g x))" + unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right + apply (rule has_derivative_subst) + apply (erule (1) has_derivative_scaleR) + apply (simp add: ac_simps) + done + +lemma GDERIV_mult: + "\GDERIV f x :> df; GDERIV g x :> dg\ + \ GDERIV (\x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df" + unfolding gderiv_def + apply (rule has_derivative_subst) + apply (erule (1) has_derivative_mult) + apply (simp add: inner_add ac_simps) + done + +lemma GDERIV_inverse: + "\GDERIV f x :> df; f x \ 0\ + \ GDERIV (\x. inverse (f x)) x :> - (inverse (f x))\<^sup>2 *\<^sub>R df" + apply (erule GDERIV_DERIV_compose) + apply (erule DERIV_inverse [folded numeral_2_eq_2]) + done + +lemma GDERIV_norm: + assumes "x \ 0" shows "GDERIV (\x. norm x) x :> sgn x" +proof - + have 1: "FDERIV (\x. inner x x) x :> (\h. inner x h + inner h x)" + by (intro has_derivative_inner has_derivative_ident) + have 2: "(\h. inner x h + inner h x) = (\h. inner h (scaleR 2 x))" + by (simp add: fun_eq_iff inner_commute) + have "0 < inner x x" using \x \ 0\ by simp + then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)" + by (rule DERIV_real_sqrt) + have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x" + by (simp add: sgn_div_norm norm_eq_sqrt_inner) + show ?thesis + unfolding norm_eq_sqrt_inner + apply (rule GDERIV_subst [OF _ 4]) + apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"]) + apply (subst gderiv_def) + apply (rule has_derivative_subst [OF _ 2]) + apply (rule 1) + apply (rule 3) + done +qed + +lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def] + +end diff -r 3b6a3632e754 -r da89140186e2 src/HOL/Analysis/Product_Vector.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Analysis/Product_Vector.thy Fri Sep 30 15:35:37 2016 +0200 @@ -0,0 +1,371 @@ +(* Title: HOL/Analysis/Product_Vector.thy + Author: Brian Huffman +*) + +section \Cartesian Products as Vector Spaces\ + +theory Product_Vector +imports + Inner_Product + "~~/src/HOL/Library/Product_plus" +begin + +subsection \Product is a real vector space\ + +instantiation prod :: (real_vector, real_vector) real_vector +begin + +definition scaleR_prod_def: + "scaleR r A = (scaleR r (fst A), scaleR r (snd A))" + +lemma fst_scaleR [simp]: "fst (scaleR r A) = scaleR r (fst A)" + unfolding scaleR_prod_def by simp + +lemma snd_scaleR [simp]: "snd (scaleR r A) = scaleR r (snd A)" + unfolding scaleR_prod_def by simp + +lemma scaleR_Pair [simp]: "scaleR r (a, b) = (scaleR r a, scaleR r b)" + unfolding scaleR_prod_def by simp + +instance +proof + fix a b :: real and x y :: "'a \ 'b" + show "scaleR a (x + y) = scaleR a x + scaleR a y" + by (simp add: prod_eq_iff scaleR_right_distrib) + show "scaleR (a + b) x = scaleR a x + scaleR b x" + by (simp add: prod_eq_iff scaleR_left_distrib) + show "scaleR a (scaleR b x) = scaleR (a * b) x" + by (simp add: prod_eq_iff) + show "scaleR 1 x = x" + by (simp add: prod_eq_iff) +qed + +end + +subsection \Product is a metric space\ + +(* TODO: Product of uniform spaces and compatibility with metric_spaces! *) + +instantiation prod :: (metric_space, metric_space) dist +begin + +definition dist_prod_def[code del]: + "dist x y = sqrt ((dist (fst x) (fst y))\<^sup>2 + (dist (snd x) (snd y))\<^sup>2)" + +instance .. +end + +instantiation prod :: (metric_space, metric_space) uniformity_dist +begin + +definition [code del]: + "(uniformity :: (('a \ 'b) \ ('a \ 'b)) filter) = + (INF e:{0 <..}. principal {(x, y). dist x y < e})" + +instance + by standard (rule uniformity_prod_def) +end + +declare uniformity_Abort[where 'a="'a :: metric_space \ 'b :: metric_space", code] + +instantiation prod :: (metric_space, metric_space) metric_space +begin + +lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)" + unfolding dist_prod_def by simp + +lemma dist_fst_le: "dist (fst x) (fst y) \ dist x y" + unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge1) + +lemma dist_snd_le: "dist (snd x) (snd y) \ dist x y" + unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2) + +instance +proof + fix x y :: "'a \ 'b" + show "dist x y = 0 \ x = y" + unfolding dist_prod_def prod_eq_iff by simp +next + fix x y z :: "'a \ 'b" + show "dist x y \ dist x z + dist y z" + unfolding dist_prod_def + by (intro order_trans [OF _ real_sqrt_sum_squares_triangle_ineq] + real_sqrt_le_mono add_mono power_mono dist_triangle2 zero_le_dist) +next + fix S :: "('a \ 'b) set" + have *: "open S \ (\x\S. \e>0. \y. dist y x < e \ y \ S)" + proof + assume "open S" show "\x\S. \e>0. \y. dist y x < e \ y \ S" + proof + fix x assume "x \ S" + obtain A B where "open A" "open B" "x \ A \ B" "A \ B \ S" + using \open S\ and \x \ S\ by (rule open_prod_elim) + obtain r where r: "0 < r" "\y. dist y (fst x) < r \ y \ A" + using \open A\ and \x \ A \ B\ unfolding open_dist by auto + obtain s where s: "0 < s" "\y. dist y (snd x) < s \ y \ B" + using \open B\ and \x \ A \ B\ unfolding open_dist by auto + let ?e = "min r s" + have "0 < ?e \ (\y. dist y x < ?e \ y \ S)" + proof (intro allI impI conjI) + show "0 < min r s" by (simp add: r(1) s(1)) + next + fix y assume "dist y x < min r s" + hence "dist y x < r" and "dist y x < s" + by simp_all + hence "dist (fst y) (fst x) < r" and "dist (snd y) (snd x) < s" + by (auto intro: le_less_trans dist_fst_le dist_snd_le) + hence "fst y \ A" and "snd y \ B" + by (simp_all add: r(2) s(2)) + hence "y \ A \ B" by (induct y, simp) + with \A \ B \ S\ show "y \ S" .. + qed + thus "\e>0. \y. dist y x < e \ y \ S" .. + qed + next + assume *: "\x\S. \e>0. \y. dist y x < e \ y \ S" show "open S" + proof (rule open_prod_intro) + fix x assume "x \ S" + then obtain e where "0 < e" and S: "\y. dist y x < e \ y \ S" + using * by fast + define r where "r = e / sqrt 2" + define s where "s = e / sqrt 2" + from \0 < e\ have "0 < r" and "0 < s" + unfolding r_def s_def by simp_all + from \0 < e\ have "e = sqrt (r\<^sup>2 + s\<^sup>2)" + unfolding r_def s_def by (simp add: power_divide) + define A where "A = {y. dist (fst x) y < r}" + define B where "B = {y. dist (snd x) y < s}" + have "open A" and "open B" + unfolding A_def B_def by (simp_all add: open_ball) + moreover have "x \ A \ B" + unfolding A_def B_def mem_Times_iff + using \0 < r\ and \0 < s\ by simp + moreover have "A \ B \ S" + proof (clarify) + fix a b assume "a \ A" and "b \ B" + hence "dist a (fst x) < r" and "dist b (snd x) < s" + unfolding A_def B_def by (simp_all add: dist_commute) + hence "dist (a, b) x < e" + unfolding dist_prod_def \e = sqrt (r\<^sup>2 + s\<^sup>2)\ + by (simp add: add_strict_mono power_strict_mono) + thus "(a, b) \ S" + by (simp add: S) + qed + ultimately show "\A B. open A \ open B \ x \ A \ B \ A \ B \ S" by fast + qed + qed + show "open S = (\x\S. \\<^sub>F (x', y) in uniformity. x' = x \ y \ S)" + unfolding * eventually_uniformity_metric + by (simp del: split_paired_All add: dist_prod_def dist_commute) +qed + +end + +declare [[code abort: "dist::('a::metric_space*'b::metric_space)\('a*'b) \ real"]] + +lemma Cauchy_fst: "Cauchy X \ Cauchy (\n. fst (X n))" + unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le]) + +lemma Cauchy_snd: "Cauchy X \ Cauchy (\n. snd (X n))" + unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_snd_le]) + +lemma Cauchy_Pair: + assumes "Cauchy X" and "Cauchy Y" + shows "Cauchy (\n. (X n, Y n))" +proof (rule metric_CauchyI) + fix r :: real assume "0 < r" + hence "0 < r / sqrt 2" (is "0 < ?s") by simp + obtain M where M: "\m\M. \n\M. dist (X m) (X n) < ?s" + using metric_CauchyD [OF \Cauchy X\ \0 < ?s\] .. + obtain N where N: "\m\N. \n\N. dist (Y m) (Y n) < ?s" + using metric_CauchyD [OF \Cauchy Y\ \0 < ?s\] .. + have "\m\max M N. \n\max M N. dist (X m, Y m) (X n, Y n) < r" + using M N by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair) + then show "\n0. \m\n0. \n\n0. dist (X m, Y m) (X n, Y n) < r" .. +qed + +subsection \Product is a complete metric space\ + +instance prod :: (complete_space, complete_space) complete_space +proof + fix X :: "nat \ 'a \ 'b" assume "Cauchy X" + have 1: "(\n. fst (X n)) \ lim (\n. fst (X n))" + using Cauchy_fst [OF \Cauchy X\] + by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) + have 2: "(\n. snd (X n)) \ lim (\n. snd (X n))" + using Cauchy_snd [OF \Cauchy X\] + by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) + have "X \ (lim (\n. fst (X n)), lim (\n. snd (X n)))" + using tendsto_Pair [OF 1 2] by simp + then show "convergent X" + by (rule convergentI) +qed + +subsection \Product is a normed vector space\ + +instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector +begin + +definition norm_prod_def[code del]: + "norm x = sqrt ((norm (fst x))\<^sup>2 + (norm (snd x))\<^sup>2)" + +definition sgn_prod_def: + "sgn (x::'a \ 'b) = scaleR (inverse (norm x)) x" + +lemma norm_Pair: "norm (a, b) = sqrt ((norm a)\<^sup>2 + (norm b)\<^sup>2)" + unfolding norm_prod_def by simp + +instance +proof + fix r :: real and x y :: "'a \ 'b" + show "norm x = 0 \ x = 0" + unfolding norm_prod_def + by (simp add: prod_eq_iff) + show "norm (x + y) \ norm x + norm y" + unfolding norm_prod_def + apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq]) + apply (simp add: add_mono power_mono norm_triangle_ineq) + done + show "norm (scaleR r x) = \r\ * norm x" + unfolding norm_prod_def + apply (simp add: power_mult_distrib) + apply (simp add: distrib_left [symmetric]) + apply (simp add: real_sqrt_mult_distrib) + done + show "sgn x = scaleR (inverse (norm x)) x" + by (rule sgn_prod_def) + show "dist x y = norm (x - y)" + unfolding dist_prod_def norm_prod_def + by (simp add: dist_norm) +qed + +end + +declare [[code abort: "norm::('a::real_normed_vector*'b::real_normed_vector) \ real"]] + +instance prod :: (banach, banach) banach .. + +subsubsection \Pair operations are linear\ + +lemma bounded_linear_fst: "bounded_linear fst" + using fst_add fst_scaleR + by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def) + +lemma bounded_linear_snd: "bounded_linear snd" + using snd_add snd_scaleR + by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def) + +lemmas bounded_linear_fst_comp = bounded_linear_fst[THEN bounded_linear_compose] + +lemmas bounded_linear_snd_comp = bounded_linear_snd[THEN bounded_linear_compose] + +lemma bounded_linear_Pair: + assumes f: "bounded_linear f" + assumes g: "bounded_linear g" + shows "bounded_linear (\x. (f x, g x))" +proof + interpret f: bounded_linear f by fact + interpret g: bounded_linear g by fact + fix x y and r :: real + show "(f (x + y), g (x + y)) = (f x, g x) + (f y, g y)" + by (simp add: f.add g.add) + show "(f (r *\<^sub>R x), g (r *\<^sub>R x)) = r *\<^sub>R (f x, g x)" + by (simp add: f.scaleR g.scaleR) + obtain Kf where "0 < Kf" and norm_f: "\x. norm (f x) \ norm x * Kf" + using f.pos_bounded by fast + obtain Kg where "0 < Kg" and norm_g: "\x. norm (g x) \ norm x * Kg" + using g.pos_bounded by fast + have "\x. norm (f x, g x) \ norm x * (Kf + Kg)" + apply (rule allI) + apply (simp add: norm_Pair) + apply (rule order_trans [OF sqrt_add_le_add_sqrt], simp, simp) + apply (simp add: distrib_left) + apply (rule add_mono [OF norm_f norm_g]) + done + then show "\K. \x. norm (f x, g x) \ norm x * K" .. +qed + +subsubsection \Frechet derivatives involving pairs\ + +lemma has_derivative_Pair [derivative_intros]: + assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)" + shows "((\x. (f x, g x)) has_derivative (\h. (f' h, g' h))) (at x within s)" +proof (rule has_derivativeI_sandwich[of 1]) + show "bounded_linear (\h. (f' h, g' h))" + using f g by (intro bounded_linear_Pair has_derivative_bounded_linear) + let ?Rf = "\y. f y - f x - f' (y - x)" + let ?Rg = "\y. g y - g x - g' (y - x)" + let ?R = "\y. ((f y, g y) - (f x, g x) - (f' (y - x), g' (y - x)))" + + show "((\y. norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)) \ 0) (at x within s)" + using f g by (intro tendsto_add_zero) (auto simp: has_derivative_iff_norm) + + fix y :: 'a assume "y \ x" + show "norm (?R y) / norm (y - x) \ norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)" + unfolding add_divide_distrib [symmetric] + by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt]) +qed simp + +lemmas has_derivative_fst [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst] +lemmas has_derivative_snd [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd] + +lemma has_derivative_split [derivative_intros]: + "((\p. f (fst p) (snd p)) has_derivative f') F \ ((\(a, b). f a b) has_derivative f') F" + unfolding split_beta' . + +subsection \Product is an inner product space\ + +instantiation prod :: (real_inner, real_inner) real_inner +begin + +definition inner_prod_def: + "inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)" + +lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d" + unfolding inner_prod_def by simp + +instance +proof + fix r :: real + fix x y z :: "'a::real_inner \ 'b::real_inner" + show "inner x y = inner y x" + unfolding inner_prod_def + by (simp add: inner_commute) + show "inner (x + y) z = inner x z + inner y z" + unfolding inner_prod_def + by (simp add: inner_add_left) + show "inner (scaleR r x) y = r * inner x y" + unfolding inner_prod_def + by (simp add: distrib_left) + show "0 \ inner x x" + unfolding inner_prod_def + by (intro add_nonneg_nonneg inner_ge_zero) + show "inner x x = 0 \ x = 0" + unfolding inner_prod_def prod_eq_iff + by (simp add: add_nonneg_eq_0_iff) + show "norm x = sqrt (inner x x)" + unfolding norm_prod_def inner_prod_def + by (simp add: power2_norm_eq_inner) +qed + +end + +lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a" + by (cases x, simp)+ + +lemma + fixes x :: "'a::real_normed_vector" + shows norm_Pair1 [simp]: "norm (0,x) = norm x" + and norm_Pair2 [simp]: "norm (x,0) = norm x" +by (auto simp: norm_Pair) + +lemma norm_commute: "norm (x,y) = norm (y,x)" + by (simp add: norm_Pair) + +lemma norm_fst_le: "norm x \ norm (x,y)" + by (metis dist_fst_le fst_conv fst_zero norm_conv_dist) + +lemma norm_snd_le: "norm y \ norm (x,y)" + by (metis dist_snd_le snd_conv snd_zero norm_conv_dist) + +end diff -r 3b6a3632e754 -r da89140186e2 src/HOL/Library/Inner_Product.thy --- a/src/HOL/Library/Inner_Product.thy Fri Sep 30 15:35:32 2016 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,402 +0,0 @@ -(* Title: HOL/Library/Inner_Product.thy - Author: Brian Huffman -*) - -section \Inner Product Spaces and the Gradient Derivative\ - -theory Inner_Product -imports "~~/src/HOL/Complex_Main" -begin - -subsection \Real inner product spaces\ - -text \ - Temporarily relax type constraints for @{term "open"}, @{term "uniformity"}, - @{term dist}, and @{term norm}. -\ - -setup \Sign.add_const_constraint - (@{const_name "open"}, SOME @{typ "'a::open set \ bool"})\ - -setup \Sign.add_const_constraint - (@{const_name dist}, SOME @{typ "'a::dist \ 'a \ real"})\ - -setup \Sign.add_const_constraint - (@{const_name uniformity}, SOME @{typ "('a::uniformity \ 'a) filter"})\ - -setup \Sign.add_const_constraint - (@{const_name norm}, SOME @{typ "'a::norm \ real"})\ - -class real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity + - fixes inner :: "'a \ 'a \ real" - assumes inner_commute: "inner x y = inner y x" - and inner_add_left: "inner (x + y) z = inner x z + inner y z" - and inner_scaleR_left [simp]: "inner (scaleR r x) y = r * (inner x y)" - and inner_ge_zero [simp]: "0 \ inner x x" - and inner_eq_zero_iff [simp]: "inner x x = 0 \ x = 0" - and norm_eq_sqrt_inner: "norm x = sqrt (inner x x)" -begin - -lemma inner_zero_left [simp]: "inner 0 x = 0" - using inner_add_left [of 0 0 x] by simp - -lemma inner_minus_left [simp]: "inner (- x) y = - inner x y" - using inner_add_left [of x "- x" y] by simp - -lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z" - using inner_add_left [of x "- y" z] by simp - -lemma inner_setsum_left: "inner (\x\A. f x) y = (\x\A. inner (f x) y)" - by (cases "finite A", induct set: finite, simp_all add: inner_add_left) - -text \Transfer distributivity rules to right argument.\ - -lemma inner_add_right: "inner x (y + z) = inner x y + inner x z" - using inner_add_left [of y z x] by (simp only: inner_commute) - -lemma inner_scaleR_right [simp]: "inner x (scaleR r y) = r * (inner x y)" - using inner_scaleR_left [of r y x] by (simp only: inner_commute) - -lemma inner_zero_right [simp]: "inner x 0 = 0" - using inner_zero_left [of x] by (simp only: inner_commute) - -lemma inner_minus_right [simp]: "inner x (- y) = - inner x y" - using inner_minus_left [of y x] by (simp only: inner_commute) - -lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z" - using inner_diff_left [of y z x] by (simp only: inner_commute) - -lemma inner_setsum_right: "inner x (\y\A. f y) = (\y\A. inner x (f y))" - using inner_setsum_left [of f A x] by (simp only: inner_commute) - -lemmas inner_add [algebra_simps] = inner_add_left inner_add_right -lemmas inner_diff [algebra_simps] = inner_diff_left inner_diff_right -lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right - -text \Legacy theorem names\ -lemmas inner_left_distrib = inner_add_left -lemmas inner_right_distrib = inner_add_right -lemmas inner_distrib = inner_left_distrib inner_right_distrib - -lemma inner_gt_zero_iff [simp]: "0 < inner x x \ x \ 0" - by (simp add: order_less_le) - -lemma power2_norm_eq_inner: "(norm x)\<^sup>2 = inner x x" - by (simp add: norm_eq_sqrt_inner) - -text \Identities involving real multiplication and division.\ - -lemma inner_mult_left: "inner (of_real m * a) b = m * (inner a b)" - by (metis real_inner_class.inner_scaleR_left scaleR_conv_of_real) - -lemma inner_mult_right: "inner a (of_real m * b) = m * (inner a b)" - by (metis real_inner_class.inner_scaleR_right scaleR_conv_of_real) - -lemma inner_mult_left': "inner (a * of_real m) b = m * (inner a b)" - by (simp add: of_real_def) - -lemma inner_mult_right': "inner a (b * of_real m) = (inner a b) * m" - by (simp add: of_real_def real_inner_class.inner_scaleR_right) - -lemma Cauchy_Schwarz_ineq: - "(inner x y)\<^sup>2 \ inner x x * inner y y" -proof (cases) - assume "y = 0" - thus ?thesis by simp -next - assume y: "y \ 0" - let ?r = "inner x y / inner y y" - have "0 \ inner (x - scaleR ?r y) (x - scaleR ?r y)" - by (rule inner_ge_zero) - also have "\ = inner x x - inner y x * ?r" - by (simp add: inner_diff) - also have "\ = inner x x - (inner x y)\<^sup>2 / inner y y" - by (simp add: power2_eq_square inner_commute) - finally have "0 \ inner x x - (inner x y)\<^sup>2 / inner y y" . - hence "(inner x y)\<^sup>2 / inner y y \ inner x x" - by (simp add: le_diff_eq) - thus "(inner x y)\<^sup>2 \ inner x x * inner y y" - by (simp add: pos_divide_le_eq y) -qed - -lemma Cauchy_Schwarz_ineq2: - "\inner x y\ \ norm x * norm y" -proof (rule power2_le_imp_le) - have "(inner x y)\<^sup>2 \ inner x x * inner y y" - using Cauchy_Schwarz_ineq . - thus "\inner x y\\<^sup>2 \ (norm x * norm y)\<^sup>2" - by (simp add: power_mult_distrib power2_norm_eq_inner) - show "0 \ norm x * norm y" - unfolding norm_eq_sqrt_inner - by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero) -qed - -lemma norm_cauchy_schwarz: "inner x y \ norm x * norm y" - using Cauchy_Schwarz_ineq2 [of x y] by auto - -subclass real_normed_vector -proof - fix a :: real and x y :: 'a - show "norm x = 0 \ x = 0" - unfolding norm_eq_sqrt_inner by simp - show "norm (x + y) \ norm x + norm y" - proof (rule power2_le_imp_le) - have "inner x y \ norm x * norm y" - by (rule norm_cauchy_schwarz) - thus "(norm (x + y))\<^sup>2 \ (norm x + norm y)\<^sup>2" - unfolding power2_sum power2_norm_eq_inner - by (simp add: inner_add inner_commute) - show "0 \ norm x + norm y" - unfolding norm_eq_sqrt_inner by simp - qed - have "sqrt (a\<^sup>2 * inner x x) = \a\ * sqrt (inner x x)" - by (simp add: real_sqrt_mult_distrib) - then show "norm (a *\<^sub>R x) = \a\ * norm x" - unfolding norm_eq_sqrt_inner - by (simp add: power2_eq_square mult.assoc) -qed - -end - -lemma inner_divide_left: - fixes a :: "'a :: {real_inner,real_div_algebra}" - shows "inner (a / of_real m) b = (inner a b) / m" - by (metis (no_types) divide_inverse inner_commute inner_scaleR_right mult.left_neutral mult.right_neutral mult_scaleR_right of_real_inverse scaleR_conv_of_real times_divide_eq_left) - -lemma inner_divide_right: - fixes a :: "'a :: {real_inner,real_div_algebra}" - shows "inner a (b / of_real m) = (inner a b) / m" - by (metis inner_commute inner_divide_left) - -text \ - Re-enable constraints for @{term "open"}, @{term "uniformity"}, - @{term dist}, and @{term norm}. -\ - -setup \Sign.add_const_constraint - (@{const_name "open"}, SOME @{typ "'a::topological_space set \ bool"})\ - -setup \Sign.add_const_constraint - (@{const_name uniformity}, SOME @{typ "('a::uniform_space \ 'a) filter"})\ - -setup \Sign.add_const_constraint - (@{const_name dist}, SOME @{typ "'a::metric_space \ 'a \ real"})\ - -setup \Sign.add_const_constraint - (@{const_name norm}, SOME @{typ "'a::real_normed_vector \ real"})\ - -lemma bounded_bilinear_inner: - "bounded_bilinear (inner::'a::real_inner \ 'a \ real)" -proof - fix x y z :: 'a and r :: real - show "inner (x + y) z = inner x z + inner y z" - by (rule inner_add_left) - show "inner x (y + z) = inner x y + inner x z" - by (rule inner_add_right) - show "inner (scaleR r x) y = scaleR r (inner x y)" - unfolding real_scaleR_def by (rule inner_scaleR_left) - show "inner x (scaleR r y) = scaleR r (inner x y)" - unfolding real_scaleR_def by (rule inner_scaleR_right) - show "\K. \x y::'a. norm (inner x y) \ norm x * norm y * K" - proof - show "\x y::'a. norm (inner x y) \ norm x * norm y * 1" - by (simp add: Cauchy_Schwarz_ineq2) - qed -qed - -lemmas tendsto_inner [tendsto_intros] = - bounded_bilinear.tendsto [OF bounded_bilinear_inner] - -lemmas isCont_inner [simp] = - bounded_bilinear.isCont [OF bounded_bilinear_inner] - -lemmas has_derivative_inner [derivative_intros] = - bounded_bilinear.FDERIV [OF bounded_bilinear_inner] - -lemmas bounded_linear_inner_left = - bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner] - -lemmas bounded_linear_inner_right = - bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner] - -lemmas bounded_linear_inner_left_comp = bounded_linear_inner_left[THEN bounded_linear_compose] - -lemmas bounded_linear_inner_right_comp = bounded_linear_inner_right[THEN bounded_linear_compose] - -lemmas has_derivative_inner_right [derivative_intros] = - bounded_linear.has_derivative [OF bounded_linear_inner_right] - -lemmas has_derivative_inner_left [derivative_intros] = - bounded_linear.has_derivative [OF bounded_linear_inner_left] - -lemma differentiable_inner [simp]: - "f differentiable (at x within s) \ g differentiable at x within s \ (\x. inner (f x) (g x)) differentiable at x within s" - unfolding differentiable_def by (blast intro: has_derivative_inner) - - -subsection \Class instances\ - -instantiation real :: real_inner -begin - -definition inner_real_def [simp]: "inner = op *" - -instance -proof - fix x y z r :: real - show "inner x y = inner y x" - unfolding inner_real_def by (rule mult.commute) - show "inner (x + y) z = inner x z + inner y z" - unfolding inner_real_def by (rule distrib_right) - show "inner (scaleR r x) y = r * inner x y" - unfolding inner_real_def real_scaleR_def by (rule mult.assoc) - show "0 \ inner x x" - unfolding inner_real_def by simp - show "inner x x = 0 \ x = 0" - unfolding inner_real_def by simp - show "norm x = sqrt (inner x x)" - unfolding inner_real_def by simp -qed - -end - -lemma - shows real_inner_1_left[simp]: "inner 1 x = x" - and real_inner_1_right[simp]: "inner x 1 = x" - by simp_all - -instantiation complex :: real_inner -begin - -definition inner_complex_def: - "inner x y = Re x * Re y + Im x * Im y" - -instance -proof - fix x y z :: complex and r :: real - show "inner x y = inner y x" - unfolding inner_complex_def by (simp add: mult.commute) - show "inner (x + y) z = inner x z + inner y z" - unfolding inner_complex_def by (simp add: distrib_right) - show "inner (scaleR r x) y = r * inner x y" - unfolding inner_complex_def by (simp add: distrib_left) - show "0 \ inner x x" - unfolding inner_complex_def by simp - show "inner x x = 0 \ x = 0" - unfolding inner_complex_def - by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff) - show "norm x = sqrt (inner x x)" - unfolding inner_complex_def complex_norm_def - by (simp add: power2_eq_square) -qed - -end - -lemma complex_inner_1 [simp]: "inner 1 x = Re x" - unfolding inner_complex_def by simp - -lemma complex_inner_1_right [simp]: "inner x 1 = Re x" - unfolding inner_complex_def by simp - -lemma complex_inner_ii_left [simp]: "inner \ x = Im x" - unfolding inner_complex_def by simp - -lemma complex_inner_ii_right [simp]: "inner x \ = Im x" - unfolding inner_complex_def by simp - - -subsection \Gradient derivative\ - -definition - gderiv :: - "['a::real_inner \ real, 'a, 'a] \ bool" - ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) -where - "GDERIV f x :> D \ FDERIV f x :> (\h. inner h D)" - -lemma gderiv_deriv [simp]: "GDERIV f x :> D \ DERIV f x :> D" - by (simp only: gderiv_def has_field_derivative_def inner_real_def mult_commute_abs) - -lemma GDERIV_DERIV_compose: - "\GDERIV f x :> df; DERIV g (f x) :> dg\ - \ GDERIV (\x. g (f x)) x :> scaleR dg df" - unfolding gderiv_def has_field_derivative_def - apply (drule (1) has_derivative_compose) - apply (simp add: ac_simps) - done - -lemma has_derivative_subst: "\FDERIV f x :> df; df = d\ \ FDERIV f x :> d" - by simp - -lemma GDERIV_subst: "\GDERIV f x :> df; df = d\ \ GDERIV f x :> d" - by simp - -lemma GDERIV_const: "GDERIV (\x. k) x :> 0" - unfolding gderiv_def inner_zero_right by (rule has_derivative_const) - -lemma GDERIV_add: - "\GDERIV f x :> df; GDERIV g x :> dg\ - \ GDERIV (\x. f x + g x) x :> df + dg" - unfolding gderiv_def inner_add_right by (rule has_derivative_add) - -lemma GDERIV_minus: - "GDERIV f x :> df \ GDERIV (\x. - f x) x :> - df" - unfolding gderiv_def inner_minus_right by (rule has_derivative_minus) - -lemma GDERIV_diff: - "\GDERIV f x :> df; GDERIV g x :> dg\ - \ GDERIV (\x. f x - g x) x :> df - dg" - unfolding gderiv_def inner_diff_right by (rule has_derivative_diff) - -lemma GDERIV_scaleR: - "\DERIV f x :> df; GDERIV g x :> dg\ - \ GDERIV (\x. scaleR (f x) (g x)) x - :> (scaleR (f x) dg + scaleR df (g x))" - unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right - apply (rule has_derivative_subst) - apply (erule (1) has_derivative_scaleR) - apply (simp add: ac_simps) - done - -lemma GDERIV_mult: - "\GDERIV f x :> df; GDERIV g x :> dg\ - \ GDERIV (\x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df" - unfolding gderiv_def - apply (rule has_derivative_subst) - apply (erule (1) has_derivative_mult) - apply (simp add: inner_add ac_simps) - done - -lemma GDERIV_inverse: - "\GDERIV f x :> df; f x \ 0\ - \ GDERIV (\x. inverse (f x)) x :> - (inverse (f x))\<^sup>2 *\<^sub>R df" - apply (erule GDERIV_DERIV_compose) - apply (erule DERIV_inverse [folded numeral_2_eq_2]) - done - -lemma GDERIV_norm: - assumes "x \ 0" shows "GDERIV (\x. norm x) x :> sgn x" -proof - - have 1: "FDERIV (\x. inner x x) x :> (\h. inner x h + inner h x)" - by (intro has_derivative_inner has_derivative_ident) - have 2: "(\h. inner x h + inner h x) = (\h. inner h (scaleR 2 x))" - by (simp add: fun_eq_iff inner_commute) - have "0 < inner x x" using \x \ 0\ by simp - then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)" - by (rule DERIV_real_sqrt) - have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x" - by (simp add: sgn_div_norm norm_eq_sqrt_inner) - show ?thesis - unfolding norm_eq_sqrt_inner - apply (rule GDERIV_subst [OF _ 4]) - apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"]) - apply (subst gderiv_def) - apply (rule has_derivative_subst [OF _ 2]) - apply (rule 1) - apply (rule 3) - done -qed - -lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def] - -end diff -r 3b6a3632e754 -r da89140186e2 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Fri Sep 30 15:35:32 2016 +0200 +++ b/src/HOL/Library/Library.thy Fri Sep 30 15:35:37 2016 +0200 @@ -37,7 +37,6 @@ Groups_Big_Fun Indicator_Function Infinite_Set - Inner_Product IArray Lattice_Algebras Lattice_Syntax @@ -62,7 +61,7 @@ Polynomial Polynomial_FPS Preorder - Product_Vector + Product_plus Quadratic_Discriminant Quotient_List Quotient_Option diff -r 3b6a3632e754 -r da89140186e2 src/HOL/Library/Product_Vector.thy --- a/src/HOL/Library/Product_Vector.thy Fri Sep 30 15:35:32 2016 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,369 +0,0 @@ -(* Title: HOL/Library/Product_Vector.thy - Author: Brian Huffman -*) - -section \Cartesian Products as Vector Spaces\ - -theory Product_Vector -imports Inner_Product Product_plus -begin - -subsection \Product is a real vector space\ - -instantiation prod :: (real_vector, real_vector) real_vector -begin - -definition scaleR_prod_def: - "scaleR r A = (scaleR r (fst A), scaleR r (snd A))" - -lemma fst_scaleR [simp]: "fst (scaleR r A) = scaleR r (fst A)" - unfolding scaleR_prod_def by simp - -lemma snd_scaleR [simp]: "snd (scaleR r A) = scaleR r (snd A)" - unfolding scaleR_prod_def by simp - -lemma scaleR_Pair [simp]: "scaleR r (a, b) = (scaleR r a, scaleR r b)" - unfolding scaleR_prod_def by simp - -instance -proof - fix a b :: real and x y :: "'a \ 'b" - show "scaleR a (x + y) = scaleR a x + scaleR a y" - by (simp add: prod_eq_iff scaleR_right_distrib) - show "scaleR (a + b) x = scaleR a x + scaleR b x" - by (simp add: prod_eq_iff scaleR_left_distrib) - show "scaleR a (scaleR b x) = scaleR (a * b) x" - by (simp add: prod_eq_iff) - show "scaleR 1 x = x" - by (simp add: prod_eq_iff) -qed - -end - -subsection \Product is a metric space\ - -(* TODO: Product of uniform spaces and compatibility with metric_spaces! *) - -instantiation prod :: (metric_space, metric_space) dist -begin - -definition dist_prod_def[code del]: - "dist x y = sqrt ((dist (fst x) (fst y))\<^sup>2 + (dist (snd x) (snd y))\<^sup>2)" - -instance .. -end - -instantiation prod :: (metric_space, metric_space) uniformity_dist -begin - -definition [code del]: - "(uniformity :: (('a \ 'b) \ ('a \ 'b)) filter) = - (INF e:{0 <..}. principal {(x, y). dist x y < e})" - -instance - by standard (rule uniformity_prod_def) -end - -declare uniformity_Abort[where 'a="'a :: metric_space \ 'b :: metric_space", code] - -instantiation prod :: (metric_space, metric_space) metric_space -begin - -lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)" - unfolding dist_prod_def by simp - -lemma dist_fst_le: "dist (fst x) (fst y) \ dist x y" - unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge1) - -lemma dist_snd_le: "dist (snd x) (snd y) \ dist x y" - unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2) - -instance -proof - fix x y :: "'a \ 'b" - show "dist x y = 0 \ x = y" - unfolding dist_prod_def prod_eq_iff by simp -next - fix x y z :: "'a \ 'b" - show "dist x y \ dist x z + dist y z" - unfolding dist_prod_def - by (intro order_trans [OF _ real_sqrt_sum_squares_triangle_ineq] - real_sqrt_le_mono add_mono power_mono dist_triangle2 zero_le_dist) -next - fix S :: "('a \ 'b) set" - have *: "open S \ (\x\S. \e>0. \y. dist y x < e \ y \ S)" - proof - assume "open S" show "\x\S. \e>0. \y. dist y x < e \ y \ S" - proof - fix x assume "x \ S" - obtain A B where "open A" "open B" "x \ A \ B" "A \ B \ S" - using \open S\ and \x \ S\ by (rule open_prod_elim) - obtain r where r: "0 < r" "\y. dist y (fst x) < r \ y \ A" - using \open A\ and \x \ A \ B\ unfolding open_dist by auto - obtain s where s: "0 < s" "\y. dist y (snd x) < s \ y \ B" - using \open B\ and \x \ A \ B\ unfolding open_dist by auto - let ?e = "min r s" - have "0 < ?e \ (\y. dist y x < ?e \ y \ S)" - proof (intro allI impI conjI) - show "0 < min r s" by (simp add: r(1) s(1)) - next - fix y assume "dist y x < min r s" - hence "dist y x < r" and "dist y x < s" - by simp_all - hence "dist (fst y) (fst x) < r" and "dist (snd y) (snd x) < s" - by (auto intro: le_less_trans dist_fst_le dist_snd_le) - hence "fst y \ A" and "snd y \ B" - by (simp_all add: r(2) s(2)) - hence "y \ A \ B" by (induct y, simp) - with \A \ B \ S\ show "y \ S" .. - qed - thus "\e>0. \y. dist y x < e \ y \ S" .. - qed - next - assume *: "\x\S. \e>0. \y. dist y x < e \ y \ S" show "open S" - proof (rule open_prod_intro) - fix x assume "x \ S" - then obtain e where "0 < e" and S: "\y. dist y x < e \ y \ S" - using * by fast - define r where "r = e / sqrt 2" - define s where "s = e / sqrt 2" - from \0 < e\ have "0 < r" and "0 < s" - unfolding r_def s_def by simp_all - from \0 < e\ have "e = sqrt (r\<^sup>2 + s\<^sup>2)" - unfolding r_def s_def by (simp add: power_divide) - define A where "A = {y. dist (fst x) y < r}" - define B where "B = {y. dist (snd x) y < s}" - have "open A" and "open B" - unfolding A_def B_def by (simp_all add: open_ball) - moreover have "x \ A \ B" - unfolding A_def B_def mem_Times_iff - using \0 < r\ and \0 < s\ by simp - moreover have "A \ B \ S" - proof (clarify) - fix a b assume "a \ A" and "b \ B" - hence "dist a (fst x) < r" and "dist b (snd x) < s" - unfolding A_def B_def by (simp_all add: dist_commute) - hence "dist (a, b) x < e" - unfolding dist_prod_def \e = sqrt (r\<^sup>2 + s\<^sup>2)\ - by (simp add: add_strict_mono power_strict_mono) - thus "(a, b) \ S" - by (simp add: S) - qed - ultimately show "\A B. open A \ open B \ x \ A \ B \ A \ B \ S" by fast - qed - qed - show "open S = (\x\S. \\<^sub>F (x', y) in uniformity. x' = x \ y \ S)" - unfolding * eventually_uniformity_metric - by (simp del: split_paired_All add: dist_prod_def dist_commute) -qed - -end - -declare [[code abort: "dist::('a::metric_space*'b::metric_space)\('a*'b) \ real"]] - -lemma Cauchy_fst: "Cauchy X \ Cauchy (\n. fst (X n))" - unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le]) - -lemma Cauchy_snd: "Cauchy X \ Cauchy (\n. snd (X n))" - unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_snd_le]) - -lemma Cauchy_Pair: - assumes "Cauchy X" and "Cauchy Y" - shows "Cauchy (\n. (X n, Y n))" -proof (rule metric_CauchyI) - fix r :: real assume "0 < r" - hence "0 < r / sqrt 2" (is "0 < ?s") by simp - obtain M where M: "\m\M. \n\M. dist (X m) (X n) < ?s" - using metric_CauchyD [OF \Cauchy X\ \0 < ?s\] .. - obtain N where N: "\m\N. \n\N. dist (Y m) (Y n) < ?s" - using metric_CauchyD [OF \Cauchy Y\ \0 < ?s\] .. - have "\m\max M N. \n\max M N. dist (X m, Y m) (X n, Y n) < r" - using M N by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair) - then show "\n0. \m\n0. \n\n0. dist (X m, Y m) (X n, Y n) < r" .. -qed - -subsection \Product is a complete metric space\ - -instance prod :: (complete_space, complete_space) complete_space -proof - fix X :: "nat \ 'a \ 'b" assume "Cauchy X" - have 1: "(\n. fst (X n)) \ lim (\n. fst (X n))" - using Cauchy_fst [OF \Cauchy X\] - by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) - have 2: "(\n. snd (X n)) \ lim (\n. snd (X n))" - using Cauchy_snd [OF \Cauchy X\] - by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) - have "X \ (lim (\n. fst (X n)), lim (\n. snd (X n)))" - using tendsto_Pair [OF 1 2] by simp - then show "convergent X" - by (rule convergentI) -qed - -subsection \Product is a normed vector space\ - -instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector -begin - -definition norm_prod_def[code del]: - "norm x = sqrt ((norm (fst x))\<^sup>2 + (norm (snd x))\<^sup>2)" - -definition sgn_prod_def: - "sgn (x::'a \ 'b) = scaleR (inverse (norm x)) x" - -lemma norm_Pair: "norm (a, b) = sqrt ((norm a)\<^sup>2 + (norm b)\<^sup>2)" - unfolding norm_prod_def by simp - -instance -proof - fix r :: real and x y :: "'a \ 'b" - show "norm x = 0 \ x = 0" - unfolding norm_prod_def - by (simp add: prod_eq_iff) - show "norm (x + y) \ norm x + norm y" - unfolding norm_prod_def - apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq]) - apply (simp add: add_mono power_mono norm_triangle_ineq) - done - show "norm (scaleR r x) = \r\ * norm x" - unfolding norm_prod_def - apply (simp add: power_mult_distrib) - apply (simp add: distrib_left [symmetric]) - apply (simp add: real_sqrt_mult_distrib) - done - show "sgn x = scaleR (inverse (norm x)) x" - by (rule sgn_prod_def) - show "dist x y = norm (x - y)" - unfolding dist_prod_def norm_prod_def - by (simp add: dist_norm) -qed - -end - -declare [[code abort: "norm::('a::real_normed_vector*'b::real_normed_vector) \ real"]] - -instance prod :: (banach, banach) banach .. - -subsubsection \Pair operations are linear\ - -lemma bounded_linear_fst: "bounded_linear fst" - using fst_add fst_scaleR - by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def) - -lemma bounded_linear_snd: "bounded_linear snd" - using snd_add snd_scaleR - by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def) - -lemmas bounded_linear_fst_comp = bounded_linear_fst[THEN bounded_linear_compose] - -lemmas bounded_linear_snd_comp = bounded_linear_snd[THEN bounded_linear_compose] - -lemma bounded_linear_Pair: - assumes f: "bounded_linear f" - assumes g: "bounded_linear g" - shows "bounded_linear (\x. (f x, g x))" -proof - interpret f: bounded_linear f by fact - interpret g: bounded_linear g by fact - fix x y and r :: real - show "(f (x + y), g (x + y)) = (f x, g x) + (f y, g y)" - by (simp add: f.add g.add) - show "(f (r *\<^sub>R x), g (r *\<^sub>R x)) = r *\<^sub>R (f x, g x)" - by (simp add: f.scaleR g.scaleR) - obtain Kf where "0 < Kf" and norm_f: "\x. norm (f x) \ norm x * Kf" - using f.pos_bounded by fast - obtain Kg where "0 < Kg" and norm_g: "\x. norm (g x) \ norm x * Kg" - using g.pos_bounded by fast - have "\x. norm (f x, g x) \ norm x * (Kf + Kg)" - apply (rule allI) - apply (simp add: norm_Pair) - apply (rule order_trans [OF sqrt_add_le_add_sqrt], simp, simp) - apply (simp add: distrib_left) - apply (rule add_mono [OF norm_f norm_g]) - done - then show "\K. \x. norm (f x, g x) \ norm x * K" .. -qed - -subsubsection \Frechet derivatives involving pairs\ - -lemma has_derivative_Pair [derivative_intros]: - assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)" - shows "((\x. (f x, g x)) has_derivative (\h. (f' h, g' h))) (at x within s)" -proof (rule has_derivativeI_sandwich[of 1]) - show "bounded_linear (\h. (f' h, g' h))" - using f g by (intro bounded_linear_Pair has_derivative_bounded_linear) - let ?Rf = "\y. f y - f x - f' (y - x)" - let ?Rg = "\y. g y - g x - g' (y - x)" - let ?R = "\y. ((f y, g y) - (f x, g x) - (f' (y - x), g' (y - x)))" - - show "((\y. norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)) \ 0) (at x within s)" - using f g by (intro tendsto_add_zero) (auto simp: has_derivative_iff_norm) - - fix y :: 'a assume "y \ x" - show "norm (?R y) / norm (y - x) \ norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)" - unfolding add_divide_distrib [symmetric] - by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt]) -qed simp - -lemmas has_derivative_fst [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst] -lemmas has_derivative_snd [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd] - -lemma has_derivative_split [derivative_intros]: - "((\p. f (fst p) (snd p)) has_derivative f') F \ ((\(a, b). f a b) has_derivative f') F" - unfolding split_beta' . - -subsection \Product is an inner product space\ - -instantiation prod :: (real_inner, real_inner) real_inner -begin - -definition inner_prod_def: - "inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)" - -lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d" - unfolding inner_prod_def by simp - -instance -proof - fix r :: real - fix x y z :: "'a::real_inner \ 'b::real_inner" - show "inner x y = inner y x" - unfolding inner_prod_def - by (simp add: inner_commute) - show "inner (x + y) z = inner x z + inner y z" - unfolding inner_prod_def - by (simp add: inner_add_left) - show "inner (scaleR r x) y = r * inner x y" - unfolding inner_prod_def - by (simp add: distrib_left) - show "0 \ inner x x" - unfolding inner_prod_def - by (intro add_nonneg_nonneg inner_ge_zero) - show "inner x x = 0 \ x = 0" - unfolding inner_prod_def prod_eq_iff - by (simp add: add_nonneg_eq_0_iff) - show "norm x = sqrt (inner x x)" - unfolding norm_prod_def inner_prod_def - by (simp add: power2_norm_eq_inner) -qed - -end - -lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a" - by (cases x, simp)+ - -lemma - fixes x :: "'a::real_normed_vector" - shows norm_Pair1 [simp]: "norm (0,x) = norm x" - and norm_Pair2 [simp]: "norm (x,0) = norm x" -by (auto simp: norm_Pair) - -lemma norm_commute: "norm (x,y) = norm (y,x)" - by (simp add: norm_Pair) - -lemma norm_fst_le: "norm x \ norm (x,y)" - by (metis dist_fst_le fst_conv fst_zero norm_conv_dist) - -lemma norm_snd_le: "norm y \ norm (x,y)" - by (metis dist_snd_le snd_conv snd_zero norm_conv_dist) - -end diff -r 3b6a3632e754 -r da89140186e2 src/HOL/Mirabelle/ex/Ex.thy --- a/src/HOL/Mirabelle/ex/Ex.thy Fri Sep 30 15:35:32 2016 +0200 +++ b/src/HOL/Mirabelle/ex/Ex.thy Fri Sep 30 15:35:37 2016 +0200 @@ -3,7 +3,7 @@ ML \ val rc = Isabelle_System.bash - "cd \"$ISABELLE_HOME/src/HOL/Library\"; isabelle mirabelle arith Inner_Product.thy"; + "cd \"$ISABELLE_HOME/src/HOL/Analysis\"; isabelle mirabelle arith Inner_Product.thy"; if rc <> 0 then error ("Mirabelle example failed: " ^ string_of_int rc) else (); \ \ "some arbitrary small test case"