# HG changeset patch # User huffman # Date 1313701719 25200 # Node ID 637297cf614222462c2febed0deb65848f2d3213 # Parent d27b9fe4759e8bc08a35e1d94086d86d5a52f4a8# Parent f0de18b62d63a97af37dfcedb475d28e27ec5fb2 merged diff -r d27b9fe4759e -r 637297cf6142 NEWS --- a/NEWS Thu Aug 18 22:50:28 2011 +0200 +++ b/NEWS Thu Aug 18 14:08:39 2011 -0700 @@ -199,6 +199,19 @@ tendsto_vector ~> vec_tendstoI Cauchy_vector ~> vec_CauchyI +* Complex_Main: The locale interpretations for the bounded_linear and +bounded_bilinear locales have been removed, in order to reduce the +number of duplicate lemmas. Users must use the original names for +distributivity theorems, potential INCOMPATIBILITY. + + divide.add ~> add_divide_distrib + divide.diff ~> diff_divide_distrib + divide.setsum ~> setsum_divide_distrib + mult.add_right ~> right_distrib + mult.diff_right ~> right_diff_distrib + mult_right.setsum ~> setsum_right_distrib + mult_left.diff ~> left_diff_distrib + *** Document preparation *** diff -r d27b9fe4759e -r 637297cf6142 src/HOL/Import/HOLLightReal.thy --- a/src/HOL/Import/HOLLightReal.thy Thu Aug 18 22:50:28 2011 +0200 +++ b/src/HOL/Import/HOLLightReal.thy Thu Aug 18 14:08:39 2011 -0700 @@ -112,7 +112,7 @@ lemma REAL_DIFFSQ: "((x :: real) + y) * (x - y) = x * x - y * y" - by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) mult.add_right mult_diff_mult) + by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) right_distrib mult_diff_mult) lemma REAL_ABS_TRIANGLE_LE: "abs (x :: real) + abs (y - x) \ z \ abs y \ z" @@ -295,7 +295,7 @@ (\(x :: real). 0 * x = 0) \ (\(x :: real) y z. x * (y + z) = x * y + x * z) \ (\(x :: real). x ^ 0 = 1) \ (\(x :: real) n. x ^ Suc n = x * x ^ n)" - by (auto simp add: mult.add_right) + by (auto simp add: right_distrib) lemma REAL_COMPLETE: "(\(x :: real). P x) \ (\(M :: real). \x. P x \ x \ M) \ diff -r d27b9fe4759e -r 637297cf6142 src/HOL/Library/Convex.thy --- a/src/HOL/Library/Convex.thy Thu Aug 18 22:50:28 2011 +0200 +++ b/src/HOL/Library/Convex.thy Thu Aug 18 14:08:39 2011 -0700 @@ -129,7 +129,7 @@ have "(\ j \ insert i s. a j) = 1" using asms by auto hence "(\ j \ s. a j) = 1 - a i" using setsum.insert asms by fastsimp hence "(\ j \ s. a j) / (1 - a i) = 1" using i0 by auto - hence a1: "(\ j \ s. ?a j) = 1" unfolding divide.setsum by simp + hence a1: "(\ j \ s. ?a j) = 1" unfolding setsum_divide_distrib by simp from this asms have "(\j\s. ?a j *\<^sub>R y j) \ C" using a_nonneg by fastsimp hence "a i *\<^sub>R y i + (1 - a i) *\<^sub>R (\ j \ s. ?a j *\<^sub>R y j) \ C" @@ -410,7 +410,7 @@ have "(\ j \ insert i s. a j) = 1" using asms by auto hence "(\ j \ s. a j) = 1 - a i" using setsum.insert asms by fastsimp hence "(\ j \ s. a j) / (1 - a i) = 1" using i0 by auto - hence a1: "(\ j \ s. ?a j) = 1" unfolding divide.setsum by simp + hence a1: "(\ j \ s. ?a j) = 1" unfolding setsum_divide_distrib by simp have "convex C" using asms by auto hence asum: "(\ j \ s. ?a j *\<^sub>R y j) \ C" using asms convex_setsum[OF `finite s` @@ -433,7 +433,7 @@ using add_right_mono[OF mult_left_mono[of _ _ "1 - a i", OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp also have "\ = (\ j \ s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)" - unfolding mult_right.setsum[of "1 - a i" "\ j. ?a j * f (y j)"] using i0 by auto + unfolding setsum_right_distrib[of "1 - a i" "\ j. ?a j * f (y j)"] using i0 by auto also have "\ = (\ j \ s. a j * f (y j)) + a i * f (y i)" using i0 by auto also have "\ = (\ j \ insert i s. a j * f (y j))" using asms by auto finally have "f (\ j \ insert i s. a j *\<^sub>R y j) \ (\ j \ insert i s. a j * f (y j))" diff -r d27b9fe4759e -r 637297cf6142 src/HOL/Library/FrechetDeriv.thy --- a/src/HOL/Library/FrechetDeriv.thy Thu Aug 18 22:50:28 2011 +0200 +++ b/src/HOL/Library/FrechetDeriv.thy Thu Aug 18 14:08:39 2011 -0700 @@ -5,7 +5,7 @@ header {* Frechet Derivative *} theory FrechetDeriv -imports Lim Complex_Main +imports Complex_Main begin definition @@ -398,9 +398,11 @@ by (simp only: FDERIV_lemma) qed -lemmas FDERIV_mult = mult.FDERIV +lemmas FDERIV_mult = + bounded_bilinear.FDERIV [OF bounded_bilinear_mult] -lemmas FDERIV_scaleR = scaleR.FDERIV +lemmas FDERIV_scaleR = + bounded_bilinear.FDERIV [OF bounded_bilinear_scaleR] subsection {* Powers *} @@ -427,10 +429,10 @@ subsection {* Inverse *} lemmas bounded_linear_mult_const = - mult.bounded_linear_left [THEN bounded_linear_compose] + bounded_linear_mult_left [THEN bounded_linear_compose] lemmas bounded_linear_const_mult = - mult.bounded_linear_right [THEN bounded_linear_compose] + bounded_linear_mult_right [THEN bounded_linear_compose] lemma FDERIV_inverse: fixes x :: "'a::real_normed_div_algebra" @@ -510,7 +512,7 @@ fixes x :: "'a::real_normed_field" shows "FDERIV f x :> (\h. h * D) = (\h. (f (x + h) - f x) / h) -- 0 --> D" apply (unfold fderiv_def) - apply (simp add: mult.bounded_linear_left) + apply (simp add: bounded_linear_mult_left) apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric]) apply (subst diff_divide_distrib) apply (subst times_divide_eq_left [symmetric]) diff -r d27b9fe4759e -r 637297cf6142 src/HOL/Library/Inner_Product.thy --- a/src/HOL/Library/Inner_Product.thy Thu Aug 18 22:50:28 2011 +0200 +++ b/src/HOL/Library/Inner_Product.thy Thu Aug 18 14:08:39 2011 -0700 @@ -5,7 +5,7 @@ header {* Inner Product Spaces and the Gradient Derivative *} theory Inner_Product -imports Complex_Main FrechetDeriv +imports FrechetDeriv begin subsection {* Real inner product spaces *} @@ -43,6 +43,9 @@ lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z" by (simp add: diff_minus inner_add_left) +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" @@ -60,6 +63,9 @@ 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 @@ -148,8 +154,8 @@ setup {* Sign.add_const_constraint (@{const_name norm}, SOME @{typ "'a::real_normed_vector \ real"}) *} -interpretation inner: - bounded_bilinear "inner::'a::real_inner \ 'a \ 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" @@ -167,15 +173,20 @@ qed qed -interpretation inner_left: - bounded_linear "\x::'a::real_inner. inner x y" - by (rule inner.bounded_linear_left) +lemmas tendsto_inner [tendsto_intros] = + bounded_bilinear.tendsto [OF bounded_bilinear_inner] + +lemmas isCont_inner [simp] = + bounded_bilinear.isCont [OF bounded_bilinear_inner] -interpretation inner_right: - bounded_linear "\y::'a::real_inner. inner x y" - by (rule inner.bounded_linear_right) +lemmas FDERIV_inner = + bounded_bilinear.FDERIV [OF bounded_bilinear_inner] -declare inner.isCont [simp] +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] subsection {* Class instances *} @@ -260,29 +271,29 @@ by simp lemma GDERIV_const: "GDERIV (\x. k) x :> 0" - unfolding gderiv_def inner_right.zero by (rule FDERIV_const) + unfolding gderiv_def inner_zero_right by (rule FDERIV_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_right.add by (rule FDERIV_add) + unfolding gderiv_def inner_add_right by (rule FDERIV_add) lemma GDERIV_minus: "GDERIV f x :> df \ GDERIV (\x. - f x) x :> - df" - unfolding gderiv_def inner_right.minus by (rule FDERIV_minus) + unfolding gderiv_def inner_minus_right by (rule FDERIV_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_right.diff by (rule FDERIV_diff) + unfolding gderiv_def inner_diff_right by (rule FDERIV_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 deriv_fderiv inner_right.add inner_right.scaleR + unfolding gderiv_def deriv_fderiv inner_add_right inner_scaleR_right apply (rule FDERIV_subst) - apply (erule (1) scaleR.FDERIV) + apply (erule (1) FDERIV_scaleR) apply (simp add: mult_ac) done @@ -306,7 +317,7 @@ 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 inner.FDERIV FDERIV_ident) + by (intro FDERIV_inner FDERIV_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 diff -r d27b9fe4759e -r 637297cf6142 src/HOL/Library/Product_Vector.thy --- a/src/HOL/Library/Product_Vector.thy Thu Aug 18 22:50:28 2011 +0200 +++ b/src/HOL/Library/Product_Vector.thy Thu Aug 18 14:08:39 2011 -0700 @@ -489,11 +489,11 @@ subsection {* Pair operations are linear *} -interpretation fst: bounded_linear fst +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) -interpretation snd: bounded_linear snd +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) diff -r d27b9fe4759e -r 637297cf6142 src/HOL/Lim.thy --- a/src/HOL/Lim.thy Thu Aug 18 22:50:28 2011 +0200 +++ b/src/HOL/Lim.thy Thu Aug 18 14:08:39 2011 -0700 @@ -321,17 +321,23 @@ "f -- a --> 0 \ (\x. c ** f x) -- a --> 0" by (rule tendsto_right_zero) -lemmas LIM_mult = mult.LIM +lemmas LIM_mult = + bounded_bilinear.LIM [OF bounded_bilinear_mult] -lemmas LIM_mult_zero = mult.LIM_prod_zero +lemmas LIM_mult_zero = + bounded_bilinear.LIM_prod_zero [OF bounded_bilinear_mult] -lemmas LIM_mult_left_zero = mult.LIM_left_zero +lemmas LIM_mult_left_zero = + bounded_bilinear.LIM_left_zero [OF bounded_bilinear_mult] -lemmas LIM_mult_right_zero = mult.LIM_right_zero +lemmas LIM_mult_right_zero = + bounded_bilinear.LIM_right_zero [OF bounded_bilinear_mult] -lemmas LIM_scaleR = scaleR.LIM +lemmas LIM_scaleR = + bounded_bilinear.LIM [OF bounded_bilinear_scaleR] -lemmas LIM_of_real = of_real.LIM +lemmas LIM_of_real = + bounded_linear.LIM [OF bounded_linear_of_real] lemma LIM_power: fixes f :: "'a::topological_space \ 'b::{power,real_normed_algebra}" @@ -446,11 +452,11 @@ "\isCont f a; isCont g a\ \ isCont (\x. f x ** g x) a" unfolding isCont_def by (rule LIM) -lemmas isCont_scaleR [simp] = scaleR.isCont +lemmas isCont_scaleR [simp] = + bounded_bilinear.isCont [OF bounded_bilinear_scaleR] -lemma isCont_of_real [simp]: - "isCont f a \ isCont (\x. of_real (f x)::'b::real_normed_algebra_1) a" - by (rule of_real.isCont) +lemmas isCont_of_real [simp] = + bounded_linear.isCont [OF bounded_linear_of_real] lemma isCont_power [simp]: fixes f :: "'a::topological_space \ 'b::{power,real_normed_algebra}" diff -r d27b9fe4759e -r 637297cf6142 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Thu Aug 18 22:50:28 2011 +0200 +++ b/src/HOL/Limits.thy Thu Aug 18 14:08:39 2011 -0700 @@ -510,9 +510,9 @@ "Zfun f F \ Zfun (\x. a ** f x) F" by (rule bounded_linear_right [THEN bounded_linear.Zfun]) -lemmas Zfun_mult = mult.Zfun -lemmas Zfun_mult_right = mult.Zfun_right -lemmas Zfun_mult_left = mult.Zfun_left +lemmas Zfun_mult = bounded_bilinear.Zfun [OF bounded_bilinear_mult] +lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult] +lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult] subsection {* Limits *} @@ -752,7 +752,7 @@ subsubsection {* Linear operators and multiplication *} -lemma (in bounded_linear) tendsto [tendsto_intros]: +lemma (in bounded_linear) tendsto: "(g ---> a) F \ ((\x. f (g x)) ---> f a) F" by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun) @@ -760,7 +760,7 @@ "(g ---> 0) F \ ((\x. f (g x)) ---> 0) F" by (drule tendsto, simp only: zero) -lemma (in bounded_bilinear) tendsto [tendsto_intros]: +lemma (in bounded_bilinear) tendsto: "\(f ---> a) F; (g ---> b) F\ \ ((\x. f x ** g x) ---> a ** b) F" by (simp only: tendsto_Zfun_iff prod_diff_prod Zfun_add Zfun Zfun_left Zfun_right) @@ -779,7 +779,14 @@ "(f ---> 0) F \ ((\x. c ** f x) ---> 0) F" by (rule bounded_linear.tendsto_zero [OF bounded_linear_right]) -lemmas tendsto_mult = mult.tendsto +lemmas tendsto_of_real [tendsto_intros] = + bounded_linear.tendsto [OF bounded_linear_of_real] + +lemmas tendsto_scaleR [tendsto_intros] = + bounded_bilinear.tendsto [OF bounded_bilinear_scaleR] + +lemmas tendsto_mult [tendsto_intros] = + bounded_bilinear.tendsto [OF bounded_bilinear_mult] lemma tendsto_power [tendsto_intros]: fixes f :: "'a \ 'b::{power,real_normed_algebra}" @@ -897,7 +904,7 @@ apply (erule (1) inverse_diff_inverse) apply (rule Zfun_minus) apply (rule Zfun_mult_left) - apply (rule mult.Bfun_prod_Zfun) + apply (rule bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult]) apply (erule (1) Bfun_inverse) apply (simp add: tendsto_Zfun_iff) done @@ -921,7 +928,7 @@ fixes a b :: "'a::real_normed_field" shows "\(f ---> a) F; (g ---> b) F; b \ 0\ \ ((\x. f x / g x) ---> a / b) F" - by (simp add: mult.tendsto tendsto_inverse divide_inverse) + by (simp add: tendsto_mult tendsto_inverse divide_inverse) lemma tendsto_sgn [tendsto_intros]: fixes l :: "'a::real_normed_vector" diff -r d27b9fe4759e -r 637297cf6142 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Aug 18 22:50:28 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Aug 18 14:08:39 2011 -0700 @@ -1202,7 +1202,7 @@ show "\(f z - z) $$ i\ < d / real n" unfolding euclidean_simps proof(rule *) show "\f x $$ i - x $$ i\ \ norm (f y -f x) + norm (y - x)" apply(rule lem1[rule_format]) using as i by auto show "\f x $$ i - f z $$ i\ \ norm (f x - f z)" "\x $$ i - z $$ i\ \ norm (x - z)" - unfolding euclidean_component.diff[THEN sym] by(rule component_le_norm)+ + unfolding euclidean_component_diff[THEN sym] by(rule component_le_norm)+ have tria:"norm (y - x) \ norm (y - z) + norm (x - z)" using dist_triangle[of y x z,unfolded dist_norm] unfolding norm_minus_commute by auto also have "\ < e / 2 + e / 2" apply(rule add_strict_mono) using as(4,5) by auto @@ -1234,7 +1234,7 @@ assume as:"\i\{1..n}. x i \ p" "i \ {1..n}" { assume "x i = p \ x i = 0" have "(\\ i. real (x (b' i)) / real p) \ {0::'a..\\ i. 1}" unfolding mem_interval - apply safe unfolding euclidean_lambda_beta euclidean_component.zero + apply safe unfolding euclidean_lambda_beta euclidean_component_zero proof (simp_all only: if_P) fix j assume j':"j {1..n}" using b' unfolding n_def bij_betw_def by auto show "0 \ real (x (b' j)) / real p" @@ -1262,11 +1262,11 @@ have "\i {0..i {0..p}" apply-apply(rule,erule_tac x=i in allE) by auto hence "z\{0..\\ i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta - unfolding euclidean_component.zero apply (simp_all only: if_P) + unfolding euclidean_component_zero apply (simp_all only: if_P) apply(rule divide_nonneg_pos) using `p>0` unfolding divide_le_eq_1 by auto hence d_fz_z:"d \ norm (f z - z)" apply(drule_tac d) . case goal1 hence as:"\if z $$ i - z $$ i\ < d / real n" using `n>0` by(auto simp add:not_le) - have "norm (f z - z) \ (\if z $$ i - z $$ i\)" unfolding euclidean_component.diff[THEN sym] by(rule norm_le_l1) + have "norm (f z - z) \ (\if z $$ i - z $$ i\)" unfolding euclidean_component_diff[THEN sym] by(rule norm_le_l1) also have "\ < (\i = d" unfolding real_eq_of_nat n_def using n using DIM_positive[where 'a='a] by auto finally show False using d_fz_z by auto qed then guess i .. note i=this @@ -1276,15 +1276,15 @@ def r' \ "(\\ i. real (r (b' i)) / real p)::'a" have "\i. i r (b' i) \ p" apply(rule order_trans) apply(rule rs(1)[OF b'_im,THEN conjunct2]) using q(1)[rule_format,OF b'_im] by(auto simp add: Suc_le_eq) - hence "r' \ {0..\\ i. 1}" unfolding r'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component.zero + hence "r' \ {0..\\ i. 1}" unfolding r'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero apply (simp only: if_P) apply(rule divide_nonneg_pos) using rs(1)[OF b'_im] q(1)[rule_format,OF b'_im] `p>0` by auto def s' \ "(\\ i. real (s (b' i)) / real p)::'a" have "\i. i s (b' i) \ p" apply(rule order_trans) apply(rule rs(2)[OF b'_im,THEN conjunct2]) using q(1)[rule_format,OF b'_im] by(auto simp add: Suc_le_eq) - hence "s' \ {0..\\ i.1}" unfolding s'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component.zero + hence "s' \ {0..\\ i.1}" unfolding s'_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero apply (simp_all only: if_P) apply(rule divide_nonneg_pos) using rs(1)[OF b'_im] q(1)[rule_format,OF b'_im] `p>0` by auto - have "z\{0..\\ i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component.zero + have "z\{0..\\ i.1}" unfolding z_def mem_interval apply safe unfolding euclidean_lambda_beta euclidean_component_zero apply (simp_all only: if_P) apply(rule divide_nonneg_pos) using q(1)[rule_format,OF b'_im] `p>0` by(auto intro:less_imp_le) have *:"\x. 1 + real x = real (Suc x)" by auto { have "(\ireal (r (b' i)) - real (q (b' i))\) \ (\iy y1 y2 d dx::real. (y1\y\y2\y) \ (y\y1\y\y2) \ d < abs dx \ abs(y1 - y - - dx) \ d \ (abs (y2 - y - dx) \ d) \ False" by arith show False apply(rule ***[OF **, where dx="d * D $ k $ j" and d="\D $ k $ j\ / 2 * \d\"]) using *[of "-d"] and *[of d] and d[THEN conjunct1] and j unfolding mult_minus_left - unfolding abs_mult diff_minus_eq_add scaleR.minus_left unfolding algebra_simps by (auto intro: mult_pos_pos) + unfolding abs_mult diff_minus_eq_add scaleR_minus_left unfolding algebra_simps by (auto intro: mult_pos_pos) qed subsection {* Lemmas for working on @{typ "real^1"} *} diff -r d27b9fe4759e -r 637297cf6142 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Aug 18 22:50:28 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Aug 18 14:08:39 2011 -0700 @@ -18,7 +18,7 @@ (* ------------------------------------------------------------------------- *) lemma linear_scaleR: "linear (%(x :: 'n::euclidean_space). scaleR c x)" - by (metis linear_conv_bounded_linear scaleR.bounded_linear_right) + by (metis linear_conv_bounded_linear bounded_linear_scaleR_right) lemma injective_scaleR: assumes "(c :: real) ~= 0" @@ -128,7 +128,7 @@ proof- have *:"\x a b P. x * (if P then a else b) = (if P then x*a else x*b)" by auto have **:"finite d" apply(rule finite_subset[OF assms]) by fastsimp have ***:"\i. (setsum (%i. f i *\<^sub>R ((basis i)::'a)) d) $$ i = (\x\d. if x = i then f x else 0)" - unfolding euclidean_component.setsum euclidean_scaleR basis_component * + unfolding euclidean_component_setsum euclidean_component_scaleR basis_component * apply(rule setsum_cong2) using assms by auto show ?thesis unfolding euclidean_eq[where 'a='a] *** setsum_delta[OF **] using assms by auto qed @@ -1175,7 +1175,7 @@ have u2:"u2 \ 1" unfolding obt2(3)[THEN sym] and not_le using obt2(2) by auto have "u1 * u + u2 * v \ (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono) apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto - also have "\ \ 1" unfolding mult.add_right[THEN sym] and as(3) using u1 u2 by auto + also have "\ \ 1" unfolding right_distrib[THEN sym] and as(3) using u1 u2 by auto finally show "u *\<^sub>R x + v *\<^sub>R y \ ?hull" unfolding mem_Collect_eq apply(rule_tac x="u * u1 + v * u2" in exI) apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def @@ -2229,7 +2229,7 @@ have *:"y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using `e>0` by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib) have "x : affine hull S" using assms hull_subset[of S] by auto moreover have "1 / e + - ((1 - e) / e) = 1" - using `e>0` mult_left.diff[of "1" "(1-e)" "1/e"] by auto + using `e>0` left_diff_distrib[of "1" "(1-e)" "1/e"] by auto ultimately have **: "(1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x : affine hull S" using as affine_affine_hull[of S] mem_affine[of "affine hull S" y x "(1 / e)" "-((1 - e) / e)"] by (simp add: algebra_simps) have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)" @@ -2957,7 +2957,7 @@ thus ?thesis apply(rule_tac x="basis 0" in exI, rule_tac x=1 in exI) using True using DIM_positive[where 'a='a] by auto next case False thus ?thesis using False using separating_hyperplane_closed_point[OF assms] - apply - apply(erule exE)+ unfolding inner.zero_right apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed + apply - apply(erule exE)+ unfolding inner_zero_right apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed subsection {* Now set-to-set for closed/compact sets. *} @@ -3053,7 +3053,7 @@ apply(rule,rule,rule,rule,rule,rule,rule,rule,rule) apply(erule_tac exE)+ apply(rule_tac x="\n. u *\<^sub>R xb n + v *\<^sub>R xc n" in exI) apply(rule,rule) apply(rule assms[unfolded convex_def, rule_format]) prefer 6 - by (auto intro: tendsto_intros) + by (auto intro!: tendsto_intros) lemma convex_interior: fixes s :: "'a::real_normed_vector set" @@ -3221,13 +3221,13 @@ ultimately have "z \ convex hull {v \ c. u v \ 0}" unfolding convex_hull_explicit mem_Collect_eq apply(rule_tac x="{v \ c. u v < 0}" in exI, rule_tac x="\y. inverse (setsum u {x\c. u x > 0}) * - u y" in exI) using assms(1) unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] and z_def - by(auto simp add: setsum_negf mult_right.setsum[THEN sym]) + by(auto simp add: setsum_negf setsum_right_distrib[THEN sym]) moreover have "\x\{v \ c. 0 < u v}. 0 \ inverse (setsum u {x \ c. 0 < u x}) * u x" apply (rule) apply (rule mult_nonneg_nonneg) using * by auto hence "z \ convex hull {v \ c. u v > 0}" unfolding convex_hull_explicit mem_Collect_eq apply(rule_tac x="{v \ c. 0 < u v}" in exI, rule_tac x="\y. inverse (setsum u {x\c. u x > 0}) * u y" in exI) using assms(1) unfolding scaleR_scaleR[THEN sym] scaleR_right.setsum [symmetric] and z_def using * - by(auto simp add: setsum_negf mult_right.setsum[THEN sym]) + by(auto simp add: setsum_negf setsum_right_distrib[THEN sym]) ultimately show ?thesis apply(rule_tac x="{v\c. u v \ 0}" in exI, rule_tac x="{v\c. u v > 0}" in exI) by auto qed @@ -4157,7 +4157,7 @@ let ?D = "{..j. if i = j then inverse (2 * real DIM('a)) else 0) ?D"]) apply(rule setsum_cong2) defer apply(subst setsum_delta') unfolding euclidean_component_def using i by(auto simp add:dot_basis) } note ** = this @@ -4270,7 +4270,7 @@ { fix i assume "i:d" have "?a $$ i = inverse (2 * real (card d))" unfolding * setsum_reindex[OF basis_inj_on, OF assms(2)] o_def apply(rule trans[of _ "setsum (\j. if i = j then inverse (2 * real (card d)) else 0) ?D"]) - unfolding euclidean_component.setsum + unfolding euclidean_component_setsum apply(rule setsum_cong2) using `i:d` `finite d` setsum_delta'[of d i "(%k. inverse (2 * real (card d)))"] d1 assms(2) by (auto simp add: Euclidean_Space.basis_component[of i])} @@ -4678,7 +4678,7 @@ hence x1: "x1 : affine hull S" using e1_def hull_subset[of S] by auto def x2 == "z+ e2 *\<^sub>R (z-x)" hence x2: "x2 : affine hull S" using e2_def hull_subset[of S] by auto - have *: "e1/(e1+e2) + e2/(e1+e2) = 1" using divide.add[of e1 e2 "e1+e2"] e1_def e2_def by simp + have *: "e1/(e1+e2) + e2/(e1+e2) = 1" using add_divide_distrib[of e1 e2 "e1+e2"] e1_def e2_def by simp hence "z = (e2/(e1+e2)) *\<^sub>R x1 + (e1/(e1+e2)) *\<^sub>R x2" using x1_def x2_def apply (auto simp add: algebra_simps) using scaleR_left_distrib[of "e1/(e1+e2)" "e2/(e1+e2)" z] by auto diff -r d27b9fe4759e -r 637297cf6142 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Aug 18 22:50:28 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu Aug 18 14:08:39 2011 -0700 @@ -93,13 +93,13 @@ proof - have "((\t. (f t - (f x + y * (t - x))) / \t - x\) ---> 0) (at x within ({x<..} \ I)) \ ((\t. (f t - f x) / (t - x) - y) ---> 0) (at x within ({x<..} \ I))" - by (intro Lim_cong_within) (auto simp add: divide.diff divide.add) + by (intro Lim_cong_within) (auto simp add: diff_divide_distrib add_divide_distrib) also have "\ \ ((\t. (f t - f x) / (t - x)) ---> y) (at x within ({x<..} \ I))" by (simp add: Lim_null[symmetric]) also have "\ \ ((\t. (f x - f t) / (x - t)) ---> y) (at x within ({x<..} \ I))" by (intro Lim_cong_within) (simp_all add: field_simps) finally show ?thesis - by (simp add: mult.bounded_linear_right has_derivative_within) + by (simp add: bounded_linear_mult_right has_derivative_within) qed lemma bounded_linear_imp_linear: "bounded_linear f \ linear f" (* TODO: move elsewhere *) @@ -140,10 +140,31 @@ apply (simp add: local.scaleR local.diff local.add local.zero) done +lemmas scaleR_right_has_derivative = + bounded_linear.has_derivative [OF bounded_linear_scaleR_right, standard] + +lemmas scaleR_left_has_derivative = + bounded_linear.has_derivative [OF bounded_linear_scaleR_left, standard] + +lemmas inner_right_has_derivative = + bounded_linear.has_derivative [OF bounded_linear_inner_right, standard] + +lemmas inner_left_has_derivative = + bounded_linear.has_derivative [OF bounded_linear_inner_left, standard] + +lemmas mult_right_has_derivative = + bounded_linear.has_derivative [OF bounded_linear_mult_right, standard] + +lemmas mult_left_has_derivative = + bounded_linear.has_derivative [OF bounded_linear_mult_left, standard] + +lemmas euclidean_component_has_derivative = + bounded_linear.has_derivative [OF bounded_linear_euclidean_component] + lemma has_derivative_neg: assumes "(f has_derivative f') net" shows "((\x. -(f x)) has_derivative (\h. -(f' h))) net" - using scaleR_right.has_derivative [where r="-1", OF assms] by auto + using scaleR_right_has_derivative [where r="-1", OF assms] by auto lemma has_derivative_add: assumes "(f has_derivative f') net" and "(g has_derivative g') net" @@ -181,9 +202,9 @@ has_derivative_id has_derivative_const has_derivative_add has_derivative_sub has_derivative_neg has_derivative_add_const - scaleR_left.has_derivative scaleR_right.has_derivative - inner_left.has_derivative inner_right.has_derivative - euclidean_component.has_derivative + scaleR_left_has_derivative scaleR_right_has_derivative + inner_left_has_derivative inner_right_has_derivative + euclidean_component_has_derivative subsubsection {* Limit transformation for derivatives *} @@ -459,7 +480,7 @@ "f differentiable net \ (\x. c *\<^sub>R f(x)) differentiable (net::'a::real_normed_vector filter)" unfolding differentiable_def - apply(erule exE, drule scaleR_right.has_derivative) by auto + apply(erule exE, drule scaleR_right_has_derivative) by auto lemma differentiable_neg [intro]: "f differentiable net \ @@ -693,7 +714,7 @@ show False apply(rule ***[OF **, where dx="d * ?D k $$ j" and d="\?D k $$ j\ / 2 * \d\"]) using *[of "-d"] and *[of d] and d[THEN conjunct1] and j unfolding mult_minus_left - unfolding abs_mult diff_minus_eq_add scaleR.minus_left + unfolding abs_mult diff_minus_eq_add scaleR_minus_left unfolding algebra_simps by (auto intro: mult_pos_pos) qed @@ -769,7 +790,7 @@ fix x assume x:"x \ {a<..x. f x - (f b - f a) / (b - a) * x) has_derivative (\xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)" by (intro has_derivative_intros assms(3)[rule_format,OF x] - mult_right.has_derivative) + mult_right_has_derivative) qed(insert assms(1), auto simp add:field_simps) then guess x .. thus ?thesis apply(rule_tac x=x in bexI) @@ -1740,7 +1761,7 @@ lemma has_vector_derivative_cmul: "(f has_vector_derivative f') net \ ((\x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net" unfolding has_vector_derivative_def - apply (drule scaleR_right.has_derivative) + apply (drule scaleR_right_has_derivative) by (auto simp add: algebra_simps) lemma has_vector_derivative_cmul_eq: @@ -1819,7 +1840,7 @@ shows "((g \ f) has_vector_derivative (f' *\<^sub>R g')) (at x)" using assms(2) unfolding has_vector_derivative_def apply- apply(drule diff_chain_at[OF assms(1)[unfolded has_vector_derivative_def]]) - unfolding o_def scaleR.scaleR_left by auto + unfolding o_def real_scaleR_def scaleR_scaleR . lemma vector_diff_chain_within: assumes "(f has_vector_derivative f') (at x within s)" @@ -1827,6 +1848,6 @@ shows "((g o f) has_vector_derivative (f' *\<^sub>R g')) (at x within s)" using assms(2) unfolding has_vector_derivative_def apply- apply(drule diff_chain_within[OF assms(1)[unfolded has_vector_derivative_def]]) - unfolding o_def scaleR.scaleR_left by auto + unfolding o_def real_scaleR_def scaleR_scaleR . end diff -r d27b9fe4759e -r 637297cf6142 src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Aug 18 22:50:28 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Aug 18 14:08:39 2011 -0700 @@ -118,20 +118,38 @@ lemma bounded_linear_euclidean_component: "bounded_linear (\x. euclidean_component x i)" unfolding euclidean_component_def - by (rule inner.bounded_linear_right) + by (rule bounded_linear_inner_right) + +lemmas tendsto_euclidean_component [tendsto_intros] = + bounded_linear.tendsto [OF bounded_linear_euclidean_component] + +lemmas isCont_euclidean_component [simp] = + bounded_linear.isCont [OF bounded_linear_euclidean_component] + +lemma euclidean_component_zero: "0 $$ i = 0" + unfolding euclidean_component_def by (rule inner_zero_right) -interpretation euclidean_component: - bounded_linear "\x. euclidean_component x i" - by (rule bounded_linear_euclidean_component) +lemma euclidean_component_add: "(x + y) $$ i = x $$ i + y $$ i" + unfolding euclidean_component_def by (rule inner_add_right) + +lemma euclidean_component_diff: "(x - y) $$ i = x $$ i - y $$ i" + unfolding euclidean_component_def by (rule inner_diff_right) -declare euclidean_component.isCont [simp] +lemma euclidean_component_minus: "(- x) $$ i = - (x $$ i)" + unfolding euclidean_component_def by (rule inner_minus_right) + +lemma euclidean_component_scaleR: "(scaleR a x) $$ i = a * (x $$ i)" + unfolding euclidean_component_def by (rule inner_scaleR_right) + +lemma euclidean_component_setsum: "(\x\A. f x) $$ i = (\x\A. f x $$ i)" + unfolding euclidean_component_def by (rule inner_setsum_right) lemma euclidean_eqI: fixes x y :: "'a::euclidean_space" assumes "\i. i < DIM('a) \ x $$ i = y $$ i" shows "x = y" proof - from assms have "\i DIM('a)" shows "x $$ i = 0" unfolding euclidean_component_def basis_zero[OF assms] by simp -lemma euclidean_scaleR: - shows "(a *\<^sub>R x) $$ i = a * (x$$i)" - unfolding euclidean_component_def by auto - lemmas euclidean_simps = - euclidean_component.add - euclidean_component.diff - euclidean_scaleR - euclidean_component.minus - euclidean_component.setsum + euclidean_component_add + euclidean_component_diff + euclidean_component_scaleR + euclidean_component_minus + euclidean_component_setsum basis_component lemma euclidean_representation: fixes x :: "'a::euclidean_space" shows "x = (\iR basis i)" apply (rule euclidean_eqI) - apply (simp add: euclidean_component.setsum euclidean_component.scaleR) + apply (simp add: euclidean_component_setsum euclidean_component_scaleR) apply (simp add: if_distrib setsum_delta cong: if_cong) done @@ -180,7 +194,7 @@ lemma euclidean_lambda_beta [simp]: "((\\ i. f i)::'a::euclidean_space) $$ j = (if j < DIM('a) then f j else 0)" - by (auto simp: euclidean_component.setsum euclidean_component.scaleR + by (auto simp: euclidean_component_setsum euclidean_component_scaleR Chi_def if_distrib setsum_cases intro!: setsum_cong) lemma euclidean_lambda_beta': @@ -201,7 +215,7 @@ lemma euclidean_inner: "inner x (y::'a) = (\ix$$i\ \ norm (x::'a::euclidean_space)" diff -r d27b9fe4759e -r 637297cf6142 src/HOL/Multivariate_Analysis/Fashoda.thy --- a/src/HOL/Multivariate_Analysis/Fashoda.thy Thu Aug 18 22:50:28 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Thu Aug 18 14:08:39 2011 -0700 @@ -66,7 +66,7 @@ apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\0" have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto thus "(0 < sqprojection x $ i) = (0 < x $ i)" "(sqprojection x $ i < 0) = (x $ i < 0)" - unfolding sqprojection_def vector_component_simps vec_nth.scaleR real_scaleR_def + unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed note lem3 = this[rule_format] have x1:"x $ 1 \ {- 1..1::real}" "x $ 2 \ {- 1..1::real}" using x(1) unfolding mem_interval_cart by auto diff -r d27b9fe4759e -r 637297cf6142 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Aug 18 22:50:28 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Aug 18 14:08:39 2011 -0700 @@ -401,14 +401,15 @@ unfolding norm_vec_def by (rule member_le_setL2) simp_all -interpretation vec_nth: bounded_linear "\x. x $ i" +lemma bounded_linear_vec_nth: "bounded_linear (\x. x $ i)" apply default apply (rule vector_add_component) apply (rule vector_scaleR_component) apply (rule_tac x="1" in exI, simp add: norm_nth_le) done -declare vec_nth.isCont [simp] +lemmas isCont_vec_nth [simp] = + bounded_linear.isCont [OF bounded_linear_vec_nth] instance vec :: (banach, finite) banach .. diff -r d27b9fe4759e -r 637297cf6142 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Thu Aug 18 22:50:28 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Thu Aug 18 14:08:39 2011 -0700 @@ -16,7 +16,7 @@ lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff - scaleR_cancel_left scaleR_cancel_right scaleR.add_right scaleR.add_left real_vector_class.scaleR_one + scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one lemma real_arch_invD: "0 < (e::real) \ (\n::nat. n \ 0 \ 0 < inverse (real n) \ inverse (real n) < e)" @@ -1225,7 +1225,7 @@ lemma has_integral_cmul: shows "(f has_integral k) s \ ((\x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s" unfolding o_def[THEN sym] apply(rule has_integral_linear,assumption) - by(rule scaleR.bounded_linear_right) + by(rule bounded_linear_scaleR_right) lemma has_integral_neg: shows "(f has_integral k) s \ ((\x. -(f x)) has_integral (-k)) s" @@ -2262,7 +2262,7 @@ assumes "p tagged_division_of {a..b}" "\x\{a..b}. norm(f x - g x) \ e" shows "norm(setsum (\(x,k). content k *\<^sub>R f x) p - setsum (\(x,k). content k *\<^sub>R g x) p) \ e * content({a..b})" apply(rule order_trans[OF _ rsum_bound[OF assms]]) apply(rule eq_refl) apply(rule arg_cong[where f=norm]) - unfolding setsum_subtractf[THEN sym] apply(rule setsum_cong2) unfolding scaleR.diff_right by auto + unfolding setsum_subtractf[THEN sym] apply(rule setsum_cong2) unfolding scaleR_diff_right by auto lemma has_integral_bound: fixes f::"'a::ordered_euclidean_space \ 'b::real_normed_vector" assumes "0 \ B" "(f has_integral i) ({a..b})" "\x\{a..b}. norm(f x) \ B" @@ -2287,7 +2287,7 @@ lemma rsum_component_le: fixes f::"'a::ordered_euclidean_space \ 'b::euclidean_space" assumes "p tagged_division_of {a..b}" "\x\{a..b}. (f x)$$i \ (g x)$$i" shows "(setsum (\(x,k). content k *\<^sub>R f x) p)$$i \ (setsum (\(x,k). content k *\<^sub>R g x) p)$$i" - unfolding euclidean_component.setsum apply(rule setsum_mono) apply safe + unfolding euclidean_component_setsum apply(rule setsum_mono) apply safe proof- fix a b assume ab:"(a,b) \ p" note assm = tagged_division_ofD(2-4)[OF assms(1) ab] from this(3) guess u v apply-by(erule exE)+ note b=this show "(content b *\<^sub>R f a) $$ i \ (content b *\<^sub>R g a) $$ i" unfolding b @@ -2988,7 +2988,7 @@ have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \ norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)" apply(rule order_trans[OF _ norm_triangle_ineq4]) apply(rule eq_refl) apply(rule arg_cong[where f=norm]) - unfolding scaleR.diff_left by(auto simp add:algebra_simps) + unfolding scaleR_diff_left by(auto simp add:algebra_simps) also have "... \ e * norm (u - x) + e * norm (v - x)" apply(rule add_mono) apply(rule d(2)[of "x" "u",unfolded o_def]) prefer 4 apply(rule d(2)[of "x" "v",unfolded o_def]) @@ -3123,7 +3123,7 @@ assumes "continuous_on {a..b} f" "x \ {a..b}" shows "((\u. integral {a..u} f) has_vector_derivative f(x)) (at x within {a..b})" unfolding has_vector_derivative_def has_derivative_within_alt -apply safe apply(rule scaleR.bounded_linear_left) +apply safe apply(rule bounded_linear_scaleR_left) proof- fix e::real assume e:"e>0" note compact_uniformly_continuous[OF assms(1) compact_interval,unfolded uniformly_continuous_on_def] from this[rule_format,OF e] guess d apply-by(erule conjE exE)+ note d=this[rule_format] @@ -3223,8 +3223,8 @@ have "(\(x, k)\(\(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\(x, k)\p. content k *\<^sub>R f (g x)) - i" (is "?l = _") unfolding algebra_simps add_left_cancel unfolding setsum_reindex[OF *] apply(subst scaleR_right.setsum) defer apply(rule setsum_cong2) unfolding o_def split_paired_all split_conv apply(drule p(4)) apply safe unfolding assms(7)[rule_format] using p by auto - also have "... = r *\<^sub>R ((\(x, k)\p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") unfolding scaleR.diff_right scaleR.scaleR_left[THEN sym] - unfolding real_scaleR_def using assms(1) by auto finally have *:"?l = ?r" . + also have "... = r *\<^sub>R ((\(x, k)\p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") unfolding scaleR_diff_right scaleR_scaleR + using assms(1) by auto finally have *:"?l = ?r" . show "norm ((\(x, k)\p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e" using ** unfolding * unfolding norm_scaleR using assms(1) by(auto simp add:field_simps) qed qed qed @@ -3256,7 +3256,7 @@ lemma has_integral_affinity: fixes a::"'a::ordered_euclidean_space" assumes "(f has_integral i) {a..b}" "m \ 0" shows "((\x. f(m *\<^sub>R x + c)) has_integral ((1 / (abs(m) ^ DIM('a))) *\<^sub>R i)) ((\x. (1 / m) *\<^sub>R x + -((1 / m) *\<^sub>R c)) ` {a..b})" apply(rule has_integral_twiddle,safe) apply(rule zero_less_power) unfolding euclidean_eq[where 'a='a] - unfolding scaleR_right_distrib euclidean_simps scaleR.scaleR_left[THEN sym] + unfolding scaleR_right_distrib euclidean_simps scaleR_scaleR defer apply(insert assms(2), simp add:field_simps) apply(insert assms(2), simp add:field_simps) apply(rule continuous_intros)+ apply(rule interval_image_affinity_interval)+ apply(rule content_image_affinity_interval) using assms by auto @@ -3442,7 +3442,7 @@ show ?case unfolding content_real[OF assms(1)] and *[of "\x. x"] *[of f] setsum_subtractf[THEN sym] split_minus unfolding setsum_right_distrib apply(subst(2) pA,subst pA) unfolding setsum_Un_disjoint[OF pA(2-)] proof(rule norm_triangle_le,rule **) - case goal1 show ?case apply(rule order_trans,rule setsum_norm_le) defer apply(subst divide.setsum) + case goal1 show ?case apply(rule order_trans,rule setsum_norm_le) defer apply(subst setsum_divide_distrib) proof(rule order_refl,safe,unfold not_le o_def split_conv fst_conv,rule ccontr) fix x k assume as:"(x,k) \ p" "e * (interval_upperbound k - interval_lowerbound k) / 2 < norm (content k *\<^sub>R f' x - (f (interval_upperbound k) - f (interval_lowerbound k)))" @@ -4159,7 +4159,7 @@ "(\(x, k)\p2. content k *\<^sub>R f x) - (\(x, k)\p2. content k *\<^sub>R g x) \ 0" "0 \ (\(x, k)\p1. content k *\<^sub>R h x) - (\(x, k)\p1. content k *\<^sub>R f x)" unfolding setsum_subtractf[THEN sym] apply- apply(rule_tac[!] setsum_nonneg) - apply safe unfolding real_scaleR_def mult.diff_right[THEN sym] + apply safe unfolding real_scaleR_def right_diff_distrib[THEN sym] apply(rule_tac[!] mult_nonneg_nonneg) proof- fix a b assume ab:"(a,b) \ p1" show "0 \ content b" using *(3)[OF ab] apply safe using content_pos_le . thus "0 \ content b" . @@ -4535,7 +4535,7 @@ show ?case apply(rule order_trans[of _ "\(x, k)\p. content k * (e / (4 * content {a..b}))"]) unfolding setsum_subtractf[THEN sym] apply(rule order_trans,rule norm_setsum) apply(rule setsum_mono) unfolding split_paired_all split_conv - unfolding split_def setsum_left_distrib[THEN sym] scaleR.diff_right[THEN sym] + unfolding split_def setsum_left_distrib[THEN sym] scaleR_diff_right[THEN sym] unfolding additive_content_tagged_division[OF p(1), unfolded split_def] proof- fix x k assume xk:"(x,k) \ p" hence x:"x\{a..b}" using p'(2-3)[OF xk] by auto from p'(4)[OF xk] guess u v apply-by(erule exE)+ note uv=this @@ -5202,7 +5202,7 @@ proof- have *:"\x. ((\\ i. abs(f x$$i))::'c::ordered_euclidean_space) = (setsum (\i. (((\y. (\\ j. if j = i then y else 0)) o (((\x. (norm((\\ j. if j = i then x$$i else 0)::'c::ordered_euclidean_space))) o f))) x)) {..i xa. ((if i = xa then f x $$ xa else 0) * (if i = xa then f x $$ xa else 0)) = (if i = xa then (f x $$ xa) * (f x $$ xa) else 0)" by auto @@ -5220,7 +5220,7 @@ apply(rule absolutely_integrable_linear) unfolding o_def apply(rule absolutely_integrable_norm) apply(rule absolutely_integrable_linear[OF assms,unfolded o_def]) unfolding linear_linear apply(rule_tac[!] linearI) unfolding euclidean_eq[where 'a='c] - by(auto simp:euclidean_scaleR[where 'a=real,unfolded real_scaleR_def]) + by(auto simp:euclidean_component_scaleR[where 'a=real,unfolded real_scaleR_def]) qed lemma absolutely_integrable_max: fixes f g::"'m::ordered_euclidean_space \ 'n::ordered_euclidean_space" @@ -5266,7 +5266,7 @@ proof- fix k and i assume "k\d" and i:"iintegral k f $$ i\ \ integral k (\x. (\