src/HOL/Analysis/Cartesian_Euclidean_Space.thy
author Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
Wed Jan 23 03:29:34 2019 +0000 (3 months ago)
changeset 69723 9b9f203e0ba3
parent 69686 aeceb14f387a
child 70113 c8deb8ba6d05
permissions -rw-r--r--
tagged 2 theories ie Cartesian_Euclidean_Space Cartesian_Space
lp15@68038
     1
(* Title:      HOL/Analysis/Cartesian_Euclidean_Space.thy
lp15@68043
     2
   Some material by Jose Divasón, Tim Makarios and L C Paulson
lp15@68038
     3
*)
lp15@68038
     4
ak2110@69723
     5
section \<open>Finite Cartesian Products of Euclidean Spaces\<close>
hoelzl@37489
     6
hoelzl@37489
     7
theory Cartesian_Euclidean_Space
immler@68072
     8
imports Cartesian_Space Derivative
hoelzl@37489
     9
begin
hoelzl@37489
    10
ak2110@69723
    11
lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}"
lp15@63016
    12
  by (simp add: subspace_def)
lp15@63016
    13
ak2110@69723
    14
lemma sum_mult_product:
nipkow@64267
    15
  "sum h {..<A * B :: nat} = (\<Sum>i\<in>{..<A}. \<Sum>j\<in>{..<B}. h (j + i * B))"
nipkow@64267
    16
  unfolding sum_nat_group[of h B A, unfolded atLeast0LessThan, symmetric]
ak2110@69723
    17
proof (rule sum.cong, simp, rule sum.reindex_cong)
wenzelm@49644
    18
  fix i
wenzelm@49644
    19
  show "inj_on (\<lambda>j. j + i * B) {..<B}" by (auto intro!: inj_onI)
hoelzl@37489
    20
  show "{i * B..<i * B + B} = (\<lambda>j. j + i * B) ` {..<B}"
hoelzl@37489
    21
  proof safe
hoelzl@37489
    22
    fix j assume "j \<in> {i * B..<i * B + B}"
wenzelm@49644
    23
    then show "j \<in> (\<lambda>j. j + i * B) ` {..<B}"
hoelzl@37489
    24
      by (auto intro!: image_eqI[of _ _ "j - i * B"])
hoelzl@37489
    25
  qed simp
hoelzl@37489
    26
qed simp
hoelzl@37489
    27
ak2110@69723
    28
lemma interval_cbox_cart: "{a::real^'n..b} = cbox a b"
immler@56188
    29
  by (auto simp add: less_eq_vec_def mem_box Basis_vec_def inner_axis)
immler@56188
    30
ak2110@69723
    31
lemma differentiable_vec:
lp15@67979
    32
  fixes S :: "'a::euclidean_space set"
lp15@67979
    33
  shows "vec differentiable_on S"
lp15@67979
    34
  by (simp add: linear_linear bounded_linear_imp_differentiable_on)
lp15@67979
    35
ak2110@69723
    36
lemma continuous_vec [continuous_intros]:
lp15@67979
    37
  fixes x :: "'a::euclidean_space"
lp15@67979
    38
  shows "isCont vec x"
lp15@67979
    39
  apply (clarsimp simp add: continuous_def LIM_def dist_vec_def L2_set_def)
lp15@67979
    40
  apply (rule_tac x="r / sqrt (real CARD('b))" in exI)
lp15@67979
    41
  by (simp add: mult.commute pos_less_divide_eq real_sqrt_mult)
lp15@67979
    42
ak2110@69723
    43
lemma box_vec_eq_empty [simp]:
lp15@67979
    44
  shows "cbox (vec a) (vec b) = {} \<longleftrightarrow> cbox a b = {}"
lp15@67979
    45
        "box (vec a) (vec b) = {} \<longleftrightarrow> box a b = {}"
lp15@67979
    46
  by (auto simp: Basis_vec_def mem_box box_eq_empty inner_axis)
lp15@67979
    47
immler@69683
    48
subsection\<open>Closures and interiors of halfspaces\<close>
lp15@62397
    49
ak2110@69723
    50
lemma interior_halfspace_le [simp]:
lp15@62397
    51
  assumes "a \<noteq> 0"
lp15@62397
    52
    shows "interior {x. a \<bullet> x \<le> b} = {x. a \<bullet> x < b}"
ak2110@69723
    53
proof -
lp15@62397
    54
  have *: "a \<bullet> x < b" if x: "x \<in> S" and S: "S \<subseteq> {x. a \<bullet> x \<le> b}" and "open S" for S x
lp15@62397
    55
  proof -
lp15@62397
    56
    obtain e where "e>0" and e: "cball x e \<subseteq> S"
lp15@62397
    57
      using \<open>open S\<close> open_contains_cball x by blast
lp15@62397
    58
    then have "x + (e / norm a) *\<^sub>R a \<in> cball x e"
lp15@62397
    59
      by (simp add: dist_norm)
lp15@62397
    60
    then have "x + (e / norm a) *\<^sub>R a \<in> S"
lp15@62397
    61
      using e by blast
lp15@62397
    62
    then have "x + (e / norm a) *\<^sub>R a \<in> {x. a \<bullet> x \<le> b}"
lp15@62397
    63
      using S by blast
lp15@62397
    64
    moreover have "e * (a \<bullet> a) / norm a > 0"
lp15@62397
    65
      by (simp add: \<open>0 < e\<close> assms)
lp15@62397
    66
    ultimately show ?thesis
lp15@62397
    67
      by (simp add: algebra_simps)
lp15@62397
    68
  qed
lp15@62397
    69
  show ?thesis
lp15@62397
    70
    by (rule interior_unique) (auto simp: open_halfspace_lt *)
lp15@62397
    71
qed
lp15@62397
    72
ak2110@69723
    73
lemma interior_halfspace_ge [simp]:
lp15@62397
    74
   "a \<noteq> 0 \<Longrightarrow> interior {x. a \<bullet> x \<ge> b} = {x. a \<bullet> x > b}"
lp15@62397
    75
using interior_halfspace_le [of "-a" "-b"] by simp
lp15@62397
    76
ak2110@69723
    77
lemma interior_halfspace_component_le [simp]:
wenzelm@67731
    78
     "interior {x. x$k \<le> a} = {x :: (real^'n). x$k < a}" (is "?LE")
