# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1523694180 -3600
# Node ID 53323937ee2599ae30995caa6b95b86bc4c8b94f
# Parent  06bce659d41bdbe05f5ec799f32969d347c12931
new material about vec, real^1, etc.

diff -r 06bce659d41b -r 53323937ee25 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Fri Apr 13 17:00:57 2018 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sat Apr 14 09:23:00 2018 +0100
@@ -139,6 +139,9 @@
 lemma vec_cmul: "vec(c * x) = c *s vec x " by vector
 lemma vec_neg: "vec(- x) = - vec x " by vector
 
+lemma vec_scaleR: "vec(c * x) = c *\<^sub>R vec x"
+  by vector
+
 lemma vec_sum:
   assumes "finite S"
   shows "vec(sum f S) = sum (vec \<circ> f) S"
@@ -263,6 +266,26 @@
 lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)"
   by (simp add: vec_eq_iff)
 
+lemma linear_vec [simp]: "linear vec"
+  by (simp add: linearI vec_add vec_eq_iff)
+
+lemma differentiable_vec:
+  fixes S :: "'a::euclidean_space set"
+  shows "vec differentiable_on S"
+  by (simp add: linear_linear bounded_linear_imp_differentiable_on)
+
+lemma continuous_vec [continuous_intros]:
+  fixes x :: "'a::euclidean_space"
+  shows "isCont vec x"
+  apply (clarsimp simp add: continuous_def LIM_def dist_vec_def L2_set_def)
+  apply (rule_tac x="r / sqrt (real CARD('b))" in exI)
+  by (simp add: mult.commute pos_less_divide_eq real_sqrt_mult)
+
+lemma box_vec_eq_empty [simp]:
+  shows "cbox (vec a) (vec b) = {} \<longleftrightarrow> cbox a b = {}"
+        "box (vec a) (vec b) = {} \<longleftrightarrow> box a b = {}"
+  by (auto simp: Basis_vec_def mem_box box_eq_empty inner_axis)
+
 lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
 
 lemma norm_axis_1 [simp]: "norm (axis m (1::real)) = 1"
@@ -283,18 +306,18 @@
 lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"
   by (metis vector_mul_rcancel)
 
-lemma component_le_norm_cart: "\<bar>x$i\<bar> <= norm x"
+lemma component_le_norm_cart: "\<bar>x$i\<bar> \<le> norm x"
   apply (simp add: norm_vec_def)
   apply (rule member_le_L2_set, simp_all)
   done
 
-lemma norm_bound_component_le_cart: "norm x <= e ==> \<bar>x$i\<bar> <= e"
+lemma norm_bound_component_le_cart: "norm x \<le> e ==> \<bar>x$i\<bar> \<le> e"
   by (metis component_le_norm_cart order_trans)
 
 lemma norm_bound_component_lt_cart: "norm x < e ==> \<bar>x$i\<bar> < e"
   by (metis component_le_norm_cart le_less_trans)
 
-lemma norm_le_l1_cart: "norm x <= sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
+lemma norm_le_l1_cart: "norm x \<le> sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
   by (simp add: norm_vec_def L2_set_le_sum)
 
 lemma scalar_mult_eq_scaleR [simp]: "c *s x = c *\<^sub>R x"
@@ -1440,7 +1463,7 @@
   shows "x = 1 \<or> x = 2"
 proof (induct x)
   case (of_int z)
-  then have "0 <= z" and "z < 2" by simp_all
+  then have "0 \<le> z" and "z < 2" by simp_all
   then have "z = 0 | z = 1" by arith
   then show ?case by auto
 qed
@@ -1453,7 +1476,7 @@
   shows "x = 1 \<or> x = 2 \<or> x = 3"
 proof (induct x)
   case (of_int z)
-  then have "0 <= z" and "z < 3" by simp_all
+  then have "0 \<le> z" and "z < 3" by simp_all
   then have "z = 0 \<or> z = 1 \<or> z = 2" by arith
   then show ?case by auto
 qed
@@ -1479,6 +1502,14 @@
 lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3"
   unfolding UNIV_3 by (simp add: ac_simps)
 
+lemma num1_eqI:
+  fixes a::num1 shows "a = b"
+  by (metis (full_types) UNIV_1 UNIV_I empty_iff insert_iff)
+
+lemma num1_eq1 [simp]:
+  fixes a::num1 shows "a = 1"
+  by (rule num1_eqI)
+
 instantiation num1 :: cart_one
 begin
 
@@ -1489,6 +1520,16 @@
 
 end
 
