src/HOL/Analysis/Cartesian_Euclidean_Space.thy
 author Angeliki KoutsoukouArgyraki 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 \Finite Cartesian Products of Euclidean Spaces\ ``` 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 {..i\{..j\{..j. j + i * B) {..j. j + i * B) ` {.. {i * B.. (\j. j + i * B) ` {.. cbox a b = {}" ``` lp15@67979 ` 45` ``` "box (vec a) (vec b) = {} \ 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\Closures and interiors of halfspaces\ ``` lp15@62397 ` 49` ak2110@69723 ` 50` ```lemma interior_halfspace_le [simp]: ``` lp15@62397 ` 51` ``` assumes "a \ 0" ``` lp15@62397 ` 52` ``` shows "interior {x. a \ x \ b} = {x. a \ x < b}" ``` ak2110@69723 ` 53` ```proof - ``` lp15@62397 ` 54` ``` have *: "a \ x < b" if x: "x \ S" and S: "S \ {x. a \ x \ b}" and "open S" for S x ``` lp15@62397 ` 55` ``` proof - ``` lp15@62397 ` 56` ``` obtain e where "e>0" and e: "cball x e \ S" ``` lp15@62397 ` 57` ``` using \open S\ open_contains_cball x by blast ``` lp15@62397 ` 58` ``` then have "x + (e / norm a) *\<^sub>R a \ cball x e" ``` lp15@62397 ` 59` ``` by (simp add: dist_norm) ``` lp15@62397 ` 60` ``` then have "x + (e / norm a) *\<^sub>R a \ S" ``` lp15@62397 ` 61` ``` using e by blast ``` lp15@62397 ` 62` ``` then have "x + (e / norm a) *\<^sub>R a \ {x. a \ x \ b}" ``` lp15@62397 ` 63` ``` using S by blast ``` lp15@62397 ` 64` ``` moreover have "e * (a \ a) / norm a > 0" ``` lp15@62397 ` 65` ``` by (simp add: \0 < e\ 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 \ 0 \ interior {x. a \ x \ b} = {x. a \ 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 \ 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 \ a} = {x :: (real^'n). x\$k > a}" (is "?GE") ``` ak2110@69723 ` 81` ```proof - ``` lp15@62397 ` 82` ``` have "axis k (1::real) \ 0" ``` lp15@62397 ` 83` ``` by (simp add: axis_def vec_eq_iff) ``` lp15@62397 ` 84` ``` moreover have "axis k (1::real) \ 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 \ 0" ``` lp15@62397 ` 93` ``` shows "closure {x. a \ x < b} = {x. a \ x \ b}" ``` lp15@62397 ` 94` ```proof - ``` lp15@62397 ` 95` ``` have [simp]: "-{x. a \ x < b} = {x. a \ x \ 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 \ 0 \ closure {x. a \ x > b} = {x. a \ x \ 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 \ 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 \ a}" (is "?GE") ``` ak2110@69723 ` 110` ```proof - ``` lp15@62397 ` 111` ``` have "axis k (1::real) \ 0" ``` lp15@62397 ` 112` ``` by (simp add: axis_def vec_eq_iff) ``` lp15@62397 ` 113` ``` moreover have "axis k (1::real) \ 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 \ 0" ``` lp15@62397 ` 122` ``` shows "interior {x. a \ x = b} = {}" ``` ak2110@69723 ` 123` ```proof - ``` lp15@62397 ` 124` ``` have [simp]: "{x. a \ x = b} = {x. a \ x \ b} \ {x. a \ x \ 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 \ 0 \ b \ 0" ``` lp15@62397 ` 132` ``` shows "frontier {x. a \ x \ b} = {x. a \ 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 \ 0 \ b \ 0" ``` lp15@62397 ` 142` ``` shows "frontier {x. a \ x \ b} = {x. a \ 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 \ 0 \ b \ 0" ``` lp15@62397 ` 152` ``` shows "frontier {x. a \ x < b} = {x. a \ 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 \ 0 \ b \ 0" ``` lp15@62397 ` 162` ``` shows "frontier {x. a \ x > b} = {x. a \ 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) \ 0" ``` lp15@62397 ` 174` ``` by (simp add: axis_def vec_eq_iff) ``` lp15@62397 ` 175` ``` moreover have "axis k (1::real) \ 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\Bounds on components etc.\ relative to operator norm\ ``` 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) \ onorm((*v) A)" ``` ak2110@69723 ` 198` ```proof - ``` lp15@67719 ` 199` ``` have "norm (\ j. A \$ j \$ i) \ norm (A *v axis i 1)" ``` lp15@67719 ` 200` ``` by (simp add: matrix_mult_dot cart_eq_inner_axis) ``` nipkow@69064 ` 201` ``` also have "\ \ 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 (\ j. A \$ j \$ i) \ 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 "\A \$ i \$ j\ \ onorm((*v) A)" ``` ak2110@69723 ` 211` ```proof - ``` lp15@67719 ` 212` ``` have "\A \$ i \$ j\ \ norm (\ n. (A \$ n \$ j))" ``` lp15@67719 ` 213` ``` by (metis (full_types, lifting) component_le_norm_cart vec_lambda_beta) ``` nipkow@69064 ` 214` ``` also have "\ \ 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 \ real^'n" ``` lp15@67719 ` 221` ``` shows "linear f \ \matrix f \$ i \$ j\ \ 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) \ (\i\UNIV. \j\UNIV. \A \$ i \$ j\)" ``` ak2110@69723 ` 227` ```proof (rule onorm_le) ``` lp15@67719 ` 228` ``` fix x ``` lp15@67719 ` 229` ``` have "norm (A *v x) \ (\i\UNIV. \(A *v x) \$ i\)" ``` lp15@67719 ` 230` ``` by (rule norm_le_l1_cart) ``` lp15@67719 ` 231` ``` also have "\ \ (\i\UNIV. \j\UNIV. \A \$ i \$ j\ * norm x)" ``` lp15@67719 ` 232` ``` proof (rule sum_mono) ``` lp15@67719 ` 233` ``` fix i ``` lp15@67719 ` 234` ``` have "\(A *v x) \$ i\ \ \\j\UNIV. A \$ i \$ j * x \$ j\" ``` lp15@67719 ` 235` ``` by (simp add: matrix_vector_mult_def) ``` lp15@67719 ` 236` ``` also have "\ \ (\j\UNIV. \A \$ i \$ j * x \$ j\)" ``` lp15@67719 ` 237` ``` by (rule sum_abs) ``` lp15@67719 ` 238` ``` also have "\ \ (\j\UNIV. \A \$ i \$ j\ * 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 "\(A *v x) \$ i\ \ (\j\UNIV. \A \$ i \$ j\ * norm x)" . ``` lp15@67719 ` 241` ``` qed ``` lp15@67719 ` 242` ``` finally show "norm (A *v x) \ (\i\UNIV. \j\UNIV. \A \$ i \$ j\) * 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 "\i j. abs(A\$i\$j) \ B" ``` nipkow@69064 ` 249` ``` shows "onorm((*v) A) \ 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) \ (\i\UNIV. \(A *v x) \$ i\)" ``` lp15@67719 ` 253` ``` by (rule norm_le_l1_cart) ``` lp15@67719 ` 254` ``` also have "\ \ (\i::'m \UNIV. real (CARD('n)) * B * norm x)" ``` lp15@67719 ` 255` ``` proof (rule sum_mono) ``` lp15@67719 ` 256` ``` fix i ``` lp15@67719 ` 257` ``` have "\(A *v x) \$ i\ \ norm(A \$ i) * norm x" ``` lp15@67719 ` 258` ``` by (simp add: matrix_mult_dot Cauchy_Schwarz_ineq2) ``` lp15@67719 ` 259` ``` also have "\ \ (\j\UNIV. \A \$ i \$ j\) * norm x" ``` lp15@67719 ` 260` ``` by (simp add: mult_right_mono norm_le_l1_cart) ``` lp15@67719 ` 261` ``` also have "\ \ real (CARD('n)) * B * norm x" ``` lp15@67719 ` 262` ``` by (simp add: assms sum_bounded_above mult_right_mono) ``` lp15@67719 ` 263` ``` finally show "\(A *v x) \$ i\ \ real (CARD('n)) * B * norm x" . ``` lp15@67719 ` 264` ``` qed ``` lp15@67719 ` 265` ``` also have "\ \ CARD('m) * real (CARD('n)) * B * norm x" ``` lp15@67719 ` 266` ``` by simp ``` lp15@67719 ` 267` ``` finally show "norm (A *v x) \ 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 \ \" "\r - x\ < 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 "\i j. B\$i\$j \ \" "onorm(\x. (A - B) *v x) < e" ``` ak2110@69723 ` 280` ```proof - ``` lp15@67719 ` 281` ``` have "\i j. \q \ \. \q - A \$ i \$ j\ < 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: "\i j. B\$i\$j \ \" and Bclo: "\i j. \B\$i\$j - A \$ i \$ j\ < 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)) \ 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 "\ < e" ``` lp15@67719 ` 292` ``` using \0 < e\ 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) \ (x - ((b \ x) / (b \ 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 {\x\$i\ |i. i\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: "\x\$i\ \ 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 \ continuous F (\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 \ continuous_on s (\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` ``` "(\i. continuous_on S (f i)) \ continuous_on S (\x. \ 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. \i. 0 \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 \ bounded ((\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 \ 'a::heine_borel ^ 'n" ``` hoelzl@50998 ` 331` ``` assumes f: "bounded (range f)" ``` eberlm@66447 ` 332` ``` shows "\l r. strict_mono r \ ``` hoelzl@37489 ` 333` ``` (\e>0. eventually (\n. \i\d. dist (f (r n) \$ i) (l \$ i) < e) sequentially)" ``` immler@62127 ` 334` ``` (is "?th d") ``` ak2110@69723 ` 335` ```proof - ``` immler@62127 ` 336` ``` have "\d' \ 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 \ '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: "\e>0. eventually (\n. \i\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 (\n. \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: "\i. dist (f (r n) \$ i) (l \$ i) < e / (real_of_nat (card ?d))" ``` hoelzl@37489 ` 358` ``` have "dist (f (r n)) l \ (\i\?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 "\ < (\i\?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 (\n. dist (f (r n)) l < e) sequentially" ``` lp15@61810 ` 365` ``` by (rule eventually_mono) ``` hoelzl@37489 ` 366` ``` } ``` wenzelm@61973 ` 367` ``` hence "((f \ r) \ l) sequentially" unfolding o_def tendsto_iff by simp ``` eberlm@66447 ` 368` ``` with r show "\l r. strict_mono r \ ((f \ r) \ 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. \i. a\$i < x\$i \ x\$i < b\$i}" ``` immler@56188 ` 374` ``` and "cbox a b = {x::real^'n. \i. a\$i \ x\$i \ x\$i \ 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 \ box a b \ (\i. a\$i < x\$i \ x\$i < b\$i)" ``` immler@56188 ` 380` ``` and "x \ cbox a b \ (\i. a\$i \ x\$i \ x\$i \ 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 = {} \ (\i. b\$i \ a\$i))" (is ?th1) ``` immler@56188 ` 386` ``` and "(cbox a b = {} \ (\i. b\$i < a\$i))" (is ?th2) ``` wenzelm@49644 ` 387` ```proof - ``` immler@54775 ` 388` ``` { fix i x assume as:"b\$i \ a\$i" and x:"x\box a b" ``` lp15@67673 ` 389` ``` hence "a \$ i < x \$ i \ 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:"\i. \ (b\$i \ 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 \ {}" 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\cbox a b" ``` lp15@67673 ` 404` ``` hence "a \$ i \ x \$ i \ x \$ i \ b \$ i" unfolding mem_box_cart by auto ``` hoelzl@37489 ` 405` ``` hence "a\$i \ b\$i" by auto ``` wenzelm@49644 ` 406` ``` hence False using as by auto } ``` hoelzl@37489 ` 407` ``` moreover ``` hoelzl@37489 ` 408` ``` { assume as:"\i. \ (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 \ b\$i" using as[THEN spec[where x=i]] by auto ``` hoelzl@37489 ` 412` ``` hence "a\$i \ ((1/2) *\<^sub>R (a+b)) \$ i" "((1/2) *\<^sub>R (a+b)) \$ i \ 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 \ {}" 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 \ {} \ (\i. a\$i \ b\$i)" ``` immler@54775 ` 422` ``` and "box a b \ {} \ (\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 "(\i. a\$i \ c\$i \ d\$i \ b\$i) \ cbox c d \ cbox a b" ``` immler@56188 ` 429` ``` and "(\i. a\$i < c\$i \ d\$i < b\$i) \ cbox c d \ box a b" ``` immler@56188 ` 430` ``` and "(\i. a\$i \ c\$i \ d\$i \ b\$i) \ box c d \ cbox a b" ``` immler@54775 ` 431` ``` and "(\i. a\$i \ c\$i \ d\$i \ b\$i) \ box c d \ 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} \ {a<.. cbox a b \ (\i. c\$i \ d\$i) --> (\i. a\$i \ c\$i \ d\$i \ b\$i)" (is ?th1) ``` immler@56188 ` 444` ``` and "cbox c d \ box a b \ (\i. c\$i \ d\$i) --> (\i. a\$i < c\$i \ d\$i < b\$i)" (is ?th2) ``` immler@56188 ` 445` ``` and "box c d \ cbox a b \ (\i. c\$i < d\$i) --> (\i. a\$i \ c\$i \ d\$i \ b\$i)" (is ?th3) ``` immler@54775 ` 446` ``` and "box c d \ box a b \ (\i. c\$i < d\$i) --> (\i. a\$i \ c\$i \ d\$i \ 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 \ cbox c d = {} \ (\i. (b\$i < a\$i \ d\$i < c\$i \ b\$i < c\$i \ d\$i < a\$i))" (is ?th1) ``` immler@56188 ` 452` ``` and "cbox a b \ box c d = {} \ (\i. (b\$i < a\$i \ d\$i \ c\$i \ b\$i \ c\$i \ d\$i \ a\$i))" (is ?th2) ``` immler@56188 ` 453` ``` and "box a b \ cbox c d = {} \ (\i. (b\$i \ a\$i \ d\$i < c\$i \ b\$i \ c\$i \ d\$i \ a\$i))" (is ?th3) ``` immler@54775 ` 454` ``` and "box a b \ box c d = {} \ (\i. (b\$i \ a\$i \ d\$i \ c\$i \ b\$i \ c\$i \ d\$i \ 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 \ cbox c d = {(\ i. max (a\$i) (c\$i)) .. (\ 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. \i. x\$i \ 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. \i. a\$i \ 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) \ ``` wenzelm@49644 ` 476` ``` (\a\s. \b\s. \x. (\i. ((a\$i \ x\$i \ x\$i \ b\$i) \ (b\$i \ x\$i \ x\$i \ a\$i))) \ x \ 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 \ 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 \ 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 \ real^'n" ``` wenzelm@61973 ` 493` ``` assumes "(f \ l) net" "\ (trivial_limit net)" "eventually (\x. f x \$i \ b) net" ``` hoelzl@37489 ` 494` ``` shows "l\$i \ 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 \ real^'n" ``` wenzelm@61973 ` 499` ``` assumes "(f \ l) net" "\ (trivial_limit net)" "eventually (\x. b \ (f x)\$i) net" ``` hoelzl@37489 ` 500` ``` shows "b \ 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 \ real^'n" ``` nipkow@69508 ` 505` ``` assumes net: "(f \ l) net" "\ trivial_limit net" and ev:"eventually (\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 \ x \ s \ y \ s \ x\$k \ a \ a \ y\$k \ (\z\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. (\i. P i \ 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. \i. P i \ x\$i = 0}" ``` ak2110@69723 ` 522` ```proof - ``` huffman@44213 ` 523` ``` { fix i::'n ``` huffman@44213 ` 524` ``` have "closed {x::'a ^ 'n. P i \ 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) = \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 "\i. convex {x. P i x}" ``` hoelzl@37489 ` 542` ``` shows "convex {x. \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. (\i. 0 \ 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. \i. (x\$i = 0) \ (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="\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 - (\ i. d)) (x + (\ 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) \ (real^'b)) differentiable net \ ``` lp15@67986 ` 572` ``` (f has_derivative (\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 \Component of the differential must be zero if it exists at a local ``` nipkow@67968 ` 583` ``` maximum or minimum for that corresponding component\ ``` hoelzl@37489 ` 584` ak2110@69723 ` 585` ```proposition differential_zero_maxmin_cart: ``` wenzelm@49644 ` 586` ``` fixes f::"real^'a \ real^'b" ``` wenzelm@49644 ` 587` ``` assumes "0 < e" "((\y \ ball x e. (f y)\$k \ (f x)\$k) \ (\y\ball x e. (f x)\$k \ (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 "\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\Routine results connecting the types \<^typ>\real^1\ and \<^typ>\real\\ ``` 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 "(\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 "(\x::'a^1. x \$ 1) ` S = cbox a b \ 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 \ S" ``` lp15@67981 ` 614` ``` then have "x \$ 1 \ (\v. v \$ (1::1)) ` cbox (vec a) (vec b)" ``` lp15@67981 ` 615` ``` using L by auto ``` lp15@67981 ` 616` ``` then show "x \ 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 \ cbox (vec a) (vec b)" ``` lp15@67981 ` 621` ``` then show "x \ 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} \ {x. x\$k \ c} = {a .. (\ i. if i = k then min (b\$k) c else b\$i)}" ``` immler@56188 ` 629` ``` "cbox a b \ {x. x\$k \ c} = {(\ 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 ```