1188 obtain y::"real^'n" where y:"norm y = b" using `b\<ge>0` |
1188 obtain y::"real^'n" where y:"norm y = b" using `b\<ge>0` |
1189 using vector_choose_size[of b] by auto |
1189 using vector_choose_size[of b] by auto |
1190 thus "?lhs" unfolding eventually_def at_infinity using b y by auto |
1190 thus "?lhs" unfolding eventually_def at_infinity using b y by auto |
1191 qed |
1191 qed |
1192 |
1192 |
1193 lemma always_eventually: "(\<forall>(x::'a::zero_neq_one). P x) ==> eventually P net" |
1193 lemma always_eventually: "(\<forall>x. P x) ==> eventually P net" |
1194 apply (auto simp add: eventually_def trivial_limit_def ) |
1194 unfolding eventually_def trivial_limit_def by (clarify, simp) |
1195 by (rule exI[where x=0], rule exI[where x=1], rule zero_neq_one) |
1195 |
|
1196 lemma eventually_True [simp]: "eventually (\<lambda>x. True) net" |
|
1197 by (simp add: always_eventually) |
1196 |
1198 |
1197 text{* Combining theorems for "eventually" *} |
1199 text{* Combining theorems for "eventually" *} |
1198 |
1200 |
1199 lemma eventually_and: " eventually (\<lambda>x. P x \<and> Q x) net \<longleftrightarrow> eventually P net \<and> eventually Q net" |
1201 lemma eventually_and: " eventually (\<lambda>x. P x \<and> Q x) net \<longleftrightarrow> eventually P net \<and> eventually Q net" |
1200 apply (simp add: eventually_def) |
1202 apply (simp add: eventually_def) |
1212 lemma eventually_false: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net" |
1214 lemma eventually_false: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net" |
1213 by (auto simp add: eventually_def) |
1215 by (auto simp add: eventually_def) |
1214 |
1216 |
1215 lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> ~(trivial_limit net) ==> ~(eventually P net)" |
1217 lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> ~(trivial_limit net) ==> ~(eventually P net)" |
1216 by (auto simp add: eventually_def) |
1218 by (auto simp add: eventually_def) |
|
1219 |
|
1220 lemma eventually_rev_mono: |
|
1221 "eventually P net \<Longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually Q net" |
|
1222 using eventually_mono [of P Q] by fast |
|
1223 |
|
1224 lemma eventually_rev_mp: |
|
1225 assumes 1: "eventually (\<lambda>x. P x) net" |
|
1226 assumes 2: "eventually (\<lambda>x. P x \<longrightarrow> Q x) net" |
|
1227 shows "eventually (\<lambda>x. Q x) net" |
|
1228 using 2 1 by (rule eventually_mp) |
|
1229 |
|
1230 lemma eventually_conjI: |
|
1231 "\<lbrakk>eventually (\<lambda>x. P x) net; eventually (\<lambda>x. Q x) net\<rbrakk> |
|
1232 \<Longrightarrow> eventually (\<lambda>x. P x \<and> Q x) net" |
|
1233 by (simp add: eventually_and) |
1217 |
1234 |
1218 subsection{* Limits, defined as vacuously true when the limit is trivial. *} |
1235 subsection{* Limits, defined as vacuously true when the limit is trivial. *} |
1219 |
1236 |
1220 definition tendsto:: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool" (infixr "--->" 55) where |
1237 definition tendsto:: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool" (infixr "--->" 55) where |
1221 tendsto_def: "(f ---> l) net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)" |
1238 tendsto_def: "(f ---> l) net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)" |
1354 text{* Basic arithmetical combining theorems for limits. *} |
1371 text{* Basic arithmetical combining theorems for limits. *} |
1355 |
1372 |
1356 lemma Lim_linear: fixes f :: "('a \<Rightarrow> real^'n::finite)" and h :: "(real^'n \<Rightarrow> real^'m::finite)" |
1373 lemma Lim_linear: fixes f :: "('a \<Rightarrow> real^'n::finite)" and h :: "(real^'n \<Rightarrow> real^'m::finite)" |
1357 assumes "(f ---> l) net" "linear h" |
1374 assumes "(f ---> l) net" "linear h" |
1358 shows "((\<lambda>x. h (f x)) ---> h l) net" |
1375 shows "((\<lambda>x. h (f x)) ---> h l) net" |
1359 proof (cases "trivial_limit net") |
1376 proof - |
1360 case True |
1377 obtain b where b: "b>0" "\<forall>x. norm (h x) \<le> b * norm x" |
1361 thus ?thesis unfolding tendsto_def unfolding eventually_def by auto |
1378 using assms(2) using linear_bounded_pos[of h] by auto |
1362 next |
|
1363 case False note cas = this |
|
1364 obtain b where b: "b>0" "\<forall>x. norm (h x) \<le> b * norm x" using assms(2) using linear_bounded_pos[of h] by auto |
|
1365 { fix e::real assume "e >0" |
1379 { fix e::real assume "e >0" |
1366 hence "e/b > 0" using `b>0` by (metis divide_pos_pos) |
1380 hence "e/b > 0" using `b>0` by (metis divide_pos_pos) |
1367 then have "(\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist (f x) l < e/b))" using assms `e>0` cas |
1381 with `(f ---> l) net` have "eventually (\<lambda>x. dist (f x) l < e/b) net" |
1368 unfolding tendsto_def unfolding eventually_def by auto |
1382 by (rule tendstoD) |
1369 then obtain y where y: "\<exists>x. netord net x y" "\<forall>x. netord net x y \<longrightarrow> dist (f x) l < e/b" by auto |
1383 then have "eventually (\<lambda>x. dist (h (f x)) (h l) < e) net" |
1370 { fix x |
1384 apply (rule eventually_rev_mono [rule_format]) |
1371 have "netord net x y \<longrightarrow> dist (h (f x)) (h l) < e" |
1385 apply (simp add: dist_norm linear_sub [OF `linear h`, symmetric]) |
1372 using y(2) b unfolding dist_norm using linear_sub[of h "f x" l] `linear h` |
1386 apply (rule le_less_trans [OF b(2) [rule_format]]) |
1373 apply auto by (metis b(1) b(2) less_le_not_le linorder_not_le mult_imp_div_pos_le real_mult_commute xt1(7)) (* FIXME: VERY slow! *) |
1387 apply (simp add: pos_less_divide_eq `0 < b` mult_commute) |
1374 } |
1388 done |
1375 hence " (\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist (h (f x)) (h l) < e))" using y |
|
1376 by(rule_tac x="y" in exI) auto |
|
1377 } |
1389 } |
1378 thus ?thesis unfolding tendsto_def eventually_def using `b>0` by auto |
1390 thus ?thesis unfolding tendsto_def by simp |
1379 qed |
1391 qed |
1380 |
1392 |
1381 lemma Lim_const: "((\<lambda>x. a) ---> a) net" |
1393 lemma Lim_const: "((\<lambda>x. a) ---> a) net" |
1382 by (auto simp add: Lim trivial_limit_def) |
1394 by (auto simp add: Lim trivial_limit_def) |
1383 |
1395 |
1405 assume "e>0" |
1417 assume "e>0" |
1406 hence *:"eventually (\<lambda>x. dist (f x) l < e/2) net" |
1418 hence *:"eventually (\<lambda>x. dist (f x) l < e/2) net" |
1407 "eventually (\<lambda>x. dist (g x) m < e/2) net" using as |
1419 "eventually (\<lambda>x. dist (g x) m < e/2) net" using as |
1408 by (auto intro: tendstoD simp del: less_divide_eq_number_of1) |
1420 by (auto intro: tendstoD simp del: less_divide_eq_number_of1) |
1409 hence "eventually (\<lambda>x. dist (f x + g x) (l + m) < e) net" |
1421 hence "eventually (\<lambda>x. dist (f x + g x) (l + m) < e) net" |
1410 proof(cases "trivial_limit net") |
1422 apply (elim eventually_rev_mp) |
1411 case True |
1423 apply (rule always_eventually, clarify) |
1412 thus ?thesis unfolding eventually_def by auto |
1424 apply (rule le_less_trans [OF dist_triangle_add]) |
1413 next |
1425 apply simp |
1414 case False |
1426 done |
1415 hence fl:"(\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist (f x) l < e / 2))" and |
|
1416 gl:"(\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist (g x) m < e / 2))" |
|
1417 using * unfolding eventually_def by auto |
|
1418 obtain c where c:"(\<exists>x. netord net x c)" "(\<forall>x. netord net x c \<longrightarrow> dist (f x) l < e / 2 \<and> dist (g x) m < e / 2)" |
|
1419 using net_dilemma[of net, OF fl gl] by auto |
|
1420 { fix x assume "netord net x c" |
|
1421 with c(2) have " dist (f x + g x) (l + m) < e" using dist_triangle_add[of "f x" "g x" l m] by auto |
|
1422 } |
|
1423 with c show ?thesis unfolding eventually_def by auto |
|
1424 qed |
|
1425 } |
1427 } |
1426 thus ?thesis unfolding tendsto_def by auto |
1428 thus ?thesis unfolding tendsto_def by simp |
1427 qed |
1429 qed |
1428 |
1430 |
1429 lemma Lim_sub: |
1431 lemma Lim_sub: |
1430 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
1432 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
1431 shows "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) ---> l - m) net" |
1433 shows "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) ---> l - m) net" |
1489 text{* Deducing things about the limit from the elements. *} |
1491 text{* Deducing things about the limit from the elements. *} |
1490 |
1492 |
1491 lemma Lim_in_closed_set: |
1493 lemma Lim_in_closed_set: |
1492 assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) net" "\<not>(trivial_limit net)" "(f ---> l) net" |
1494 assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) net" "\<not>(trivial_limit net)" "(f ---> l) net" |
1493 shows "l \<in> S" |
1495 shows "l \<in> S" |
1494 proof- |
1496 proof (rule ccontr) |
1495 { assume "l \<notin> S" |
1497 assume "l \<notin> S" |
1496 obtain e where e:"e>0" "ball l e \<subseteq> UNIV - S" using assms(1) `l \<notin> S` unfolding closed_def open_contains_ball by auto |
1498 obtain e where e:"e>0" "ball l e \<subseteq> UNIV - S" using assms(1) `l \<notin> S` unfolding closed_def open_contains_ball by auto |
1497 hence *:"\<forall>x. dist l x < e \<longrightarrow> x \<notin> S" by auto |
1499 hence *:"\<forall>x. dist l x < e \<longrightarrow> x \<notin> S" by auto |
1498 obtain y where "(\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist (f x) l < e)" |
1500 have "eventually (\<lambda>x. dist (f x) l < e) net" |
1499 using assms(3,4) `e>0` unfolding tendsto_def eventually_def by blast |
1501 using assms(4) `e>0` by (rule tendstoD) |
1500 hence "(\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> f x \<notin> S)" using * by (auto simp add: dist_commute) |
1502 with assms(2) have "eventually (\<lambda>x. f x \<in> S \<and> dist (f x) l < e) net" |
1501 hence False using assms(2,3) |
1503 by (rule eventually_conjI) |
1502 using eventually_and[of "(\<lambda>x. f x \<in> S)" "(\<lambda>x. f x \<notin> S)"] not_eventually[of "(\<lambda>x. f x \<in> S \<and> f x \<notin> S)" net] |
1504 then obtain x where "f x \<in> S" "dist (f x) l < e" |
1503 unfolding eventually_def by blast |
1505 using assms(3) eventually_happens by auto |
1504 } |
1506 with * show "False" by (simp add: dist_commute) |
1505 thus ?thesis by blast |
|
1506 qed |
1507 qed |
1507 |
1508 |
1508 text{* Need to prove closed(cball(x,e)) before deducing this as a corollary. *} |
1509 text{* Need to prove closed(cball(x,e)) before deducing this as a corollary. *} |
1509 |
1510 |
1510 lemma Lim_norm_ubound: |
1511 lemma Lim_norm_ubound: |
1511 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
1512 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
1512 assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net" |
1513 assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net" |
1513 shows "norm(l) <= e" |
1514 shows "norm(l) <= e" |
1514 proof- |
1515 proof (rule ccontr) |
1515 obtain y where y: "\<exists>x. netord net x y" "\<forall>x. netord net x y \<longrightarrow> norm (f x) \<le> e" using assms(1,3) unfolding eventually_def by auto |
1516 assume "\<not> norm l \<le> e" |
1516 show ?thesis |
1517 then have "0 < norm l - e" by simp |
1517 proof(rule ccontr) |
1518 with assms(2) have "eventually (\<lambda>x. dist (f x) l < norm l - e) net" |
1518 assume "\<not> norm l \<le> e" |
1519 by (rule tendstoD) |
1519 then obtain z where z: "\<exists>x. netord net x z" "\<forall>x. netord net x z \<longrightarrow> dist (f x) l < norm l - e" |
1520 with assms(3) have "eventually (\<lambda>x. norm (f x) \<le> e \<and> dist (f x) l < norm l - e) net" |
1520 using assms(2)[unfolded Lim] using assms(1) apply simp apply(erule_tac x="norm l - e" in allE) by auto |
1521 by (rule eventually_conjI) |
1521 obtain w where w:"netord net w z" "netord net w y" using net[of net] using z(1) y(1) by blast |
1522 then obtain w where "norm (f w) \<le> e" "dist (f w) l < norm l - e" |
1522 hence "dist (f w) l < norm l - e \<and> norm (f w) <= e" using z(2) y(2) by auto |
1523 using assms(1) eventually_happens by auto |
1523 hence "norm (f w - l) < norm l - e" "norm (f w) \<le> e" by (simp_all add: dist_norm) |
1524 hence "norm (f w - l) < norm l - e" "norm (f w) \<le> e" by (simp_all add: dist_norm) |
1524 hence "norm (f w - l) + norm (f w) < norm l" by simp |
1525 hence "norm (f w - l) + norm (f w) < norm l" by simp |
1525 hence "norm (f w - l - f w) < norm l" by (rule le_less_trans [OF norm_triangle_ineq4]) |
1526 hence "norm (f w - l - f w) < norm l" by (rule le_less_trans [OF norm_triangle_ineq4]) |
1526 thus False using `\<not> norm l \<le> e` by simp |
1527 thus False using `\<not> norm l \<le> e` by simp |
1527 qed |
|
1528 qed |
1528 qed |
1529 |
1529 |
1530 lemma Lim_norm_lbound: |
1530 lemma Lim_norm_lbound: |
1531 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
1531 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
1532 assumes "\<not> (trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. e <= norm(f x)) net" |
1532 assumes "\<not> (trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. e <= norm(f x)) net" |
1533 shows "e \<le> norm l" |
1533 shows "e \<le> norm l" |
1534 proof- |
1534 proof (rule ccontr) |
1535 obtain y where y: "\<exists>x. netord net x y" "\<forall>x. netord net x y \<longrightarrow> e \<le> norm (f x)" using assms(1,3) unfolding eventually_def by auto |
1535 assume "\<not> e \<le> norm l" |
1536 show ?thesis |
1536 then have "0 < e - norm l" by simp |
1537 proof(rule ccontr) |
1537 with assms(2) have "eventually (\<lambda>x. dist (f x) l < e - norm l) net" |
1538 assume "\<not> e \<le> norm l" |
1538 by (rule tendstoD) |
1539 then obtain z where z: "\<exists>x. netord net x z" "\<forall>x. netord net x z \<longrightarrow> dist (f x) l < e - norm l" |
1539 with assms(3) have "eventually (\<lambda>x. e \<le> norm (f x) \<and> dist (f x) l < e - norm l) net" |
1540 using assms(2)[unfolded Lim] using assms(1) apply simp apply(erule_tac x="e - norm l" in allE) by auto |
1540 by (rule eventually_conjI) |
1541 obtain w where w:"netord net w z" "netord net w y" using net[of net] using z(1) y(1) by blast |
1541 then obtain w where "e \<le> norm (f w)" "dist (f w) l < e - norm l" |
1542 hence "dist (f w) l < e - norm l \<and> e \<le> norm (f w)" using z(2) y(2) by auto |
1542 using assms(1) eventually_happens by auto |
1543 hence "norm (f w - l) + norm l < e" "e \<le> norm (f w)" by (simp_all add: dist_norm) |
1543 hence "norm (f w - l) + norm l < e" "e \<le> norm (f w)" by (simp_all add: dist_norm) |
1544 hence "norm (f w - l) + norm l < norm (f w)" by (rule less_le_trans) |
1544 hence "norm (f w - l) + norm l < norm (f w)" by (rule less_le_trans) |
1545 hence "norm (f w - l + l) < norm (f w)" by (rule le_less_trans [OF norm_triangle_ineq]) |
1545 hence "norm (f w - l + l) < norm (f w)" by (rule le_less_trans [OF norm_triangle_ineq]) |
1546 thus False by simp |
1546 thus False by simp |
1547 qed |
|
1548 qed |
1547 qed |
1549 |
1548 |
1550 text{* Uniqueness of the limit, when nontrivial. *} |
1549 text{* Uniqueness of the limit, when nontrivial. *} |
1551 |
1550 |
1552 lemma Lim_unique: |
1551 lemma Lim_unique: |
1604 |
1603 |
1605 lemma Lim_bilinear: |
1604 lemma Lim_bilinear: |
1606 fixes net :: "'a net" and h:: "real ^'m::finite \<Rightarrow> real ^'n::finite \<Rightarrow> real ^'p::finite" |
1605 fixes net :: "'a net" and h:: "real ^'m::finite \<Rightarrow> real ^'n::finite \<Rightarrow> real ^'p::finite" |
1607 assumes "(f ---> l) net" and "(g ---> m) net" and "bilinear h" |
1606 assumes "(f ---> l) net" and "(g ---> m) net" and "bilinear h" |
1608 shows "((\<lambda>x. h (f x) (g x)) ---> (h l m)) net" |
1607 shows "((\<lambda>x. h (f x) (g x)) ---> (h l m)) net" |
1609 proof(cases "trivial_limit net") |
1608 proof - |
1610 case True thus "((\<lambda>x. h (f x) (g x)) ---> h l m) net" unfolding Lim .. |
|
1611 next |
|
1612 case False note ntriv = this |
|
1613 obtain B where "B>0" and B:"\<forall>x y. norm (h x y) \<le> B * norm x * norm y" using bilinear_bounded_pos[OF assms(3)] by auto |
1609 obtain B where "B>0" and B:"\<forall>x y. norm (h x y) \<le> B * norm x * norm y" using bilinear_bounded_pos[OF assms(3)] by auto |
1614 { fix e::real assume "e>0" |
1610 { fix e::real assume "e>0" |
1615 obtain d where "d>0" and d:"\<forall>x' y'. norm (x' - l) < d \<and> norm (y' - m) < d \<longrightarrow> norm x' * norm (y' - m) + norm (x' - l) * norm m < e / B" using `B>0` `e>0` |
1611 obtain d where "d>0" and d:"\<forall>x' y'. norm (x' - l) < d \<and> norm (y' - m) < d \<longrightarrow> norm x' * norm (y' - m) + norm (x' - l) * norm m < e / B" using `B>0` `e>0` |
1616 using norm_bound_lemma[of "e / B" l m] using divide_pos_pos by auto |
1612 using norm_bound_lemma[of "e / B" l m] using divide_pos_pos by auto |
1617 |
1613 |
1618 have *:"\<And>x y. h (f x) (g x) - h l m = h (f x) (g x - m) + h (f x - l) m" |
1614 have *:"\<And>x y. h (f x) (g x) - h l m = h (f x) (g x - m) + h (f x - l) m" |
1619 unfolding bilinear_rsub[OF assms(3)] |
1615 unfolding bilinear_rsub[OF assms(3)] |
1620 unfolding bilinear_lsub[OF assms(3)] by auto |
1616 unfolding bilinear_lsub[OF assms(3)] by auto |
1621 |
1617 |
|
1618 have "eventually (\<lambda>x. dist (f x) l < d) net" |
|
1619 using assms(1) `d>0` by (rule tendstoD) |
|
1620 moreover |
|
1621 have "eventually (\<lambda>x. dist (g x) m < d) net" |
|
1622 using assms(2) `d>0` by (rule tendstoD) |
|
1623 ultimately |
|
1624 have "eventually (\<lambda>x. dist (f x) l < d \<and> dist (g x) m < d) net" |
|
1625 by (rule eventually_conjI) |
|
1626 moreover |
1622 { fix x assume "dist (f x) l < d \<and> dist (g x) m < d" |
1627 { fix x assume "dist (f x) l < d \<and> dist (g x) m < d" |
1623 hence **:"norm (f x) * norm (g x - m) + norm (f x - l) * norm m < e / B" |
1628 hence **:"norm (f x) * norm (g x - m) + norm (f x - l) * norm m < e / B" |
1624 using d[THEN spec[where x="f x"], THEN spec[where x="g x"]] unfolding dist_norm by auto |
1629 using d[THEN spec[where x="f x"], THEN spec[where x="g x"]] unfolding dist_norm by auto |
1625 have "norm (h (f x) (g x - m)) + norm (h (f x - l) m) \<le> B * norm (f x) * norm (g x - m) + B * norm (f x - l) * norm m" |
1630 have "norm (h (f x) (g x - m)) + norm (h (f x - l) m) \<le> B * norm (f x) * norm (g x - m) + B * norm (f x - l) * norm m" |
1626 using B[THEN spec[where x="f x"], THEN spec[where x="g x - m"]] |
1631 using B[THEN spec[where x="f x"], THEN spec[where x="g x - m"]] |
1627 using B[THEN spec[where x="f x - l"], THEN spec[where x="m"]] by auto |
1632 using B[THEN spec[where x="f x - l"], THEN spec[where x="m"]] by auto |
1628 also have "\<dots> < e" using ** and `B>0` by(auto simp add: field_simps) |
1633 also have "\<dots> < e" using ** and `B>0` by(auto simp add: field_simps) |
1629 finally have "dist (h (f x) (g x)) (h l m) < e" unfolding dist_norm and * using norm_triangle_lt by auto |
1634 finally have "dist (h (f x) (g x)) (h l m) < e" unfolding dist_norm and * using norm_triangle_lt by auto |
1630 } |
1635 } |
1631 moreover |
1636 ultimately have "eventually (\<lambda>x. dist (h (f x) (g x)) (h l m) < e) net" |
1632 obtain c where "(\<exists>x. netord net x c) \<and> (\<forall>x. netord net x c \<longrightarrow> dist (f x) l < d \<and> dist (g x) m < d)" |
1637 by (auto elim: eventually_rev_mono) |
1633 using net_dilemma[of net "\<lambda>x. dist (f x) l < d" "\<lambda>x. dist (g x) m < d"] using assms(1,2) unfolding Lim using False and `d>0` by (auto elim!: allE[where x=d]) |
1638 } |
1634 ultimately have "\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist (h (f x) (g x)) (h l m) < e)" by auto } |
1639 thus "((\<lambda>x. h (f x) (g x)) ---> h l m) net" |
1635 thus "((\<lambda>x. h (f x) (g x)) ---> h l m) net" unfolding Lim by auto |
1640 unfolding tendsto_def by simp |
1636 qed |
1641 qed |
1637 |
1642 |
1638 text{* These are special for limits out of the same vector space. *} |
1643 text{* These are special for limits out of the same vector space. *} |
1639 |
1644 |
1640 lemma Lim_within_id: "(id ---> a) (at a within s)" by (auto simp add: Lim_within id_def) |
1645 lemma Lim_within_id: "(id ---> a) (at a within s)" by (auto simp add: Lim_within id_def) |
2071 lemma bounded_closure[intro]: assumes "bounded S" shows "bounded(closure S)" |
2076 lemma bounded_closure[intro]: assumes "bounded S" shows "bounded(closure S)" |
2072 proof- |
2077 proof- |
2073 from assms obtain a where a:"\<forall>x\<in>S. norm x \<le> a" unfolding bounded_def by auto |
2078 from assms obtain a where a:"\<forall>x\<in>S. norm x \<le> a" unfolding bounded_def by auto |
2074 { fix x assume "x\<in>closure S" |
2079 { fix x assume "x\<in>closure S" |
2075 then obtain xa where xa:"\<forall>n. xa n \<in> S" "(xa ---> x) sequentially" unfolding closure_sequential by auto |
2080 then obtain xa where xa:"\<forall>n. xa n \<in> S" "(xa ---> x) sequentially" unfolding closure_sequential by auto |
2076 moreover have "\<exists>y. \<exists>x. netord sequentially x y" using trivial_limit_sequentially unfolding trivial_limit_def by blast |
2081 have "\<forall>n. xa n \<in> S \<longrightarrow> norm (xa n) \<le> a" using a by simp |
2077 hence "\<exists>y. (\<exists>x. netord sequentially x y) \<and> (\<forall>x. netord sequentially x y \<longrightarrow> norm (xa x) \<le> a)" unfolding sequentially_def using a xa(1) by auto |
2082 hence "eventually (\<lambda>n. norm (xa n) \<le> a) sequentially" |
2078 ultimately have "norm x \<le> a" using Lim_norm_ubound[of sequentially xa x a] trivial_limit_sequentially unfolding eventually_def by auto |
2083 by (rule eventually_mono, simp add: xa(1)) |
|
2084 have "norm x \<le> a" |
|
2085 apply (rule Lim_norm_ubound[of sequentially xa x a]) |
|
2086 apply (rule trivial_limit_sequentially) |
|
2087 apply (rule xa(2)) |
|
2088 apply fact |
|
2089 done |
2079 } |
2090 } |
2080 thus ?thesis unfolding bounded_def by auto |
2091 thus ?thesis unfolding bounded_def by auto |
2081 qed |
2092 qed |
2082 |
2093 |
2083 lemma bounded_cball[simp,intro]: "bounded (cball x e)" |
2094 lemma bounded_cball[simp,intro]: "bounded (cball x e)" |
4122 |
4133 |
4123 lemma Lim_inv: |
4134 lemma Lim_inv: |
4124 fixes f :: "'a \<Rightarrow> real" |
4135 fixes f :: "'a \<Rightarrow> real" |
4125 assumes "((vec1 o f) ---> vec1 l) (net::'a net)" "l \<noteq> 0" |
4136 assumes "((vec1 o f) ---> vec1 l) (net::'a net)" "l \<noteq> 0" |
4126 shows "((vec1 o inverse o f) ---> vec1(inverse l)) net" |
4137 shows "((vec1 o inverse o f) ---> vec1(inverse l)) net" |
4127 proof(cases "trivial_limit net") |
4138 proof - |
4128 case True thus ?thesis unfolding tendsto_def unfolding eventually_def by auto |
|
4129 next |
|
4130 case False note ntriv = this |
|
4131 { fix e::real assume "e>0" |
4139 { fix e::real assume "e>0" |
4132 hence "0 < min (\<bar>l\<bar> / 2) (l\<twosuperior> * e / 2)" using `l\<noteq>0` mult_pos_pos[of "l^2" "e/2"] by auto |
4140 let ?d = "min (\<bar>l\<bar> / 2) (l\<twosuperior> * e / 2)" |
4133 then obtain y where y1:"\<exists>x. netord net x y" and |
4141 have "0 < ?d" using `l\<noteq>0` `e>0` mult_pos_pos[of "l^2" "e/2"] by auto |
4134 y:"\<forall>x. netord net x y \<longrightarrow> dist ((vec1 \<circ> f) x) (vec1 l) < min (\<bar>l\<bar> / 2) (l\<twosuperior> * e / 2)" using ntriv |
4142 with assms(1) have "eventually (\<lambda>x. dist ((vec1 o f) x) (vec1 l) < ?d) net" |
4135 using assms(1)[unfolded tendsto_def eventually_def, THEN spec[where x="min (abs l / 2) (l ^ 2 * e / 2)"]] by auto |
4143 by (rule tendstoD) |
4136 { fix x assume "netord net x y" |
4144 moreover |
4137 hence *:"\<bar>f x - l\<bar> < min (\<bar>l\<bar> / 2) (l\<twosuperior> * e / 2)" using y[THEN spec[where x=x]] unfolding o_def dist_vec1 by auto |
4145 { fix x assume "dist ((vec1 o f) x) (vec1 l) < ?d" |
|
4146 hence *:"\<bar>f x - l\<bar> < min (\<bar>l\<bar> / 2) (l\<twosuperior> * e / 2)" unfolding o_def dist_vec1 by auto |
4138 hence fx0:"f x \<noteq> 0" using `l \<noteq> 0` by auto |
4147 hence fx0:"f x \<noteq> 0" using `l \<noteq> 0` by auto |
4139 hence fxl0: "(f x) * l \<noteq> 0" using `l \<noteq> 0` by auto |
4148 hence fxl0: "(f x) * l \<noteq> 0" using `l \<noteq> 0` by auto |
4140 from * have **:"\<bar>f x - l\<bar> < l\<twosuperior> * e / 2" by auto |
4149 from * have **:"\<bar>f x - l\<bar> < l\<twosuperior> * e / 2" by auto |
4141 have "\<bar>f x\<bar> * 2 \<ge> \<bar>l\<bar>" using * by (auto simp del: less_divide_eq_number_of1) |
4150 have "\<bar>f x\<bar> * 2 \<ge> \<bar>l\<bar>" using * by (auto simp del: less_divide_eq_number_of1) |
4142 hence "\<bar>f x\<bar> * 2 * \<bar>l\<bar> \<ge> \<bar>l\<bar> * \<bar>l\<bar>" unfolding mult_le_cancel_right by auto |
4151 hence "\<bar>f x\<bar> * 2 * \<bar>l\<bar> \<ge> \<bar>l\<bar> * \<bar>l\<bar>" unfolding mult_le_cancel_right by auto |
4149 unfolding mult_commute[of "inverse (f x)"] |
4158 unfolding mult_commute[of "inverse (f x)"] |
4150 unfolding real_divide_def[THEN sym] |
4159 unfolding real_divide_def[THEN sym] |
4151 unfolding divide_divide_eq_left |
4160 unfolding divide_divide_eq_left |
4152 unfolding nonzero_abs_divide[OF fxl0] |
4161 unfolding nonzero_abs_divide[OF fxl0] |
4153 using mult_less_le_imp_less[OF **, of "inverse \<bar>f x * l\<bar>", of "inverse (l^2 / 2)"] using *** using fx0 `l\<noteq>0` |
4162 using mult_less_le_imp_less[OF **, of "inverse \<bar>f x * l\<bar>", of "inverse (l^2 / 2)"] using *** using fx0 `l\<noteq>0` |
4154 unfolding inverse_eq_divide using `e>0` by auto } |
4163 unfolding inverse_eq_divide using `e>0` by auto |
4155 hence "(\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist ((vec1 \<circ> inverse \<circ> f) x) (vec1 (inverse l)) < e))" |
4164 } |
4156 using y1 by auto } |
4165 ultimately |
4157 thus ?thesis unfolding tendsto_def eventually_def by auto |
4166 have "eventually (\<lambda>x. dist ((vec1 o inverse o f) x) (vec1(inverse l)) < e) net" |
|
4167 by (auto elim: eventually_rev_mono) |
|
4168 } |
|
4169 thus ?thesis unfolding tendsto_def by auto |
4158 qed |
4170 qed |
4159 |
4171 |
4160 lemma continuous_inv: |
4172 lemma continuous_inv: |
4161 fixes f :: "'a \<Rightarrow> real" |
4173 fixes f :: "'a \<Rightarrow> real" |
4162 shows "continuous net (vec1 o f) \<Longrightarrow> f(netlimit net) \<noteq> 0 |
4174 shows "continuous net (vec1 o f) \<Longrightarrow> f(netlimit net) \<noteq> 0 |
4973 proof(cases "a = vec 0") |
4985 proof(cases "a = vec 0") |
4974 case True thus ?thesis using dot_lzero and Lim_const[of 0 net] unfolding vec1_vec and o_def by auto |
4986 case True thus ?thesis using dot_lzero and Lim_const[of 0 net] unfolding vec1_vec and o_def by auto |
4975 next |
4987 next |
4976 case False |
4988 case False |
4977 { fix e::real |
4989 { fix e::real |
4978 assume "0 < e" "\<forall>e>0. \<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist l (f x) < e)" |
4990 assume "0 < e" |
4979 then obtain x y where x:"netord net x y" and y:"\<forall>x. netord net x y \<longrightarrow> dist l (f x) < e / norm a" apply(erule_tac x="e / norm a" in allE) apply auto using False using norm_ge_zero[of a] apply auto |
4991 with `a \<noteq> vec 0` have "0 < e / norm a" by (simp add: divide_pos_pos) |
4980 using divide_pos_pos[of e "norm a"] by auto |
4992 with assms(1) have "eventually (\<lambda>x. dist (f x) l < e / norm a) net" |
4981 { fix z assume "netord net z y" hence "dist l (f z) < e / norm a" using y by blast |
4993 by (rule tendstoD) |
4982 hence "norm a * norm (l - f z) < e" unfolding dist_norm and |
4994 moreover |
|
4995 { fix z assume "dist (f z) l < e / norm a" |
|
4996 hence "norm a * norm (f z - l) < e" unfolding dist_norm and |
4983 pos_less_divide_eq[OF False[unfolded vec_0 zero_less_norm_iff[of a, THEN sym]]] and real_mult_commute by auto |
4997 pos_less_divide_eq[OF False[unfolded vec_0 zero_less_norm_iff[of a, THEN sym]]] and real_mult_commute by auto |
4984 hence "\<bar>a \<bullet> l - a \<bullet> f z\<bar> < e" using order_le_less_trans[OF norm_cauchy_schwarz_abs[of a "l - f z"], of e] unfolding dot_rsub[symmetric] by auto } |
4998 hence "\<bar>a \<bullet> f z - a \<bullet> l\<bar> < e" |
4985 hence "\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> \<bar>a \<bullet> l - a \<bullet> f x\<bar> < e)" using x by auto } |
4999 using order_le_less_trans[OF norm_cauchy_schwarz_abs[of a "f z - l"], of e] |
4986 thus ?thesis using assms unfolding Lim apply (auto simp add: dist_commute) |
5000 unfolding dot_rsub[symmetric] by auto } |
4987 unfolding dist_vec1 by auto |
5001 ultimately have "eventually (\<lambda>x. \<bar>a \<bullet> f x - a \<bullet> l\<bar> < e) net" |
|
5002 by (auto elim: eventually_rev_mono) |
|
5003 } |
|
5004 thus ?thesis unfolding tendsto_def |
|
5005 by (auto simp add: dist_vec1) |
4988 qed |
5006 qed |
4989 |
5007 |
4990 lemma continuous_at_vec1_dot: |
5008 lemma continuous_at_vec1_dot: |
4991 fixes x :: "real ^ _" |
5009 fixes x :: "real ^ _" |
4992 shows "continuous (at x) (vec1 o (\<lambda>y. a \<bullet> y))" |
5010 shows "continuous (at x) (vec1 o (\<lambda>y. a \<bullet> y))" |