+instantiation num1 :: linorder begin
+definition "a < b \<longleftrightarrow> Rep_num1 a < Rep_num1 b"
+definition "a \<le> b \<longleftrightarrow> Rep_num1 a \<le> Rep_num1 b"
+instance
+  by intro_classes (auto simp: less_eq_num1_def less_num1_def intro: num1_eqI)
+end
+
+instance num1 :: wellorder
+  by intro_classes (auto simp: less_eq_num1_def less_num1_def)
+
 subsection\<open>The collapse of the general concepts to dimension one\<close>
 
 lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
@@ -1503,6 +1544,11 @@
 lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
   by (simp add: norm_vec_def)
 
+lemma dist_vector_1:
+  fixes x :: "'a::real_normed_vector^1"
+  shows "dist x y = dist (x$1) (y$1)"
+  by (simp add: dist_norm norm_vector_1)
+
 lemma norm_real: "norm(x::real ^ 1) = \<bar>x$1\<bar>"
   by (simp add: norm_vector_1)
 
@@ -1510,6 +1556,33 @@
   by (auto simp add: norm_real dist_norm)
 
 
+lemma tendsto_at_within_vector_1:
+  fixes S :: "'a :: metric_space set"
+  assumes "(f \<longlongrightarrow> fx) (at x within S)"
+  shows "((\<lambda>y::'a^1. \<chi> i. f (y $ 1)) \<longlongrightarrow> (vec fx::'a^1)) (at (vec x) within vec ` S)"
+proof (rule topological_tendstoI)
+  fix T :: "('a^1) set"
+  assume "open T" "vec fx \<in> T"
+  have "\<forall>\<^sub>F x in at x within S. f x \<in> (\<lambda>x. x $ 1) ` T"
+    using \<open>open T\<close> \<open>vec fx \<in> T\<close> assms open_image_vec_nth tendsto_def by fastforce
+  then show "\<forall>\<^sub>F x::'a^1 in at (vec x) within vec ` S. (\<chi> i. f (x $ 1)) \<in> T"
+    unfolding eventually_at dist_norm [symmetric]
+    by (rule ex_forward)
+       (use \<open>open T\<close> in 
+         \<open>fastforce simp: dist_norm dist_vec_def L2_set_def image_iff vector_one open_vec_def\<close>)
+qed
+
+lemma has_derivative_vector_1:
+  assumes der_g: "(g has_derivative (\<lambda>x. x * g' a)) (at a within S)"
+  shows "((\<lambda>x. vec (g (x $ 1))) has_derivative ( *\<^sub>R) (g' a))
+         (at ((vec a)::real^1) within vec ` S)"
+    using der_g
+    apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1)
+    apply (drule tendsto_at_within_vector_1, vector)
+    apply (auto simp: algebra_simps eventually_at tendsto_def)
+    done
+
+
 subsection\<open>Explicit vector construction from lists\<close>
 
 definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)"
diff -r 06bce659d41b -r 53323937ee25 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri Apr 13 17:00:57 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat Apr 14 09:23:00 2018 +0100
@@ -378,7 +378,7 @@
     "f piecewise_C1_differentiable_on i \<Longrightarrow> f piecewise_differentiable_on i"
   by (auto simp: piecewise_C1_differentiable_on_def piecewise_differentiable_on_def
            C1_differentiable_on_def differentiable_def has_vector_derivative_def
-           intro: has_derivative_at_within)
+           intro: has_derivative_at_withinI)
 
 lemma piecewise_C1_differentiable_compose:
     "\<lbrakk>f piecewise_C1_differentiable_on s; g piecewise_C1_differentiable_on (f ` s);
@@ -3807,7 +3807,7 @@
           (at x within {a..b})"
         using x gdx t
         apply (clarsimp simp add: differentiable_iff_scaleR)
-        apply (rule exp_fg [unfolded has_vector_derivative_def, simplified], blast intro: has_derivative_at_within)
+        apply (rule exp_fg [unfolded has_vector_derivative_def, simplified], blast intro: has_derivative_at_withinI)
         apply (simp_all add: has_vector_derivative_def [symmetric])
         done
       } note * = this
diff -r 06bce659d41b -r 53323937ee25 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Fri Apr 13 17:00:57 2018 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat Apr 14 09:23:00 2018 +0100
@@ -1113,7 +1113,7 @@
     apply auto
     apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI)
     apply (auto simp: closed_segment_def twz) []
-    apply (intro derivative_eq_intros has_derivative_at_within, simp_all)
+    apply (intro derivative_eq_intros has_derivative_at_withinI, simp_all)
     apply (simp add: fun_eq_iff real_vector.scale_right_diff_distrib)
     apply (force simp: twz closed_segment_def)
     done