lp15@62397
    79
  and interior_halfspace_component_ge [simp]:
wenzelm@67731
    80
     "interior {x. x$k \<ge> a} = {x :: (real^'n). x$k > a}" (is "?GE")
ak2110@69723
    81
proof -
lp15@62397
    82
  have "axis k (1::real) \<noteq> 0"
lp15@62397
    83
    by (simp add: axis_def vec_eq_iff)
lp15@62397
    84
  moreover have "axis k (1::real) \<bullet> x = x$k" for x
lp15@62397
    85
    by (simp add: cart_eq_inner_axis inner_commute)
lp15@62397
    86
  ultimately show ?LE ?GE
lp15@62397
    87
    using interior_halfspace_le [of "axis k (1::real)" a]
lp15@62397
    88
          interior_halfspace_ge [of "axis k (1::real)" a] by auto
lp15@62397
    89
qed
lp15@62397
    90
ak2110@69723
    91
lemma closure_halfspace_lt [simp]:
lp15@62397
    92
  assumes "a \<noteq> 0"
lp15@62397
    93
    shows "closure {x. a \<bullet> x < b} = {x. a \<bullet> x \<le> b}"
lp15@62397
    94
proof -
lp15@62397
    95
  have [simp]: "-{x. a \<bullet> x < b} = {x. a \<bullet> x \<ge> b}"
lp15@62397
    96
    by (force simp:)
lp15@62397
    97
  then show ?thesis
lp15@62397
    98
    using interior_halfspace_ge [of a b] assms
lp15@62397
    99
    by (force simp: closure_interior)
lp15@62397
   100
qed
lp15@62397
   101
ak2110@69723
   102
lemma closure_halfspace_gt [simp]:
lp15@62397
   103
   "a \<noteq> 0 \<Longrightarrow> closure {x. a \<bullet> x > b} = {x. a \<bullet> x \<ge> b}"
lp15@62397
   104
using closure_halfspace_lt [of "-a" "-b"] by simp
lp15@62397
   105
ak2110@69723
   106
lemma closure_halfspace_component_lt [simp]:
wenzelm@67731
   107
     "closure {x. x$k < a} = {x :: (real^'n). x$k \<le> a}" (is "?LE")
lp15@62397
   108
  and closure_halfspace_component_gt [simp]:
wenzelm@67731
   109
     "closure {x. x$k > a} = {x :: (real^'n). x$k \<ge> a}" (is "?GE")
ak2110@69723
   110
proof -
lp15@62397
   111
  have "axis k (1::real) \<noteq> 0"
lp15@62397
   112
    by (simp add: axis_def vec_eq_iff)
lp15@62397
   113
  moreover have "axis k (1::real) \<bullet> x = x$k" for x
lp15@62397
   114
    by (simp add: cart_eq_inner_axis inner_commute)
lp15@62397
   115
  ultimately show ?LE ?GE
lp15@62397
   116
    using closure_halfspace_lt [of "axis k (1::real)" a]
lp15@62397
   117
          closure_halfspace_gt [of "axis k (1::real)" a] by auto
lp15@62397
   118
qed
lp15@62397
   119
ak2110@69723
   120
lemma interior_hyperplane [simp]:
lp15@62397
   121
  assumes "a \<noteq> 0"
lp15@62397
   122
    shows "interior {x. a \<bullet> x = b} = {}"
ak2110@69723
   123
proof -
lp15@62397
   124
  have [simp]: "{x. a \<bullet> x = b} = {x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x \<ge> b}"
lp15@62397
   125
    by (force simp:)
lp15@62397
   126
  then show ?thesis
lp15@62397
   127
    by (auto simp: assms)
lp15@62397
   128
qed
lp15@62397
   129
ak2110@69723
   130
lemma frontier_halfspace_le:
lp15@62397
   131
  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
lp15@62397
   132
    shows "frontier {x. a \<bullet> x \<le> b} = {x. a \<bullet> x = b}"
lp15@62397
   133
proof (cases "a = 0")
lp15@62397
   134
  case True with assms show ?thesis by simp
lp15@62397
   135
next
lp15@62397
   136
  case False then show ?thesis
lp15@62397
   137
    by (force simp: frontier_def closed_halfspace_le)
lp15@62397
   138
qed
lp15@62397
   139
ak2110@69723
   140
lemma frontier_halfspace_ge:
lp15@62397
   141
  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
lp15@62397
   142
    shows "frontier {x. a \<bullet> x \<ge> b} = {x. a \<bullet> x = b}"
lp15@62397
   143
proof (cases "a = 0")
lp15@62397
   144
  case True with assms show ?thesis by simp
lp15@62397
   145
next
lp15@62397
   146
  case False then show ?thesis
lp15@62397
   147
    by (force simp: frontier_def closed_halfspace_ge)
lp15@62397
   148
qed
lp15@62397
   149
ak2110@69723
   150
lemma frontier_halfspace_lt:
lp15@62397
   151
  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
lp15@62397
   152
    shows "frontier {x. a \<bullet> x < b} = {x. a \<bullet> x = b}"
lp15@62397
   153
proof (cases "a = 0")
lp15@62397
   154
  case True with assms show ?thesis by simp
lp15@62397
   155
next
lp15@62397
   156
  case False then show ?thesis
lp15@62397
   157
    by (force simp: frontier_def interior_open open_halfspace_lt)
lp15@62397
   158
qed
lp15@62397
   159
ak2110@69723
   160
lemma frontier_halfspace_gt:
lp15@62397
   161
  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
lp15@62397
   162
    shows "frontier {x. a \<bullet> x > b} = {x. a \<bullet> x = b}"
ak2110@69723
   163
proof (cases "a = 0")
lp15@62397
   164
  case True with assms show ?thesis by simp
lp15@62397
   165
next
lp15@62397
   166
  case False then show ?thesis
lp15@62397
   167
    by (force simp: frontier_def interior_open open_halfspace_gt)
lp15@62397
   168
qed
lp15@62397
   169
ak2110@69723
   170
lemma interior_standard_hyperplane:
wenzelm@67731
   171
   "interior {x :: (real^'n). x$k = a} = {}"
