author | hoelzl |
Wed, 10 Feb 2016 18:43:19 +0100 | |
changeset 62376 | 85f38d5f8807 |
parent 62375 | 670063003ad3 |
child 62378 | 85ed00c1fe7c |
permissions | -rw-r--r-- |
62375 | 1 |
(* Title: HOL/Library/Extended_Nonnegative_Real.thy |
2 |
Author: Johannes Hölzl |
|
3 |
*) |
|
4 |
||
5 |
subsection \<open>The type of non-negative extended real numbers\<close> |
|
6 |
||
7 |
theory Extended_Nonnegative_Real |
|
8 |
imports Extended_Real |
|
9 |
begin |
|
10 |
||
11 |
typedef ennreal = "{x :: ereal. 0 \<le> x}" |
|
12 |
morphisms enn2ereal e2ennreal |
|
13 |
by auto |
|
14 |
||
15 |
setup_lifting type_definition_ennreal |
|
16 |
||
17 |
||
18 |
lift_definition ennreal :: "real \<Rightarrow> ennreal" is "max 0 \<circ> ereal" |
|
19 |
by simp |
|
20 |
||
21 |
declare [[coercion ennreal]] |
|
22 |
declare [[coercion e2ennreal]] |
|
23 |
||
24 |
instantiation ennreal :: semiring_1_no_zero_divisors |
|
25 |
begin |
|
26 |
||
27 |
lift_definition one_ennreal :: ennreal is 1 by simp |
|
28 |
lift_definition zero_ennreal :: ennreal is 0 by simp |
|
29 |
lift_definition plus_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "op +" by simp |
|
30 |
lift_definition times_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "op *" by simp |
|
31 |
||
32 |
instance |
|
33 |
by standard (transfer; auto simp: field_simps ereal_right_distrib)+ |
|
34 |
||
35 |
end |
|
36 |
||
37 |
instance ennreal :: numeral .. |
|
38 |
||
39 |
instantiation ennreal :: inverse |
|
40 |
begin |
|
41 |
||
42 |
lift_definition inverse_ennreal :: "ennreal \<Rightarrow> ennreal" is inverse |
|
43 |
by (rule inverse_ereal_ge0I) |
|
44 |
||
45 |
definition divide_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" |
|
46 |
where "x div y = x * inverse (y :: ennreal)" |
|
47 |
||
48 |
instance .. |
|
49 |
||
50 |
end |
|
51 |
||
52 |
||
53 |
instantiation ennreal :: complete_linorder |
|
54 |
begin |
|
55 |
||
56 |
lift_definition top_ennreal :: ennreal is top by simp |
|
57 |
lift_definition bot_ennreal :: ennreal is 0 by simp |
|
58 |
lift_definition sup_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is sup by (simp add: max.coboundedI1) |
|
59 |
lift_definition inf_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is inf by (simp add: min.boundedI) |
|
60 |
||
61 |
lift_definition Inf_ennreal :: "ennreal set \<Rightarrow> ennreal" is "Inf" |
|
62 |
by (auto intro: Inf_greatest) |
|
63 |
||
64 |
lift_definition Sup_ennreal :: "ennreal set \<Rightarrow> ennreal" is "sup 0 \<circ> Sup" |
|
65 |
by auto |
|
66 |
||
67 |
lift_definition less_eq_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> bool" is "op \<le>" . |
|
68 |
lift_definition less_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> bool" is "op <" . |
|
69 |
||
70 |
instance |
|
71 |
by standard |
|
72 |
(transfer ; auto simp: Inf_lower Inf_greatest Sup_upper Sup_least le_max_iff_disj max.absorb1)+ |
|
73 |
||
74 |
end |
|
75 |
||
76 |
||
77 |
||
78 |
lemma ennreal_zero_less_one: "0 < (1::ennreal)" |
|
79 |
by transfer auto |
|
80 |
||
62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62375
diff
changeset
|
81 |
instance ennreal :: dioid |
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62375
diff
changeset
|
82 |
proof (standard; transfer) |
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62375
diff
changeset
|
83 |
fix a b :: ereal assume "0 \<le> a" "0 \<le> b" then show "(a \<le> b) = (\<exists>c\<in>Collect (op \<le> 0). b = a + c)" |
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62375
diff
changeset
|
84 |
unfolding ereal_ex_split Bex_def |
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62375
diff
changeset
|
85 |
by (cases a b rule: ereal2_cases) (auto intro!: exI[of _ "real_of_ereal (b - a)"]) |
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62375
diff
changeset
|
86 |
qed |
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62375
diff
changeset
|
87 |
|
62375 | 88 |
instance ennreal :: ordered_comm_semiring |
89 |
by standard |
|
90 |
(transfer ; auto intro: add_mono mult_mono mult_ac ereal_left_distrib ereal_mult_left_mono)+ |
|
91 |
||
92 |
instantiation ennreal :: linear_continuum_topology |
|
93 |
begin |
|
94 |
||
95 |
definition open_ennreal :: "ennreal set \<Rightarrow> bool" |
|
96 |
where "(open :: ennreal set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)" |
|
97 |
||
98 |
instance |
|
99 |
proof |
|
100 |
show "\<exists>a b::ennreal. a \<noteq> b" |
|
101 |
using ennreal_zero_less_one by (auto dest: order.strict_implies_not_eq) |
|
102 |
show "\<And>x y::ennreal. x < y \<Longrightarrow> \<exists>z>x. z < y" |
|
103 |
proof transfer |
|
104 |
fix x y :: ereal assume "0 \<le> x" "x < y" |
|
105 |
moreover from dense[OF this(2)] guess z .. |
|
106 |
ultimately show "\<exists>z\<in>Collect (op \<le> 0). x < z \<and> z < y" |
|
107 |
by (intro bexI[of _ z]) auto |
|
108 |
qed |
|
109 |
qed (rule open_ennreal_def) |
|
110 |
||
111 |
end |
|
112 |
||
113 |
lemma ennreal_rat_dense: |
|
114 |
fixes x y :: ennreal |
|
115 |
shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y" |
|
116 |
proof transfer |
|
117 |
fix x y :: ereal assume xy: "0 \<le> x" "0 \<le> y" "x < y" |
|
118 |
moreover |
|
119 |
from ereal_dense3[OF \<open>x < y\<close>] |
|
120 |
obtain r where "x < ereal (real_of_rat r)" "ereal (real_of_rat r) < y" |
|
121 |
by auto |
|
122 |
moreover then have "0 \<le> r" |
|
123 |
using le_less_trans[OF \<open>0 \<le> x\<close> \<open>x < ereal (real_of_rat r)\<close>] by auto |
|
124 |
ultimately show "\<exists>r. x < (max 0 \<circ> ereal) (real_of_rat r) \<and> (max 0 \<circ> ereal) (real_of_rat r) < y" |
|
125 |
by (intro exI[of _ r]) (auto simp: max_absorb2) |
|
126 |
qed |
|
127 |
||
128 |
lemma enn2ereal_range: "e2ennreal ` {0..} = UNIV" |
|
129 |
proof - |
|
130 |
have "\<exists>y\<ge>0. x = e2ennreal y" for x |
|
131 |
by (cases x) auto |
|
132 |
then show ?thesis |
|
133 |
by (auto simp: image_iff Bex_def) |
|
134 |
qed |
|
135 |
||
136 |
lemma enn2ereal_nonneg: "0 \<le> enn2ereal x" |
|
137 |
using ennreal.enn2ereal[of x] by simp |
|
138 |
||
139 |
lemma ereal_ennreal_cases: |
|
140 |
obtains b where "0 \<le> a" "a = enn2ereal b" | "a < 0" |
|
141 |
using e2ennreal_inverse[of a, symmetric] by (cases "0 \<le> a") (auto intro: enn2ereal_nonneg) |
|
142 |
||
143 |
lemma enn2ereal_Iio: "enn2ereal -` {..<a} = (if 0 \<le> a then {..< e2ennreal a} else {})" |
|
144 |
using enn2ereal_nonneg |
|
145 |
by (cases a rule: ereal_ennreal_cases) |
|
146 |
(auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq |
|
147 |
intro: le_less_trans less_imp_le) |
|
148 |
||
149 |
lemma enn2ereal_Ioi: "enn2ereal -` {a <..} = (if 0 \<le> a then {e2ennreal a <..} else UNIV)" |
|
150 |
using enn2ereal_nonneg |
|
151 |
by (cases a rule: ereal_ennreal_cases) |
|
152 |
(auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq |
|
153 |
intro: less_le_trans) |
|
154 |
||
155 |
lemma continuous_e2ennreal: "continuous_on {0 ..} e2ennreal" |
|
156 |
by (rule continuous_onI_mono) |
|
157 |
(auto simp add: less_eq_ennreal.abs_eq eq_onp_def enn2ereal_range) |
|
158 |
||
159 |
lemma continuous_enn2ereal: "continuous_on UNIV enn2ereal" |
|
160 |
by (rule continuous_on_generate_topology[OF open_generated_order]) |
|
161 |
(auto simp add: enn2ereal_Iio enn2ereal_Ioi) |
|
162 |
||
163 |
lemma transfer_enn2ereal_continuous_on [transfer_rule]: |
|
164 |
"rel_fun (op =) (rel_fun (rel_fun op = pcr_ennreal) op =) continuous_on continuous_on" |
|
165 |
proof - |
|
166 |
have "continuous_on A f" if "continuous_on A (\<lambda>x. enn2ereal (f x))" for A and f :: "'a \<Rightarrow> ennreal" |
|
167 |
using continuous_on_compose2[OF continuous_e2ennreal that] |
|
168 |
by (auto simp: ennreal.enn2ereal_inverse subset_eq enn2ereal_nonneg) |
|
169 |
moreover |
|
170 |
have "continuous_on A (\<lambda>x. enn2ereal (f x))" if "continuous_on A f" for A and f :: "'a \<Rightarrow> ennreal" |
|
171 |
using continuous_on_compose2[OF continuous_enn2ereal that] by auto |
|
172 |
ultimately |
|
173 |
show ?thesis |
|
174 |
by (auto simp add: rel_fun_def ennreal.pcr_cr_eq cr_ennreal_def) |
|
175 |
qed |
|
176 |
||
177 |
lemma continuous_on_add_ennreal[continuous_intros]: |
|
178 |
fixes f g :: "'a::topological_space \<Rightarrow> ennreal" |
|
179 |
shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. f x + g x)" |
|
180 |
by (transfer fixing: A) (auto intro!: tendsto_add_ereal_nonneg simp: continuous_on_def) |
|
181 |
||
182 |
lemma continuous_on_inverse_ennreal[continuous_intros]: |
|
183 |
fixes f :: "_ \<Rightarrow> ennreal" |
|
184 |
shows "continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. inverse (f x))" |
|
185 |
proof (transfer fixing: A) |
|
186 |
show "pred_fun (op \<le> 0) f \<Longrightarrow> continuous_on A (\<lambda>x. inverse (f x))" if "continuous_on A f" |
|
187 |
for f :: "_ \<Rightarrow> ereal" |
|
188 |
using continuous_on_compose2[OF continuous_on_inverse_ereal that] by (auto simp: subset_eq) |
|
189 |
qed |
|
190 |
||
191 |
end |