diff -r 06bce659d41b -r 53323937ee25 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Fri Apr 13 17:00:57 2018 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Sat Apr 14 09:23:00 2018 +0100
@@ -66,7 +66,7 @@
   using has_derivative_within' [of f f' x UNIV]
   by simp
 
-lemma has_derivative_at_within:
+lemma has_derivative_at_withinI:
   "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)"
   unfolding has_derivative_within' has_derivative_at'
   by blast
@@ -135,7 +135,7 @@
 
 lemma differentiable_at_withinI: "f differentiable (at x) \<Longrightarrow> f differentiable (at x within s)"
   unfolding differentiable_def
-  using has_derivative_at_within
+  using has_derivative_at_withinI
   by blast
 
 lemma differentiable_at_imp_differentiable_on:
@@ -1819,7 +1819,7 @@
           apply (rule derivative_intros)
           defer
           apply (rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
-          apply (rule has_derivative_at_within)
+          apply (rule has_derivative_at_withinI)
           using assms(5) and \<open>u \<in> s\<close> \<open>a \<in> s\<close>
           apply (auto intro!: derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] has_derivative_bounded_linear)
           done
@@ -2526,7 +2526,7 @@
 lemma has_vector_derivative_at_within:
   "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within s)"
   unfolding has_vector_derivative_def
-  by (rule has_derivative_at_within)
+  by (rule has_derivative_at_withinI)
 
 lemma has_vector_derivative_weaken:
   fixes x D and f g s t
diff -r 06bce659d41b -r 53323937ee25 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Apr 13 17:00:57 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Apr 14 09:23:00 2018 +0100
@@ -917,6 +917,9 @@
   where "f absolutely_integrable_on s \<equiv> set_integrable lebesgue s f"
 
 
+lemma absolutely_integrable_zero [simp]: "(\<lambda>x. 0) absolutely_integrable_on S"
+    by (simp add: set_integrable_def)
+
 lemma absolutely_integrable_on_def:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   shows "f absolutely_integrable_on S \<longleftrightarrow> f integrable_on S \<and> (\<lambda>x. norm (f x)) integrable_on S"
@@ -987,6 +990,18 @@
     unfolding absolutely_integrable_on_def by auto
 qed
 
+lemma absolutely_integrable_on_scaleR_iff:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows
+   "(\<lambda>x. c *\<^sub>R f x) absolutely_integrable_on S \<longleftrightarrow>
+      c = 0 \<or> f absolutely_integrable_on S"
+proof (cases "c=0")
+  case False
+  then show ?thesis
+  unfolding absolutely_integrable_on_def 
+  by (simp add: norm_mult)
+qed auto
+
 lemma lmeasurable_iff_integrable_on: "S \<in> lmeasurable \<longleftrightarrow> (\<lambda>x. 1::real) integrable_on S"
   by (subst absolutely_integrable_on_iff_nonneg[symmetric])
      (simp_all add: lmeasurable_iff_integrable set_integrable_def)
@@ -2128,9 +2143,6 @@
   using integrable_bounded_linear[of h lebesgue "\<lambda>x. indicator s x *\<^sub>R f x"]
   by (simp add: linear_simps[of h] set_integrable_def)
 
-lemma absolutely_integrable_zero [simp]: "(\<lambda>x. 0) absolutely_integrable_on S"
-    by (simp add: set_integrable_def)
-
 lemma absolutely_integrable_sum:
   fixes f :: "'a \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   assumes "finite T" and "\<And>a. a \<in> T \<Longrightarrow> (f a) absolutely_integrable_on S"
@@ -2477,6 +2489,75 @@
     by simp
 qed
 