ak2110@69723
   172
proof -
lp15@62397
   173
  have "axis k (1::real) \<noteq> 0"
lp15@62397
   174
    by (simp add: axis_def vec_eq_iff)
lp15@62397
   175
  moreover have "axis k (1::real) \<bullet> x = x$k" for x
lp15@62397
   176
    by (simp add: cart_eq_inner_axis inner_commute)
lp15@62397
   177
  ultimately show ?thesis
lp15@62397
   178
    using interior_hyperplane [of "axis k (1::real)" a]
lp15@62397
   179
    by force
lp15@62397
   180
qed
lp15@62397
   181
ak2110@69723
   182
lemma matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear ((*v) A)" for A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
immler@68072
   183
  using matrix_vector_mul_linear[of A]
immler@68072
   184
  by (simp add: linear_conv_bounded_linear linear_matrix_vector_mul_eq)
immler@68072
   185
ak2110@69723
   186
lemma
immler@68073
   187
  fixes A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
nipkow@69064
   188
  shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont ((*v) A) z"
nipkow@69064
   189
    and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S ((*v) A)"
immler@68072
   190
  by (simp_all add: linear_continuous_at linear_continuous_on)
lp15@67981
   191
hoelzl@37489
   192
immler@69683
   193
subsection\<open>Bounds on components etc.\ relative to operator norm\<close>
lp15@67719
   194
ak2110@69723
   195
lemma norm_column_le_onorm:
lp15@67719
   196
  fixes A :: "real^'n^'m"
nipkow@69064
   197
  shows "norm(column i A) \<le> onorm((*v) A)"
ak2110@69723
   198
proof -
lp15@67719
   199
  have "norm (\<chi> j. A $ j $ i) \<le> norm (A *v axis i 1)"
lp15@67719
   200
    by (simp add: matrix_mult_dot cart_eq_inner_axis)
nipkow@69064
   201
  also have "\<dots> \<le> onorm ((*v) A)"
immler@68072
   202
    using onorm [OF matrix_vector_mul_bounded_linear, of A "axis i 1"] by auto
nipkow@69064
   203
  finally have "norm (\<chi> j. A $ j $ i) \<le> onorm ((*v) A)" .
lp15@67719
   204
  then show ?thesis
lp15@67719
   205
    unfolding column_def .
lp15@67719
   206
qed
lp15@67719
   207
ak2110@69723
   208
lemma matrix_component_le_onorm:
lp15@67719
   209
  fixes A :: "real^'n^'m"
nipkow@69064
   210
  shows "\<bar>A $ i $ j\<bar> \<le> onorm((*v) A)"
ak2110@69723
   211
proof -
lp15@67719
   212
  have "\<bar>A $ i $ j\<bar> \<le> norm (\<chi> n. (A $ n $ j))"
lp15@67719
   213
    by (metis (full_types, lifting) component_le_norm_cart vec_lambda_beta)
nipkow@69064
   214
  also have "\<dots> \<le> onorm ((*v) A)"
lp15@67719
   215
    by (metis (no_types) column_def norm_column_le_onorm)
lp15@67719
   216
  finally show ?thesis .
lp15@67719
   217
qed
lp15@67719
   218
ak2110@69723
   219
lemma component_le_onorm:
lp15@67719
   220
  fixes f :: "real^'m \<Rightarrow> real^'n"
lp15@67719
   221
  shows "linear f \<Longrightarrow> \<bar>matrix f $ i $ j\<bar> \<le> onorm f"
immler@68072
   222
  by (metis linear_matrix_vector_mul_eq matrix_component_le_onorm matrix_vector_mul)
hoelzl@37489
   223
ak2110@69723
   224
lemma onorm_le_matrix_component_sum:
lp15@67719
   225
  fixes A :: "real^'n^'m"
nipkow@69064
   226
  shows "onorm((*v) A) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>A $ i $ j\<bar>)"
ak2110@69723
   227
proof (rule onorm_le)
lp15@67719
   228
  fix x
lp15@67719
   229
  have "norm (A *v x) \<le> (\<Sum>i\<in>UNIV. \<bar>(A *v x) $ i\<bar>)"
lp15@67719
   230
    by (rule norm_le_l1_cart)
lp15@67719
   231
  also have "\<dots> \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>A $ i $ j\<bar> * norm x)"
lp15@67719
   232
  proof (rule sum_mono)
lp15@67719
   233
    fix i
lp15@67719
   234
    have "\<bar>(A *v x) $ i\<bar> \<le> \<bar>\<Sum>j\<in>UNIV. A $ i $ j * x $ j\<bar>"
lp15@67719
   235
      by (simp add: matrix_vector_mult_def)
lp15@67719
   236
    also have "\<dots> \<le> (\<Sum>j\<in>UNIV. \<bar>A $ i $ j * x $ j\<bar>)"
lp15@67719
   237
      by (rule sum_abs)
lp15@67719
   238
    also have "\<dots> \<le> (\<Sum>j\<in>UNIV. \<bar>A $ i $ j\<bar> * norm x)"
lp15@67719
   239
      by (rule sum_mono) (simp add: abs_mult component_le_norm_cart mult_left_mono)
lp15@67719
   240
    finally show "\<bar>(A *v x) $ i\<bar> \<le> (\<Sum>j\<in>UNIV. \<bar>A $ i $ j\<bar> * norm x)" .
lp15@67719
   241
  qed
lp15@67719
   242
  finally show "norm (A *v x) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>A $ i $ j\<bar>) * norm x"
lp15@67719
   243
    by (simp add: sum_distrib_right)
lp15@67719
   244
qed
lp15@67719
   245
ak2110@69723
   246
lemma onorm_le_matrix_component:
lp15@67719
   247
  fixes A :: "real^'n^'m"
lp15@67719
   248
  assumes "\<And>i j. abs(A$i$j) \<le> B"
nipkow@69064
   249
  shows "onorm((*v) A) \<le> real (CARD('m)) * real (CARD('n)) * B"
ak2110@69723
   250
proof (rule onorm_le)
wenzelm@67731
   251
  fix x :: "real^'n::_"
lp15@67719
   252
  have "norm (A *v x) \<le> (\<Sum>i\<in>UNIV. \<bar>(A *v x) $ i\<bar>)"
