src/HOL/Analysis/Cartesian_Euclidean_Space.thy
 author immler Wed May 02 13:49:38 2018 +0200 (2018-05-02) changeset 68072 493b818e8e10 parent 67986 b65c4a6a015e child 68073 fad29d2a17a5 permissions -rw-r--r--
 nipkow@67968 ` 1` ```section \Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space\ ``` hoelzl@37489 ` 2` hoelzl@37489 ` 3` ```theory Cartesian_Euclidean_Space ``` immler@68072 ` 4` ```imports Cartesian_Space Derivative ``` hoelzl@37489 ` 5` ```begin ``` hoelzl@37489 ` 6` lp15@63016 ` 7` ```lemma subspace_special_hyperplane: "subspace {x. x \$ k = 0}" ``` lp15@63016 ` 8` ``` by (simp add: subspace_def) ``` lp15@63016 ` 9` nipkow@64267 ` 10` ```lemma sum_mult_product: ``` nipkow@64267 ` 11` ``` "sum h {..i\{..j\{..j. j + i * B) {..j. j + i * B) ` {.. {i * B.. (\j. j + i * B) ` {.. cbox a b = {}" ``` lp15@67979 ` 41` ``` "box (vec a) (vec b) = {} \ box a b = {}" ``` lp15@67979 ` 42` ``` by (auto simp: Basis_vec_def mem_box box_eq_empty inner_axis) ``` lp15@67979 ` 43` lp15@62397 ` 44` ```subsection\Closures and interiors of halfspaces\ ``` lp15@62397 ` 45` lp15@62397 ` 46` ```lemma interior_halfspace_le [simp]: ``` lp15@62397 ` 47` ``` assumes "a \ 0" ``` lp15@62397 ` 48` ``` shows "interior {x. a \ x \ b} = {x. a \ x < b}" ``` lp15@62397 ` 49` ```proof - ``` lp15@62397 ` 50` ``` have *: "a \ x < b" if x: "x \ S" and S: "S \ {x. a \ x \ b}" and "open S" for S x ``` lp15@62397 ` 51` ``` proof - ``` lp15@62397 ` 52` ``` obtain e where "e>0" and e: "cball x e \ S" ``` lp15@62397 ` 53` ``` using \open S\ open_contains_cball x by blast ``` lp15@62397 ` 54` ``` then have "x + (e / norm a) *\<^sub>R a \ cball x e" ``` lp15@62397 ` 55` ``` by (simp add: dist_norm) ``` lp15@62397 ` 56` ``` then have "x + (e / norm a) *\<^sub>R a \ S" ``` lp15@62397 ` 57` ``` using e by blast ``` lp15@62397 ` 58` ``` then have "x + (e / norm a) *\<^sub>R a \ {x. a \ x \ b}" ``` lp15@62397 ` 59` ``` using S by blast ``` lp15@62397 ` 60` ``` moreover have "e * (a \ a) / norm a > 0" ``` lp15@62397 ` 61` ``` by (simp add: \0 < e\ assms) ``` lp15@62397 ` 62` ``` ultimately show ?thesis ``` lp15@62397 ` 63` ``` by (simp add: algebra_simps) ``` lp15@62397 ` 64` ``` qed ``` lp15@62397 ` 65` ``` show ?thesis ``` lp15@62397 ` 66` ``` by (rule interior_unique) (auto simp: open_halfspace_lt *) ``` lp15@62397 ` 67` ```qed ``` lp15@62397 ` 68` lp15@62397 ` 69` ```lemma interior_halfspace_ge [simp]: ``` lp15@62397 ` 70` ``` "a \ 0 \ interior {x. a \ x \ b} = {x. a \ x > b}" ``` lp15@62397 ` 71` ```using interior_halfspace_le [of "-a" "-b"] by simp ``` lp15@62397 ` 72` lp15@62397 ` 73` ```lemma interior_halfspace_component_le [simp]: ``` wenzelm@67731 ` 74` ``` "interior {x. x\$k \ a} = {x :: (real^'n). x\$k < a}" (is "?LE") ``` lp15@62397 ` 75` ``` and interior_halfspace_component_ge [simp]: ``` wenzelm@67731 ` 76` ``` "interior {x. x\$k \ a} = {x :: (real^'n). x\$k > a}" (is "?GE") ``` lp15@62397 ` 77` ```proof - ``` lp15@62397 ` 78` ``` have "axis k (1::real) \ 0" ``` lp15@62397 ` 79` ``` by (simp add: axis_def vec_eq_iff) ``` lp15@62397 ` 80` ``` moreover have "axis k (1::real) \ x = x\$k" for x ``` lp15@62397 ` 81` ``` by (simp add: cart_eq_inner_axis inner_commute) ``` lp15@62397 ` 82` ``` ultimately show ?LE ?GE ``` lp15@62397 ` 83` ``` using interior_halfspace_le [of "axis k (1::real)" a] ``` lp15@62397 ` 84` ``` interior_halfspace_ge [of "axis k (1::real)" a] by auto ``` lp15@62397 ` 85` ```qed ``` lp15@62397 ` 86` lp15@62397 ` 87` ```lemma closure_halfspace_lt [simp]: ``` lp15@62397 ` 88` ``` assumes "a \ 0" ``` lp15@62397 ` 89` ``` shows "closure {x. a \ x < b} = {x. a \ x \ b}" ``` lp15@62397 ` 90` ```proof - ``` lp15@62397 ` 91` ``` have [simp]: "-{x. a \ x < b} = {x. a \ x \ b}" ``` lp15@62397 ` 92` ``` by (force simp:) ``` lp15@62397 ` 93` ``` then show ?thesis ``` lp15@62397 ` 94` ``` using interior_halfspace_ge [of a b] assms ``` lp15@62397 ` 95` ``` by (force simp: closure_interior) ``` lp15@62397 ` 96` ```qed ``` lp15@62397 ` 97` lp15@62397 ` 98` ```lemma closure_halfspace_gt [simp]: ``` lp15@62397 ` 99` ``` "a \ 0 \ closure {x. a \ x > b} = {x. a \ x \ b}" ``` lp15@62397 ` 100` ```using closure_halfspace_lt [of "-a" "-b"] by simp ``` lp15@62397 ` 101` lp15@62397 ` 102` ```lemma closure_halfspace_component_lt [simp]: ``` wenzelm@67731 ` 103` ``` "closure {x. x\$k < a} = {x :: (real^'n). x\$k \ a}" (is "?LE") ``` lp15@62397 ` 104` ``` and closure_halfspace_component_gt [simp]: ``` wenzelm@67731 ` 105` ``` "closure {x. x\$k > a} = {x :: (real^'n). x\$k \ a}" (is "?GE") ``` lp15@62397 ` 106` ```proof - ``` lp15@62397 ` 107` ``` have "axis k (1::real) \ 0" ``` lp15@62397 ` 108` ``` by (simp add: axis_def vec_eq_iff) ``` lp15@62397 ` 109` ``` moreover have "axis k (1::real) \ x = x\$k" for x ``` lp15@62397 ` 110` ``` by (simp add: cart_eq_inner_axis inner_commute) ``` lp15@62397 ` 111` ``` ultimately show ?LE ?GE ``` lp15@62397 ` 112` ``` using closure_halfspace_lt [of "axis k (1::real)" a] ``` lp15@62397 ` 113` ``` closure_halfspace_gt [of "axis k (1::real)" a] by auto ``` lp15@62397 ` 114` ```qed ``` lp15@62397 ` 115` lp15@62397 ` 116` ```lemma interior_hyperplane [simp]: ``` lp15@62397 ` 117` ``` assumes "a \ 0" ``` lp15@62397 ` 118` ``` shows "interior {x. a \ x = b} = {}" ``` lp15@62397 ` 119` ```proof - ``` lp15@62397 ` 120` ``` have [simp]: "{x. a \ x = b} = {x. a \ x \ b} \ {x. a \ x \ b}" ``` lp15@62397 ` 121` ``` by (force simp:) ``` lp15@62397 ` 122` ``` then show ?thesis ``` lp15@62397 ` 123` ``` by (auto simp: assms) ``` lp15@62397 ` 124` ```qed ``` lp15@62397 ` 125` lp15@62397 ` 126` ```lemma frontier_halfspace_le: ``` lp15@62397 ` 127` ``` assumes "a \ 0 \ b \ 0" ``` lp15@62397 ` 128` ``` shows "frontier {x. a \ x \ b} = {x. a \ x = b}" ``` lp15@62397 ` 129` ```proof (cases "a = 0") ``` lp15@62397 ` 130` ``` case True with assms show ?thesis by simp ``` lp15@62397 ` 131` ```next ``` lp15@62397 ` 132` ``` case False then show ?thesis ``` lp15@62397 ` 133` ``` by (force simp: frontier_def closed_halfspace_le) ``` lp15@62397 ` 134` ```qed ``` lp15@62397 ` 135` lp15@62397 ` 136` ```lemma frontier_halfspace_ge: ``` lp15@62397 ` 137` ``` assumes "a \ 0 \ b \ 0" ``` lp15@62397 ` 138` ``` shows "frontier {x. a \ x \ b} = {x. a \ x = b}" ``` lp15@62397 ` 139` ```proof (cases "a = 0") ``` lp15@62397 ` 140` ``` case True with assms show ?thesis by simp ``` lp15@62397 ` 141` ```next ``` lp15@62397 ` 142` ``` case False then show ?thesis ``` lp15@62397 ` 143` ``` by (force simp: frontier_def closed_halfspace_ge) ``` lp15@62397 ` 144` ```qed ``` lp15@62397 ` 145` lp15@62397 ` 146` ```lemma frontier_halfspace_lt: ``` lp15@62397 ` 147` ``` assumes "a \ 0 \ b \ 0" ``` lp15@62397 ` 148` ``` shows "frontier {x. a \ x < b} = {x. a \ x = b}" ``` lp15@62397 ` 149` ```proof (cases "a = 0") ``` lp15@62397 ` 150` ``` case True with assms show ?thesis by simp ``` lp15@62397 ` 151` ```next ``` lp15@62397 ` 152` ``` case False then show ?thesis ``` lp15@62397 ` 153` ``` by (force simp: frontier_def interior_open open_halfspace_lt) ``` lp15@62397 ` 154` ```qed ``` lp15@62397 ` 155` lp15@62397 ` 156` ```lemma frontier_halfspace_gt: ``` lp15@62397 ` 157` ``` assumes "a \ 0 \ b \ 0" ``` lp15@62397 ` 158` ``` shows "frontier {x. a \ x > b} = {x. a \ x = b}" ``` lp15@62397 ` 159` ```proof (cases "a = 0") ``` lp15@62397 ` 160` ``` case True with assms show ?thesis by simp ``` lp15@62397 ` 161` ```next ``` lp15@62397 ` 162` ``` case False then show ?thesis ``` lp15@62397 ` 163` ``` by (force simp: frontier_def interior_open open_halfspace_gt) ``` lp15@62397 ` 164` ```qed ``` lp15@62397 ` 165` lp15@62397 ` 166` ```lemma interior_standard_hyperplane: ``` wenzelm@67731 ` 167` ``` "interior {x :: (real^'n). x\$k = a} = {}" ``` lp15@62397 ` 168` ```proof - ``` lp15@62397 ` 169` ``` have "axis k (1::real) \ 0" ``` lp15@62397 ` 170` ``` by (simp add: axis_def vec_eq_iff) ``` lp15@62397 ` 171` ``` moreover have "axis k (1::real) \ x = x\$k" for x ``` lp15@62397 ` 172` ``` by (simp add: cart_eq_inner_axis inner_commute) ``` lp15@62397 ` 173` ``` ultimately show ?thesis ``` lp15@62397 ` 174` ``` using interior_hyperplane [of "axis k (1::real)" a] ``` lp15@62397 ` 175` ``` by force ``` lp15@62397 ` 176` ```qed ``` lp15@62397 ` 177` lp15@67673 ` 178` ```lemma matrix_mult_transpose_dot_column: ``` lp15@67673 ` 179` ``` fixes A :: "real^'n^'n" ``` immler@68072 ` 180` ``` shows "transpose A ** A = (\ i j. inner (column i A) (column j A))" ``` lp15@67673 ` 181` ``` by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def) ``` lp15@67673 ` 182` lp15@67673 ` 183` ```lemma matrix_mult_transpose_dot_row: ``` lp15@67673 ` 184` ``` fixes A :: "real^'n^'n" ``` immler@68072 ` 185` ``` shows "A ** transpose A = (\ i j. inner (row i A) (row j A))" ``` lp15@67673 ` 186` ``` by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def) ``` lp15@67673 ` 187` wenzelm@60420 ` 188` ```text\Two sometimes fruitful ways of looking at matrix-vector multiplication.\ ``` hoelzl@37489 ` 189` immler@68072 ` 190` ```lemma matrix_mult_dot: "A *v x = (\ i. inner (A\$i) x)" ``` huffman@44136 ` 191` ``` by (simp add: matrix_vector_mult_def inner_vec_def) ``` hoelzl@37489 ` 192` hoelzl@37489 ` 193` ```lemma adjoint_matrix: "adjoint(\x. (A::real^'n^'m) *v x) = (\x. transpose A *v x)" ``` hoelzl@37489 ` 194` ``` apply (rule adjoint_unique) ``` wenzelm@49644 ` 195` ``` apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def ``` nipkow@64267 ` 196` ``` sum_distrib_right sum_distrib_left) ``` haftmann@66804 ` 197` ``` apply (subst sum.swap) ``` immler@68072 ` 198` ``` apply (simp add: ac_simps) ``` hoelzl@37489 ` 199` ``` done ``` hoelzl@37489 ` 200` hoelzl@37489 ` 201` ```lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \ real ^'m)" ``` hoelzl@37489 ` 202` ``` shows "matrix(adjoint f) = transpose(matrix f)" ``` immler@68072 ` 203` ```proof - ``` immler@68072 ` 204` ``` have "matrix(adjoint f) = matrix(adjoint (( *v) (matrix f)))" ``` immler@68072 ` 205` ``` by (simp add: lf) ``` immler@68072 ` 206` ``` also have "\ = transpose(matrix f)" ``` immler@68072 ` 207` ``` unfolding adjoint_matrix matrix_of_matrix_vector_mul ``` immler@68072 ` 208` ``` apply rule ``` immler@68072 ` 209` ``` done ``` immler@68072 ` 210` ``` finally show ?thesis . ``` immler@68072 ` 211` ```qed ``` wenzelm@49644 ` 212` immler@68072 ` 213` ```lemma matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear (( *v) A)" for A :: "real^'n^'m" ``` immler@68072 ` 214` ``` using matrix_vector_mul_linear[of A] ``` immler@68072 ` 215` ``` by (simp add: linear_conv_bounded_linear linear_matrix_vector_mul_eq) ``` immler@68072 ` 216` immler@68072 ` 217` ```lemma ``` immler@68072 ` 218` ``` fixes A :: "real^'n^'m" ``` immler@68072 ` 219` ``` shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont (( *v) A) z" ``` immler@68072 ` 220` ``` and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S (( *v) A)" ``` immler@68072 ` 221` ``` by (simp_all add: linear_continuous_at linear_continuous_on) ``` lp15@67981 ` 222` hoelzl@37489 ` 223` nipkow@67968 ` 224` ```subsection\Some bounds on components etc. relative to operator norm\ ``` lp15@67719 ` 225` lp15@67719 ` 226` ```lemma norm_column_le_onorm: ``` lp15@67719 ` 227` ``` fixes A :: "real^'n^'m" ``` lp15@67719 ` 228` ``` shows "norm(column i A) \ onorm(( *v) A)" ``` lp15@67719 ` 229` ```proof - ``` lp15@67719 ` 230` ``` have "norm (\ j. A \$ j \$ i) \ norm (A *v axis i 1)" ``` lp15@67719 ` 231` ``` by (simp add: matrix_mult_dot cart_eq_inner_axis) ``` lp15@67719 ` 232` ``` also have "\ \ onorm (( *v) A)" ``` immler@68072 ` 233` ``` using onorm [OF matrix_vector_mul_bounded_linear, of A "axis i 1"] by auto ``` lp15@67719 ` 234` ``` finally have "norm (\ j. A \$ j \$ i) \ onorm (( *v) A)" . ``` lp15@67719 ` 235` ``` then show ?thesis ``` lp15@67719 ` 236` ``` unfolding column_def . ``` lp15@67719 ` 237` ```qed ``` lp15@67719 ` 238` lp15@67719 ` 239` ```lemma matrix_component_le_onorm: ``` lp15@67719 ` 240` ``` fixes A :: "real^'n^'m" ``` lp15@67719 ` 241` ``` shows "\A \$ i \$ j\ \ onorm(( *v) A)" ``` lp15@67719 ` 242` ```proof - ``` lp15@67719 ` 243` ``` have "\A \$ i \$ j\ \ norm (\ n. (A \$ n \$ j))" ``` lp15@67719 ` 244` ``` by (metis (full_types, lifting) component_le_norm_cart vec_lambda_beta) ``` lp15@67719 ` 245` ``` also have "\ \ onorm (( *v) A)" ``` lp15@67719 ` 246` ``` by (metis (no_types) column_def norm_column_le_onorm) ``` lp15@67719 ` 247` ``` finally show ?thesis . ``` lp15@67719 ` 248` ```qed ``` lp15@67719 ` 249` lp15@67719 ` 250` ```lemma component_le_onorm: ``` lp15@67719 ` 251` ``` fixes f :: "real^'m \ real^'n" ``` lp15@67719 ` 252` ``` shows "linear f \ \matrix f \$ i \$ j\ \ onorm f" ``` immler@68072 ` 253` ``` by (metis linear_matrix_vector_mul_eq matrix_component_le_onorm matrix_vector_mul) ``` hoelzl@37489 ` 254` lp15@67719 ` 255` ```lemma onorm_le_matrix_component_sum: ``` lp15@67719 ` 256` ``` fixes A :: "real^'n^'m" ``` lp15@67719 ` 257` ``` shows "onorm(( *v) A) \ (\i\UNIV. \j\UNIV. \A \$ i \$ j\)" ``` lp15@67719 ` 258` ```proof (rule onorm_le) ``` lp15@67719 ` 259` ``` fix x ``` lp15@67719 ` 260` ``` have "norm (A *v x) \ (\i\UNIV. \(A *v x) \$ i\)" ``` lp15@67719 ` 261` ``` by (rule norm_le_l1_cart) ``` lp15@67719 ` 262` ``` also have "\ \ (\i\UNIV. \j\UNIV. \A \$ i \$ j\ * norm x)" ``` lp15@67719 ` 263` ``` proof (rule sum_mono) ``` lp15@67719 ` 264` ``` fix i ``` lp15@67719 ` 265` ``` have "\(A *v x) \$ i\ \ \\j\UNIV. A \$ i \$ j * x \$ j\" ``` lp15@67719 ` 266` ``` by (simp add: matrix_vector_mult_def) ``` lp15@67719 ` 267` ``` also have "\ \ (\j\UNIV. \A \$ i \$ j * x \$ j\)" ``` lp15@67719 ` 268` ``` by (rule sum_abs) ``` lp15@67719 ` 269` ``` also have "\ \ (\j\UNIV. \A \$ i \$ j\ * norm x)" ``` lp15@67719 ` 270` ``` by (rule sum_mono) (simp add: abs_mult component_le_norm_cart mult_left_mono) ``` lp15@67719 ` 271` ``` finally show "\(A *v x) \$ i\ \ (\j\UNIV. \A \$ i \$ j\ * norm x)" . ``` lp15@67719 ` 272` ``` qed ``` lp15@67719 ` 273` ``` finally show "norm (A *v x) \ (\i\UNIV. \j\UNIV. \A \$ i \$ j\) * norm x" ``` lp15@67719 ` 274` ``` by (simp add: sum_distrib_right) ``` lp15@67719 ` 275` ```qed ``` lp15@67719 ` 276` lp15@67719 ` 277` ```lemma onorm_le_matrix_component: ``` lp15@67719 ` 278` ``` fixes A :: "real^'n^'m" ``` lp15@67719 ` 279` ``` assumes "\i j. abs(A\$i\$j) \ B" ``` lp15@67719 ` 280` ``` shows "onorm(( *v) A) \ real (CARD('m)) * real (CARD('n)) * B" ``` lp15@67719 ` 281` ```proof (rule onorm_le) ``` wenzelm@67731 ` 282` ``` fix x :: "real^'n::_" ``` lp15@67719 ` 283` ``` have "norm (A *v x) \ (\i\UNIV. \(A *v x) \$ i\)" ``` lp15@67719 ` 284` ``` by (rule norm_le_l1_cart) ``` lp15@67719 ` 285` ``` also have "\ \ (\i::'m \UNIV. real (CARD('n)) * B * norm x)" ``` lp15@67719 ` 286` ``` proof (rule sum_mono) ``` lp15@67719 ` 287` ``` fix i ``` lp15@67719 ` 288` ``` have "\(A *v x) \$ i\ \ norm(A \$ i) * norm x" ``` lp15@67719 ` 289` ``` by (simp add: matrix_mult_dot Cauchy_Schwarz_ineq2) ``` lp15@67719 ` 290` ``` also have "\ \ (\j\UNIV. \A \$ i \$ j\) * norm x" ``` lp15@67719 ` 291` ``` by (simp add: mult_right_mono norm_le_l1_cart) ``` lp15@67719 ` 292` ``` also have "\ \ real (CARD('n)) * B * norm x" ``` lp15@67719 ` 293` ``` by (simp add: assms sum_bounded_above mult_right_mono) ``` lp15@67719 ` 294` ``` finally show "\(A *v x) \$ i\ \ real (CARD('n)) * B * norm x" . ``` lp15@67719 ` 295` ``` qed ``` lp15@67719 ` 296` ``` also have "\ \ CARD('m) * real (CARD('n)) * B * norm x" ``` lp15@67719 ` 297` ``` by simp ``` lp15@67719 ` 298` ``` finally show "norm (A *v x) \ CARD('m) * real (CARD('n)) * B * norm x" . ``` lp15@67719 ` 299` ```qed ``` lp15@67719 ` 300` lp15@67719 ` 301` ```subsection \lambda skolemization on cartesian products\ ``` hoelzl@37489 ` 302` hoelzl@37489 ` 303` ```lemma lambda_skolem: "(\i. \x. P i x) \ ``` hoelzl@37494 ` 304` ``` (\x::'a ^ 'n. \i. P i (x \$ i))" (is "?lhs \ ?rhs") ``` wenzelm@49644 ` 305` ```proof - ``` hoelzl@37489 ` 306` ``` let ?S = "(UNIV :: 'n set)" ``` wenzelm@49644 ` 307` ``` { assume H: "?rhs" ``` wenzelm@49644 ` 308` ``` then have ?lhs by auto } ``` hoelzl@37489 ` 309` ``` moreover ``` wenzelm@49644 ` 310` ``` { assume H: "?lhs" ``` hoelzl@37489 ` 311` ``` then obtain f where f:"\i. P i (f i)" unfolding choice_iff by metis ``` hoelzl@37489 ` 312` ``` let ?x = "(\ i. (f i)) :: 'a ^ 'n" ``` wenzelm@49644 ` 313` ``` { fix i ``` hoelzl@37489 ` 314` ``` from f have "P i (f i)" by metis ``` hoelzl@37494 ` 315` ``` then have "P i (?x \$ i)" by auto ``` hoelzl@37489 ` 316` ``` } ``` hoelzl@37489 ` 317` ``` hence "\i. P i (?x\$i)" by metis ``` hoelzl@37489 ` 318` ``` hence ?rhs by metis } ``` hoelzl@37489 ` 319` ``` ultimately show ?thesis by metis ``` hoelzl@37489 ` 320` ```qed ``` hoelzl@37489 ` 321` lp15@67719 ` 322` ```lemma rational_approximation: ``` lp15@67719 ` 323` ``` assumes "e > 0" ``` lp15@67719 ` 324` ``` obtains r::real where "r \ \" "\r - x\ < e" ``` lp15@67719 ` 325` ``` using Rats_dense_in_real [of "x - e/2" "x + e/2"] assms by auto ``` lp15@67719 ` 326` lp15@67719 ` 327` ```lemma matrix_rational_approximation: ``` lp15@67719 ` 328` ``` fixes A :: "real^'n^'m" ``` lp15@67719 ` 329` ``` assumes "e > 0" ``` lp15@67719 ` 330` ``` obtains B where "\i j. B\$i\$j \ \" "onorm(\x. (A - B) *v x) < e" ``` lp15@67719 ` 331` ```proof - ``` lp15@67719 ` 332` ``` have "\i j. \q \ \. \q - A \$ i \$ j\ < e / (2 * CARD('m) * CARD('n))" ``` lp15@67719 ` 333` ``` using assms by (force intro: rational_approximation [of "e / (2 * CARD('m) * CARD('n))"]) ``` lp15@67719 ` 334` ``` 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 ` 335` ``` by (auto simp: lambda_skolem Bex_def) ``` lp15@67719 ` 336` ``` show ?thesis ``` lp15@67719 ` 337` ``` proof ``` lp15@67719 ` 338` ``` have "onorm (( *v) (A - B)) \ real CARD('m) * real CARD('n) * ``` lp15@67719 ` 339` ``` (e / (2 * real CARD('m) * real CARD('n)))" ``` lp15@67719 ` 340` ``` apply (rule onorm_le_matrix_component) ``` lp15@67719 ` 341` ``` using Bclo by (simp add: abs_minus_commute less_imp_le) ``` lp15@67719 ` 342` ``` also have "\ < e" ``` lp15@67719 ` 343` ``` using \0 < e\ by (simp add: divide_simps) ``` lp15@67719 ` 344` ``` finally show "onorm (( *v) (A - B)) < e" . ``` lp15@67719 ` 345` ``` qed (use B in auto) ``` lp15@67719 ` 346` ```qed ``` lp15@67719 ` 347` hoelzl@37489 ` 348` ```lemma vector_sub_project_orthogonal_cart: "(b::real^'n) \ (x - ((b \ x) / (b \ b)) *s b) = 0" ``` hoelzl@50526 ` 349` ``` unfolding inner_simps scalar_mult_eq_scaleR by auto ``` hoelzl@37489 ` 350` hoelzl@37489 ` 351` ```lemma matrix_left_invertible_injective: ``` immler@68072 ` 352` ``` fixes A :: "'a::field^'n^'m" ``` lp15@67986 ` 353` ``` shows "(\B. B ** A = mat 1) \ inj (( *v) A)" ``` lp15@67986 ` 354` ```proof safe ``` lp15@67986 ` 355` ``` fix B ``` lp15@67986 ` 356` ``` assume B: "B ** A = mat 1" ``` lp15@67986 ` 357` ``` show "inj (( *v) A)" ``` lp15@67986 ` 358` ``` unfolding inj_on_def ``` lp15@67986 ` 359` ``` by (metis B matrix_vector_mul_assoc matrix_vector_mul_lid) ``` lp15@67986 ` 360` ```next ``` lp15@67986 ` 361` ``` assume "inj (( *v) A)" ``` immler@68072 ` 362` ``` from vec.linear_injective_left_inverse[OF matrix_vector_mul_linear_gen this] ``` immler@68072 ` 363` ``` obtain g where "Vector_Spaces.linear ( *s) ( *s) g" and g: "g \ ( *v) A = id" ``` lp15@67986 ` 364` ``` by blast ``` lp15@67986 ` 365` ``` have "matrix g ** A = mat 1" ``` immler@68072 ` 366` ``` by (metis matrix_vector_mul_linear_gen \Vector_Spaces.linear ( *s) ( *s) g\ g matrix_compose_gen ``` immler@68072 ` 367` ``` matrix_eq matrix_id_mat_1 matrix_vector_mul(1)) ``` lp15@67986 ` 368` ``` then show "\B. B ** A = mat 1" ``` lp15@67986 ` 369` ``` by metis ``` hoelzl@37489 ` 370` ```qed ``` hoelzl@37489 ` 371` hoelzl@37489 ` 372` ```lemma matrix_right_invertible_surjective: ``` immler@68072 ` 373` ``` "(\B. (A::'a::field^'n^'m) ** (B::'a::field^'m^'n) = mat 1) \ surj (\x. A *v x)" ``` wenzelm@49644 ` 374` ```proof - ``` immler@68072 ` 375` ``` { fix B :: "'a ^'m^'n" ``` wenzelm@49644 ` 376` ``` assume AB: "A ** B = mat 1" ``` immler@68072 ` 377` ``` { fix x :: "'a ^ 'm" ``` hoelzl@37489 ` 378` ``` have "A *v (B *v x) = x" ``` immler@68072 ` 379` ``` by (simp add: matrix_vector_mul_assoc AB) } ``` nipkow@67399 ` 380` ``` hence "surj (( *v) A)" unfolding surj_def by metis } ``` hoelzl@37489 ` 381` ``` moreover ``` nipkow@67399 ` 382` ``` { assume sf: "surj (( *v) A)" ``` immler@68072 ` 383` ``` from vec.linear_surjective_right_inverse[OF _ this] ``` immler@68072 ` 384` ``` obtain g:: "'a ^'m \ 'a ^'n" where g: "Vector_Spaces.linear ( *s) ( *s) g" "( *v) A \ g = id" ``` hoelzl@37489 ` 385` ``` by blast ``` hoelzl@37489 ` 386` hoelzl@37489 ` 387` ``` have "A ** (matrix g) = mat 1" ``` hoelzl@37489 ` 388` ``` unfolding matrix_eq matrix_vector_mul_lid ``` hoelzl@37489 ` 389` ``` matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)] ``` huffman@44165 ` 390` ``` using g(2) unfolding o_def fun_eq_iff id_def ``` hoelzl@37489 ` 391` ``` . ``` immler@68072 ` 392` ``` hence "\B. A ** (B::'a^'m^'n) = mat 1" by blast ``` hoelzl@37489 ` 393` ``` } ``` hoelzl@37489 ` 394` ``` ultimately show ?thesis unfolding surj_def by blast ``` hoelzl@37489 ` 395` ```qed ``` hoelzl@37489 ` 396` hoelzl@37489 ` 397` ```lemma matrix_right_invertible_span_columns: ``` immler@68072 ` 398` ``` "(\(B::'a::field ^'n^'m). (A::'a ^'m^'n) ** B = mat 1) \ ``` immler@68072 ` 399` ``` vec.span (columns A) = UNIV" (is "?lhs = ?rhs") ``` wenzelm@49644 ` 400` ```proof - ``` hoelzl@37489 ` 401` ``` let ?U = "UNIV :: 'm set" ``` hoelzl@37489 ` 402` ``` have fU: "finite ?U" by simp ``` immler@68072 ` 403` ``` have lhseq: "?lhs \ (\y. \(x::'a^'m). sum (\i. (x\$i) *s column i A) ?U = y)" ``` lp15@67673 ` 404` ``` unfolding matrix_right_invertible_surjective matrix_mult_sum surj_def ``` wenzelm@49644 ` 405` ``` apply (subst eq_commute) ``` wenzelm@49644 ` 406` ``` apply rule ``` wenzelm@49644 ` 407` ``` done ``` immler@68072 ` 408` ``` have rhseq: "?rhs \ (\x. x \ vec.span (columns A))" by blast ``` wenzelm@49644 ` 409` ``` { assume h: ?lhs ``` immler@68072 ` 410` ``` { fix x:: "'a ^'n" ``` immler@68072 ` 411` ``` from h[unfolded lhseq, rule_format, of x] obtain y :: "'a ^'m" ``` nipkow@64267 ` 412` ``` where y: "sum (\i. (y\$i) *s column i A) ?U = x" by blast ``` immler@68072 ` 413` ``` have "x \ vec.span (columns A)" ``` wenzelm@49644 ` 414` ``` unfolding y[symmetric] ``` immler@68072 ` 415` ``` apply (rule vec.span_sum) ``` immler@68072 ` 416` ``` apply (rule vec.span_scale) ``` immler@68072 ` 417` ``` apply (rule vec.span_base) ``` wenzelm@49644 ` 418` ``` unfolding columns_def ``` wenzelm@49644 ` 419` ``` apply blast ``` wenzelm@49644 ` 420` ``` done ``` wenzelm@49644 ` 421` ``` } ``` wenzelm@49644 ` 422` ``` then have ?rhs unfolding rhseq by blast } ``` hoelzl@37489 ` 423` ``` moreover ``` wenzelm@49644 ` 424` ``` { assume h:?rhs ``` immler@68072 ` 425` ``` let ?P = "\(y::'a ^'n). \(x::'a^'m). sum (\i. (x\$i) *s column i A) ?U = y" ``` wenzelm@49644 ` 426` ``` { fix y ``` immler@68072 ` 427` ``` have "y \ vec.span (columns A)" ``` immler@68072 ` 428` ``` unfolding h by blast ``` immler@68072 ` 429` ``` then have "?P y" ``` immler@68072 ` 430` ``` proof (induction rule: vec.span_induct_alt) ``` immler@68072 ` 431` ``` show "\x::'a ^ 'm. sum (\i. (x\$i) *s column i A) ?U = 0" ``` hoelzl@37489 ` 432` ``` by (rule exI[where x=0], simp) ``` hoelzl@37489 ` 433` ``` next ``` wenzelm@49644 ` 434` ``` fix c y1 y2 ``` wenzelm@49644 ` 435` ``` assume y1: "y1 \ columns A" and y2: "?P y2" ``` hoelzl@37489 ` 436` ``` from y1 obtain i where i: "i \ ?U" "y1 = column i A" ``` hoelzl@37489 ` 437` ``` unfolding columns_def by blast ``` immler@68072 ` 438` ``` from y2 obtain x:: "'a ^'m" where ``` nipkow@64267 ` 439` ``` x: "sum (\i. (x\$i) *s column i A) ?U = y2" by blast ``` immler@68072 ` 440` ``` let ?x = "(\ j. if j = i then c + (x\$i) else (x\$j))::'a^'m" ``` hoelzl@37489 ` 441` ``` show "?P (c*s y1 + y2)" ``` immler@68072 ` 442` ``` proof (rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib distrib_left if_distribR cong del: if_weak_cong) ``` wenzelm@49644 ` 443` ``` fix j ``` wenzelm@49644 ` 444` ``` have th: "\xa \ ?U. (if xa = i then (c + (x\$i)) * ((column xa A)\$j) ``` wenzelm@49644 ` 445` ``` else (x\$xa) * ((column xa A\$j))) = (if xa = i then c * ((column i A)\$j) else 0) + ((x\$xa) * ((column xa A)\$j))" ``` wenzelm@49644 ` 446` ``` using i(1) by (simp add: field_simps) ``` nipkow@64267 ` 447` ``` have "sum (\xa. if xa = i then (c + (x\$i)) * ((column xa A)\$j) ``` nipkow@64267 ` 448` ``` else (x\$xa) * ((column xa A\$j))) ?U = sum (\xa. (if xa = i then c * ((column i A)\$j) else 0) + ((x\$xa) * ((column xa A)\$j))) ?U" ``` nipkow@64267 ` 449` ``` apply (rule sum.cong[OF refl]) ``` wenzelm@49644 ` 450` ``` using th apply blast ``` wenzelm@49644 ` 451` ``` done ``` nipkow@64267 ` 452` ``` also have "\ = sum (\xa. if xa = i then c * ((column i A)\$j) else 0) ?U + sum (\xa. ((x\$xa) * ((column xa A)\$j))) ?U" ``` nipkow@64267 ` 453` ``` by (simp add: sum.distrib) ``` nipkow@64267 ` 454` ``` also have "\ = c * ((column i A)\$j) + sum (\xa. ((x\$xa) * ((column xa A)\$j))) ?U" ``` nipkow@64267 ` 455` ``` unfolding sum.delta[OF fU] ``` wenzelm@49644 ` 456` ``` using i(1) by simp ``` nipkow@64267 ` 457` ``` finally show "sum (\xa. if xa = i then (c + (x\$i)) * ((column xa A)\$j) ``` nipkow@64267 ` 458` ``` else (x\$xa) * ((column xa A\$j))) ?U = c * ((column i A)\$j) + sum (\xa. ((x\$xa) * ((column xa A)\$j))) ?U" . ``` wenzelm@49644 ` 459` ``` qed ``` wenzelm@49644 ` 460` ``` qed ``` wenzelm@49644 ` 461` ``` } ``` wenzelm@49644 ` 462` ``` then have ?lhs unfolding lhseq .. ``` wenzelm@49644 ` 463` ``` } ``` hoelzl@37489 ` 464` ``` ultimately show ?thesis by blast ``` hoelzl@37489 ` 465` ```qed ``` hoelzl@37489 ` 466` immler@68072 ` 467` ```lemma matrix_left_invertible_span_rows_gen: ``` immler@68072 ` 468` ``` "(\(B::'a^'m^'n). B ** (A::'a::field^'n^'m) = mat 1) \ vec.span (rows A) = UNIV" ``` hoelzl@37489 ` 469` ``` unfolding right_invertible_transpose[symmetric] ``` hoelzl@37489 ` 470` ``` unfolding columns_transpose[symmetric] ``` hoelzl@37489 ` 471` ``` unfolding matrix_right_invertible_span_columns ``` wenzelm@49644 ` 472` ``` .. ``` hoelzl@37489 ` 473` immler@68072 ` 474` ```lemma matrix_left_invertible_span_rows: ``` immler@68072 ` 475` ``` "(\(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \ span (rows A) = UNIV" ``` immler@68072 ` 476` ``` using matrix_left_invertible_span_rows_gen[of A] by (simp add: span_vec_eq) ``` immler@68072 ` 477` immler@68072 ` 478` wenzelm@60420 ` 479` ```text \The same result in terms of square matrices.\ ``` hoelzl@37489 ` 480` hoelzl@37489 ` 481` wenzelm@60420 ` 482` ```text \Considering an n-element vector as an n-by-1 or 1-by-n matrix.\ ``` hoelzl@37489 ` 483` hoelzl@37489 ` 484` ```definition "rowvector v = (\ i j. (v\$j))" ``` hoelzl@37489 ` 485` hoelzl@37489 ` 486` ```definition "columnvector v = (\ i j. (v\$i))" ``` hoelzl@37489 ` 487` wenzelm@49644 ` 488` ```lemma transpose_columnvector: "transpose(columnvector v) = rowvector v" ``` huffman@44136 ` 489` ``` by (simp add: transpose_def rowvector_def columnvector_def vec_eq_iff) ``` hoelzl@37489 ` 490` hoelzl@37489 ` 491` ```lemma transpose_rowvector: "transpose(rowvector v) = columnvector v" ``` huffman@44136 ` 492` ``` by (simp add: transpose_def columnvector_def rowvector_def vec_eq_iff) ``` hoelzl@37489 ` 493` wenzelm@49644 ` 494` ```lemma dot_rowvector_columnvector: "columnvector (A *v v) = A ** columnvector v" ``` hoelzl@37489 ` 495` ``` by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def) ``` hoelzl@37489 ` 496` wenzelm@49644 ` 497` ```lemma dot_matrix_product: ``` wenzelm@49644 ` 498` ``` "(x::real^'n) \ y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))\$1)\$1" ``` huffman@44136 ` 499` ``` by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def) ``` hoelzl@37489 ` 500` hoelzl@37489 ` 501` ```lemma dot_matrix_vector_mul: ``` hoelzl@37489 ` 502` ``` fixes A B :: "real ^'n ^'n" and x y :: "real ^'n" ``` hoelzl@37489 ` 503` ``` shows "(A *v x) \ (B *v y) = ``` hoelzl@37489 ` 504` ``` (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))\$1)\$1" ``` wenzelm@49644 ` 505` ``` unfolding dot_matrix_product transpose_columnvector[symmetric] ``` wenzelm@49644 ` 506` ``` dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc .. ``` hoelzl@37489 ` 507` wenzelm@61945 ` 508` ```lemma infnorm_cart:"infnorm (x::real^'n) = Sup {\x\$i\ |i. i\UNIV}" ``` hoelzl@50526 ` 509` ``` by (simp add: infnorm_def inner_axis Basis_vec_def) (metis (lifting) inner_axis real_inner_1_right) ``` hoelzl@37489 ` 510` wenzelm@49644 ` 511` ```lemma component_le_infnorm_cart: "\x\$i\ \ infnorm (x::real^'n)" ``` hoelzl@50526 ` 512` ``` using Basis_le_infnorm[of "axis i 1" x] ``` hoelzl@50526 ` 513` ``` by (simp add: Basis_vec_def axis_eq_axis inner_axis) ``` hoelzl@37489 ` 514` hoelzl@63334 ` 515` ```lemma continuous_component[continuous_intros]: "continuous F f \ continuous F (\x. f x \$ i)" ``` huffman@44647 ` 516` ``` unfolding continuous_def by (rule tendsto_vec_nth) ``` huffman@44213 ` 517` hoelzl@63334 ` 518` ```lemma continuous_on_component[continuous_intros]: "continuous_on s f \ continuous_on s (\x. f x \$ i)" ``` huffman@44647 ` 519` ``` unfolding continuous_on_def by (fast intro: tendsto_vec_nth) ``` huffman@44213 ` 520` hoelzl@63334 ` 521` ```lemma continuous_on_vec_lambda[continuous_intros]: ``` hoelzl@63334 ` 522` ``` "(\i. continuous_on S (f i)) \ continuous_on S (\x. \ i. f i x)" ``` hoelzl@63334 ` 523` ``` unfolding continuous_on_def by (auto intro: tendsto_vec_lambda) ``` hoelzl@63334 ` 524` hoelzl@37489 ` 525` ```lemma closed_positive_orthant: "closed {x::real^'n. \i. 0 \x\$i}" ``` hoelzl@63332 ` 526` ``` by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) ``` huffman@44213 ` 527` hoelzl@37489 ` 528` ```lemma bounded_component_cart: "bounded s \ bounded ((\x. x \$ i) ` s)" ``` wenzelm@49644 ` 529` ``` unfolding bounded_def ``` wenzelm@49644 ` 530` ``` apply clarify ``` wenzelm@49644 ` 531` ``` apply (rule_tac x="x \$ i" in exI) ``` wenzelm@49644 ` 532` ``` apply (rule_tac x="e" in exI) ``` wenzelm@49644 ` 533` ``` apply clarify ``` wenzelm@49644 ` 534` ``` apply (rule order_trans [OF dist_vec_nth_le], simp) ``` wenzelm@49644 ` 535` ``` done ``` hoelzl@37489 ` 536` hoelzl@37489 ` 537` ```lemma compact_lemma_cart: ``` hoelzl@37489 ` 538` ``` fixes f :: "nat \ 'a::heine_borel ^ 'n" ``` hoelzl@50998 ` 539` ``` assumes f: "bounded (range f)" ``` eberlm@66447 ` 540` ``` shows "\l r. strict_mono r \ ``` hoelzl@37489 ` 541` ``` (\e>0. eventually (\n. \i\d. dist (f (r n) \$ i) (l \$ i) < e) sequentially)" ``` immler@62127 ` 542` ``` (is "?th d") ``` immler@62127 ` 543` ```proof - ``` immler@62127 ` 544` ``` have "\d' \ d. ?th d'" ``` immler@62127 ` 545` ``` by (rule compact_lemma_general[where unproj=vec_lambda]) ``` immler@62127 ` 546` ``` (auto intro!: f bounded_component_cart simp: vec_lambda_eta) ``` immler@62127 ` 547` ``` then show "?th d" by simp ``` hoelzl@37489 ` 548` ```qed ``` hoelzl@37489 ` 549` huffman@44136 ` 550` ```instance vec :: (heine_borel, finite) heine_borel ``` hoelzl@37489 ` 551` ```proof ``` hoelzl@50998 ` 552` ``` fix f :: "nat \ 'a ^ 'b" ``` hoelzl@50998 ` 553` ``` assume f: "bounded (range f)" ``` eberlm@66447 ` 554` ``` then obtain l r where r: "strict_mono r" ``` wenzelm@49644 ` 555` ``` and l: "\e>0. eventually (\n. \i\UNIV. dist (f (r n) \$ i) (l \$ i) < e) sequentially" ``` hoelzl@50998 ` 556` ``` using compact_lemma_cart [OF f] by blast ``` hoelzl@37489 ` 557` ``` let ?d = "UNIV::'b set" ``` hoelzl@37489 ` 558` ``` { fix e::real assume "e>0" ``` hoelzl@37489 ` 559` ``` hence "0 < e / (real_of_nat (card ?d))" ``` wenzelm@49644 ` 560` ``` using zero_less_card_finite divide_pos_pos[of e, of "real_of_nat (card ?d)"] by auto ``` hoelzl@37489 ` 561` ``` with l have "eventually (\n. \i. dist (f (r n) \$ i) (l \$ i) < e / (real_of_nat (card ?d))) sequentially" ``` hoelzl@37489 ` 562` ``` by simp ``` hoelzl@37489 ` 563` ``` moreover ``` wenzelm@49644 ` 564` ``` { fix n ``` wenzelm@49644 ` 565` ``` assume n: "\i. dist (f (r n) \$ i) (l \$ i) < e / (real_of_nat (card ?d))" ``` hoelzl@37489 ` 566` ``` have "dist (f (r n)) l \ (\i\?d. dist (f (r n) \$ i) (l \$ i))" ``` nipkow@67155 ` 567` ``` unfolding dist_vec_def using zero_le_dist by (rule L2_set_le_sum) ``` hoelzl@37489 ` 568` ``` also have "\ < (\i\?d. e / (real_of_nat (card ?d)))" ``` nipkow@64267 ` 569` ``` by (rule sum_strict_mono) (simp_all add: n) ``` hoelzl@37489 ` 570` ``` finally have "dist (f (r n)) l < e" by simp ``` hoelzl@37489 ` 571` ``` } ``` hoelzl@37489 ` 572` ``` ultimately have "eventually (\n. dist (f (r n)) l < e) sequentially" ``` lp15@61810 ` 573` ``` by (rule eventually_mono) ``` hoelzl@37489 ` 574` ``` } ``` wenzelm@61973 ` 575` ``` hence "((f \ r) \ l) sequentially" unfolding o_def tendsto_iff by simp ``` eberlm@66447 ` 576` ``` with r show "\l r. strict_mono r \ ((f \ r) \ l) sequentially" by auto ``` hoelzl@37489 ` 577` ```qed ``` hoelzl@37489 ` 578` wenzelm@49644 ` 579` ```lemma interval_cart: ``` immler@54775 ` 580` ``` fixes a :: "real^'n" ``` immler@54775 ` 581` ``` shows "box a b = {x::real^'n. \i. a\$i < x\$i \ x\$i < b\$i}" ``` immler@56188 ` 582` ``` and "cbox a b = {x::real^'n. \i. a\$i \ x\$i \ x\$i \ b\$i}" ``` immler@56188 ` 583` ``` by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def mem_box Basis_vec_def inner_axis) ``` hoelzl@37489 ` 584` lp15@67673 ` 585` ```lemma mem_box_cart: ``` immler@54775 ` 586` ``` fixes a :: "real^'n" ``` immler@54775 ` 587` ``` shows "x \ box a b \ (\i. a\$i < x\$i \ x\$i < b\$i)" ``` immler@56188 ` 588` ``` and "x \ cbox a b \ (\i. a\$i \ x\$i \ x\$i \ b\$i)" ``` wenzelm@49644 ` 589` ``` using interval_cart[of a b] by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def) ``` hoelzl@37489 ` 590` wenzelm@49644 ` 591` ```lemma interval_eq_empty_cart: ``` wenzelm@49644 ` 592` ``` fixes a :: "real^'n" ``` immler@54775 ` 593` ``` shows "(box a b = {} \ (\i. b\$i \ a\$i))" (is ?th1) ``` immler@56188 ` 594` ``` and "(cbox a b = {} \ (\i. b\$i < a\$i))" (is ?th2) ``` wenzelm@49644 ` 595` ```proof - ``` immler@54775 ` 596` ``` { fix i x assume as:"b\$i \ a\$i" and x:"x\box a b" ``` lp15@67673 ` 597` ``` hence "a \$ i < x \$ i \ x \$ i < b \$ i" unfolding mem_box_cart by auto ``` hoelzl@37489 ` 598` ``` hence "a\$i < b\$i" by auto ``` wenzelm@49644 ` 599` ``` hence False using as by auto } ``` hoelzl@37489 ` 600` ``` moreover ``` hoelzl@37489 ` 601` ``` { assume as:"\i. \ (b\$i \ a\$i)" ``` hoelzl@37489 ` 602` ``` let ?x = "(1/2) *\<^sub>R (a + b)" ``` hoelzl@37489 ` 603` ``` { fix i ``` hoelzl@37489 ` 604` ``` have "a\$i < b\$i" using as[THEN spec[where x=i]] by auto ``` hoelzl@37489 ` 605` ``` hence "a\$i < ((1/2) *\<^sub>R (a+b)) \$ i" "((1/2) *\<^sub>R (a+b)) \$ i < b\$i" ``` hoelzl@37489 ` 606` ``` unfolding vector_smult_component and vector_add_component ``` wenzelm@49644 ` 607` ``` by auto } ``` lp15@67673 ` 608` ``` hence "box a b \ {}" using mem_box_cart(1)[of "?x" a b] by auto } ``` hoelzl@37489 ` 609` ``` ultimately show ?th1 by blast ``` hoelzl@37489 ` 610` immler@56188 ` 611` ``` { fix i x assume as:"b\$i < a\$i" and x:"x\cbox a b" ``` lp15@67673 ` 612` ``` hence "a \$ i \ x \$ i \ x \$ i \ b \$ i" unfolding mem_box_cart by auto ``` hoelzl@37489 ` 613` ``` hence "a\$i \ b\$i" by auto ``` wenzelm@49644 ` 614` ``` hence False using as by auto } ``` hoelzl@37489 ` 615` ``` moreover ``` hoelzl@37489 ` 616` ``` { assume as:"\i. \ (b\$i < a\$i)" ``` hoelzl@37489 ` 617` ``` let ?x = "(1/2) *\<^sub>R (a + b)" ``` hoelzl@37489 ` 618` ``` { fix i ``` hoelzl@37489 ` 619` ``` have "a\$i \ b\$i" using as[THEN spec[where x=i]] by auto ``` hoelzl@37489 ` 620` ``` hence "a\$i \ ((1/2) *\<^sub>R (a+b)) \$ i" "((1/2) *\<^sub>R (a+b)) \$ i \ b\$i" ``` hoelzl@37489 ` 621` ``` unfolding vector_smult_component and vector_add_component ``` wenzelm@49644 ` 622` ``` by auto } ``` lp15@67673 ` 623` ``` hence "cbox a b \ {}" using mem_box_cart(2)[of "?x" a b] by auto } ``` hoelzl@37489 ` 624` ``` ultimately show ?th2 by blast ``` hoelzl@37489 ` 625` ```qed ``` hoelzl@37489 ` 626` wenzelm@49644 ` 627` ```lemma interval_ne_empty_cart: ``` wenzelm@49644 ` 628` ``` fixes a :: "real^'n" ``` immler@56188 ` 629` ``` shows "cbox a b \ {} \ (\i. a\$i \ b\$i)" ``` immler@54775 ` 630` ``` and "box a b \ {} \ (\i. a\$i < b\$i)" ``` hoelzl@37489 ` 631` ``` unfolding interval_eq_empty_cart[of a b] by (auto simp add: not_less not_le) ``` hoelzl@37489 ` 632` ``` (* BH: Why doesn't just "auto" work here? *) ``` hoelzl@37489 ` 633` wenzelm@49644 ` 634` ```lemma subset_interval_imp_cart: ``` wenzelm@49644 ` 635` ``` fixes a :: "real^'n" ``` immler@56188 ` 636` ``` shows "(\i. a\$i \ c\$i \ d\$i \ b\$i) \ cbox c d \ cbox a b" ``` immler@56188 ` 637` ``` and "(\i. a\$i < c\$i \ d\$i < b\$i) \ cbox c d \ box a b" ``` immler@56188 ` 638` ``` and "(\i. a\$i \ c\$i \ d\$i \ b\$i) \ box c d \ cbox a b" ``` immler@54775 ` 639` ``` and "(\i. a\$i \ c\$i \ d\$i \ b\$i) \ box c d \ box a b" ``` lp15@67673 ` 640` ``` unfolding subset_eq[unfolded Ball_def] unfolding mem_box_cart ``` hoelzl@37489 ` 641` ``` by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *) ``` hoelzl@37489 ` 642` wenzelm@49644 ` 643` ```lemma interval_sing: ``` wenzelm@49644 ` 644` ``` fixes a :: "'a::linorder^'n" ``` wenzelm@49644 ` 645` ``` 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 ` 652` ``` 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 ` 653` ``` 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 ` 654` ``` 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 ` 655` ``` using subset_box[of c d a b] by (simp_all add: Basis_vec_def inner_axis) ``` hoelzl@37489 ` 656` wenzelm@49644 ` 657` ```lemma disjoint_interval_cart: ``` wenzelm@49644 ` 658` ``` fixes a::"real^'n" ``` immler@56188 ` 659` ``` 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 ` 660` ``` 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 ` 661` ``` 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 ` 662` ``` 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 ` 663` ``` using disjoint_interval[of a b c d] by (simp_all add: Basis_vec_def inner_axis) ``` hoelzl@37489 ` 664` lp15@67719 ` 665` ```lemma Int_interval_cart: ``` immler@54775 ` 666` ``` fixes a :: "real^'n" ``` immler@56188 ` 667` ``` shows "cbox a b \ cbox c d = {(\ i. max (a\$i) (c\$i)) .. (\ i. min (b\$i) (d\$i))}" ``` lp15@63945 ` 668` ``` unfolding Int_interval ``` immler@56188 ` 669` ``` by (auto simp: mem_box less_eq_vec_def) ``` immler@56188 ` 670` ``` (auto simp: Basis_vec_def inner_axis) ``` hoelzl@37489 ` 671` wenzelm@49644 ` 672` ```lemma closed_interval_left_cart: ``` wenzelm@49644 ` 673` ``` fixes b :: "real^'n" ``` hoelzl@37489 ` 674` ``` shows "closed {x::real^'n. \i. x\$i \ b\$i}" ``` hoelzl@63332 ` 675` ``` by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) ``` hoelzl@37489 ` 676` wenzelm@49644 ` 677` ```lemma closed_interval_right_cart: ``` wenzelm@49644 ` 678` ``` fixes a::"real^'n" ``` hoelzl@37489 ` 679` ``` shows "closed {x::real^'n. \i. a\$i \ x\$i}" ``` hoelzl@63332 ` 680` ``` by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) ``` hoelzl@37489 ` 681` wenzelm@49644 ` 682` ```lemma is_interval_cart: ``` wenzelm@49644 ` 683` ``` "is_interval (s::(real^'n) set) \ ``` wenzelm@49644 ` 684` ``` (\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 ` 685` ``` by (simp add: is_interval_def Ball_def Basis_vec_def inner_axis imp_ex) ``` hoelzl@37489 ` 686` wenzelm@49644 ` 687` ```lemma closed_halfspace_component_le_cart: "closed {x::real^'n. x\$i \ a}" ``` hoelzl@63332 ` 688` ``` by (simp add: closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) ``` hoelzl@37489 ` 689` wenzelm@49644 ` 690` ```lemma closed_halfspace_component_ge_cart: "closed {x::real^'n. x\$i \ a}" ``` hoelzl@63332 ` 691` ``` by (simp add: closed_Collect_le continuous_on_const continuous_on_id continuous_on_component) ``` hoelzl@37489 ` 692` wenzelm@49644 ` 693` ```lemma open_halfspace_component_lt_cart: "open {x::real^'n. x\$i < a}" ``` hoelzl@63332 ` 694` ``` by (simp add: open_Collect_less continuous_on_const continuous_on_id continuous_on_component) ``` wenzelm@49644 ` 695` wenzelm@49644 ` 696` ```lemma open_halfspace_component_gt_cart: "open {x::real^'n. x\$i > a}" ``` hoelzl@63332 ` 697` ``` by (simp add: open_Collect_less continuous_on_const continuous_on_id continuous_on_component) ``` hoelzl@37489 ` 698` wenzelm@49644 ` 699` ```lemma Lim_component_le_cart: ``` wenzelm@49644 ` 700` ``` fixes f :: "'a \ real^'n" ``` wenzelm@61973 ` 701` ``` assumes "(f \ l) net" "\ (trivial_limit net)" "eventually (\x. f x \$i \ b) net" ``` hoelzl@37489 ` 702` ``` shows "l\$i \ b" ``` hoelzl@50526 ` 703` ``` by (rule tendsto_le[OF assms(2) tendsto_const tendsto_vec_nth, OF assms(1, 3)]) ``` hoelzl@37489 ` 704` wenzelm@49644 ` 705` ```lemma Lim_component_ge_cart: ``` wenzelm@49644 ` 706` ``` fixes f :: "'a \ real^'n" ``` wenzelm@61973 ` 707` ``` assumes "(f \ l) net" "\ (trivial_limit net)" "eventually (\x. b \ (f x)\$i) net" ``` hoelzl@37489 ` 708` ``` shows "b \ l\$i" ``` hoelzl@50526 ` 709` ``` by (rule tendsto_le[OF assms(2) tendsto_vec_nth tendsto_const, OF assms(1, 3)]) ``` hoelzl@37489 ` 710` wenzelm@49644 ` 711` ```lemma Lim_component_eq_cart: ``` wenzelm@49644 ` 712` ``` fixes f :: "'a \ real^'n" ``` wenzelm@61973 ` 713` ``` assumes net: "(f \ l) net" "~(trivial_limit net)" and ev:"eventually (\x. f(x)\$i = b) net" ``` hoelzl@37489 ` 714` ``` shows "l\$i = b" ``` wenzelm@49644 ` 715` ``` using ev[unfolded order_eq_iff eventually_conj_iff] and ``` wenzelm@49644 ` 716` ``` Lim_component_ge_cart[OF net, of b i] and ``` hoelzl@37489 ` 717` ``` Lim_component_le_cart[OF net, of i b] by auto ``` hoelzl@37489 ` 718` wenzelm@49644 ` 719` ```lemma connected_ivt_component_cart: ``` wenzelm@49644 ` 720` ``` fixes x :: "real^'n" ``` wenzelm@49644 ` 721` ``` shows "connected s \ x \ s \ y \ s \ x\$k \ a \ a \ y\$k \ (\z\s. z\$k = a)" ``` hoelzl@50526 ` 722` ``` using connected_ivt_hyperplane[of s x y "axis k 1" a] ``` hoelzl@50526 ` 723` ``` by (auto simp add: inner_axis inner_commute) ``` hoelzl@37489 ` 724` immler@68072 ` 725` ```lemma subspace_substandard_cart: "vec.subspace {x. (\i. P i \ x\$i = 0)}" ``` immler@68072 ` 726` ``` unfolding vec.subspace_def by auto ``` hoelzl@37489 ` 727` hoelzl@37489 ` 728` ```lemma closed_substandard_cart: ``` huffman@44213 ` 729` ``` "closed {x::'a::real_normed_vector ^ 'n. \i. P i \ x\$i = 0}" ``` wenzelm@49644 ` 730` ```proof - ``` huffman@44213 ` 731` ``` { fix i::'n ``` huffman@44213 ` 732` ``` have "closed {x::'a ^ 'n. P i \ x\$i = 0}" ``` hoelzl@63332 ` 733` ``` by (cases "P i") (simp_all add: closed_Collect_eq continuous_on_const continuous_on_id continuous_on_component) } ``` huffman@44213 ` 734` ``` thus ?thesis ``` huffman@44213 ` 735` ``` unfolding Collect_all_eq by (simp add: closed_INT) ``` hoelzl@37489 ` 736` ```qed ``` hoelzl@37489 ` 737` immler@68072 ` 738` ```lemma dim_substandard_cart: "vec.dim {x::'a::field^'n. \i. i \ d \ x\$i = 0} = card d" ``` immler@68072 ` 739` ``` (is "vec.dim ?A = _") ``` immler@68072 ` 740` ```proof (rule vec.dim_unique) ``` immler@68072 ` 741` ``` let ?B = "((\x. axis x 1) ` d)" ``` immler@68072 ` 742` ``` have subset_basis: "?B \ cart_basis" ``` immler@68072 ` 743` ``` by (auto simp: cart_basis_def) ``` immler@68072 ` 744` ``` show "?B \ ?A" ``` immler@68072 ` 745` ``` by (auto simp: axis_def) ``` immler@68072 ` 746` ``` show "vec.independent ((\x. axis x 1) ` d)" ``` immler@68072 ` 747` ``` using subset_basis ``` immler@68072 ` 748` ``` by (rule vec.independent_mono[OF vec.independent_Basis]) ``` immler@68072 ` 749` ``` have "x \ vec.span ?B" if "\i. i \ d \ x \$ i = 0" for x::"'a^'n" ``` immler@68072 ` 750` ``` proof - ``` immler@68072 ` 751` ``` have "finite ?B" ``` immler@68072 ` 752` ``` using subset_basis finite_cart_basis ``` immler@68072 ` 753` ``` by (rule finite_subset) ``` immler@68072 ` 754` ``` have "x = (\i\UNIV. x \$ i *s axis i 1)" ``` immler@68072 ` 755` ``` by (rule basis_expansion[symmetric]) ``` immler@68072 ` 756` ``` also have "\ = (\i\d. (x \$ i) *s axis i 1)" ``` immler@68072 ` 757` ``` by (rule sum.mono_neutral_cong_right) (auto simp: that) ``` immler@68072 ` 758` ``` also have "\ \ vec.span ?B" ``` immler@68072 ` 759` ``` by (simp add: vec.span_sum vec.span_clauses) ``` immler@68072 ` 760` ``` finally show "x \ vec.span ?B" . ``` immler@68072 ` 761` ``` qed ``` immler@68072 ` 762` ``` then show "?A \ vec.span ?B" by auto ``` immler@68072 ` 763` ```qed (simp add: card_image inj_on_def axis_eq_axis) ``` immler@68072 ` 764` immler@68072 ` 765` ```lemma dim_subset_UNIV_cart_gen: ``` immler@68072 ` 766` ``` fixes S :: "('a::field^'n) set" ``` immler@68072 ` 767` ``` shows "vec.dim S \ CARD('n)" ``` immler@68072 ` 768` ``` by (metis vec.dim_eq_full vec.dim_subset_UNIV vec.span_UNIV vec_dim_card) ``` hoelzl@37489 ` 769` lp15@67719 ` 770` ```lemma dim_subset_UNIV_cart: ``` lp15@67719 ` 771` ``` fixes S :: "(real^'n) set" ``` lp15@67719 ` 772` ``` shows "dim S \ CARD('n)" ``` immler@68072 ` 773` ``` using dim_subset_UNIV_cart_gen[of S] by (simp add: dim_vec_eq) ``` lp15@67719 ` 774` hoelzl@37489 ` 775` ```lemma affinity_inverses: ``` hoelzl@37489 ` 776` ``` assumes m0: "m \ (0::'a::field)" ``` wenzelm@61736 ` 777` ``` shows "(\x. m *s x + c) \ (\x. inverse(m) *s x + (-(inverse(m) *s c))) = id" ``` wenzelm@61736 ` 778` ``` "(\x. inverse(m) *s x + (-(inverse(m) *s c))) \ (\x. m *s x + c) = id" ``` hoelzl@37489 ` 779` ``` using m0 ``` immler@68072 ` 780` ``` by (auto simp add: fun_eq_iff vector_add_ldistrib diff_conv_add_uminus simp del: add_uminus_conv_diff) ``` hoelzl@37489 ` 781` hoelzl@37489 ` 782` ```lemma vector_affinity_eq: ``` hoelzl@37489 ` 783` ``` assumes m0: "(m::'a::field) \ 0" ``` hoelzl@37489 ` 784` ``` shows "m *s x + c = y \ x = inverse m *s y + -(inverse m *s c)" ``` hoelzl@37489 ` 785` ```proof ``` hoelzl@37489 ` 786` ``` assume h: "m *s x + c = y" ``` hoelzl@37489 ` 787` ``` hence "m *s x = y - c" by (simp add: field_simps) ``` hoelzl@37489 ` 788` ``` hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp ``` hoelzl@37489 ` 789` ``` then show "x = inverse m *s y + - (inverse m *s c)" ``` hoelzl@37489 ` 790` ``` using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib) ``` hoelzl@37489 ` 791` ```next ``` hoelzl@37489 ` 792` ``` assume h: "x = inverse m *s y + - (inverse m *s c)" ``` haftmann@54230 ` 793` ``` show "m *s x + c = y" unfolding h ``` hoelzl@37489 ` 794` ``` using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib) ``` hoelzl@37489 ` 795` ```qed ``` hoelzl@37489 ` 796` hoelzl@37489 ` 797` ```lemma vector_eq_affinity: ``` wenzelm@49644 ` 798` ``` "(m::'a::field) \ 0 ==> (y = m *s x + c \ inverse(m) *s y + -(inverse(m) *s c) = x)" ``` hoelzl@37489 ` 799` ``` using vector_affinity_eq[where m=m and x=x and y=y and c=c] ``` hoelzl@37489 ` 800` ``` by metis ``` hoelzl@37489 ` 801` hoelzl@50526 ` 802` ```lemma vector_cart: ``` hoelzl@50526 ` 803` ``` fixes f :: "real^'n \ real" ``` hoelzl@50526 ` 804` ``` shows "(\ i. f (axis i 1)) = (\i\Basis. f i *\<^sub>R i)" ``` hoelzl@50526 ` 805` ``` unfolding euclidean_eq_iff[where 'a="real^'n"] ``` hoelzl@50526 ` 806` ``` by simp (simp add: Basis_vec_def inner_axis) ``` hoelzl@63332 ` 807` hoelzl@50526 ` 808` ```lemma const_vector_cart:"((\ i. d)::real^'n) = (\i\Basis. d *\<^sub>R i)" ``` hoelzl@50526 ` 809` ``` by (rule vector_cart) ``` wenzelm@49644 ` 810` huffman@44360 ` 811` ```subsection "Convex Euclidean Space" ``` hoelzl@37489 ` 812` hoelzl@50526 ` 813` ```lemma Cart_1:"(1::real^'n) = \Basis" ``` hoelzl@50526 ` 814` ``` using const_vector_cart[of 1] by (simp add: one_vec_def) ``` hoelzl@37489 ` 815` hoelzl@37489 ` 816` ```declare vector_add_ldistrib[simp] vector_ssub_ldistrib[simp] vector_smult_assoc[simp] vector_smult_rneg[simp] ``` hoelzl@37489 ` 817` ```declare vector_sadd_rdistrib[simp] vector_sub_rdistrib[simp] ``` hoelzl@37489 ` 818` hoelzl@50526 ` 819` ```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 ` 820` hoelzl@37489 ` 821` ```lemma convex_box_cart: ``` hoelzl@37489 ` 822` ``` assumes "\i. convex {x. P i x}" ``` hoelzl@37489 ` 823` ``` shows "convex {x. \i. P i (x\$i)}" ``` hoelzl@37489 ` 824` ``` using assms unfolding convex_def by auto ``` hoelzl@37489 ` 825` hoelzl@37489 ` 826` ```lemma convex_positive_orthant_cart: "convex {x::real^'n. (\i. 0 \ x\$i)}" ``` hoelzl@63334 ` 827` ``` by (rule convex_box_cart) (simp add: atLeast_def[symmetric]) ``` hoelzl@37489 ` 828` hoelzl@37489 ` 829` ```lemma unit_interval_convex_hull_cart: ``` immler@56188 ` 830` ``` "cbox (0::real^'n) 1 = convex hull {x. \i. (x\$i = 0) \ (x\$i = 1)}" ``` immler@56188 ` 831` ``` unfolding Cart_1 unit_interval_convex_hull[where 'a="real^'n"] box_real[symmetric] ``` hoelzl@50526 ` 832` ``` by (rule arg_cong[where f="\x. convex hull x"]) (simp add: Basis_vec_def inner_axis) ``` hoelzl@37489 ` 833` hoelzl@37489 ` 834` ```lemma cube_convex_hull_cart: ``` wenzelm@49644 ` 835` ``` assumes "0 < d" ``` wenzelm@49644 ` 836` ``` obtains s::"(real^'n) set" ``` immler@56188 ` 837` ``` where "finite s" "cbox (x - (\ i. d)) (x + (\ i. d)) = convex hull s" ``` wenzelm@49644 ` 838` ```proof - ``` wenzelm@55522 ` 839` ``` from assms obtain s where "finite s" ``` nipkow@67399 ` 840` ``` and "cbox (x - sum (( *\<^sub>R) d) Basis) (x + sum (( *\<^sub>R) d) Basis) = convex hull s" ``` wenzelm@55522 ` 841` ``` by (rule cube_convex_hull) ``` wenzelm@55522 ` 842` ``` with that[of s] show thesis ``` wenzelm@55522 ` 843` ``` by (simp add: const_vector_cart) ``` hoelzl@37489 ` 844` ```qed ``` hoelzl@37489 ` 845` hoelzl@37489 ` 846` hoelzl@37489 ` 847` ```subsection "Derivative" ``` hoelzl@37489 ` 848` hoelzl@37489 ` 849` ```definition "jacobian f net = matrix(frechet_derivative f net)" ``` hoelzl@37489 ` 850` wenzelm@49644 ` 851` ```lemma jacobian_works: ``` wenzelm@49644 ` 852` ``` "(f::(real^'a) \ (real^'b)) differentiable net \ ``` lp15@67986 ` 853` ``` (f has_derivative (\h. (jacobian f net) *v h)) net" (is "?lhs = ?rhs") ``` lp15@67986 ` 854` ```proof ``` lp15@67986 ` 855` ``` assume ?lhs then show ?rhs ``` lp15@67986 ` 856` ``` by (simp add: frechet_derivative_works has_derivative_linear jacobian_def) ``` lp15@67986 ` 857` ```next ``` lp15@67986 ` 858` ``` assume ?rhs then show ?lhs ``` lp15@67986 ` 859` ``` by (rule differentiableI) ``` lp15@67986 ` 860` ```qed ``` hoelzl@37489 ` 861` hoelzl@37489 ` 862` wenzelm@60420 ` 863` ```subsection \Component of the differential must be zero if it exists at a local ``` nipkow@67968 ` 864` ``` maximum or minimum for that corresponding component\ ``` hoelzl@37489 ` 865` hoelzl@50526 ` 866` ```lemma differential_zero_maxmin_cart: ``` wenzelm@49644 ` 867` ``` fixes f::"real^'a \ real^'b" ``` wenzelm@49644 ` 868` ``` 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 ` 869` ``` "f differentiable (at x)" ``` hoelzl@50526 ` 870` ``` shows "jacobian f (at x) \$ k = 0" ``` hoelzl@50526 ` 871` ``` using differential_zero_maxmin_component[of "axis k 1" e x f] assms ``` hoelzl@50526 ` 872` ``` vector_cart[of "\j. frechet_derivative f (at x) j \$ k"] ``` hoelzl@50526 ` 873` ``` by (simp add: Basis_vec_def axis_eq_axis inner_axis jacobian_def matrix_def) ``` wenzelm@49644 ` 874` wenzelm@60420 ` 875` ```subsection \Lemmas for working on @{typ "real^1"}\ ``` hoelzl@37489 ` 876` hoelzl@37489 ` 877` ```lemma forall_1[simp]: "(\i::1. P i) \ P 1" ``` wenzelm@49644 ` 878` ``` by (metis (full_types) num1_eq_iff) ``` hoelzl@37489 ` 879` hoelzl@37489 ` 880` ```lemma ex_1[simp]: "(\x::1. P x) \ P 1" ``` wenzelm@49644 ` 881` ``` by auto (metis (full_types) num1_eq_iff) ``` hoelzl@37489 ` 882` hoelzl@37489 ` 883` ```lemma exhaust_2: ``` wenzelm@49644 ` 884` ``` fixes x :: 2 ``` wenzelm@49644 ` 885` ``` shows "x = 1 \ x = 2" ``` hoelzl@37489 ` 886` ```proof (induct x) ``` hoelzl@37489 ` 887` ``` case (of_int z) ``` lp15@67979 ` 888` ``` then have "0 \ z" and "z < 2" by simp_all ``` hoelzl@37489 ` 889` ``` then have "z = 0 | z = 1" by arith ``` hoelzl@37489 ` 890` ``` then show ?case by auto ``` hoelzl@37489 ` 891` ```qed ``` hoelzl@37489 ` 892` hoelzl@37489 ` 893` ```lemma forall_2: "(\i::2. P i) \ P 1 \ P 2" ``` hoelzl@37489 ` 894` ``` by (metis exhaust_2) ``` hoelzl@37489 ` 895` hoelzl@37489 ` 896` ```lemma exhaust_3: ``` wenzelm@49644 ` 897` ``` fixes x :: 3 ``` wenzelm@49644 ` 898` ``` shows "x = 1 \ x = 2 \ x = 3" ``` hoelzl@37489 ` 899` ```proof (induct x) ``` hoelzl@37489 ` 900` ``` case (of_int z) ``` lp15@67979 ` 901` ``` then have "0 \ z" and "z < 3" by simp_all ``` hoelzl@37489 ` 902` ``` then have "z = 0 \ z = 1 \ z = 2" by arith ``` hoelzl@37489 ` 903` ``` then show ?case by auto ``` hoelzl@37489 ` 904` ```qed ``` hoelzl@37489 ` 905` hoelzl@37489 ` 906` ```lemma forall_3: "(\i::3. P i) \ P 1 \ P 2 \ P 3" ``` hoelzl@37489 ` 907` ``` by (metis exhaust_3) ``` hoelzl@37489 ` 908` hoelzl@37489 ` 909` ```lemma UNIV_1 [simp]: "UNIV = {1::1}" ``` hoelzl@37489 ` 910` ``` by (auto simp add: num1_eq_iff) ``` hoelzl@37489 ` 911` hoelzl@37489 ` 912` ```lemma UNIV_2: "UNIV = {1::2, 2::2}" ``` hoelzl@37489 ` 913` ``` using exhaust_2 by auto ``` hoelzl@37489 ` 914` hoelzl@37489 ` 915` ```lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}" ``` hoelzl@37489 ` 916` ``` using exhaust_3 by auto ``` hoelzl@37489 ` 917` nipkow@64267 ` 918` ```lemma sum_1: "sum f (UNIV::1 set) = f 1" ``` hoelzl@37489 ` 919` ``` unfolding UNIV_1 by simp ``` hoelzl@37489 ` 920` nipkow@64267 ` 921` ```lemma sum_2: "sum f (UNIV::2 set) = f 1 + f 2" ``` hoelzl@37489 ` 922` ``` unfolding UNIV_2 by simp ``` hoelzl@37489 ` 923` nipkow@64267 ` 924` ```lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3" ``` haftmann@57514 ` 925` ``` unfolding UNIV_3 by (simp add: ac_simps) ``` hoelzl@37489 ` 926` lp15@67979 ` 927` ```lemma num1_eqI: ``` lp15@67979 ` 928` ``` fixes a::num1 shows "a = b" ``` lp15@67979 ` 929` ``` by (metis (full_types) UNIV_1 UNIV_I empty_iff insert_iff) ``` lp15@67979 ` 930` lp15@67979 ` 931` ```lemma num1_eq1 [simp]: ``` lp15@67979 ` 932` ``` fixes a::num1 shows "a = 1" ``` lp15@67979 ` 933` ``` by (rule num1_eqI) ``` lp15@67979 ` 934` wenzelm@49644 ` 935` ```instantiation num1 :: cart_one ``` wenzelm@49644 ` 936` ```begin ``` wenzelm@49644 ` 937` wenzelm@49644 ` 938` ```instance ``` wenzelm@49644 ` 939` ```proof ``` hoelzl@37489 ` 940` ``` show "CARD(1) = Suc 0" by auto ``` wenzelm@49644 ` 941` ```qed ``` wenzelm@49644 ` 942` wenzelm@49644 ` 943` ```end ``` hoelzl@37489 ` 944` lp15@67979 ` 945` ```instantiation num1 :: linorder begin ``` lp15@67979 ` 946` ```definition "a < b \ Rep_num1 a < Rep_num1 b" ``` lp15@67979 ` 947` ```definition "a \ b \ Rep_num1 a \ Rep_num1 b" ``` lp15@67979 ` 948` ```instance ``` lp15@67979 ` 949` ``` by intro_classes (auto simp: less_eq_num1_def less_num1_def intro: num1_eqI) ``` lp15@67979 ` 950` ```end ``` lp15@67979 ` 951` lp15@67979 ` 952` ```instance num1 :: wellorder ``` lp15@67979 ` 953` ``` by intro_classes (auto simp: less_eq_num1_def less_num1_def) ``` lp15@67979 ` 954` nipkow@67968 ` 955` ```subsection\The collapse of the general concepts to dimension one\ ``` hoelzl@37489 ` 956` hoelzl@37489 ` 957` ```lemma vector_one: "(x::'a ^1) = (\ i. (x\$1))" ``` huffman@44136 ` 958` ``` by (simp add: vec_eq_iff) ``` hoelzl@37489 ` 959` hoelzl@37489 ` 960` ```lemma forall_one: "(\(x::'a ^1). P x) \ (\x. P(\ i. x))" ``` hoelzl@37489 ` 961` ``` apply auto ``` hoelzl@37489 ` 962` ``` apply (erule_tac x= "x\$1" in allE) ``` hoelzl@37489 ` 963` ``` apply (simp only: vector_one[symmetric]) ``` hoelzl@37489 ` 964` ``` done ``` hoelzl@37489 ` 965` hoelzl@37489 ` 966` ```lemma norm_vector_1: "norm (x :: _^1) = norm (x\$1)" ``` huffman@44136 ` 967` ``` by (simp add: norm_vec_def) ``` hoelzl@37489 ` 968` lp15@67979 ` 969` ```lemma dist_vector_1: ``` lp15@67979 ` 970` ``` fixes x :: "'a::real_normed_vector^1" ``` lp15@67979 ` 971` ``` shows "dist x y = dist (x\$1) (y\$1)" ``` lp15@67979 ` 972` ``` by (simp add: dist_norm norm_vector_1) ``` lp15@67979 ` 973` wenzelm@61945 ` 974` ```lemma norm_real: "norm(x::real ^ 1) = \x\$1\" ``` hoelzl@37489 ` 975` ``` by (simp add: norm_vector_1) ``` hoelzl@37489 ` 976` wenzelm@61945 ` 977` ```lemma dist_real: "dist(x::real ^ 1) y = \(x\$1) - (y\$1)\" ``` hoelzl@37489 ` 978` ``` by (auto simp add: norm_real dist_norm) ``` hoelzl@37489 ` 979` lp15@67986 ` 980` ```subsection\ Rank of a matrix\ ``` lp15@67986 ` 981` lp15@67986 ` 982` ```text\Equivalence of row and column rank is taken from George Mackiw's paper, Mathematics Magazine 1995, p. 285.\ ``` lp15@67986 ` 983` immler@68072 ` 984` ```lemma matrix_vector_mult_in_columnspace_gen: ``` immler@68072 ` 985` ``` fixes A :: "'a::field^'n^'m" ``` immler@68072 ` 986` ``` shows "(A *v x) \ vec.span(columns A)" ``` immler@68072 ` 987` ``` apply (simp add: matrix_vector_column columns_def transpose_def column_def) ``` immler@68072 ` 988` ``` apply (intro vec.span_sum vec.span_scale) ``` immler@68072 ` 989` ``` apply (force intro: vec.span_base) ``` immler@68072 ` 990` ``` done ``` immler@68072 ` 991` lp15@67986 ` 992` ```lemma matrix_vector_mult_in_columnspace: ``` lp15@67986 ` 993` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 994` ``` shows "(A *v x) \ span(columns A)" ``` immler@68072 ` 995` ``` using matrix_vector_mult_in_columnspace_gen[of A x] by (simp add: span_vec_eq) ``` lp15@67986 ` 996` lp15@67986 ` 997` ```lemma orthogonal_nullspace_rowspace: ``` lp15@67986 ` 998` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 999` ``` assumes 0: "A *v x = 0" and y: "y \ span(rows A)" ``` lp15@67986 ` 1000` ``` shows "orthogonal x y" ``` lp15@67986 ` 1001` ```proof (rule span_induct [OF y]) ``` lp15@67986 ` 1002` ``` show "subspace {a. orthogonal x a}" ``` lp15@67986 ` 1003` ``` by (simp add: subspace_orthogonal_to_vector) ``` lp15@67986 ` 1004` ```next ``` lp15@67986 ` 1005` ``` fix v ``` lp15@67986 ` 1006` ``` assume "v \ rows A" ``` lp15@67986 ` 1007` ``` then obtain i where "v = row i A" ``` lp15@67986 ` 1008` ``` by (auto simp: rows_def) ``` lp15@67986 ` 1009` ``` with 0 show "orthogonal x v" ``` lp15@67986 ` 1010` ``` unfolding orthogonal_def inner_vec_def matrix_vector_mult_def row_def ``` lp15@67986 ` 1011` ``` by (simp add: mult.commute) (metis (no_types) vec_lambda_beta zero_index) ``` lp15@67986 ` 1012` ```qed ``` lp15@67986 ` 1013` lp15@67986 ` 1014` ```lemma nullspace_inter_rowspace: ``` lp15@67986 ` 1015` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1016` ``` shows "A *v x = 0 \ x \ span(rows A) \ x = 0" ``` immler@68072 ` 1017` ``` using orthogonal_nullspace_rowspace orthogonal_self span_zero matrix_vector_mult_0_right ``` immler@68072 ` 1018` ``` by blast ``` lp15@67986 ` 1019` lp15@67986 ` 1020` ```lemma matrix_vector_mul_injective_on_rowspace: ``` lp15@67986 ` 1021` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1022` ``` shows "\A *v x = A *v y; x \ span(rows A); y \ span(rows A)\ \ x = y" ``` lp15@67986 ` 1023` ``` using nullspace_inter_rowspace [of A "x-y"] ``` immler@68072 ` 1024` ``` by (metis diff_eq_diff_eq diff_self matrix_vector_mult_diff_distrib span_diff) ``` lp15@67986 ` 1025` immler@68072 ` 1026` ```definition rank :: "'a::field^'n^'m=>nat" ``` immler@68072 ` 1027` ``` where row_rank_def_gen: "rank A \ vec.dim(rows A)" ``` immler@68072 ` 1028` immler@68072 ` 1029` ```lemma row_rank_def: "rank A = dim (rows A)" for A::"real^'n^'m" ``` immler@68072 ` 1030` ``` by (auto simp: row_rank_def_gen dim_vec_eq) ``` lp15@67986 ` 1031` lp15@67986 ` 1032` ```lemma dim_rows_le_dim_columns: ``` lp15@67986 ` 1033` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1034` ``` shows "dim(rows A) \ dim(columns A)" ``` lp15@67986 ` 1035` ```proof - ``` lp15@67986 ` 1036` ``` have "dim (span (rows A)) \ dim (span (columns A))" ``` lp15@67986 ` 1037` ``` proof - ``` lp15@67986 ` 1038` ``` obtain B where "independent B" "span(rows A) \ span B" ``` lp15@67986 ` 1039` ``` and B: "B \ span(rows A)""card B = dim (span(rows A))" ``` lp15@67986 ` 1040` ``` using basis_exists [of "span(rows A)"] by blast ``` immler@68072 ` 1041` ``` then have eq: "span B = span(rows A)" ``` immler@68072 ` 1042` ``` using span_subspace subspace_span by blast ``` lp15@67986 ` 1043` ``` then have inj: "inj_on (( *v) A) (span B)" ``` immler@68072 ` 1044` ``` by (simp add: inj_on_def matrix_vector_mul_injective_on_rowspace) ``` lp15@67986 ` 1045` ``` then have ind: "independent (( *v) A ` B)" ``` immler@68072 ` 1046` ``` by (rule linear_independent_injective_image [OF Finite_Cartesian_Product.matrix_vector_mul_linear \independent B\]) ``` immler@68072 ` 1047` ``` have "dim (span (rows A)) \ card (( *v) A ` B)" ``` immler@68072 ` 1048` ``` unfolding B(2)[symmetric] ``` immler@68072 ` 1049` ``` using inj ``` immler@68072 ` 1050` ``` by (auto simp: card_image inj_on_subset span_superset) ``` immler@68072 ` 1051` ``` also have "\ \ dim (span (columns A))" ``` immler@68072 ` 1052` ``` using _ ind ``` immler@68072 ` 1053` ``` by (rule independent_card_le_dim) (auto intro!: matrix_vector_mult_in_columnspace) ``` immler@68072 ` 1054` ``` finally show ?thesis . ``` lp15@67986 ` 1055` ``` qed ``` lp15@67986 ` 1056` ``` then show ?thesis ``` immler@68072 ` 1057` ``` by (simp add: dim_span) ``` lp15@67986 ` 1058` ```qed ``` lp15@67986 ` 1059` immler@68072 ` 1060` ```lemma column_rank_def: ``` lp15@67986 ` 1061` ``` fixes A :: "real^'n^'m" ``` immler@68072 ` 1062` ``` shows "rank A = dim(columns A)" ``` immler@68072 ` 1063` ``` unfolding row_rank_def ``` immler@68072 ` 1064` ``` by (metis columns_transpose dim_rows_le_dim_columns le_antisym rows_transpose) ``` lp15@67986 ` 1065` lp15@67986 ` 1066` ```lemma rank_transpose: ``` lp15@67986 ` 1067` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1068` ``` shows "rank(transpose A) = rank A" ``` immler@68072 ` 1069` ``` by (metis column_rank_def row_rank_def rows_transpose) ``` lp15@67986 ` 1070` lp15@67986 ` 1071` ```lemma matrix_vector_mult_basis: ``` lp15@67986 ` 1072` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1073` ``` shows "A *v (axis k 1) = column k A" ``` lp15@67986 ` 1074` ``` by (simp add: cart_eq_inner_axis column_def matrix_mult_dot) ``` lp15@67986 ` 1075` lp15@67986 ` 1076` ```lemma columns_image_basis: ``` lp15@67986 ` 1077` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1078` ``` shows "columns A = ( *v) A ` (range (\i. axis i 1))" ``` lp15@67986 ` 1079` ``` by (force simp: columns_def matrix_vector_mult_basis [symmetric]) ``` lp15@67986 ` 1080` lp15@67986 ` 1081` ```lemma rank_dim_range: ``` lp15@67986 ` 1082` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1083` ``` shows "rank A = dim(range (\x. A *v x))" ``` immler@68072 ` 1084` ``` unfolding column_rank_def ``` lp15@67986 ` 1085` ```proof (rule span_eq_dim) ``` immler@68072 ` 1086` ``` have "span (columns A) \ span (range (( *v) A))" (is "?l \ ?r") ``` immler@68072 ` 1087` ``` by (simp add: columns_image_basis image_subsetI span_mono) ``` immler@68072 ` 1088` ``` then show "?l = ?r" ``` immler@68072 ` 1089` ``` by (metis (no_types, lifting) image_subset_iff matrix_vector_mult_in_columnspace ``` immler@68072 ` 1090` ``` span_eq span_span) ``` lp15@67986 ` 1091` ```qed ``` lp15@67986 ` 1092` lp15@67986 ` 1093` ```lemma rank_bound: ``` lp15@67986 ` 1094` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1095` ``` shows "rank A \ min CARD('m) (CARD('n))" ``` immler@68072 ` 1096` ``` by (metis (mono_tags, lifting) dim_subset_UNIV_cart min.bounded_iff ``` immler@68072 ` 1097` ``` column_rank_def row_rank_def) ``` lp15@67986 ` 1098` lp15@67986 ` 1099` ```lemma full_rank_injective: ``` lp15@67986 ` 1100` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1101` ``` shows "rank A = CARD('n) \ inj (( *v) A)" ``` immler@68072 ` 1102` ``` by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows row_rank_def ``` immler@68072 ` 1103` ``` dim_eq_full [symmetric] card_cart_basis vec.dimension_def) ``` lp15@67986 ` 1104` lp15@67986 ` 1105` ```lemma full_rank_surjective: ``` lp15@67986 ` 1106` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1107` ``` shows "rank A = CARD('m) \ surj (( *v) A)" ``` lp15@67986 ` 1108` ``` by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric] ``` lp15@67986 ` 1109` ``` matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose) ``` lp15@67986 ` 1110` lp15@67986 ` 1111` ```lemma rank_I: "rank(mat 1::real^'n^'n) = CARD('n)" ``` lp15@67986 ` 1112` ``` by (simp add: full_rank_injective inj_on_def) ``` lp15@67986 ` 1113` lp15@67986 ` 1114` ```lemma less_rank_noninjective: ``` lp15@67986 ` 1115` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1116` ``` shows "rank A < CARD('n) \ \ inj (( *v) A)" ``` lp15@67986 ` 1117` ```using less_le rank_bound by (auto simp: full_rank_injective [symmetric]) ``` lp15@67986 ` 1118` lp15@67986 ` 1119` ```lemma matrix_nonfull_linear_equations_eq: ``` lp15@67986 ` 1120` ``` fixes A :: "real^'n^'m" ``` lp15@67986 ` 1121` ``` shows "(\x. (x \ 0) \ A *v x = 0) \ ~(rank A = CARD('n))" ``` lp15@67986 ` 1122` ``` by (meson matrix_left_invertible_injective full_rank_injective matrix_left_invertible_ker) ``` lp15@67986 ` 1123` immler@68072 ` 1124` ```lemma rank_eq_0: "rank A = 0 \ A = 0" and rank_0 [simp]: "rank (0::real^'n^'m) = 0" ``` immler@68072 ` 1125` ``` for A :: "real^'n^'m" ``` lp15@67986 ` 1126` ``` by (auto simp: rank_dim_range matrix_eq) ``` lp15@67986 ` 1127` lp15@67986 ` 1128` ```lemma rank_mul_le_right: ``` lp15@67986 ` 1129` ``` fixes A :: "real^'n^'m" and B :: "real^'p^'n" ``` lp15@67986 ` 1130` ``` shows "rank(A ** B) \ rank B" ``` lp15@67986 ` 1131` ```proof - ``` lp15@67986 ` 1132` ``` have "rank(A ** B) \ dim (( *v) A ` range (( *v) B))" ``` lp15@67986 ` 1133` ``` by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc) ``` lp15@67986 ` 1134` ``` also have "\ \ rank B" ``` immler@68072 ` 1135` ``` by (simp add: rank_dim_range dim_image_le) ``` lp15@67986 ` 1136` ``` finally show ?thesis . ``` lp15@67986 ` 1137` ```qed ``` lp15@67986 ` 1138` lp15@67986 ` 1139` ```lemma rank_mul_le_left: ``` lp15@67986 ` 1140` ``` fixes A :: "real^'n^'m" and B :: "real^'p^'n" ``` lp15@67986 ` 1141` ``` shows "rank(A ** B) \ rank A" ``` lp15@67986 ` 1142` ``` by (metis matrix_transpose_mul rank_mul_le_right rank_transpose) ``` lp15@67986 ` 1143` lp15@67981 ` 1144` ```subsection\Routine results connecting the types @{typ "real^1"} and @{typ real}\ ``` lp15@67981 ` 1145` lp15@67981 ` 1146` ```lemma vector_one_nth [simp]: ``` lp15@67981 ` 1147` ``` fixes x :: "'a^1" shows "vec (x \$ 1) = x" ``` lp15@67981 ` 1148` ``` by (metis vec_def vector_one) ``` lp15@67981 ` 1149` lp15@67981 ` 1150` ```lemma vec_cbox_1_eq [simp]: ``` lp15@67981 ` 1151` ``` shows "vec ` cbox u v = cbox (vec u) (vec v ::real^1)" ``` lp15@67981 ` 1152` ``` by (force simp: Basis_vec_def cart_eq_inner_axis [symmetric] mem_box) ``` lp15@67981 ` 1153` lp15@67981 ` 1154` ```lemma vec_nth_cbox_1_eq [simp]: ``` lp15@67981 ` 1155` ``` fixes u v :: "'a::euclidean_space^1" ``` lp15@67981 ` 1156` ``` shows "(\x. x \$ 1) ` cbox u v = cbox (u\$1) (v\$1)" ``` lp15@67981 ` 1157` ``` by (auto simp: Basis_vec_def cart_eq_inner_axis [symmetric] mem_box image_iff Bex_def inner_axis) (metis vec_component) ``` lp15@67981 ` 1158` lp15@67981 ` 1159` ```lemma vec_nth_1_iff_cbox [simp]: ``` lp15@67981 ` 1160` ``` fixes a b :: "'a::euclidean_space" ``` lp15@67981 ` 1161` ``` shows "(\x::'a^1. x \$ 1) ` S = cbox a b \ S = cbox (vec a) (vec b)" ``` lp15@67981 ` 1162` ``` (is "?lhs = ?rhs") ``` lp15@67981 ` 1163` ```proof ``` lp15@67981 ` 1164` ``` assume L: ?lhs show ?rhs ``` lp15@67981 ` 1165` ``` proof (intro equalityI subsetI) ``` lp15@67981 ` 1166` ``` fix x ``` lp15@67981 ` 1167` ``` assume "x \ S" ``` lp15@67981 ` 1168` ``` then have "x \$ 1 \ (\v. v \$ (1::1)) ` cbox (vec a) (vec b)" ``` lp15@67981 ` 1169` ``` using L by auto ``` lp15@67981 ` 1170` ``` then show "x \ cbox (vec a) (vec b)" ``` lp15@67981 ` 1171` ``` by (metis (no_types, lifting) imageE vector_one_nth) ``` lp15@67981 ` 1172` ``` next ``` lp15@67981 ` 1173` ``` fix x :: "'a^1" ``` lp15@67981 ` 1174` ``` assume "x \ cbox (vec a) (vec b)" ``` lp15@67981 ` 1175` ``` then show "x \ S" ``` lp15@67981 ` 1176` ``` by (metis (no_types, lifting) L imageE imageI vec_component vec_nth_cbox_1_eq vector_one_nth) ``` lp15@67981 ` 1177` ``` qed ``` lp15@67981 ` 1178` ```qed simp ``` wenzelm@49644 ` 1179` lp15@67979 ` 1180` ```lemma tendsto_at_within_vector_1: ``` lp15@67979 ` 1181` ``` fixes S :: "'a :: metric_space set" ``` lp15@67979 ` 1182` ``` assumes "(f \ fx) (at x within S)" ``` lp15@67979 ` 1183` ``` shows "((\y::'a^1. \ i. f (y \$ 1)) \ (vec fx::'a^1)) (at (vec x) within vec ` S)" ``` lp15@67979 ` 1184` ```proof (rule topological_tendstoI) ``` lp15@67979 ` 1185` ``` fix T :: "('a^1) set" ``` lp15@67979 ` 1186` ``` assume "open T" "vec fx \ T" ``` lp15@67979 ` 1187` ``` have "\\<^sub>F x in at x within S. f x \ (\x. x \$ 1) ` T" ``` lp15@67979 ` 1188` ``` using \open T\ \vec fx \ T\ assms open_image_vec_nth tendsto_def by fastforce ``` lp15@67979 ` 1189` ``` then show "\\<^sub>F x::'a^1 in at (vec x) within vec ` S. (\ i. f (x \$ 1)) \ T" ``` lp15@67979 ` 1190` ``` unfolding eventually_at dist_norm [symmetric] ``` lp15@67979 ` 1191` ``` by (rule ex_forward) ``` lp15@67979 ` 1192` ``` (use \open T\ in ``` lp15@67979 ` 1193` ``` \fastforce simp: dist_norm dist_vec_def L2_set_def image_iff vector_one open_vec_def\) ``` lp15@67979 ` 1194` ```qed ``` lp15@67979 ` 1195` lp15@67979 ` 1196` ```lemma has_derivative_vector_1: ``` lp15@67979 ` 1197` ``` assumes der_g: "(g has_derivative (\x. x * g' a)) (at a within S)" ``` lp15@67979 ` 1198` ``` shows "((\x. vec (g (x \$ 1))) has_derivative ( *\<^sub>R) (g' a)) ``` lp15@67979 ` 1199` ``` (at ((vec a)::real^1) within vec ` S)" ``` lp15@67979 ` 1200` ``` using der_g ``` lp15@67979 ` 1201` ``` apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1) ``` lp15@67979 ` 1202` ``` apply (drule tendsto_at_within_vector_1, vector) ``` lp15@67979 ` 1203` ``` apply (auto simp: algebra_simps eventually_at tendsto_def) ``` lp15@67979 ` 1204` ``` done ``` lp15@67979 ` 1205` lp15@67979 ` 1206` nipkow@67968 ` 1207` ```subsection\Explicit vector construction from lists\ ``` hoelzl@37489 ` 1208` hoelzl@43995 ` 1209` ```definition "vector l = (\ i. foldr (\x f n. fun_upd (f (n+1)) n x) l (\n x. 0) 1 i)" ``` hoelzl@37489 ` 1210` hoelzl@37489 ` 1211` ```lemma vector_1: "(vector[x]) \$1 = x" ``` hoelzl@37489 ` 1212` ``` unfolding vector_def by simp ``` hoelzl@37489 ` 1213` hoelzl@37489 ` 1214` ```lemma vector_2: ``` hoelzl@37489 ` 1215` ``` "(vector[x,y]) \$1 = x" ``` hoelzl@37489 ` 1216` ``` "(vector[x,y] :: 'a^2)\$2 = (y::'a::zero)" ``` hoelzl@37489 ` 1217` ``` unfolding vector_def by simp_all ``` hoelzl@37489 ` 1218` hoelzl@37489 ` 1219` ```lemma vector_3: ``` hoelzl@37489 ` 1220` ``` "(vector [x,y,z] ::('a::zero)^3)\$1 = x" ``` hoelzl@37489 ` 1221` ``` "(vector [x,y,z] ::('a::zero)^3)\$2 = y" ``` hoelzl@37489 ` 1222` ``` "(vector [x,y,z] ::('a::zero)^3)\$3 = z" ``` hoelzl@37489 ` 1223` ``` unfolding vector_def by simp_all ``` hoelzl@37489 ` 1224` hoelzl@37489 ` 1225` ```lemma forall_vector_1: "(\v::'a::zero^1. P v) \ (\x. P(vector[x]))" ``` lp15@67719 ` 1226` ``` by (metis vector_1 vector_one) ``` hoelzl@37489 ` 1227` hoelzl@37489 ` 1228` ```lemma forall_vector_2: "(\v::'a::zero^2. P v) \ (\x y. P(vector[x, y]))" ``` hoelzl@37489 ` 1229` ``` apply auto ``` hoelzl@37489 ` 1230` ``` apply (erule_tac x="v\$1" in allE) ``` hoelzl@37489 ` 1231` ``` apply (erule_tac x="v\$2" in allE) ``` hoelzl@37489 ` 1232` ``` apply (subgoal_tac "vector [v\$1, v\$2] = v") ``` hoelzl@37489 ` 1233` ``` apply simp ``` hoelzl@37489 ` 1234` ``` apply (vector vector_def) ``` hoelzl@37489 ` 1235` ``` apply (simp add: forall_2) ``` hoelzl@37489 ` 1236` ``` done ``` hoelzl@37489 ` 1237` hoelzl@37489 ` 1238` ```lemma forall_vector_3: "(\v::'a::zero^3. P v) \ (\x y z. P(vector[x, y, z]))" ``` hoelzl@37489 ` 1239` ``` apply auto ``` hoelzl@37489 ` 1240` ``` apply (erule_tac x="v\$1" in allE) ``` hoelzl@37489 ` 1241` ``` apply (erule_tac x="v\$2" in allE) ``` hoelzl@37489 ` 1242` ``` apply (erule_tac x="v\$3" in allE) ``` hoelzl@37489 ` 1243` ``` apply (subgoal_tac "vector [v\$1, v\$2, v\$3] = v") ``` hoelzl@37489 ` 1244` ``` apply simp ``` hoelzl@37489 ` 1245` ``` apply (vector vector_def) ``` hoelzl@37489 ` 1246` ``` apply (simp add: forall_3) ``` hoelzl@37489 ` 1247` ``` done ``` hoelzl@37489 ` 1248` hoelzl@37489 ` 1249` ```lemma bounded_linear_component_cart[intro]: "bounded_linear (\x::real^'n. x \$ k)" ``` wenzelm@49644 ` 1250` ``` apply (rule bounded_linearI[where K=1]) ``` hoelzl@37489 ` 1251` ``` using component_le_norm_cart[of _ k] unfolding real_norm_def by auto ``` hoelzl@37489 ` 1252` hoelzl@37489 ` 1253` ```lemma interval_split_cart: ``` hoelzl@37489 ` 1254` ``` "{a..b::real^'n} \ {x. x\$k \ c} = {a .. (\ i. if i = k then min (b\$k) c else b\$i)}" ``` immler@56188 ` 1255` ``` "cbox a b \ {x. x\$k \ c} = {(\ i. if i = k then max (a\$k) c else a\$i) .. b}" ``` wenzelm@49644 ` 1256` ``` apply (rule_tac[!] set_eqI) ``` lp15@67673 ` 1257` ``` unfolding Int_iff mem_box_cart mem_Collect_eq interval_cbox_cart ``` wenzelm@49644 ` 1258` ``` unfolding vec_lambda_beta ``` wenzelm@49644 ` 1259` ``` by auto ``` hoelzl@37489 ` 1260` immler@67685 ` 1261` ```lemmas cartesian_euclidean_space_uniform_limit_intros[uniform_limit_intros] = ``` immler@67685 ` 1262` ``` bounded_linear.uniform_limit[OF blinfun.bounded_linear_right] ``` immler@67685 ` 1263` ``` bounded_linear.uniform_limit[OF bounded_linear_vec_nth] ``` immler@67685 ` 1264` ``` bounded_linear.uniform_limit[OF bounded_linear_component_cart] ``` immler@67685 ` 1265` immler@68072 ` 1266` `end`