+lemma dominated_convergence_integrable_1:
+  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
+  assumes f: "\<And>k. f k absolutely_integrable_on S"
+    and h: "h integrable_on S"
+    and normg: "\<And>x. x \<in> S \<Longrightarrow> norm(g x) \<le> (h x)"
+    and lim: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
+ shows "g integrable_on S"
+proof -
+  have habs: "h absolutely_integrable_on S"
+    using h normg nonnegative_absolutely_integrable_1 norm_ge_zero order_trans by blast
+  let ?f = "\<lambda>n x. (min (max (- h x) (f n x)) (h x))"
+  have h0: "h x \<ge> 0" if "x \<in> S" for x
+    using normg that by force
+  have leh: "norm (?f k x) \<le> h x" if "x \<in> S" for k x
+    using h0 that by force
+  have limf: "(\<lambda>k. ?f k x) \<longlonglongrightarrow> g x" if "x \<in> S" for x
+  proof -
+    have "\<And>e y. \<bar>f y x - g x\<bar> < e \<Longrightarrow> \<bar>min (max (- h x) (f y x)) (h x) - g x\<bar> < e"
+      using h0 [OF that] normg [OF that] by simp
+    then show ?thesis
+      using lim [OF that] by (auto simp add: tendsto_iff dist_norm elim!: eventually_mono)
+  qed
+  show ?thesis
+  proof (rule dominated_convergence [of ?f S h g])
+    have "(\<lambda>x. - h x) absolutely_integrable_on S"
+      using habs unfolding set_integrable_def by auto
+    then show "?f k integrable_on S" for k
+      by (intro set_lebesgue_integral_eq_integral absolutely_integrable_min_1 absolutely_integrable_max_1 f habs)
+  qed (use assms leh limf in auto)
+qed
+
+lemma dominated_convergence_integrable:
+  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes f: "\<And>k. f k absolutely_integrable_on S"
+    and h: "h integrable_on S"
+    and normg: "\<And>x. x \<in> S \<Longrightarrow> norm(g x) \<le> (h x)"
+    and lim: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
+  shows "g integrable_on S"
+  using f
+  unfolding integrable_componentwise_iff [of g] absolutely_integrable_componentwise_iff [where f = "f k" for k]
+proof clarify
+  fix b :: "'m"
+  assume fb [rule_format]: "\<And>k. \<forall>b\<in>Basis. (\<lambda>x. f k x \<bullet> b) absolutely_integrable_on S" and b: "b \<in> Basis"
+  show "(\<lambda>x. g x \<bullet> b) integrable_on S"
+  proof (rule dominated_convergence_integrable_1 [OF fb h])
+    fix x 
+    assume "x \<in> S"
+    show "norm (g x \<bullet> b) \<le> h x"
+      using norm_nth_le \<open>x \<in> S\<close> b normg order.trans by blast
+    show "(\<lambda>k. f k x \<bullet> b) \<longlonglongrightarrow> g x \<bullet> b"
+      using \<open>x \<in> S\<close> b lim tendsto_componentwise_iff by fastforce
+  qed (use b in auto)
+qed
+
+
+lemma dominated_convergence_absolutely_integrable:
+  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes f: "\<And>k. f k absolutely_integrable_on S"
+    and h: "h integrable_on S"
+    and normg: "\<And>x. x \<in> S \<Longrightarrow> norm(g x) \<le> (h x)"
+    and lim: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
+  shows "g absolutely_integrable_on S"
+proof -
+  have "g integrable_on S"
+    by (rule dominated_convergence_integrable [OF assms])
+  with assms show ?thesis
+    by (blast intro:  absolutely_integrable_integrable_bound [where g=h])
+qed
+
 subsection \<open>Fundamental Theorem of Calculus for the Lebesgue integral\<close>
 
 text \<open>
diff -r 06bce659d41b -r 53323937ee25 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Apr 13 17:00:57 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Apr 14 09:23:00 2018 +0100
@@ -5258,7 +5258,7 @@
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   assumes "f integrable_on S" "f integrable_on T" "negligible (S \<inter> T)"
   shows "integral (S \<union> T) f = integral S f + integral T f"
-  using has_integral_Un by (simp add: has_integral_Un assms integrable_integral integral_unique)
+  by (simp add: has_integral_Un assms integrable_integral integral_unique)
 
 lemma integrable_Un:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: banach"
diff -r 06bce659d41b -r 53323937ee25 src/HOL/Analysis/Lipschitz.thy
--- a/src/HOL/Analysis/Lipschitz.thy	Fri Apr 13 17:00:57 2018 +0100
+++ b/src/HOL/Analysis/Lipschitz.thy	Sat Apr 14 09:23:00 2018 +0100
@@ -816,7 +816,7 @@
     finally
     have deriv: "\<forall>y\<in>cball x u. (f s has_derivative blinfun_apply (f' (s, y))) (at y within cball x u)"
       using \<open>_ \<subseteq> X\<close>
-      by (auto intro!: has_derivative_at_within[OF f'])
+      by (auto intro!: has_derivative_at_withinI[OF f'])
     have "norm (f s y - f s z) \<le> B * norm (y - z)"
       if "y \<in> cball x u" "z \<in> cball x u"
       for y z
diff -r 06bce659d41b -r 53323937ee25 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Apr 13 17:00:57 2018 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sat Apr 14 09:23:00 2018 +0100
@@ -3219,7 +3219,7 @@
 lemma netlimit_within: "\<not> trivial_limit (at a within S) \<Longrightarrow> netlimit (at a within S) = a"
   by (rule tendsto_Lim) (auto intro: tendsto_intros)
 
-lemma netlimit_at:
+lemma netlimit_at [simp]:
   fixes a :: "'a::{perfect_space,t2_space}"
   shows "netlimit (at a) = a"
   using netlimit_within [of a UNIV] by simp