lp15@67719
   253
    by (rule norm_le_l1_cart)
lp15@67719
   254
  also have "\<dots> \<le> (\<Sum>i::'m \<in>UNIV. real (CARD('n)) * B * norm x)"
lp15@67719
   255
  proof (rule sum_mono)
lp15@67719
   256
    fix i
lp15@67719
   257
    have "\<bar>(A *v x) $ i\<bar> \<le> norm(A $ i) * norm x"
lp15@67719
   258
      by (simp add: matrix_mult_dot Cauchy_Schwarz_ineq2)
lp15@67719
   259
    also have "\<dots> \<le> (\<Sum>j\<in>UNIV. \<bar>A $ i $ j\<bar>) * norm x"
lp15@67719
   260
      by (simp add: mult_right_mono norm_le_l1_cart)
lp15@67719
   261
    also have "\<dots> \<le> real (CARD('n)) * B * norm x"
lp15@67719
   262
      by (simp add: assms sum_bounded_above mult_right_mono)
lp15@67719
   263
    finally show "\<bar>(A *v x) $ i\<bar> \<le> real (CARD('n)) * B * norm x" .
lp15@67719
   264
  qed
lp15@67719
   265
  also have "\<dots> \<le> CARD('m) * real (CARD('n)) * B * norm x"
lp15@67719
   266
    by simp
lp15@67719
   267
  finally show "norm (A *v x) \<le> CARD('m) * real (CARD('n)) * B * norm x" .
lp15@67719
   268
qed
lp15@67719
   269
hoelzl@37489
   270
ak2110@69723
   271
lemma rational_approximation:
lp15@67719
   272
  assumes "e > 0"
lp15@67719
   273
  obtains r::real where "r \<in> \<rat>" "\<bar>r - x\<bar> < e"
lp15@67719
   274
  using Rats_dense_in_real [of "x - e/2" "x + e/2"] assms by auto
lp15@67719
   275
ak2110@69723
   276
proposition matrix_rational_approximation:
lp15@67719
   277
  fixes A :: "real^'n^'m"
lp15@67719
   278
  assumes "e > 0"
lp15@67719
   279
  obtains B where "\<And>i j. B$i$j \<in> \<rat>" "onorm(\<lambda>x. (A - B) *v x) < e"
ak2110@69723
   280
proof -
lp15@67719
   281
  have "\<forall>i j. \<exists>q \<in> \<rat>. \<bar>q - A $ i $ j\<bar> < e / (2 * CARD('m) * CARD('n))"
lp15@67719
   282
    using assms by (force intro: rational_approximation [of "e / (2 * CARD('m) * CARD('n))"])
lp15@67719
   283
  then obtain B where B: "\<And>i j. B$i$j \<in> \<rat>" and Bclo: "\<And>i j. \<bar>B$i$j - A $ i $ j\<bar> < e / (2 * CARD('m) * CARD('n))"
lp15@67719
   284
    by (auto simp: lambda_skolem Bex_def)
lp15@67719
   285
  show ?thesis
lp15@67719
   286
  proof
nipkow@69064
   287
    have "onorm ((*v) (A - B)) \<le> real CARD('m) * real CARD('n) *
lp15@67719
   288
    (e / (2 * real CARD('m) * real CARD('n)))"
lp15@67719
   289
      apply (rule onorm_le_matrix_component)
lp15@67719
   290
      using Bclo by (simp add: abs_minus_commute less_imp_le)
lp15@67719
   291
    also have "\<dots> < e"
lp15@67719
   292
      using \<open>0 < e\<close> by (simp add: divide_simps)
nipkow@69064
   293
    finally show "onorm ((*v) (A - B)) < e" .
lp15@67719
   294
  qed (use B in auto)
lp15@67719
   295
qed
lp15@67719
   296
ak2110@69723
   297
lemma vector_sub_project_orthogonal_cart: "(b::real^'n) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *s b) = 0"
hoelzl@50526
   298
  unfolding inner_simps scalar_mult_eq_scaleR by auto
hoelzl@37489
   299
ak2110@69723
   300
lemma infnorm_cart:"infnorm (x::real^'n) = Sup {\<bar>x$i\<bar> |i. i\<in>UNIV}"
hoelzl@50526
   301
  by (simp add: infnorm_def inner_axis Basis_vec_def) (metis (lifting) inner_axis real_inner_1_right)
hoelzl@37489
   302
ak2110@69723
   303
lemma component_le_infnorm_cart: "\<bar>x$i\<bar> \<le> infnorm (x::real^'n)"
hoelzl@50526
   304
  using Basis_le_infnorm[of "axis i 1" x]
hoelzl@50526
   305
  by (simp add: Basis_vec_def axis_eq_axis inner_axis)
hoelzl@37489
   306
ak2110@69723
   307
lemma continuous_component[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x $ i)"
huffman@44647
   308
  unfolding continuous_def by (rule tendsto_vec_nth)
huffman@44213
   309
ak2110@69723
   310
lemma continuous_on_component[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x $ i)"
huffman@44647
   311
  unfolding continuous_on_def by (fast intro: tendsto_vec_nth)
huffman@44213
   312
ak2110@69723
   313
lemma continuous_on_vec_lambda[continuous_intros]:
hoelzl@63334
   314
  "(\<And>i. continuous_on S (f i)) \<Longrightarrow> continuous_on S (\<lambda>x. \<chi> i. f i x)"
hoelzl@63334
   315
  unfolding continuous_on_def by (auto intro: tendsto_vec_lambda)
hoelzl@63334
   316
ak2110@69723
   317
lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}"
hoelzl@63332
   318
  by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component)
huffman@44213
   319
ak2110@69723
   320
lemma bounded_component_cart: "bounded s \<Longrightarrow> bounded ((\<lambda>x. x $ i) ` s)"
wenzelm@49644
   321
  unfolding bounded_def
wenzelm@49644
   322
  apply clarify
wenzelm@49644
   323
  apply (rule_tac x="x $ i" in exI)
wenzelm@49644
   324
  apply (rule_tac x="e" in exI)
wenzelm@49644
   325
  apply clarify
wenzelm@49644
   326
  apply (rule order_trans [OF dist_vec_nth_le], simp)
wenzelm@49644
   327
  done
