author paulson Sat Apr 14 09:23:00 2018 +0100 (13 months ago) changeset 67979 53323937ee25 parent 67978 06bce659d41b child 67980 a8177d098b74
new material about vec, real^1, etc.
```     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Fri Apr 13 17:00:57 2018 +0100
1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sat Apr 14 09:23:00 2018 +0100
1.3 @@ -139,6 +139,9 @@
1.4  lemma vec_cmul: "vec(c * x) = c *s vec x " by vector
1.5  lemma vec_neg: "vec(- x) = - vec x " by vector
1.6
1.7 +lemma vec_scaleR: "vec(c * x) = c *\<^sub>R vec x"
1.8 +  by vector
1.9 +
1.10  lemma vec_sum:
1.11    assumes "finite S"
1.12    shows "vec(sum f S) = sum (vec \<circ> f) S"
1.13 @@ -263,6 +266,26 @@
1.14  lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)"
1.16
1.17 +lemma linear_vec [simp]: "linear vec"
1.19 +
1.20 +lemma differentiable_vec:
1.21 +  fixes S :: "'a::euclidean_space set"
1.22 +  shows "vec differentiable_on S"
1.23 +  by (simp add: linear_linear bounded_linear_imp_differentiable_on)
1.24 +
1.25 +lemma continuous_vec [continuous_intros]:
1.26 +  fixes x :: "'a::euclidean_space"
1.27 +  shows "isCont vec x"
1.28 +  apply (clarsimp simp add: continuous_def LIM_def dist_vec_def L2_set_def)
1.29 +  apply (rule_tac x="r / sqrt (real CARD('b))" in exI)
1.30 +  by (simp add: mult.commute pos_less_divide_eq real_sqrt_mult)
1.31 +
1.32 +lemma box_vec_eq_empty [simp]:
1.33 +  shows "cbox (vec a) (vec b) = {} \<longleftrightarrow> cbox a b = {}"
1.34 +        "box (vec a) (vec b) = {} \<longleftrightarrow> box a b = {}"
1.35 +  by (auto simp: Basis_vec_def mem_box box_eq_empty inner_axis)
1.36 +
1.37  lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
1.38
1.39  lemma norm_axis_1 [simp]: "norm (axis m (1::real)) = 1"
1.40 @@ -283,18 +306,18 @@
1.41  lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"
1.42    by (metis vector_mul_rcancel)
1.43
1.44 -lemma component_le_norm_cart: "\<bar>x\$i\<bar> <= norm x"
1.45 +lemma component_le_norm_cart: "\<bar>x\$i\<bar> \<le> norm x"
1.47    apply (rule member_le_L2_set, simp_all)
1.48    done
1.49
1.50 -lemma norm_bound_component_le_cart: "norm x <= e ==> \<bar>x\$i\<bar> <= e"
1.51 +lemma norm_bound_component_le_cart: "norm x \<le> e ==> \<bar>x\$i\<bar> \<le> e"
1.52    by (metis component_le_norm_cart order_trans)
1.53
1.54  lemma norm_bound_component_lt_cart: "norm x < e ==> \<bar>x\$i\<bar> < e"
1.55    by (metis component_le_norm_cart le_less_trans)
1.56
1.57 -lemma norm_le_l1_cart: "norm x <= sum(\<lambda>i. \<bar>x\$i\<bar>) UNIV"
1.58 +lemma norm_le_l1_cart: "norm x \<le> sum(\<lambda>i. \<bar>x\$i\<bar>) UNIV"
1.59    by (simp add: norm_vec_def L2_set_le_sum)
1.60
1.61  lemma scalar_mult_eq_scaleR [simp]: "c *s x = c *\<^sub>R x"
1.62 @@ -1440,7 +1463,7 @@
1.63    shows "x = 1 \<or> x = 2"
1.64  proof (induct x)
1.65    case (of_int z)
1.66 -  then have "0 <= z" and "z < 2" by simp_all
1.67 +  then have "0 \<le> z" and "z < 2" by simp_all
1.68    then have "z = 0 | z = 1" by arith
1.69    then show ?case by auto
1.70  qed
1.71 @@ -1453,7 +1476,7 @@
1.72    shows "x = 1 \<or> x = 2 \<or> x = 3"
1.73  proof (induct x)
1.74    case (of_int z)
1.75 -  then have "0 <= z" and "z < 3" by simp_all
1.76 +  then have "0 \<le> z" and "z < 3" by simp_all
1.77    then have "z = 0 \<or> z = 1 \<or> z = 2" by arith
1.78    then show ?case by auto
1.79  qed
1.80 @@ -1479,6 +1502,14 @@
1.81  lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3"
1.82    unfolding UNIV_3 by (simp add: ac_simps)
1.83
1.84 +lemma num1_eqI:
1.85 +  fixes a::num1 shows "a = b"
1.86 +  by (metis (full_types) UNIV_1 UNIV_I empty_iff insert_iff)
1.87 +
1.88 +lemma num1_eq1 [simp]:
1.89 +  fixes a::num1 shows "a = 1"
1.90 +  by (rule num1_eqI)
1.91 +
1.92  instantiation num1 :: cart_one
1.93  begin
1.94
1.95 @@ -1489,6 +1520,16 @@
1.96
1.97  end
1.98
1.99 +instantiation num1 :: linorder begin
1.100 +definition "a < b \<longleftrightarrow> Rep_num1 a < Rep_num1 b"
1.101 +definition "a \<le> b \<longleftrightarrow> Rep_num1 a \<le> Rep_num1 b"
1.102 +instance
1.103 +  by intro_classes (auto simp: less_eq_num1_def less_num1_def intro: num1_eqI)
1.104 +end
1.105 +
1.106 +instance num1 :: wellorder
1.107 +  by intro_classes (auto simp: less_eq_num1_def less_num1_def)
1.108 +
1.109  subsection\<open>The collapse of the general concepts to dimension one\<close>
1.110
1.111  lemma vector_one: "(x::'a ^1) = (\<chi> i. (x\$1))"
1.112 @@ -1503,6 +1544,11 @@
1.113  lemma norm_vector_1: "norm (x :: _^1) = norm (x\$1)"
1.115
1.116 +lemma dist_vector_1:
1.117 +  fixes x :: "'a::real_normed_vector^1"
1.118 +  shows "dist x y = dist (x\$1) (y\$1)"
1.119 +  by (simp add: dist_norm norm_vector_1)
1.120 +
1.121  lemma norm_real: "norm(x::real ^ 1) = \<bar>x\$1\<bar>"
1.123
1.124 @@ -1510,6 +1556,33 @@
1.125    by (auto simp add: norm_real dist_norm)
1.126
1.127
1.128 +lemma tendsto_at_within_vector_1:
1.129 +  fixes S :: "'a :: metric_space set"
1.130 +  assumes "(f \<longlongrightarrow> fx) (at x within S)"
1.131 +  shows "((\<lambda>y::'a^1. \<chi> i. f (y \$ 1)) \<longlongrightarrow> (vec fx::'a^1)) (at (vec x) within vec ` S)"
1.132 +proof (rule topological_tendstoI)
1.133 +  fix T :: "('a^1) set"
1.134 +  assume "open T" "vec fx \<in> T"
1.135 +  have "\<forall>\<^sub>F x in at x within S. f x \<in> (\<lambda>x. x \$ 1) ` T"
1.136 +    using \<open>open T\<close> \<open>vec fx \<in> T\<close> assms open_image_vec_nth tendsto_def by fastforce
1.137 +  then show "\<forall>\<^sub>F x::'a^1 in at (vec x) within vec ` S. (\<chi> i. f (x \$ 1)) \<in> T"
1.138 +    unfolding eventually_at dist_norm [symmetric]
1.139 +    by (rule ex_forward)
1.140 +       (use \<open>open T\<close> in
1.141 +         \<open>fastforce simp: dist_norm dist_vec_def L2_set_def image_iff vector_one open_vec_def\<close>)
1.142 +qed
1.143 +
1.144 +lemma has_derivative_vector_1:
1.145 +  assumes der_g: "(g has_derivative (\<lambda>x. x * g' a)) (at a within S)"
1.146 +  shows "((\<lambda>x. vec (g (x \$ 1))) has_derivative ( *\<^sub>R) (g' a))
1.147 +         (at ((vec a)::real^1) within vec ` S)"
1.148 +    using der_g
1.149 +    apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1)
1.150 +    apply (drule tendsto_at_within_vector_1, vector)
1.151 +    apply (auto simp: algebra_simps eventually_at tendsto_def)
1.152 +    done
1.153 +
1.154 +
1.155  subsection\<open>Explicit vector construction from lists\<close>
1.156
1.157  definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)"
```
```     2.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri Apr 13 17:00:57 2018 +0100
2.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat Apr 14 09:23:00 2018 +0100
2.3 @@ -378,7 +378,7 @@
2.4      "f piecewise_C1_differentiable_on i \<Longrightarrow> f piecewise_differentiable_on i"
2.5    by (auto simp: piecewise_C1_differentiable_on_def piecewise_differentiable_on_def
2.6             C1_differentiable_on_def differentiable_def has_vector_derivative_def
2.7 -           intro: has_derivative_at_within)
2.8 +           intro: has_derivative_at_withinI)
2.9
2.10  lemma piecewise_C1_differentiable_compose:
2.11      "\<lbrakk>f piecewise_C1_differentiable_on s; g piecewise_C1_differentiable_on (f ` s);
2.12 @@ -3807,7 +3807,7 @@
2.13            (at x within {a..b})"
2.14          using x gdx t
2.15          apply (clarsimp simp add: differentiable_iff_scaleR)
2.16 -        apply (rule exp_fg [unfolded has_vector_derivative_def, simplified], blast intro: has_derivative_at_within)
2.17 +        apply (rule exp_fg [unfolded has_vector_derivative_def, simplified], blast intro: has_derivative_at_withinI)
2.18          apply (simp_all add: has_vector_derivative_def [symmetric])
2.19          done
2.20        } note * = this
```
```     3.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Fri Apr 13 17:00:57 2018 +0100
3.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat Apr 14 09:23:00 2018 +0100
3.3 @@ -1113,7 +1113,7 @@
3.4      apply auto
3.5      apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI)
3.6      apply (auto simp: closed_segment_def twz) []
3.7 -    apply (intro derivative_eq_intros has_derivative_at_within, simp_all)
3.8 +    apply (intro derivative_eq_intros has_derivative_at_withinI, simp_all)
3.9      apply (simp add: fun_eq_iff real_vector.scale_right_diff_distrib)
3.10      apply (force simp: twz closed_segment_def)
3.11      done
```
```     4.1 --- a/src/HOL/Analysis/Derivative.thy	Fri Apr 13 17:00:57 2018 +0100
4.2 +++ b/src/HOL/Analysis/Derivative.thy	Sat Apr 14 09:23:00 2018 +0100
4.3 @@ -66,7 +66,7 @@
4.4    using has_derivative_within' [of f f' x UNIV]
4.5    by simp
4.6
4.7 -lemma has_derivative_at_within:
4.8 +lemma has_derivative_at_withinI:
4.9    "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)"
4.10    unfolding has_derivative_within' has_derivative_at'
4.11    by blast
4.12 @@ -135,7 +135,7 @@
4.13
4.14  lemma differentiable_at_withinI: "f differentiable (at x) \<Longrightarrow> f differentiable (at x within s)"
4.15    unfolding differentiable_def
4.16 -  using has_derivative_at_within
4.17 +  using has_derivative_at_withinI
4.18    by blast
4.19
4.20  lemma differentiable_at_imp_differentiable_on:
4.21 @@ -1819,7 +1819,7 @@
4.22            apply (rule derivative_intros)
4.23            defer
4.24            apply (rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
4.25 -          apply (rule has_derivative_at_within)
4.26 +          apply (rule has_derivative_at_withinI)
4.27            using assms(5) and \<open>u \<in> s\<close> \<open>a \<in> s\<close>
4.28            apply (auto intro!: derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] has_derivative_bounded_linear)
4.29            done
4.30 @@ -2526,7 +2526,7 @@
4.31  lemma has_vector_derivative_at_within:
4.32    "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within s)"
4.33    unfolding has_vector_derivative_def
4.34 -  by (rule has_derivative_at_within)
4.35 +  by (rule has_derivative_at_withinI)
4.36
4.37  lemma has_vector_derivative_weaken:
4.38    fixes x D and f g s t
```
```     5.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Apr 13 17:00:57 2018 +0100
5.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Apr 14 09:23:00 2018 +0100
5.3 @@ -917,6 +917,9 @@
5.4    where "f absolutely_integrable_on s \<equiv> set_integrable lebesgue s f"
5.5
5.6
5.7 +lemma absolutely_integrable_zero [simp]: "(\<lambda>x. 0) absolutely_integrable_on S"
5.8 +    by (simp add: set_integrable_def)
5.9 +
5.10  lemma absolutely_integrable_on_def:
5.11    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
5.12    shows "f absolutely_integrable_on S \<longleftrightarrow> f integrable_on S \<and> (\<lambda>x. norm (f x)) integrable_on S"
5.13 @@ -987,6 +990,18 @@
5.14      unfolding absolutely_integrable_on_def by auto
5.15  qed
5.16
5.17 +lemma absolutely_integrable_on_scaleR_iff:
5.18 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
5.19 +  shows
5.20 +   "(\<lambda>x. c *\<^sub>R f x) absolutely_integrable_on S \<longleftrightarrow>
5.21 +      c = 0 \<or> f absolutely_integrable_on S"
5.22 +proof (cases "c=0")
5.23 +  case False
5.24 +  then show ?thesis
5.25 +  unfolding absolutely_integrable_on_def
5.26 +  by (simp add: norm_mult)
5.27 +qed auto
5.28 +
5.29  lemma lmeasurable_iff_integrable_on: "S \<in> lmeasurable \<longleftrightarrow> (\<lambda>x. 1::real) integrable_on S"
5.30    by (subst absolutely_integrable_on_iff_nonneg[symmetric])
5.32 @@ -2128,9 +2143,6 @@
5.33    using integrable_bounded_linear[of h lebesgue "\<lambda>x. indicator s x *\<^sub>R f x"]
5.34    by (simp add: linear_simps[of h] set_integrable_def)
5.35
5.36 -lemma absolutely_integrable_zero [simp]: "(\<lambda>x. 0) absolutely_integrable_on S"
5.37 -    by (simp add: set_integrable_def)
5.38 -
5.39  lemma absolutely_integrable_sum:
5.40    fixes f :: "'a \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
5.41    assumes "finite T" and "\<And>a. a \<in> T \<Longrightarrow> (f a) absolutely_integrable_on S"
5.42 @@ -2477,6 +2489,75 @@
5.43      by simp
5.44  qed
5.45
5.46 +lemma dominated_convergence_integrable_1:
5.47 +  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
5.48 +  assumes f: "\<And>k. f k absolutely_integrable_on S"
5.49 +    and h: "h integrable_on S"
5.50 +    and normg: "\<And>x. x \<in> S \<Longrightarrow> norm(g x) \<le> (h x)"
5.51 +    and lim: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
5.52 + shows "g integrable_on S"
5.53 +proof -
5.54 +  have habs: "h absolutely_integrable_on S"
5.55 +    using h normg nonnegative_absolutely_integrable_1 norm_ge_zero order_trans by blast
5.56 +  let ?f = "\<lambda>n x. (min (max (- h x) (f n x)) (h x))"
5.57 +  have h0: "h x \<ge> 0" if "x \<in> S" for x
5.58 +    using normg that by force
5.59 +  have leh: "norm (?f k x) \<le> h x" if "x \<in> S" for k x
5.60 +    using h0 that by force
5.61 +  have limf: "(\<lambda>k. ?f k x) \<longlonglongrightarrow> g x" if "x \<in> S" for x
5.62 +  proof -
5.63 +    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"
5.64 +      using h0 [OF that] normg [OF that] by simp
5.65 +    then show ?thesis
5.66 +      using lim [OF that] by (auto simp add: tendsto_iff dist_norm elim!: eventually_mono)
5.67 +  qed
5.68 +  show ?thesis
5.69 +  proof (rule dominated_convergence [of ?f S h g])
5.70 +    have "(\<lambda>x. - h x) absolutely_integrable_on S"
5.71 +      using habs unfolding set_integrable_def by auto
5.72 +    then show "?f k integrable_on S" for k
5.73 +      by (intro set_lebesgue_integral_eq_integral absolutely_integrable_min_1 absolutely_integrable_max_1 f habs)
5.74 +  qed (use assms leh limf in auto)
5.75 +qed
5.76 +
5.77 +lemma dominated_convergence_integrable:
5.78 +  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
5.79 +  assumes f: "\<And>k. f k absolutely_integrable_on S"
5.80 +    and h: "h integrable_on S"
5.81 +    and normg: "\<And>x. x \<in> S \<Longrightarrow> norm(g x) \<le> (h x)"
5.82 +    and lim: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
5.83 +  shows "g integrable_on S"
5.84 +  using f
5.85 +  unfolding integrable_componentwise_iff [of g] absolutely_integrable_componentwise_iff [where f = "f k" for k]
5.86 +proof clarify
5.87 +  fix b :: "'m"
5.88 +  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"
5.89 +  show "(\<lambda>x. g x \<bullet> b) integrable_on S"
5.90 +  proof (rule dominated_convergence_integrable_1 [OF fb h])
5.91 +    fix x
5.92 +    assume "x \<in> S"
5.93 +    show "norm (g x \<bullet> b) \<le> h x"
5.94 +      using norm_nth_le \<open>x \<in> S\<close> b normg order.trans by blast
5.95 +    show "(\<lambda>k. f k x \<bullet> b) \<longlonglongrightarrow> g x \<bullet> b"
5.96 +      using \<open>x \<in> S\<close> b lim tendsto_componentwise_iff by fastforce
5.97 +  qed (use b in auto)
5.98 +qed
5.99 +
5.100 +
5.101 +lemma dominated_convergence_absolutely_integrable:
5.102 +  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
5.103 +  assumes f: "\<And>k. f k absolutely_integrable_on S"
5.104 +    and h: "h integrable_on S"
5.105 +    and normg: "\<And>x. x \<in> S \<Longrightarrow> norm(g x) \<le> (h x)"
5.106 +    and lim: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
5.107 +  shows "g absolutely_integrable_on S"
5.108 +proof -
5.109 +  have "g integrable_on S"
5.110 +    by (rule dominated_convergence_integrable [OF assms])
5.111 +  with assms show ?thesis
5.112 +    by (blast intro:  absolutely_integrable_integrable_bound [where g=h])
5.113 +qed
5.114 +
5.115  subsection \<open>Fundamental Theorem of Calculus for the Lebesgue integral\<close>
5.116
5.117  text \<open>
```
```     6.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Apr 13 17:00:57 2018 +0100
6.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Apr 14 09:23:00 2018 +0100
6.3 @@ -5258,7 +5258,7 @@
6.4    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
6.5    assumes "f integrable_on S" "f integrable_on T" "negligible (S \<inter> T)"
6.6    shows "integral (S \<union> T) f = integral S f + integral T f"
6.7 -  using has_integral_Un by (simp add: has_integral_Un assms integrable_integral integral_unique)
6.8 +  by (simp add: has_integral_Un assms integrable_integral integral_unique)
6.9
6.10  lemma integrable_Un:
6.11    fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: banach"
```
```     7.1 --- a/src/HOL/Analysis/Lipschitz.thy	Fri Apr 13 17:00:57 2018 +0100
7.2 +++ b/src/HOL/Analysis/Lipschitz.thy	Sat Apr 14 09:23:00 2018 +0100
7.3 @@ -816,7 +816,7 @@
7.4      finally
7.5      have deriv: "\<forall>y\<in>cball x u. (f s has_derivative blinfun_apply (f' (s, y))) (at y within cball x u)"
7.6        using \<open>_ \<subseteq> X\<close>
7.7 -      by (auto intro!: has_derivative_at_within[OF f'])
7.8 +      by (auto intro!: has_derivative_at_withinI[OF f'])
7.9      have "norm (f s y - f s z) \<le> B * norm (y - z)"
7.10        if "y \<in> cball x u" "z \<in> cball x u"
7.11        for y z
```
```     8.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Apr 13 17:00:57 2018 +0100
8.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sat Apr 14 09:23:00 2018 +0100
8.3 @@ -3219,7 +3219,7 @@
8.4  lemma netlimit_within: "\<not> trivial_limit (at a within S) \<Longrightarrow> netlimit (at a within S) = a"
8.5    by (rule tendsto_Lim) (auto intro: tendsto_intros)
8.6
8.7 -lemma netlimit_at:
8.8 +lemma netlimit_at [simp]:
8.9    fixes a :: "'a::{perfect_space,t2_space}"
8.10    shows "netlimit (at a) = a"
8.11    using netlimit_within [of a UNIV] by simp
```