15 |
15 |
16 For more lemmas about the extended real numbers go to |
16 For more lemmas about the extended real numbers go to |
17 @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"} |
17 @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"} |
18 |
18 |
19 *} |
19 *} |
20 |
|
21 lemma LIMSEQ_SUP: |
|
22 fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}" |
|
23 assumes "incseq X" |
|
24 shows "X ----> (SUP i. X i)" |
|
25 using `incseq X` |
|
26 by (intro increasing_tendsto) |
|
27 (auto simp: SUP_upper less_SUP_iff incseq_def eventually_sequentially intro: less_le_trans) |
|
28 |
|
29 lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P" |
|
30 by (cases P) (simp_all add: eventually_False) |
|
31 |
|
32 lemma (in complete_lattice) Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A" |
|
33 by (metis Sup_upper2 Inf_lower ex_in_conv) |
|
34 |
|
35 lemma (in complete_lattice) INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f" |
|
36 unfolding INF_def SUP_def by (rule Inf_le_Sup) auto |
|
37 |
|
38 lemma (in complete_linorder) le_Sup_iff: |
|
39 "x \<le> Sup A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)" |
|
40 proof safe |
|
41 fix y assume "x \<le> Sup A" "y < x" |
|
42 then have "y < Sup A" by auto |
|
43 then show "\<exists>a\<in>A. y < a" |
|
44 unfolding less_Sup_iff . |
|
45 qed (auto elim!: allE[of _ "Sup A"] simp add: not_le[symmetric] Sup_upper) |
|
46 |
|
47 lemma (in complete_linorder) le_SUP_iff: |
|
48 "x \<le> SUPR A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)" |
|
49 unfolding le_Sup_iff SUP_def by simp |
|
50 |
|
51 lemma (in complete_linorder) Inf_le_iff: |
|
52 "Inf A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)" |
|
53 proof safe |
|
54 fix y assume "x \<ge> Inf A" "y > x" |
|
55 then have "y > Inf A" by auto |
|
56 then show "\<exists>a\<in>A. y > a" |
|
57 unfolding Inf_less_iff . |
|
58 qed (auto elim!: allE[of _ "Inf A"] simp add: not_le[symmetric] Inf_lower) |
|
59 |
|
60 lemma (in complete_linorder) le_INF_iff: |
|
61 "INFI A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)" |
|
62 unfolding Inf_le_iff INF_def by simp |
|
63 |
|
64 lemma (in complete_lattice) Sup_eqI: |
|
65 assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" |
|
66 assumes "\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y" |
|
67 shows "Sup A = x" |
|
68 by (metis antisym Sup_least Sup_upper assms) |
|
69 |
|
70 lemma (in complete_lattice) Inf_eqI: |
|
71 assumes "\<And>i. i \<in> A \<Longrightarrow> x \<le> i" |
|
72 assumes "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> i) \<Longrightarrow> y \<le> x" |
|
73 shows "Inf A = x" |
|
74 by (metis antisym Inf_greatest Inf_lower assms) |
|
75 |
|
76 lemma (in complete_lattice) SUP_eqI: |
|
77 "(\<And>i. i \<in> A \<Longrightarrow> f i \<le> x) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> (SUP i:A. f i) = x" |
|
78 unfolding SUP_def by (rule Sup_eqI) auto |
|
79 |
|
80 lemma (in complete_lattice) INF_eqI: |
|
81 "(\<And>i. i \<in> A \<Longrightarrow> x \<le> f i) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<ge> y) \<Longrightarrow> x \<ge> y) \<Longrightarrow> (INF i:A. f i) = x" |
|
82 unfolding INF_def by (rule Inf_eqI) auto |
|
83 |
|
84 lemma (in complete_lattice) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot" |
|
85 proof |
|
86 assume "{x..} = UNIV" |
|
87 show "x = bot" |
|
88 proof (rule ccontr) |
|
89 assume "x \<noteq> bot" then have "bot \<notin> {x..}" by (simp add: le_less) |
|
90 then show False using `{x..} = UNIV` by simp |
|
91 qed |
|
92 qed auto |
|
93 |
20 |
94 lemma SUPR_pair: |
21 lemma SUPR_pair: |
95 "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))" |
22 "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))" |
96 by (rule antisym) (auto intro!: SUP_least SUP_upper2) |
23 by (rule antisym) (auto intro!: SUP_least SUP_upper2) |
97 |
24 |
1445 then show ?thesis |
1372 then show ?thesis |
1446 using SUP_eq_top_iff[of UNIV "\<lambda>n::nat. ereal (real n)"] |
1373 using SUP_eq_top_iff[of UNIV "\<lambda>n::nat. ereal (real n)"] |
1447 by (auto simp: top_ereal_def) |
1374 by (auto simp: top_ereal_def) |
1448 qed |
1375 qed |
1449 |
1376 |
1450 lemma ereal_le_Sup: |
|
1451 fixes x :: ereal |
|
1452 shows "(x <= (SUP i:A. f i)) <-> (ALL y. y < x --> (EX i. i : A & y <= f i))" (is "?lhs = ?rhs") |
|
1453 proof- |
|
1454 { assume "?rhs" |
|
1455 { assume "~(x <= (SUP i:A. f i))" hence "(SUP i:A. f i)<x" by (simp add: not_le) |
|
1456 then obtain y where y_def: "(SUP i:A. f i)<y & y<x" using ereal_dense by auto |
|
1457 then obtain i where "i : A & y <= f i" using `?rhs` by auto |
|
1458 hence "y <= (SUP i:A. f i)" using SUP_upper[of i A f] by auto |
|
1459 hence False using y_def by auto |
|
1460 } hence "?lhs" by auto |
|
1461 } |
|
1462 moreover |
|
1463 { assume "?lhs" hence "?rhs" |
|
1464 by (metis less_SUP_iff order_less_imp_le order_less_le_trans) |
|
1465 } ultimately show ?thesis by auto |
|
1466 qed |
|
1467 |
|
1468 lemma ereal_Inf_le: |
|
1469 fixes x :: ereal |
|
1470 shows "((INF i:A. f i) <= x) <-> (ALL y. x < y --> (EX i. i : A & f i <= y))" |
|
1471 (is "?lhs <-> ?rhs") |
|
1472 proof- |
|
1473 { assume "?rhs" |
|
1474 { assume "~((INF i:A. f i) <= x)" hence "x < (INF i:A. f i)" by (simp add: not_le) |
|
1475 then obtain y where y_def: "x<y & y<(INF i:A. f i)" using ereal_dense by auto |
|
1476 then obtain i where "i : A & f i <= y" using `?rhs` by auto |
|
1477 hence "(INF i:A. f i) <= y" using INF_lower[of i A f] by auto |
|
1478 hence False using y_def by auto |
|
1479 } hence "?lhs" by auto |
|
1480 } |
|
1481 moreover |
|
1482 { assume "?lhs" hence "?rhs" |
|
1483 by (metis INF_less_iff order_le_less order_less_le_trans) |
|
1484 } ultimately show ?thesis by auto |
|
1485 qed |
|
1486 |
|
1487 lemma Inf_less: |
1377 lemma Inf_less: |
1488 fixes x :: ereal |
1378 fixes x :: ereal |
1489 assumes "(INF i:A. f i) < x" |
1379 assumes "(INF i:A. f i) < x" |
1490 shows "EX i. i : A & f i <= x" |
1380 shows "EX i. i : A & f i <= x" |
1491 proof(rule ccontr) |
1381 proof(rule ccontr) |
1492 assume "~ (EX i. i : A & f i <= x)" |
1382 assume "~ (EX i. i : A & f i <= x)" |
1493 hence "ALL i:A. f i > x" by auto |
1383 hence "ALL i:A. f i > x" by auto |
1494 hence "(INF i:A. f i) >= x" apply (subst INF_greatest) by auto |
1384 hence "(INF i:A. f i) >= x" apply (subst INF_greatest) by auto |
1495 thus False using assms by auto |
1385 thus False using assms by auto |
1496 qed |
|
1497 |
|
1498 lemma same_INF: |
|
1499 assumes "ALL e:A. f e = g e" |
|
1500 shows "(INF e:A. f e) = (INF e:A. g e)" |
|
1501 proof- |
|
1502 have "f ` A = g ` A" unfolding image_def using assms by auto |
|
1503 thus ?thesis unfolding INF_def by auto |
|
1504 qed |
|
1505 |
|
1506 lemma same_SUP: |
|
1507 assumes "ALL e:A. f e = g e" |
|
1508 shows "(SUP e:A. f e) = (SUP e:A. g e)" |
|
1509 proof- |
|
1510 have "f ` A = g ` A" unfolding image_def using assms by auto |
|
1511 thus ?thesis unfolding SUP_def by auto |
|
1512 qed |
|
1513 |
|
1514 lemma SUPR_eq: |
|
1515 assumes "\<forall>i\<in>A. \<exists>j\<in>B. f i \<le> g j" |
|
1516 assumes "\<forall>j\<in>B. \<exists>i\<in>A. g j \<le> f i" |
|
1517 shows "(SUP i:A. f i) = (SUP j:B. g j)" |
|
1518 proof (intro antisym) |
|
1519 show "(SUP i:A. f i) \<le> (SUP j:B. g j)" |
|
1520 using assms by (metis SUP_least SUP_upper2) |
|
1521 show "(SUP i:B. g i) \<le> (SUP j:A. f j)" |
|
1522 using assms by (metis SUP_least SUP_upper2) |
|
1523 qed |
|
1524 |
|
1525 lemma INFI_eq: |
|
1526 assumes "\<forall>i\<in>A. \<exists>j\<in>B. f i \<ge> g j" |
|
1527 assumes "\<forall>j\<in>B. \<exists>i\<in>A. g j \<ge> f i" |
|
1528 shows "(INF i:A. f i) = (INF j:B. g j)" |
|
1529 proof (intro antisym) |
|
1530 show "(INF i:A. f i) \<le> (INF j:B. g j)" |
|
1531 using assms by (metis INF_greatest INF_lower2) |
|
1532 show "(INF i:B. g i) \<le> (INF j:A. f j)" |
|
1533 using assms by (metis INF_greatest INF_lower2) |
|
1534 qed |
1386 qed |
1535 |
1387 |
1536 lemma SUP_ereal_le_addI: |
1388 lemma SUP_ereal_le_addI: |
1537 fixes f :: "'i \<Rightarrow> ereal" |
1389 fixes f :: "'i \<Rightarrow> ereal" |
1538 assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>" |
1390 assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>" |