hoelzl@37489
   328
ak2110@69723
   329
lemma compact_lemma_cart:
hoelzl@37489
   330
  fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n"
hoelzl@50998
   331
  assumes f: "bounded (range f)"
eberlm@66447
   332
  shows "\<exists>l r. strict_mono r \<and>
hoelzl@37489
   333
        (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
immler@62127
   334
    (is "?th d")
ak2110@69723
   335
proof -
immler@62127
   336
  have "\<forall>d' \<subseteq> d. ?th d'"
immler@62127
   337
    by (rule compact_lemma_general[where unproj=vec_lambda])
immler@62127
   338
      (auto intro!: f bounded_component_cart simp: vec_lambda_eta)
immler@62127
   339
  then show "?th d" by simp
hoelzl@37489
   340
qed
hoelzl@37489
   341
huffman@44136
   342
instance vec :: (heine_borel, finite) heine_borel
hoelzl@37489
   343
proof
hoelzl@50998
   344
  fix f :: "nat \<Rightarrow> 'a ^ 'b"
hoelzl@50998
   345
  assume f: "bounded (range f)"
eberlm@66447
   346
  then obtain l r where r: "strict_mono r"
wenzelm@49644
   347
      and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>UNIV. dist (f (r n) $ i) (l $ i) < e) sequentially"
hoelzl@50998
   348
    using compact_lemma_cart [OF f] by blast
hoelzl@37489
   349
  let ?d = "UNIV::'b set"
hoelzl@37489
   350
  { fix e::real assume "e>0"
hoelzl@37489
   351
    hence "0 < e / (real_of_nat (card ?d))"
wenzelm@49644
   352
      using zero_less_card_finite divide_pos_pos[of e, of "real_of_nat (card ?d)"] by auto
hoelzl@37489
   353
    with l have "eventually (\<lambda>n. \<forall>i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))) sequentially"
hoelzl@37489
   354
      by simp
hoelzl@37489
   355
    moreover
wenzelm@49644
   356
    { fix n
wenzelm@49644
   357
      assume n: "\<forall>i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))"
hoelzl@37489
   358
      have "dist (f (r n)) l \<le> (\<Sum>i\<in>?d. dist (f (r n) $ i) (l $ i))"
nipkow@67155
   359
        unfolding dist_vec_def using zero_le_dist by (rule L2_set_le_sum)
hoelzl@37489
   360
      also have "\<dots> < (\<Sum>i\<in>?d. e / (real_of_nat (card ?d)))"
nipkow@64267
   361
        by (rule sum_strict_mono) (simp_all add: n)
hoelzl@37489
   362
      finally have "dist (f (r n)) l < e" by simp
hoelzl@37489
   363
    }
hoelzl@37489
   364
    ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
lp15@61810
   365
      by (rule eventually_mono)
hoelzl@37489
   366
  }
wenzelm@61973
   367
  hence "((f \<circ> r) \<longlongrightarrow> l) sequentially" unfolding o_def tendsto_iff by simp
eberlm@66447
   368
  with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" by auto
hoelzl@37489
   369
qed
hoelzl@37489
   370
ak2110@69723
   371
lemma interval_cart:
immler@54775
   372
  fixes a :: "real^'n"
immler@54775
   373
  shows "box a b = {x::real^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}"
immler@56188
   374
    and "cbox a b = {x::real^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
immler@56188
   375
  by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def mem_box Basis_vec_def inner_axis)
hoelzl@37489
   376
ak2110@69723
   377
lemma mem_box_cart:
immler@54775
   378
  fixes a :: "real^'n"
immler@54775
   379
  shows "x \<in> box a b \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
immler@56188
   380
    and "x \<in> cbox a b \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
wenzelm@49644
   381
  using interval_cart[of a b] by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def)
hoelzl@37489
   382
ak2110@69723
   383
lemma interval_eq_empty_cart:
wenzelm@49644
   384
  fixes a :: "real^'n"
immler@54775
   385
  shows "(box a b = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1)
immler@56188
   386
    and "(cbox a b = {} \<longleftrightarrow> (\<exists>i. b$i < a$i))" (is ?th2)
wenzelm@49644
   387
proof -
immler@54775
   388
  { fix i x assume as:"b$i \<le> a$i" and x:"x\<in>box a b"
lp15@67673
   389
    hence "a $ i < x $ i \<and> x $ i < b $ i" unfolding mem_box_cart by auto
hoelzl@37489
   390
    hence "a$i < b$i" by auto
wenzelm@49644
   391
    hence False using as by auto }
hoelzl@37489
   392
  moreover
hoelzl@37489
   393
  { assume as:"\<forall>i. \<not> (b$i \<le> a$i)"
hoelzl@37489
   394
    let ?x = "(1/2) *\<^sub>R (a + b)"
hoelzl@37489
   395
    { fix i
hoelzl@37489
   396
      have "a$i < b$i" using as[THEN spec[where x=i]] by auto
hoelzl@37489
   397
      hence "a$i < ((1/2) *\<^sub>R (a+b)) $ i" "((1/2) *\<^sub>R (a+b)) $ i < b$i"
hoelzl@37489
   398
        unfolding vector_smult_component and vector_add_component
wenzelm@49644
   399
        by auto }
lp15@67673
   400
    hence "box a b \<noteq> {}" using mem_box_cart(1)[of "?x" a b] by auto }
hoelzl@37489
   401
  ultimately show ?th1 by blast
hoelzl@37489
   402
immler@56188
   403
  { fix i x assume as:"b$i < a$i" and x:"x\<in>cbox a b"
lp15@67673
   404
    hence "a $ i \<le> x $ i \<and> x $ i \<le> b $ i" unfolding mem_box_cart by auto
hoelzl@37489
   405
    hence "a$i \<le> b$i" by auto
wenzelm@49644
   406
    hence False using as by auto }
hoelzl@37489
   407
  moreover
hoelzl@37489
   408
  { assume as:"\<forall>i. \<not> (b$i < a$i)"
hoelzl@37489
   409
    let ?x = "(1/2) *\<^sub>R (a + b)"
hoelzl@37489
   410
    { fix i
hoelzl@37489
   411
      have "a$i \<le> b$i" using as[THEN spec[where x=i]] by auto
hoelzl@37489
   412
      hence "a$i \<le> ((1/2) *\<^sub>R (a+b)) $ i" "((1/2) *\<^sub>R (a+b)) $ i \<le> b$i"
hoelzl@37489
   413
        unfolding vector_smult_component and vector_add_component
wenzelm@49644
   414
        by auto }
lp15@67673
   415
    hence "cbox a b \<noteq> {}" using mem_box_cart(2)[of "?x" a b] by auto  }
hoelzl@37489
   416
  ultimately show ?th2 by blast
hoelzl@37489
   417
qed
hoelzl@37489
   418
ak2110@69723
   419
lemma interval_ne_empty_cart:
wenzelm@49644
   420
  fixes a :: "real^'n"
immler@56188
   421
  shows "cbox a b \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i \<le> b$i)"
immler@54775
   422
    and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i < b$i)"
hoelzl@37489
   423
  unfolding interval_eq_empty_cart[of a b] by (auto simp add: not_less not_le)
hoelzl@37489
   424
    (* BH: Why doesn't just "auto" work here? *)
hoelzl@37489
   425
ak2110@69723
   426
lemma subset_interval_imp_cart:
wenzelm@49644
   427
  fixes a :: "real^'n"
immler@56188
   428
  shows "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> cbox c d \<subseteq> cbox a b"
immler@56188
   429
    and "(\<forall>i. a$i < c$i \<and> d$i < b$i) \<Longrightarrow> cbox c d \<subseteq> box a b"
immler@56188
   430
    and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> box c d \<subseteq> cbox a b"
immler@54775
   431
    and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> box c d \<subseteq> box a b"
lp15@67673
   432
  unfolding subset_eq[unfolded Ball_def] unfolding mem_box_cart
hoelzl@37489
   433
  by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *)
hoelzl@37489
   434
ak2110@69723
   435
lemma interval_sing:
wenzelm@49644
   436
  fixes a :: "'a::linorder^'n"
wenzelm@49644
   437
  shows "{a .. a} = {a} \<and> {a<..<a} = {}"
wenzelm@49644
   438
  apply (auto simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff)
wenzelm@49644
   439
  done
hoelzl@37489
   440
ak2110@69723
   441
lemma subset_interval_cart:
wenzelm@49644
   442
  fixes a :: "real^'n"
immler@56188
   443
  shows "cbox c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i. c$i \<le> d$i) --> (\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i)" (is ?th1)
immler@56188
   444
    and "cbox c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i. c$i \<le> d$i) --> (\<forall>i. a$i < c$i \<and> d$i < b$i)" (is ?th2)
immler@56188
   445
    and "box c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i. c$i < d$i) --> (\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i)" (is ?th3)
immler@54775
   446
    and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i. c$i < d$i) --> (\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i)" (is ?th4)
immler@56188
   447
  using subset_box[of c d a b] by (simp_all add: Basis_vec_def inner_axis)
hoelzl@37489
   448
ak2110@69723
   449
lemma disjoint_interval_cart:
wenzelm@49644
   450
  fixes a::"real^'n"
immler@56188
   451
  shows "cbox a b \<inter> cbox c d = {} \<longleftrightarrow> (\<exists>i. (b$i < a$i \<or> d$i < c$i \<or> b$i < c$i \<or> d$i < a$i))" (is ?th1)
immler@56188
   452
    and "cbox a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i. (b$i < a$i \<or> d$i \<le> c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th2)
immler@56188
   453
    and "box a b \<inter> cbox c d = {} \<longleftrightarrow> (\<exists>i. (b$i \<le> a$i \<or> d$i < c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th3)
immler@54775
   454
    and "box a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i. (b$i \<le> a$i \<or> d$i \<le> c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th4)
hoelzl@50526
   455
  using disjoint_interval[of a b c d] by (simp_all add: Basis_vec_def inner_axis)
hoelzl@37489
   456
ak2110@69723
   457
lemma Int_interval_cart:
immler@54775
   458
  fixes a :: "real^'n"
immler@56188
   459
  shows "cbox a b \<inter> cbox c d =  {(\<chi> i. max (a$i) (c$i)) .. (\<chi> i. min (b$i) (d$i))}"
lp15@63945
   460
  unfolding Int_interval
immler@56188
   461
  by (auto simp: mem_box less_eq_vec_def)
immler@56188
   462
    (auto simp: Basis_vec_def inner_axis)
hoelzl@37489
   463
ak2110@69723
   464
lemma closed_interval_left_cart:
wenzelm@49644
   465
  fixes b :: "real^'n"
hoelzl@37489
   466
  shows "closed {x::real^'n. \<forall>i. x$i \<le> b$i}"
hoelzl@63332
   467
  by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component)
hoelzl@37489
   468
ak2110@69723
   469
lemma closed_interval_right_cart:
wenzelm@49644
   470
  fixes a::"real^'n"
hoelzl@37489
   471
  shows "closed {x::real^'n. \<forall>i. a$i \<le> x$i}"
hoelzl@63332
   472
  by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component)
hoelzl@37489
   473
ak2110@69723
   474
lemma is_interval_cart:
wenzelm@49644
   475
  "is_interval (s::(real^'n) set) \<longleftrightarrow>
wenzelm@49644
   476
    (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i. ((a$i \<le> x$i \<and> x$i \<le> b$i) \<or> (b$i \<le> x$i \<and> x$i \<le> a$i))) \<longrightarrow> x \<in> s)"
hoelzl@50526
   477
  by (simp add: is_interval_def Ball_def Basis_vec_def inner_axis imp_ex)
hoelzl@37489
   478
ak2110@69723
   479
lemma closed_halfspace_component_le_cart: "closed {x::real^'n. x$i \<le> a}"
nipkow@69669
   480
  by (simp add: closed_Collect_le continuous_on_component)
hoelzl@37489
   481
ak2110@69723
   482
lemma closed_halfspace_component_ge_cart: "closed {x::real^'n. x$i \<ge> a}"
nipkow@69669
   483
  by (simp add: closed_Collect_le continuous_on_component)
hoelzl@37489
   484
ak2110@69723
   485
lemma open_halfspace_component_lt_cart: "open {x::real^'n. x$i < a}"
nipkow@69669
   486
  by (simp add: open_Collect_less continuous_on_component)
wenzelm@49644
   487
ak2110@69723
   488
lemma open_halfspace_component_gt_cart: "open {x::real^'n. x$i  > a}"
nipkow@69669
   489
  by (simp add: open_Collect_less continuous_on_component)
hoelzl@37489
   490
ak2110@69723
   491
lemma Lim_component_le_cart:
wenzelm@49644
   492
  fixes f :: "'a \<Rightarrow> real^'n"
wenzelm@61973
   493
  assumes "(f \<longlongrightarrow> l) net" "\<not> (trivial_limit net)"  "eventually (\<lambda>x. f x $i \<le> b) net"
hoelzl@37489
   494
  shows "l$i \<le> b"
hoelzl@50526
   495
  by (rule tendsto_le[OF assms(2) tendsto_const tendsto_vec_nth, OF assms(1, 3)])
hoelzl@37489
   496
ak2110@69723
   497
lemma Lim_component_ge_cart:
wenzelm@49644
   498
  fixes f :: "'a \<Rightarrow> real^'n"
wenzelm@61973
   499
  assumes "(f \<longlongrightarrow> l) net"  "\<not> (trivial_limit net)"  "eventually (\<lambda>x. b \<le> (f x)$i) net"
hoelzl@37489
   500
  shows "b \<le> l$i"
hoelzl@50526
   501
  by (rule tendsto_le[OF assms(2) tendsto_vec_nth tendsto_const, OF assms(1, 3)])
hoelzl@37489
   502
ak2110@69723
   503
lemma Lim_component_eq_cart:
wenzelm@49644
   504
  fixes f :: "'a \<Rightarrow> real^'n"
nipkow@69508
   505
  assumes net: "(f \<longlongrightarrow> l) net" "\<not> trivial_limit net" and ev:"eventually (\<lambda>x. f(x)$i = b) net"
hoelzl@37489
   506
  shows "l$i = b"
wenzelm@49644
   507
  using ev[unfolded order_eq_iff eventually_conj_iff] and
wenzelm@49644
   508
    Lim_component_ge_cart[OF net, of b i] and
hoelzl@37489
   509
    Lim_component_le_cart[OF net, of i b] by auto
hoelzl@37489
   510
ak2110@69723
   511
lemma connected_ivt_component_cart:
wenzelm@49644
   512
  fixes x :: "real^'n"
wenzelm@49644
   513
  shows "connected s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x$k \<le> a \<Longrightarrow> a \<le> y$k \<Longrightarrow> (\<exists>z\<in>s.  z$k = a)"
hoelzl@50526
   514
  using connected_ivt_hyperplane[of s x y "axis k 1" a]
hoelzl@50526
   515
  by (auto simp add: inner_axis inner_commute)
hoelzl@37489
   516
ak2110@69723
   517
lemma subspace_substandard_cart: "vec.subspace {x. (\<forall>i. P i \<longrightarrow> x$i = 0)}"
immler@68072
   518
  unfolding vec.subspace_def by auto
hoelzl@37489
   519
ak2110@69723
   520
lemma closed_substandard_cart:
huffman@44213
   521
  "closed {x::'a::real_normed_vector ^ 'n. \<forall>i. P i \<longrightarrow> x$i = 0}"
ak2110@69723
   522
proof -
huffman@44213
   523
  { fix i::'n
huffman@44213
   524
    have "closed {x::'a ^ 'n. P i \<longrightarrow> x$i = 0}"
hoelzl@63332
   525
      by (cases "P i") (simp_all add: closed_Collect_eq continuous_on_const continuous_on_id continuous_on_component) }
huffman@44213
   526
  thus ?thesis
huffman@44213
   527
    unfolding Collect_all_eq by (simp add: closed_INT)
hoelzl@37489
   528
qed
hoelzl@37489
   529
immler@69683
   530
subsection "Convex Euclidean Space"
hoelzl@37489
   531
ak2110@69723
   532
lemma Cart_1:"(1::real^'n) = \<Sum>Basis"
hoelzl@50526
   533
  using const_vector_cart[of 1] by (simp add: one_vec_def)
hoelzl@37489
   534
hoelzl@37489
   535
declare vector_add_ldistrib[simp] vector_ssub_ldistrib[simp] vector_smult_assoc[simp] vector_smult_rneg[simp]
hoelzl@37489
   536
declare vector_sadd_rdistrib[simp] vector_sub_rdistrib[simp]
hoelzl@37489
   537
ak2110@69723
   538
lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component less_eq_vec_def vec_lambda_beta vector_uminus_component
hoelzl@37489
   539
ak2110@69723
   540
lemma convex_box_cart:
hoelzl@37489
   541
  assumes "\<And>i. convex {x. P i x}"
hoelzl@37489
   542
  shows "convex {x. \<forall>i. P i (x$i)}"
hoelzl@37489
   543
  using assms unfolding convex_def by auto
hoelzl@37489
   544
ak2110@69723
   545
lemma convex_positive_orthant_cart: "convex {x::real^'n. (\<forall>i. 0 \<le> x$i)}"
hoelzl@63334
   546
  by (rule convex_box_cart) (simp add: atLeast_def[symmetric])
hoelzl@37489
   547
ak2110@69723
   548
lemma unit_interval_convex_hull_cart:
immler@56188
   549
  "cbox (0::real^'n) 1 = convex hull {x. \<forall>i. (x$i = 0) \<or> (x$i = 1)}"
immler@56188
   550
  unfolding Cart_1 unit_interval_convex_hull[where 'a="real^'n"] box_real[symmetric]
hoelzl@50526
   551
  by (rule arg_cong[where f="\<lambda>x. convex hull x"]) (simp add: Basis_vec_def inner_axis)
hoelzl@37489
   552
ak2110@69723
   553
proposition cube_convex_hull_cart:
wenzelm@49644
   554
  assumes "0 < d"
wenzelm@49644
   555
  obtains s::"(real^'n) set"
immler@56188
   556
    where "finite s" "cbox (x - (\<chi> i. d)) (x + (\<chi> i. d)) = convex hull s"
ak2110@69723
   557
proof -
wenzelm@55522
   558
  from assms obtain s where "finite s"
nipkow@69064
   559
    and "cbox (x - sum ((*\<^sub>R) d) Basis) (x + sum ((*\<^sub>R) d) Basis) = convex hull s"
wenzelm@55522
   560
    by (rule cube_convex_hull)
wenzelm@55522
   561
  with that[of s] show thesis
wenzelm@55522
   562
    by (simp add: const_vector_cart)
hoelzl@37489
   563
qed
hoelzl@37489
   564
hoelzl@37489
   565
immler@69683
   566
subsection "Derivative"
hoelzl@37489
   567
ak2110@68833
   568
definition%important "jacobian f net = matrix(frechet_derivative f net)"
hoelzl@37489
   569
ak2110@69723
   570
proposition jacobian_works:
wenzelm@49644
   571
  "(f::(real^'a) \<Rightarrow> (real^'b)) differentiable net \<longleftrightarrow>
lp15@67986
   572
    (f has_derivative (\<lambda>h. (jacobian f net) *v h)) net" (is "?lhs = ?rhs")
ak2110@69723
   573
proof
lp15@67986
   574
  assume ?lhs then show ?rhs
lp15@67986
   575
    by (simp add: frechet_derivative_works has_derivative_linear jacobian_def)
lp15@67986
   576
next
lp15@67986
   577
  assume ?rhs then show ?lhs
lp15@67986
   578
    by (rule differentiableI)
lp15@67986
   579
qed
hoelzl@37489
   580
hoelzl@37489
   581
ak2110@69723
   582
text \<open>Component of the differential must be zero if it exists at a local
nipkow@67968
   583
  maximum or minimum for that corresponding component\<close>
hoelzl@37489
   584
ak2110@69723
   585
proposition differential_zero_maxmin_cart:
wenzelm@49644
   586
  fixes f::"real^'a \<Rightarrow> real^'b"
wenzelm@49644
   587
  assumes "0 < e" "((\<forall>y \<in> ball x e. (f y)$k \<le> (f x)$k) \<or> (\<forall>y\<in>ball x e. (f x)$k \<le> (f y)$k))"
hoelzl@50526
   588
    "f differentiable (at x)"
hoelzl@50526
   589
  shows "jacobian f (at x) $ k = 0"
hoelzl@50526
   590
  using differential_zero_maxmin_component[of "axis k 1" e x f] assms
hoelzl@50526
   591
    vector_cart[of "\<lambda>j. frechet_derivative f (at x) j $ k"]
hoelzl@50526
   592
  by (simp add: Basis_vec_def axis_eq_axis inner_axis jacobian_def matrix_def)
wenzelm@49644
   593
wenzelm@69597
   594
subsection%unimportant\<open>Routine results connecting the types \<^typ>\<open>real^1\<close> and \<^typ>\<open>real\<close>\<close>
lp15@67981
   595
lp15@67981
   596
lemma vec_cbox_1_eq [simp]:
lp15@67981
   597
  shows "vec ` cbox u v = cbox (vec u) (vec v ::real^1)"
lp15@67981
   598
  by (force simp: Basis_vec_def cart_eq_inner_axis [symmetric] mem_box)
lp15@67981
   599
lp15@67981
   600
lemma vec_nth_cbox_1_eq [simp]:
lp15@67981
   601
  fixes u v :: "'a::euclidean_space^1"
lp15@67981
   602
  shows "(\<lambda>x. x $ 1) ` cbox u v = cbox (u$1) (v$1)"
lp15@67981
   603
    by (auto simp: Basis_vec_def cart_eq_inner_axis [symmetric] mem_box image_iff Bex_def inner_axis) (metis vec_component)
lp15@67981
   604
lp15@67981
   605
lemma vec_nth_1_iff_cbox [simp]:
lp15@67981
   606
  fixes a b :: "'a::euclidean_space"
lp15@67981
   607
  shows "(\<lambda>x::'a^1. x $ 1) ` S = cbox a b \<longleftrightarrow> S = cbox (vec a) (vec b)"
lp15@67981
   608
    (is "?lhs = ?rhs")
lp15@67981
   609
proof
lp15@67981
   610
  assume L: ?lhs show ?rhs
lp15@67981
   611
  proof (intro equalityI subsetI)
lp15@67981
   612
    fix x 
lp15@67981
   613
    assume "x \<in> S"
lp15@67981
   614
    then have "x $ 1 \<in> (\<lambda>v. v $ (1::1)) ` cbox (vec a) (vec b)"
lp15@67981
   615
      using L by auto
lp15@67981
   616
    then show "x \<in> cbox (vec a) (vec b)"
lp15@67981
   617
      by (metis (no_types, lifting) imageE vector_one_nth)
lp15@67981
   618
  next
lp15@67981
   619
    fix x :: "'a^1"
lp15@67981
   620
    assume "x \<in> cbox (vec a) (vec b)"
lp15@67981
   621
    then show "x \<in> S"
lp15@67981
   622
      by (metis (no_types, lifting) L imageE imageI vec_component vec_nth_cbox_1_eq vector_one_nth)
lp15@67981
   623
  qed
lp15@67981
   624
qed simp
wenzelm@49644
   625
hoelzl@37489
   626
hoelzl@37489
   627
lemma interval_split_cart:
hoelzl@37489
   628
  "{a..b::real^'n} \<inter> {x. x$k \<le> c} = {a .. (\<chi> i. if i = k then min (b$k) c else b$i)}"
immler@56188
   629
  "cbox a b \<inter> {x. x$k \<ge> c} = {(\<chi> i. if i = k then max (a$k) c else a$i) .. b}"
wenzelm@49644
   630
  apply (rule_tac[!] set_eqI)
lp15@67673
   631
  unfolding Int_iff mem_box_cart mem_Collect_eq interval_cbox_cart
wenzelm@49644
   632
  unfolding vec_lambda_beta
wenzelm@49644
   633
  by auto
hoelzl@37489
   634
immler@67685
   635
lemmas cartesian_euclidean_space_uniform_limit_intros[uniform_limit_intros] =
immler@67685
   636
  bounded_linear.uniform_limit[OF blinfun.bounded_linear_right]
immler@67685
   637
  bounded_linear.uniform_limit[OF bounded_linear_vec_nth]
immler@67685
   638
hoelzl@37489
   639
end