src/HOL/Library/Extended_Reals.thy
 author hoelzl Mon Mar 14 14:37:46 2011 +0100 (2011-03-14) changeset 41979 b10ec1f5e9d5 parent 41978 656298577a33 child 41980 28b51effc5ed permissions -rw-r--r--
lemmas about addition, SUP on countable sets and infinite sums for extreal
 hoelzl@41978 ` 1` ```(* Title: Extended_Reals.thy ``` hoelzl@41973 ` 2` ``` Author: Johannes Hölzl, Robert Himmelmann, Armin Heller; TU München ``` hoelzl@41973 ` 3` ``` Author: Bogdan Grechuk; University of Edinburgh *) ``` hoelzl@41973 ` 4` hoelzl@41973 ` 5` ```header {* Extended real number line *} ``` hoelzl@41973 ` 6` hoelzl@41973 ` 7` ```theory Extended_Reals ``` hoelzl@41973 ` 8` ``` imports Topology_Euclidean_Space ``` hoelzl@41973 ` 9` ```begin ``` hoelzl@41973 ` 10` hoelzl@41979 ` 11` ```lemma (in complete_lattice) atLeast_eq_UNIV_iff: "{x..} = UNIV \ x = bot" ``` hoelzl@41979 ` 12` ```proof ``` hoelzl@41979 ` 13` ``` assume "{x..} = UNIV" ``` hoelzl@41979 ` 14` ``` show "x = bot" ``` hoelzl@41979 ` 15` ``` proof (rule ccontr) ``` hoelzl@41979 ` 16` ``` assume "x \ bot" then have "bot \ {x..}" by (simp add: le_less) ``` hoelzl@41979 ` 17` ``` then show False using `{x..} = UNIV` by simp ``` hoelzl@41979 ` 18` ``` qed ``` hoelzl@41979 ` 19` ```qed auto ``` hoelzl@41979 ` 20` hoelzl@41979 ` 21` ```lemma SUPR_pair: ``` hoelzl@41979 ` 22` ``` "(SUP i : A. SUP j : B. f i j) = (SUP p : A \ B. f (fst p) (snd p))" ``` hoelzl@41979 ` 23` ``` by (rule antisym) (auto intro!: SUP_leI le_SUPI_trans) ``` hoelzl@41979 ` 24` hoelzl@41979 ` 25` ```lemma INFI_pair: ``` hoelzl@41979 ` 26` ``` "(INF i : A. INF j : B. f i j) = (INF p : A \ B. f (fst p) (snd p))" ``` hoelzl@41979 ` 27` ``` by (rule antisym) (auto intro!: le_INFI INF_leI_trans) ``` hoelzl@41979 ` 28` hoelzl@41973 ` 29` ```subsection {* Definition and basic properties *} ``` hoelzl@41973 ` 30` hoelzl@41973 ` 31` ```datatype extreal = extreal real | PInfty | MInfty ``` hoelzl@41973 ` 32` hoelzl@41973 ` 33` ```notation (xsymbols) ``` hoelzl@41973 ` 34` ``` PInfty ("\") ``` hoelzl@41973 ` 35` hoelzl@41973 ` 36` ```notation (HTML output) ``` hoelzl@41973 ` 37` ``` PInfty ("\") ``` hoelzl@41973 ` 38` hoelzl@41979 ` 39` ```declare [[coercion "extreal :: real \ extreal"]] ``` hoelzl@41979 ` 40` hoelzl@41973 ` 41` ```instantiation extreal :: uminus ``` hoelzl@41973 ` 42` ```begin ``` hoelzl@41973 ` 43` ``` fun uminus_extreal where ``` hoelzl@41973 ` 44` ``` "- (extreal r) = extreal (- r)" ``` hoelzl@41973 ` 45` ``` | "- \ = MInfty" ``` hoelzl@41973 ` 46` ``` | "- MInfty = \" ``` hoelzl@41973 ` 47` ``` instance .. ``` hoelzl@41973 ` 48` ```end ``` hoelzl@41973 ` 49` hoelzl@41976 ` 50` ```lemma inj_extreal[simp]: "inj_on extreal A" ``` hoelzl@41976 ` 51` ``` unfolding inj_on_def by auto ``` hoelzl@41976 ` 52` hoelzl@41973 ` 53` ```lemma MInfty_neq_PInfty[simp]: ``` hoelzl@41973 ` 54` ``` "\ \ - \" "- \ \ \" by simp_all ``` hoelzl@41973 ` 55` hoelzl@41973 ` 56` ```lemma MInfty_neq_extreal[simp]: ``` hoelzl@41973 ` 57` ``` "extreal r \ - \" "- \ \ extreal r" by simp_all ``` hoelzl@41973 ` 58` hoelzl@41973 ` 59` ```lemma MInfinity_cases[simp]: ``` hoelzl@41973 ` 60` ``` "(case - \ of extreal r \ f r | \ \ y | MInfinity \ z) = z" ``` hoelzl@41973 ` 61` ``` by simp ``` hoelzl@41973 ` 62` hoelzl@41973 ` 63` ```lemma extreal_uminus_uminus[simp]: ``` hoelzl@41973 ` 64` ``` fixes a :: extreal shows "- (- a) = a" ``` hoelzl@41973 ` 65` ``` by (cases a) simp_all ``` hoelzl@41973 ` 66` hoelzl@41973 ` 67` ```lemma MInfty_eq[simp]: ``` hoelzl@41973 ` 68` ``` "MInfty = - \" by simp ``` hoelzl@41973 ` 69` hoelzl@41973 ` 70` ```declare uminus_extreal.simps(2)[simp del] ``` hoelzl@41973 ` 71` hoelzl@41973 ` 72` ```lemma extreal_cases[case_names real PInf MInf, cases type: extreal]: ``` hoelzl@41973 ` 73` ``` assumes "\r. x = extreal r \ P" ``` hoelzl@41973 ` 74` ``` assumes "x = \ \ P" ``` hoelzl@41973 ` 75` ``` assumes "x = -\ \ P" ``` hoelzl@41973 ` 76` ``` shows P ``` hoelzl@41973 ` 77` ``` using assms by (cases x) auto ``` hoelzl@41973 ` 78` hoelzl@41974 ` 79` ```lemmas extreal2_cases = extreal_cases[case_product extreal_cases] ``` hoelzl@41974 ` 80` ```lemmas extreal3_cases = extreal2_cases[case_product extreal_cases] ``` hoelzl@41973 ` 81` hoelzl@41973 ` 82` ```lemma extreal_uminus_eq_iff[simp]: ``` hoelzl@41973 ` 83` ``` fixes a b :: extreal shows "-a = -b \ a = b" ``` hoelzl@41973 ` 84` ``` by (cases rule: extreal2_cases[of a b]) simp_all ``` hoelzl@41973 ` 85` hoelzl@41973 ` 86` ```function of_extreal :: "extreal \ real" where ``` hoelzl@41973 ` 87` ```"of_extreal (extreal r) = r" | ``` hoelzl@41973 ` 88` ```"of_extreal \ = 0" | ``` hoelzl@41973 ` 89` ```"of_extreal (-\) = 0" ``` hoelzl@41973 ` 90` ``` by (auto intro: extreal_cases) ``` hoelzl@41973 ` 91` ```termination proof qed (rule wf_empty) ``` hoelzl@41973 ` 92` hoelzl@41973 ` 93` ```defs (overloaded) ``` hoelzl@41973 ` 94` ``` real_of_extreal_def [code_unfold]: "real \ of_extreal" ``` hoelzl@41973 ` 95` hoelzl@41973 ` 96` ```lemma real_of_extreal[simp]: ``` hoelzl@41973 ` 97` ``` "real (- x :: extreal) = - (real x)" ``` hoelzl@41973 ` 98` ``` "real (extreal r) = r" ``` hoelzl@41973 ` 99` ``` "real \ = 0" ``` hoelzl@41973 ` 100` ``` by (cases x) (simp_all add: real_of_extreal_def) ``` hoelzl@41973 ` 101` hoelzl@41973 ` 102` ```lemma range_extreal[simp]: "range extreal = UNIV - {\, -\}" ``` hoelzl@41973 ` 103` ```proof safe ``` hoelzl@41973 ` 104` ``` fix x assume "x \ range extreal" "x \ \" ``` hoelzl@41973 ` 105` ``` then show "x = -\" by (cases x) auto ``` hoelzl@41973 ` 106` ```qed auto ``` hoelzl@41973 ` 107` hoelzl@41979 ` 108` ```lemma extreal_range_uminus[simp]: "range uminus = (UNIV::extreal set)" ``` hoelzl@41979 ` 109` ```proof safe ``` hoelzl@41979 ` 110` ``` fix x :: extreal show "x \ range uminus" by (intro image_eqI[of _ _ "-x"]) auto ``` hoelzl@41979 ` 111` ```qed auto ``` hoelzl@41979 ` 112` hoelzl@41973 ` 113` ```instantiation extreal :: number ``` hoelzl@41973 ` 114` ```begin ``` hoelzl@41973 ` 115` ```definition [simp]: "number_of x = extreal (number_of x)" ``` hoelzl@41973 ` 116` ```instance proof qed ``` hoelzl@41973 ` 117` ```end ``` hoelzl@41973 ` 118` hoelzl@41976 ` 119` ```instantiation extreal :: abs ``` hoelzl@41976 ` 120` ```begin ``` hoelzl@41976 ` 121` ``` function abs_extreal where ``` hoelzl@41976 ` 122` ``` "\extreal r\ = extreal \r\" ``` hoelzl@41976 ` 123` ``` | "\-\\ = \" ``` hoelzl@41976 ` 124` ``` | "\\\ = \" ``` hoelzl@41976 ` 125` ``` by (auto intro: extreal_cases) ``` hoelzl@41976 ` 126` ``` termination proof qed (rule wf_empty) ``` hoelzl@41976 ` 127` ``` instance .. ``` hoelzl@41976 ` 128` ```end ``` hoelzl@41976 ` 129` hoelzl@41976 ` 130` ```lemma abs_eq_infinity_cases[elim!]: "\ \x\ = \ ; x = \ \ P ; x = -\ \ P \ \ P" ``` hoelzl@41976 ` 131` ``` by (cases x) auto ``` hoelzl@41976 ` 132` hoelzl@41976 ` 133` ```lemma abs_neq_infinity_cases[elim!]: "\ \x\ \ \ ; \r. x = extreal r \ P \ \ P" ``` hoelzl@41976 ` 134` ``` by (cases x) auto ``` hoelzl@41976 ` 135` hoelzl@41976 ` 136` ```lemma abs_extreal_uminus[simp]: "\- x\ = \x::extreal\" ``` hoelzl@41976 ` 137` ``` by (cases x) auto ``` hoelzl@41976 ` 138` hoelzl@41973 ` 139` ```subsubsection "Addition" ``` hoelzl@41973 ` 140` hoelzl@41973 ` 141` ```instantiation extreal :: comm_monoid_add ``` hoelzl@41973 ` 142` ```begin ``` hoelzl@41973 ` 143` hoelzl@41973 ` 144` ```definition "0 = extreal 0" ``` hoelzl@41973 ` 145` hoelzl@41973 ` 146` ```function plus_extreal where ``` hoelzl@41973 ` 147` ```"extreal r + extreal p = extreal (r + p)" | ``` hoelzl@41973 ` 148` ```"\ + a = \" | ``` hoelzl@41973 ` 149` ```"a + \ = \" | ``` hoelzl@41973 ` 150` ```"extreal r + -\ = - \" | ``` hoelzl@41973 ` 151` ```"-\ + extreal p = -\" | ``` hoelzl@41973 ` 152` ```"-\ + -\ = -\" ``` hoelzl@41973 ` 153` ```proof - ``` hoelzl@41973 ` 154` ``` case (goal1 P x) ``` hoelzl@41973 ` 155` ``` moreover then obtain a b where "x = (a, b)" by (cases x) auto ``` hoelzl@41973 ` 156` ``` ultimately show P ``` hoelzl@41973 ` 157` ``` by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@41973 ` 158` ```qed auto ``` hoelzl@41973 ` 159` ```termination proof qed (rule wf_empty) ``` hoelzl@41973 ` 160` hoelzl@41973 ` 161` ```lemma Infty_neq_0[simp]: ``` hoelzl@41973 ` 162` ``` "\ \ 0" "0 \ \" ``` hoelzl@41973 ` 163` ``` "-\ \ 0" "0 \ -\" ``` hoelzl@41973 ` 164` ``` by (simp_all add: zero_extreal_def) ``` hoelzl@41973 ` 165` hoelzl@41973 ` 166` ```lemma extreal_eq_0[simp]: ``` hoelzl@41973 ` 167` ``` "extreal r = 0 \ r = 0" ``` hoelzl@41973 ` 168` ``` "0 = extreal r \ r = 0" ``` hoelzl@41973 ` 169` ``` unfolding zero_extreal_def by simp_all ``` hoelzl@41973 ` 170` hoelzl@41973 ` 171` ```instance ``` hoelzl@41973 ` 172` ```proof ``` hoelzl@41973 ` 173` ``` fix a :: extreal show "0 + a = a" ``` hoelzl@41973 ` 174` ``` by (cases a) (simp_all add: zero_extreal_def) ``` hoelzl@41973 ` 175` ``` fix b :: extreal show "a + b = b + a" ``` hoelzl@41973 ` 176` ``` by (cases rule: extreal2_cases[of a b]) simp_all ``` hoelzl@41973 ` 177` ``` fix c :: extreal show "a + b + c = a + (b + c)" ``` hoelzl@41973 ` 178` ``` by (cases rule: extreal3_cases[of a b c]) simp_all ``` hoelzl@41973 ` 179` ```qed ``` hoelzl@41973 ` 180` ```end ``` hoelzl@41973 ` 181` hoelzl@41976 ` 182` ```lemma abs_extreal_zero[simp]: "\0\ = (0::extreal)" ``` hoelzl@41976 ` 183` ``` unfolding zero_extreal_def abs_extreal.simps by simp ``` hoelzl@41976 ` 184` hoelzl@41973 ` 185` ```lemma extreal_uminus_zero[simp]: ``` hoelzl@41973 ` 186` ``` "- 0 = (0::extreal)" ``` hoelzl@41973 ` 187` ``` by (simp add: zero_extreal_def) ``` hoelzl@41973 ` 188` hoelzl@41973 ` 189` ```lemma extreal_uminus_zero_iff[simp]: ``` hoelzl@41973 ` 190` ``` fixes a :: extreal shows "-a = 0 \ a = 0" ``` hoelzl@41973 ` 191` ``` by (cases a) simp_all ``` hoelzl@41973 ` 192` hoelzl@41973 ` 193` ```lemma extreal_plus_eq_PInfty[simp]: ``` hoelzl@41973 ` 194` ``` shows "a + b = \ \ a = \ \ b = \" ``` hoelzl@41973 ` 195` ``` by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@41973 ` 196` hoelzl@41973 ` 197` ```lemma extreal_plus_eq_MInfty[simp]: ``` hoelzl@41973 ` 198` ``` shows "a + b = -\ \ ``` hoelzl@41973 ` 199` ``` (a = -\ \ b = -\) \ a \ \ \ b \ \" ``` hoelzl@41973 ` 200` ``` by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@41973 ` 201` hoelzl@41973 ` 202` ```lemma extreal_add_cancel_left: ``` hoelzl@41973 ` 203` ``` assumes "a \ -\" ``` hoelzl@41973 ` 204` ``` shows "a + b = a + c \ (a = \ \ b = c)" ``` hoelzl@41973 ` 205` ``` using assms by (cases rule: extreal3_cases[of a b c]) auto ``` hoelzl@41973 ` 206` hoelzl@41973 ` 207` ```lemma extreal_add_cancel_right: ``` hoelzl@41973 ` 208` ``` assumes "a \ -\" ``` hoelzl@41973 ` 209` ``` shows "b + a = c + a \ (a = \ \ b = c)" ``` hoelzl@41973 ` 210` ``` using assms by (cases rule: extreal3_cases[of a b c]) auto ``` hoelzl@41973 ` 211` hoelzl@41973 ` 212` ```lemma extreal_real: ``` hoelzl@41976 ` 213` ``` "extreal (real x) = (if \x\ = \ then 0 else x)" ``` hoelzl@41973 ` 214` ``` by (cases x) simp_all ``` hoelzl@41973 ` 215` hoelzl@41979 ` 216` ```lemma real_of_extreal_add: ``` hoelzl@41979 ` 217` ``` fixes a b :: extreal ``` hoelzl@41979 ` 218` ``` shows "real (a + b) = (if (\a\ = \) \ (\b\ = \) \ (\a\ \ \) \ (\b\ \ \) then real a + real b else 0)" ``` hoelzl@41979 ` 219` ``` by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@41979 ` 220` hoelzl@41973 ` 221` ```subsubsection "Linear order on @{typ extreal}" ``` hoelzl@41973 ` 222` hoelzl@41973 ` 223` ```instantiation extreal :: linorder ``` hoelzl@41973 ` 224` ```begin ``` hoelzl@41973 ` 225` hoelzl@41973 ` 226` ```function less_extreal where ``` hoelzl@41973 ` 227` ```"extreal x < extreal y \ x < y" | ``` hoelzl@41973 ` 228` ```" \ < a \ False" | ``` hoelzl@41973 ` 229` ```" a < -\ \ False" | ``` hoelzl@41973 ` 230` ```"extreal x < \ \ True" | ``` hoelzl@41973 ` 231` ```" -\ < extreal r \ True" | ``` hoelzl@41973 ` 232` ```" -\ < \ \ True" ``` hoelzl@41973 ` 233` ```proof - ``` hoelzl@41973 ` 234` ``` case (goal1 P x) ``` hoelzl@41973 ` 235` ``` moreover then obtain a b where "x = (a,b)" by (cases x) auto ``` hoelzl@41973 ` 236` ``` ultimately show P by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@41973 ` 237` ```qed simp_all ``` hoelzl@41973 ` 238` ```termination by (relation "{}") simp ``` hoelzl@41973 ` 239` hoelzl@41973 ` 240` ```definition "x \ (y::extreal) \ x < y \ x = y" ``` hoelzl@41973 ` 241` hoelzl@41973 ` 242` ```lemma extreal_infty_less[simp]: ``` hoelzl@41973 ` 243` ``` "x < \ \ (x \ \)" ``` hoelzl@41973 ` 244` ``` "-\ < x \ (x \ -\)" ``` hoelzl@41973 ` 245` ``` by (cases x, simp_all) (cases x, simp_all) ``` hoelzl@41973 ` 246` hoelzl@41973 ` 247` ```lemma extreal_infty_less_eq[simp]: ``` hoelzl@41973 ` 248` ``` "\ \ x \ x = \" ``` hoelzl@41973 ` 249` ``` "x \ -\ \ x = -\" ``` hoelzl@41973 ` 250` ``` by (auto simp add: less_eq_extreal_def) ``` hoelzl@41973 ` 251` hoelzl@41973 ` 252` ```lemma extreal_less[simp]: ``` hoelzl@41973 ` 253` ``` "extreal r < 0 \ (r < 0)" ``` hoelzl@41973 ` 254` ``` "0 < extreal r \ (0 < r)" ``` hoelzl@41973 ` 255` ``` "0 < \" ``` hoelzl@41973 ` 256` ``` "-\ < 0" ``` hoelzl@41973 ` 257` ``` by (simp_all add: zero_extreal_def) ``` hoelzl@41973 ` 258` hoelzl@41973 ` 259` ```lemma extreal_less_eq[simp]: ``` hoelzl@41973 ` 260` ``` "x \ \" ``` hoelzl@41973 ` 261` ``` "-\ \ x" ``` hoelzl@41973 ` 262` ``` "extreal r \ extreal p \ r \ p" ``` hoelzl@41973 ` 263` ``` "extreal r \ 0 \ r \ 0" ``` hoelzl@41973 ` 264` ``` "0 \ extreal r \ 0 \ r" ``` hoelzl@41973 ` 265` ``` by (auto simp add: less_eq_extreal_def zero_extreal_def) ``` hoelzl@41973 ` 266` hoelzl@41973 ` 267` ```lemma extreal_infty_less_eq2: ``` hoelzl@41973 ` 268` ``` "a \ b \ a = \ \ b = \" ``` hoelzl@41973 ` 269` ``` "a \ b \ b = -\ \ a = -\" ``` hoelzl@41973 ` 270` ``` by simp_all ``` hoelzl@41973 ` 271` hoelzl@41973 ` 272` ```instance ``` hoelzl@41973 ` 273` ```proof ``` hoelzl@41973 ` 274` ``` fix x :: extreal show "x \ x" ``` hoelzl@41973 ` 275` ``` by (cases x) simp_all ``` hoelzl@41973 ` 276` ``` fix y :: extreal show "x < y \ x \ y \ \ y \ x" ``` hoelzl@41973 ` 277` ``` by (cases rule: extreal2_cases[of x y]) auto ``` hoelzl@41973 ` 278` ``` show "x \ y \ y \ x " ``` hoelzl@41973 ` 279` ``` by (cases rule: extreal2_cases[of x y]) auto ``` hoelzl@41973 ` 280` ``` { assume "x \ y" "y \ x" then show "x = y" ``` hoelzl@41973 ` 281` ``` by (cases rule: extreal2_cases[of x y]) auto } ``` hoelzl@41973 ` 282` ``` { fix z assume "x \ y" "y \ z" then show "x \ z" ``` hoelzl@41973 ` 283` ``` by (cases rule: extreal3_cases[of x y z]) auto } ``` hoelzl@41973 ` 284` ```qed ``` hoelzl@41973 ` 285` ```end ``` hoelzl@41973 ` 286` hoelzl@41978 ` 287` ```instance extreal :: ordered_ab_semigroup_add ``` hoelzl@41978 ` 288` ```proof ``` hoelzl@41978 ` 289` ``` fix a b c :: extreal assume "a \ b" then show "c + a \ c + b" ``` hoelzl@41978 ` 290` ``` by (cases rule: extreal3_cases[of a b c]) auto ``` hoelzl@41978 ` 291` ```qed ``` hoelzl@41978 ` 292` hoelzl@41973 ` 293` ```lemma extreal_MInfty_lessI[intro, simp]: ``` hoelzl@41973 ` 294` ``` "a \ -\ \ -\ < a" ``` hoelzl@41973 ` 295` ``` by (cases a) auto ``` hoelzl@41973 ` 296` hoelzl@41973 ` 297` ```lemma extreal_less_PInfty[intro, simp]: ``` hoelzl@41973 ` 298` ``` "a \ \ \ a < \" ``` hoelzl@41973 ` 299` ``` by (cases a) auto ``` hoelzl@41973 ` 300` hoelzl@41973 ` 301` ```lemma extreal_less_extreal_Ex: ``` hoelzl@41973 ` 302` ``` fixes a b :: extreal ``` hoelzl@41973 ` 303` ``` shows "x < extreal r \ x = -\ \ (\p. p < r \ x = extreal p)" ``` hoelzl@41973 ` 304` ``` by (cases x) auto ``` hoelzl@41973 ` 305` hoelzl@41979 ` 306` ```lemma less_PInf_Ex_of_nat: "x \ \ \ (\n::nat. x < extreal (real n))" ``` hoelzl@41979 ` 307` ```proof (cases x) ``` hoelzl@41979 ` 308` ``` case (real r) then show ?thesis ``` hoelzl@41979 ` 309` ``` using real_arch_lt[of r] by simp ``` hoelzl@41979 ` 310` ```qed simp_all ``` hoelzl@41979 ` 311` hoelzl@41973 ` 312` ```lemma extreal_add_mono: ``` hoelzl@41973 ` 313` ``` fixes a b c d :: extreal assumes "a \ b" "c \ d" shows "a + c \ b + d" ``` hoelzl@41973 ` 314` ``` using assms ``` hoelzl@41973 ` 315` ``` apply (cases a) ``` hoelzl@41973 ` 316` ``` apply (cases rule: extreal3_cases[of b c d], auto) ``` hoelzl@41973 ` 317` ``` apply (cases rule: extreal3_cases[of b c d], auto) ``` hoelzl@41973 ` 318` ``` done ``` hoelzl@41973 ` 319` hoelzl@41973 ` 320` ```lemma extreal_minus_le_minus[simp]: ``` hoelzl@41973 ` 321` ``` fixes a b :: extreal shows "- a \ - b \ b \ a" ``` hoelzl@41973 ` 322` ``` by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@41973 ` 323` hoelzl@41973 ` 324` ```lemma extreal_minus_less_minus[simp]: ``` hoelzl@41973 ` 325` ``` fixes a b :: extreal shows "- a < - b \ b < a" ``` hoelzl@41973 ` 326` ``` by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@41973 ` 327` hoelzl@41973 ` 328` ```lemma extreal_le_real_iff: ``` hoelzl@41976 ` 329` ``` "x \ real y \ ((\y\ \ \ \ extreal x \ y) \ (\y\ = \ \ x \ 0))" ``` hoelzl@41973 ` 330` ``` by (cases y) auto ``` hoelzl@41973 ` 331` hoelzl@41973 ` 332` ```lemma real_le_extreal_iff: ``` hoelzl@41976 ` 333` ``` "real y \ x \ ((\y\ \ \ \ y \ extreal x) \ (\y\ = \ \ 0 \ x))" ``` hoelzl@41973 ` 334` ``` by (cases y) auto ``` hoelzl@41973 ` 335` hoelzl@41973 ` 336` ```lemma extreal_less_real_iff: ``` hoelzl@41976 ` 337` ``` "x < real y \ ((\y\ \ \ \ extreal x < y) \ (\y\ = \ \ x < 0))" ``` hoelzl@41973 ` 338` ``` by (cases y) auto ``` hoelzl@41973 ` 339` hoelzl@41973 ` 340` ```lemma real_less_extreal_iff: ``` hoelzl@41976 ` 341` ``` "real y < x \ ((\y\ \ \ \ y < extreal x) \ (\y\ = \ \ 0 < x))" ``` hoelzl@41973 ` 342` ``` by (cases y) auto ``` hoelzl@41973 ` 343` hoelzl@41979 ` 344` ```lemma real_of_extreal_positive_mono: ``` hoelzl@41979 ` 345` ``` assumes "x \ \" "y \ \" "0 \ x" "x \ y" ``` hoelzl@41979 ` 346` ``` shows "real x \ real y" ``` hoelzl@41979 ` 347` ``` using assms by (cases rule: extreal2_cases[of x y]) auto ``` hoelzl@41979 ` 348` hoelzl@41979 ` 349` ```lemma real_of_extreal_pos: ``` hoelzl@41979 ` 350` ``` fixes x :: extreal shows "0 \ x \ 0 \ real x" by (cases x) auto ``` hoelzl@41979 ` 351` hoelzl@41973 ` 352` ```lemmas real_of_extreal_ord_simps = ``` hoelzl@41973 ` 353` ``` extreal_le_real_iff real_le_extreal_iff extreal_less_real_iff real_less_extreal_iff ``` hoelzl@41973 ` 354` hoelzl@41973 ` 355` ```lemma extreal_dense: ``` hoelzl@41973 ` 356` ``` fixes x y :: extreal assumes "x < y" ``` hoelzl@41973 ` 357` ``` shows "EX z. x < z & z < y" ``` hoelzl@41973 ` 358` ```proof - ``` hoelzl@41973 ` 359` ```{ assume a: "x = (-\)" ``` hoelzl@41973 ` 360` ``` { assume "y = \" hence ?thesis using a by (auto intro!: exI[of _ "0"]) } ``` hoelzl@41973 ` 361` ``` moreover ``` hoelzl@41973 ` 362` ``` { assume "y ~= \" ``` hoelzl@41973 ` 363` ``` with `x < y` obtain r where r: "y = extreal r" by (cases y) auto ``` hoelzl@41973 ` 364` ``` hence ?thesis using `x < y` a by (auto intro!: exI[of _ "extreal (r - 1)"]) ``` hoelzl@41973 ` 365` ``` } ultimately have ?thesis by auto ``` hoelzl@41973 ` 366` ```} ``` hoelzl@41973 ` 367` ```moreover ``` hoelzl@41973 ` 368` ```{ assume "x ~= (-\)" ``` hoelzl@41973 ` 369` ``` with `x < y` obtain p where p: "x = extreal p" by (cases x) auto ``` hoelzl@41973 ` 370` ``` { assume "y = \" hence ?thesis using `x < y` p ``` hoelzl@41973 ` 371` ``` by (auto intro!: exI[of _ "extreal (p + 1)"]) } ``` hoelzl@41973 ` 372` ``` moreover ``` hoelzl@41973 ` 373` ``` { assume "y ~= \" ``` hoelzl@41973 ` 374` ``` with `x < y` obtain r where r: "y = extreal r" by (cases y) auto ``` hoelzl@41973 ` 375` ``` with p `x < y` have "p < r" by auto ``` hoelzl@41973 ` 376` ``` with dense obtain z where "p < z" "z < r" by auto ``` hoelzl@41973 ` 377` ``` hence ?thesis using r p by (auto intro!: exI[of _ "extreal z"]) ``` hoelzl@41973 ` 378` ``` } ultimately have ?thesis by auto ``` hoelzl@41973 ` 379` ```} ultimately show ?thesis by auto ``` hoelzl@41973 ` 380` ```qed ``` hoelzl@41973 ` 381` hoelzl@41973 ` 382` ```lemma extreal_dense2: ``` hoelzl@41973 ` 383` ``` fixes x y :: extreal assumes "x < y" ``` hoelzl@41973 ` 384` ``` shows "EX z. x < extreal z & extreal z < y" ``` hoelzl@41973 ` 385` ``` by (metis extreal_dense[OF `x < y`] extreal_cases less_extreal.simps(2,3)) ``` hoelzl@41973 ` 386` hoelzl@41979 ` 387` ```lemma extreal_add_strict_mono: ``` hoelzl@41979 ` 388` ``` fixes a b c d :: extreal ``` hoelzl@41979 ` 389` ``` assumes "a = b" "0 \ a" "a \ \" "c < d" ``` hoelzl@41979 ` 390` ``` shows "a + c < b + d" ``` hoelzl@41979 ` 391` ``` using assms by (cases rule: extreal3_cases[case_product extreal_cases, of a b c d]) auto ``` hoelzl@41979 ` 392` hoelzl@41979 ` 393` ```lemma extreal_less_add: "\a\ \ \ \ c < b \ a + c < a + b" ``` hoelzl@41979 ` 394` ``` by (cases rule: extreal2_cases[of b c]) auto ``` hoelzl@41979 ` 395` hoelzl@41979 ` 396` ```lemma extreal_uminus_eq_reorder: "- a = b \ a = (-b::extreal)" by auto ``` hoelzl@41979 ` 397` hoelzl@41979 ` 398` ```lemma extreal_uminus_less_reorder: "- a < b \ -b < (a::extreal)" ``` hoelzl@41979 ` 399` ``` by (subst (3) extreal_uminus_uminus[symmetric]) (simp only: extreal_minus_less_minus) ``` hoelzl@41979 ` 400` hoelzl@41979 ` 401` ```lemma extreal_uminus_le_reorder: "- a \ b \ -b \ (a::extreal)" ``` hoelzl@41979 ` 402` ``` by (subst (3) extreal_uminus_uminus[symmetric]) (simp only: extreal_minus_le_minus) ``` hoelzl@41979 ` 403` hoelzl@41979 ` 404` ```lemmas extreal_uminus_reorder = ``` hoelzl@41979 ` 405` ``` extreal_uminus_eq_reorder extreal_uminus_less_reorder extreal_uminus_le_reorder ``` hoelzl@41979 ` 406` hoelzl@41979 ` 407` ```lemma extreal_bot: ``` hoelzl@41979 ` 408` ``` fixes x :: extreal assumes "\B. x \ extreal B" shows "x = - \" ``` hoelzl@41979 ` 409` ```proof (cases x) ``` hoelzl@41979 ` 410` ``` case (real r) with assms[of "r - 1"] show ?thesis by auto ``` hoelzl@41979 ` 411` ```next case PInf with assms[of 0] show ?thesis by auto ``` hoelzl@41979 ` 412` ```next case MInf then show ?thesis by simp ``` hoelzl@41979 ` 413` ```qed ``` hoelzl@41979 ` 414` hoelzl@41979 ` 415` ```lemma extreal_top: ``` hoelzl@41979 ` 416` ``` fixes x :: extreal assumes "\B. x \ extreal B" shows "x = \" ``` hoelzl@41979 ` 417` ```proof (cases x) ``` hoelzl@41979 ` 418` ``` case (real r) with assms[of "r + 1"] show ?thesis by auto ``` hoelzl@41979 ` 419` ```next case MInf with assms[of 0] show ?thesis by auto ``` hoelzl@41979 ` 420` ```next case PInf then show ?thesis by simp ``` hoelzl@41979 ` 421` ```qed ``` hoelzl@41979 ` 422` hoelzl@41979 ` 423` ```lemma ``` hoelzl@41979 ` 424` ``` shows extreal_max[simp]: "extreal (max x y) = max (extreal x) (extreal y)" ``` hoelzl@41979 ` 425` ``` and extreal_min[simp]: "extreal (min x y) = min (extreal x) (extreal y)" ``` hoelzl@41979 ` 426` ``` by (simp_all add: min_def max_def) ``` hoelzl@41979 ` 427` hoelzl@41979 ` 428` ```lemma extreal_max_0: "max 0 (extreal r) = extreal (max 0 r)" ``` hoelzl@41979 ` 429` ``` by (auto simp: zero_extreal_def) ``` hoelzl@41979 ` 430` hoelzl@41978 ` 431` ```lemma ``` hoelzl@41978 ` 432` ``` fixes f :: "nat \ extreal" ``` hoelzl@41978 ` 433` ``` shows incseq_uminus[simp]: "incseq (\x. - f x) \ decseq f" ``` hoelzl@41978 ` 434` ``` and decseq_uminus[simp]: "decseq (\x. - f x) \ incseq f" ``` hoelzl@41978 ` 435` ``` unfolding decseq_def incseq_def by auto ``` hoelzl@41978 ` 436` hoelzl@41978 ` 437` ```lemma extreal_add_nonneg_nonneg: ``` hoelzl@41978 ` 438` ``` fixes a b :: extreal shows "0 \ a \ 0 \ b \ 0 \ a + b" ``` hoelzl@41978 ` 439` ``` using add_mono[of 0 a 0 b] by simp ``` hoelzl@41978 ` 440` hoelzl@41978 ` 441` ```lemma image_eqD: "f ` A = B \ (\x\A. f x \ B)" ``` hoelzl@41978 ` 442` ``` by auto ``` hoelzl@41978 ` 443` hoelzl@41978 ` 444` ```lemma incseq_setsumI: ``` hoelzl@41979 ` 445` ``` fixes f :: "nat \ 'a::{comm_monoid_add, ordered_ab_semigroup_add}" ``` hoelzl@41978 ` 446` ``` assumes "\i. 0 \ f i" ``` hoelzl@41978 ` 447` ``` shows "incseq (\i. setsum f {..< i})" ``` hoelzl@41978 ` 448` ```proof (intro incseq_SucI) ``` hoelzl@41978 ` 449` ``` fix n have "setsum f {..< n} + 0 \ setsum f {.. setsum f {..< Suc n}" ``` hoelzl@41978 ` 452` ``` by auto ``` hoelzl@41978 ` 453` ```qed ``` hoelzl@41978 ` 454` hoelzl@41979 ` 455` ```lemma incseq_setsumI2: ``` hoelzl@41979 ` 456` ``` fixes f :: "'i \ nat \ 'a::{comm_monoid_add, ordered_ab_semigroup_add}" ``` hoelzl@41979 ` 457` ``` assumes "\n. n \ A \ incseq (f n)" ``` hoelzl@41979 ` 458` ``` shows "incseq (\i. \n\A. f n i)" ``` hoelzl@41979 ` 459` ``` using assms unfolding incseq_def by (auto intro: setsum_mono) ``` hoelzl@41979 ` 460` hoelzl@41973 ` 461` ```subsubsection "Multiplication" ``` hoelzl@41973 ` 462` hoelzl@41976 ` 463` ```instantiation extreal :: "{comm_monoid_mult, sgn}" ``` hoelzl@41973 ` 464` ```begin ``` hoelzl@41973 ` 465` hoelzl@41973 ` 466` ```definition "1 = extreal 1" ``` hoelzl@41973 ` 467` hoelzl@41976 ` 468` ```function sgn_extreal where ``` hoelzl@41976 ` 469` ``` "sgn (extreal r) = extreal (sgn r)" ``` hoelzl@41976 ` 470` ```| "sgn \ = 1" ``` hoelzl@41976 ` 471` ```| "sgn (-\) = -1" ``` hoelzl@41976 ` 472` ```by (auto intro: extreal_cases) ``` hoelzl@41976 ` 473` ```termination proof qed (rule wf_empty) ``` hoelzl@41976 ` 474` hoelzl@41973 ` 475` ```function times_extreal where ``` hoelzl@41973 ` 476` ```"extreal r * extreal p = extreal (r * p)" | ``` hoelzl@41973 ` 477` ```"extreal r * \ = (if r = 0 then 0 else if r > 0 then \ else -\)" | ``` hoelzl@41973 ` 478` ```"\ * extreal r = (if r = 0 then 0 else if r > 0 then \ else -\)" | ``` hoelzl@41973 ` 479` ```"extreal r * -\ = (if r = 0 then 0 else if r > 0 then -\ else \)" | ``` hoelzl@41973 ` 480` ```"-\ * extreal r = (if r = 0 then 0 else if r > 0 then -\ else \)" | ``` hoelzl@41973 ` 481` ```"\ * \ = \" | ``` hoelzl@41973 ` 482` ```"-\ * \ = -\" | ``` hoelzl@41973 ` 483` ```"\ * -\ = -\" | ``` hoelzl@41973 ` 484` ```"-\ * -\ = \" ``` hoelzl@41973 ` 485` ```proof - ``` hoelzl@41973 ` 486` ``` case (goal1 P x) ``` hoelzl@41973 ` 487` ``` moreover then obtain a b where "x = (a, b)" by (cases x) auto ``` hoelzl@41973 ` 488` ``` ultimately show P by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@41973 ` 489` ```qed simp_all ``` hoelzl@41973 ` 490` ```termination by (relation "{}") simp ``` hoelzl@41973 ` 491` hoelzl@41973 ` 492` ```instance ``` hoelzl@41973 ` 493` ```proof ``` hoelzl@41973 ` 494` ``` fix a :: extreal show "1 * a = a" ``` hoelzl@41973 ` 495` ``` by (cases a) (simp_all add: one_extreal_def) ``` hoelzl@41973 ` 496` ``` fix b :: extreal show "a * b = b * a" ``` hoelzl@41973 ` 497` ``` by (cases rule: extreal2_cases[of a b]) simp_all ``` hoelzl@41973 ` 498` ``` fix c :: extreal show "a * b * c = a * (b * c)" ``` hoelzl@41973 ` 499` ``` by (cases rule: extreal3_cases[of a b c]) ``` hoelzl@41973 ` 500` ``` (simp_all add: zero_extreal_def zero_less_mult_iff) ``` hoelzl@41973 ` 501` ```qed ``` hoelzl@41973 ` 502` ```end ``` hoelzl@41973 ` 503` hoelzl@41976 ` 504` ```lemma abs_extreal_one[simp]: "\1\ = (1::extreal)" ``` hoelzl@41976 ` 505` ``` unfolding one_extreal_def by simp ``` hoelzl@41976 ` 506` hoelzl@41973 ` 507` ```lemma extreal_mult_zero[simp]: ``` hoelzl@41973 ` 508` ``` fixes a :: extreal shows "a * 0 = 0" ``` hoelzl@41973 ` 509` ``` by (cases a) (simp_all add: zero_extreal_def) ``` hoelzl@41973 ` 510` hoelzl@41973 ` 511` ```lemma extreal_zero_mult[simp]: ``` hoelzl@41973 ` 512` ``` fixes a :: extreal shows "0 * a = 0" ``` hoelzl@41973 ` 513` ``` by (cases a) (simp_all add: zero_extreal_def) ``` hoelzl@41973 ` 514` hoelzl@41973 ` 515` ```lemma extreal_m1_less_0[simp]: ``` hoelzl@41973 ` 516` ``` "-(1::extreal) < 0" ``` hoelzl@41973 ` 517` ``` by (simp add: zero_extreal_def one_extreal_def) ``` hoelzl@41973 ` 518` hoelzl@41973 ` 519` ```lemma extreal_zero_m1[simp]: ``` hoelzl@41973 ` 520` ``` "1 \ (0::extreal)" ``` hoelzl@41973 ` 521` ``` by (simp add: zero_extreal_def one_extreal_def) ``` hoelzl@41973 ` 522` hoelzl@41973 ` 523` ```lemma extreal_times_0[simp]: ``` hoelzl@41973 ` 524` ``` fixes x :: extreal shows "0 * x = 0" ``` hoelzl@41973 ` 525` ``` by (cases x) (auto simp: zero_extreal_def) ``` hoelzl@41973 ` 526` hoelzl@41973 ` 527` ```lemma extreal_times[simp]: ``` hoelzl@41973 ` 528` ``` "1 \ \" "\ \ 1" ``` hoelzl@41973 ` 529` ``` "1 \ -\" "-\ \ 1" ``` hoelzl@41973 ` 530` ``` by (auto simp add: times_extreal_def one_extreal_def) ``` hoelzl@41973 ` 531` hoelzl@41973 ` 532` ```lemma extreal_plus_1[simp]: ``` hoelzl@41973 ` 533` ``` "1 + extreal r = extreal (r + 1)" "extreal r + 1 = extreal (r + 1)" ``` hoelzl@41973 ` 534` ``` "1 + -\ = -\" "-\ + 1 = -\" ``` hoelzl@41973 ` 535` ``` unfolding one_extreal_def by auto ``` hoelzl@41973 ` 536` hoelzl@41973 ` 537` ```lemma extreal_zero_times[simp]: ``` hoelzl@41973 ` 538` ``` fixes a b :: extreal shows "a * b = 0 \ a = 0 \ b = 0" ``` hoelzl@41973 ` 539` ``` by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@41973 ` 540` hoelzl@41973 ` 541` ```lemma extreal_mult_eq_PInfty[simp]: ``` hoelzl@41973 ` 542` ``` shows "a * b = \ \ ``` hoelzl@41973 ` 543` ``` (a = \ \ b > 0) \ (a > 0 \ b = \) \ (a = -\ \ b < 0) \ (a < 0 \ b = -\)" ``` hoelzl@41973 ` 544` ``` by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@41973 ` 545` hoelzl@41973 ` 546` ```lemma extreal_mult_eq_MInfty[simp]: ``` hoelzl@41973 ` 547` ``` shows "a * b = -\ \ ``` hoelzl@41973 ` 548` ``` (a = \ \ b < 0) \ (a < 0 \ b = \) \ (a = -\ \ b > 0) \ (a > 0 \ b = -\)" ``` hoelzl@41973 ` 549` ``` by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@41973 ` 550` hoelzl@41973 ` 551` ```lemma extreal_0_less_1[simp]: "0 < (1::extreal)" ``` hoelzl@41973 ` 552` ``` by (simp_all add: zero_extreal_def one_extreal_def) ``` hoelzl@41973 ` 553` hoelzl@41973 ` 554` ```lemma extreal_zero_one[simp]: "0 \ (1::extreal)" ``` hoelzl@41973 ` 555` ``` by (simp_all add: zero_extreal_def one_extreal_def) ``` hoelzl@41973 ` 556` hoelzl@41973 ` 557` ```lemma extreal_mult_minus_left[simp]: ``` hoelzl@41973 ` 558` ``` fixes a b :: extreal shows "-a * b = - (a * b)" ``` hoelzl@41973 ` 559` ``` by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@41973 ` 560` hoelzl@41973 ` 561` ```lemma extreal_mult_minus_right[simp]: ``` hoelzl@41973 ` 562` ``` fixes a b :: extreal shows "a * -b = - (a * b)" ``` hoelzl@41973 ` 563` ``` by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@41973 ` 564` hoelzl@41973 ` 565` ```lemma extreal_mult_infty[simp]: ``` hoelzl@41973 ` 566` ``` "a * \ = (if a = 0 then 0 else if 0 < a then \ else - \)" ``` hoelzl@41973 ` 567` ``` by (cases a) auto ``` hoelzl@41973 ` 568` hoelzl@41973 ` 569` ```lemma extreal_infty_mult[simp]: ``` hoelzl@41973 ` 570` ``` "\ * a = (if a = 0 then 0 else if 0 < a then \ else - \)" ``` hoelzl@41973 ` 571` ``` by (cases a) auto ``` hoelzl@41973 ` 572` hoelzl@41973 ` 573` ```lemma extreal_mult_strict_right_mono: ``` hoelzl@41973 ` 574` ``` assumes "a < b" and "0 < c" "c < \" ``` hoelzl@41973 ` 575` ``` shows "a * c < b * c" ``` hoelzl@41973 ` 576` ``` using assms ``` hoelzl@41973 ` 577` ``` by (cases rule: extreal3_cases[of a b c]) ``` hoelzl@41973 ` 578` ``` (auto simp: zero_le_mult_iff extreal_less_PInfty) ``` hoelzl@41973 ` 579` hoelzl@41973 ` 580` ```lemma extreal_mult_strict_left_mono: ``` hoelzl@41973 ` 581` ``` "\ a < b ; 0 < c ; c < \\ \ c * a < c * b" ``` hoelzl@41973 ` 582` ``` using extreal_mult_strict_right_mono by (simp add: mult_commute[of c]) ``` hoelzl@41973 ` 583` hoelzl@41973 ` 584` ```lemma extreal_mult_right_mono: ``` hoelzl@41973 ` 585` ``` fixes a b c :: extreal shows "\a \ b; 0 \ c\ \ a*c \ b*c" ``` hoelzl@41973 ` 586` ``` using assms ``` hoelzl@41973 ` 587` ``` apply (cases "c = 0") apply simp ``` hoelzl@41973 ` 588` ``` by (cases rule: extreal3_cases[of a b c]) ``` hoelzl@41973 ` 589` ``` (auto simp: zero_le_mult_iff extreal_less_PInfty) ``` hoelzl@41973 ` 590` hoelzl@41973 ` 591` ```lemma extreal_mult_left_mono: ``` hoelzl@41973 ` 592` ``` fixes a b c :: extreal shows "\a \ b; 0 \ c\ \ c * a \ c * b" ``` hoelzl@41973 ` 593` ``` using extreal_mult_right_mono by (simp add: mult_commute[of c]) ``` hoelzl@41973 ` 594` hoelzl@41978 ` 595` ```lemma zero_less_one_extreal[simp]: "0 \ (1::extreal)" ``` hoelzl@41978 ` 596` ``` by (simp add: one_extreal_def zero_extreal_def) ``` hoelzl@41978 ` 597` hoelzl@41979 ` 598` ```lemma extreal_0_le_mult[simp]: "0 \ a \ 0 \ b \ 0 \ a * (b :: extreal)" ``` hoelzl@41979 ` 599` ``` by (cases rule: extreal2_cases[of a b]) (auto simp: mult_nonneg_nonneg) ``` hoelzl@41979 ` 600` hoelzl@41979 ` 601` ```lemma extreal_right_distrib: ``` hoelzl@41979 ` 602` ``` fixes r a b :: extreal shows "0 \ a \ 0 \ b \ r * (a + b) = r * a + r * b" ``` hoelzl@41979 ` 603` ``` by (cases rule: extreal3_cases[of r a b]) (simp_all add: field_simps) ``` hoelzl@41979 ` 604` hoelzl@41979 ` 605` ```lemma extreal_left_distrib: ``` hoelzl@41979 ` 606` ``` fixes r a b :: extreal shows "0 \ a \ 0 \ b \ (a + b) * r = a * r + b * r" ``` hoelzl@41979 ` 607` ``` by (cases rule: extreal3_cases[of r a b]) (simp_all add: field_simps) ``` hoelzl@41979 ` 608` hoelzl@41979 ` 609` ```lemma extreal_mult_le_0_iff: ``` hoelzl@41979 ` 610` ``` fixes a b :: extreal ``` hoelzl@41979 ` 611` ``` shows "a * b \ 0 \ (0 \ a \ b \ 0) \ (a \ 0 \ 0 \ b)" ``` hoelzl@41979 ` 612` ``` by (cases rule: extreal2_cases[of a b]) (simp_all add: mult_le_0_iff) ``` hoelzl@41979 ` 613` hoelzl@41979 ` 614` ```lemma extreal_zero_le_0_iff: ``` hoelzl@41979 ` 615` ``` fixes a b :: extreal ``` hoelzl@41979 ` 616` ``` shows "0 \ a * b \ (0 \ a \ 0 \ b) \ (a \ 0 \ b \ 0)" ``` hoelzl@41979 ` 617` ``` by (cases rule: extreal2_cases[of a b]) (simp_all add: zero_le_mult_iff) ``` hoelzl@41979 ` 618` hoelzl@41979 ` 619` ```lemma extreal_mult_less_0_iff: ``` hoelzl@41979 ` 620` ``` fixes a b :: extreal ``` hoelzl@41979 ` 621` ``` shows "a * b < 0 \ (0 < a \ b < 0) \ (a < 0 \ 0 < b)" ``` hoelzl@41979 ` 622` ``` by (cases rule: extreal2_cases[of a b]) (simp_all add: mult_less_0_iff) ``` hoelzl@41979 ` 623` hoelzl@41979 ` 624` ```lemma extreal_zero_less_0_iff: ``` hoelzl@41979 ` 625` ``` fixes a b :: extreal ``` hoelzl@41979 ` 626` ``` shows "0 < a * b \ (0 < a \ 0 < b) \ (a < 0 \ b < 0)" ``` hoelzl@41979 ` 627` ``` by (cases rule: extreal2_cases[of a b]) (simp_all add: zero_less_mult_iff) ``` hoelzl@41979 ` 628` hoelzl@41979 ` 629` ```lemma extreal_distrib: ``` hoelzl@41978 ` 630` ``` fixes a b c :: extreal ``` hoelzl@41979 ` 631` ``` assumes "a \ \ \ b \ -\" "a \ -\ \ b \ \" "\c\ \ \" ``` hoelzl@41979 ` 632` ``` shows "(a + b) * c = a * c + b * c" ``` hoelzl@41979 ` 633` ``` using assms ``` hoelzl@41979 ` 634` ``` by (cases rule: extreal3_cases[of a b c]) (simp_all add: field_simps) ``` hoelzl@41979 ` 635` hoelzl@41979 ` 636` ```lemma extreal_le_epsilon: ``` hoelzl@41979 ` 637` ``` fixes x y :: extreal ``` hoelzl@41979 ` 638` ``` assumes "ALL e. 0 < e --> x <= y + e" ``` hoelzl@41979 ` 639` ``` shows "x <= y" ``` hoelzl@41979 ` 640` ```proof- ``` hoelzl@41979 ` 641` ```{ assume a: "EX r. y = extreal r" ``` hoelzl@41979 ` 642` ``` from this obtain r where r_def: "y = extreal r" by auto ``` hoelzl@41979 ` 643` ``` { assume "x=(-\)" hence ?thesis by auto } ``` hoelzl@41979 ` 644` ``` moreover ``` hoelzl@41979 ` 645` ``` { assume "~(x=(-\))" ``` hoelzl@41979 ` 646` ``` from this obtain p where p_def: "x = extreal p" ``` hoelzl@41979 ` 647` ``` using a assms[rule_format, of 1] by (cases x) auto ``` hoelzl@41979 ` 648` ``` { fix e have "0 < e --> p <= r + e" ``` hoelzl@41979 ` 649` ``` using assms[rule_format, of "extreal e"] p_def r_def by auto } ``` hoelzl@41979 ` 650` ``` hence "p <= r" apply (subst field_le_epsilon) by auto ``` hoelzl@41979 ` 651` ``` hence ?thesis using r_def p_def by auto ``` hoelzl@41979 ` 652` ``` } ultimately have ?thesis by blast ``` hoelzl@41979 ` 653` ```} ``` hoelzl@41979 ` 654` ```moreover ``` hoelzl@41979 ` 655` ```{ assume "y=(-\) | y=\" hence ?thesis ``` hoelzl@41979 ` 656` ``` using assms[rule_format, of 1] by (cases x) auto ``` hoelzl@41979 ` 657` ```} ultimately show ?thesis by (cases y) auto ``` hoelzl@41979 ` 658` ```qed ``` hoelzl@41979 ` 659` hoelzl@41979 ` 660` hoelzl@41979 ` 661` ```lemma extreal_le_epsilon2: ``` hoelzl@41979 ` 662` ``` fixes x y :: extreal ``` hoelzl@41979 ` 663` ``` assumes "ALL e. 0 < e --> x <= y + extreal e" ``` hoelzl@41979 ` 664` ``` shows "x <= y" ``` hoelzl@41979 ` 665` ```proof- ``` hoelzl@41979 ` 666` ```{ fix e :: extreal assume "e>0" ``` hoelzl@41979 ` 667` ``` { assume "e=\" hence "x<=y+e" by auto } ``` hoelzl@41979 ` 668` ``` moreover ``` hoelzl@41979 ` 669` ``` { assume "e~=\" ``` hoelzl@41979 ` 670` ``` from this obtain r where "e = extreal r" using `e>0` apply (cases e) by auto ``` hoelzl@41979 ` 671` ``` hence "x<=y+e" using assms[rule_format, of r] `e>0` by auto ``` hoelzl@41979 ` 672` ``` } ultimately have "x<=y+e" by blast ``` hoelzl@41979 ` 673` ```} from this show ?thesis using extreal_le_epsilon by auto ``` hoelzl@41979 ` 674` ```qed ``` hoelzl@41979 ` 675` hoelzl@41979 ` 676` ```lemma extreal_le_real: ``` hoelzl@41979 ` 677` ``` fixes x y :: extreal ``` hoelzl@41979 ` 678` ``` assumes "ALL z. x <= extreal z --> y <= extreal z" ``` hoelzl@41979 ` 679` ``` shows "y <= x" ``` hoelzl@41979 ` 680` ```by (metis assms extreal.exhaust extreal_bot extreal_less_eq(1) ``` hoelzl@41979 ` 681` ``` extreal_less_eq(2) order_refl uminus_extreal.simps(2)) ``` hoelzl@41979 ` 682` hoelzl@41979 ` 683` ```lemma extreal_le_extreal: ``` hoelzl@41979 ` 684` ``` fixes x y :: extreal ``` hoelzl@41979 ` 685` ``` assumes "\B. B < x \ B <= y" ``` hoelzl@41979 ` 686` ``` shows "x <= y" ``` hoelzl@41979 ` 687` ```by (metis assms extreal_dense leD linorder_le_less_linear) ``` hoelzl@41979 ` 688` hoelzl@41979 ` 689` ```lemma extreal_ge_extreal: ``` hoelzl@41979 ` 690` ``` fixes x y :: extreal ``` hoelzl@41979 ` 691` ``` assumes "ALL B. B>x --> B >= y" ``` hoelzl@41979 ` 692` ``` shows "x >= y" ``` hoelzl@41979 ` 693` ```by (metis assms extreal_dense leD linorder_le_less_linear) ``` hoelzl@41978 ` 694` hoelzl@41978 ` 695` ```subsubsection {* Power *} ``` hoelzl@41978 ` 696` hoelzl@41978 ` 697` ```instantiation extreal :: power ``` hoelzl@41978 ` 698` ```begin ``` hoelzl@41978 ` 699` ```primrec power_extreal where ``` hoelzl@41978 ` 700` ``` "power_extreal x 0 = 1" | ``` hoelzl@41978 ` 701` ``` "power_extreal x (Suc n) = x * x ^ n" ``` hoelzl@41978 ` 702` ```instance .. ``` hoelzl@41978 ` 703` ```end ``` hoelzl@41978 ` 704` hoelzl@41978 ` 705` ```lemma extreal_power[simp]: "(extreal x) ^ n = extreal (x^n)" ``` hoelzl@41978 ` 706` ``` by (induct n) (auto simp: one_extreal_def) ``` hoelzl@41978 ` 707` hoelzl@41978 ` 708` ```lemma extreal_power_PInf[simp]: "\ ^ n = (if n = 0 then 1 else \)" ``` hoelzl@41978 ` 709` ``` by (induct n) (auto simp: one_extreal_def) ``` hoelzl@41978 ` 710` hoelzl@41978 ` 711` ```lemma extreal_power_uminus[simp]: ``` hoelzl@41978 ` 712` ``` fixes x :: extreal ``` hoelzl@41978 ` 713` ``` shows "(- x) ^ n = (if even n then x ^ n else - (x^n))" ``` hoelzl@41978 ` 714` ``` by (induct n) (auto simp: one_extreal_def) ``` hoelzl@41978 ` 715` hoelzl@41979 ` 716` ```lemma extreal_power_number_of[simp]: ``` hoelzl@41979 ` 717` ``` "(number_of num :: extreal) ^ n = extreal (number_of num ^ n)" ``` hoelzl@41979 ` 718` ``` by (induct n) (auto simp: one_extreal_def) ``` hoelzl@41979 ` 719` hoelzl@41979 ` 720` ```lemma zero_le_power_extreal[simp]: ``` hoelzl@41979 ` 721` ``` fixes a :: extreal assumes "0 \ a" ``` hoelzl@41979 ` 722` ``` shows "0 \ a ^ n" ``` hoelzl@41979 ` 723` ``` using assms by (induct n) (auto simp: extreal_zero_le_0_iff) ``` hoelzl@41979 ` 724` hoelzl@41973 ` 725` ```subsubsection {* Subtraction *} ``` hoelzl@41973 ` 726` hoelzl@41973 ` 727` ```lemma extreal_minus_minus_image[simp]: ``` hoelzl@41973 ` 728` ``` fixes S :: "extreal set" ``` hoelzl@41973 ` 729` ``` shows "uminus ` uminus ` S = S" ``` hoelzl@41973 ` 730` ``` by (auto simp: image_iff) ``` hoelzl@41973 ` 731` hoelzl@41973 ` 732` ```lemma extreal_uminus_lessThan[simp]: ``` hoelzl@41973 ` 733` ``` fixes a :: extreal shows "uminus ` {.. - extreal r = -\" ``` hoelzl@41973 ` 754` ``` "extreal r - \ = -\" ``` hoelzl@41973 ` 755` ``` "\ - x = \" ``` hoelzl@41973 ` 756` ``` "-\ - \ = -\" ``` hoelzl@41973 ` 757` ``` "x - -y = x + y" ``` hoelzl@41973 ` 758` ``` "x - 0 = x" ``` hoelzl@41973 ` 759` ``` "0 - x = -x" ``` hoelzl@41973 ` 760` ``` by (simp_all add: minus_extreal_def) ``` hoelzl@41973 ` 761` hoelzl@41973 ` 762` ```lemma extreal_x_minus_x[simp]: ``` hoelzl@41976 ` 763` ``` "x - x = (if \x\ = \ then \ else 0)" ``` hoelzl@41973 ` 764` ``` by (cases x) simp_all ``` hoelzl@41973 ` 765` hoelzl@41973 ` 766` ```lemma extreal_eq_minus_iff: ``` hoelzl@41973 ` 767` ``` fixes x y z :: extreal ``` hoelzl@41973 ` 768` ``` shows "x = z - y \ ``` hoelzl@41976 ` 769` ``` (\y\ \ \ \ x + y = z) \ ``` hoelzl@41973 ` 770` ``` (y = -\ \ x = \) \ ``` hoelzl@41973 ` 771` ``` (y = \ \ z = \ \ x = \) \ ``` hoelzl@41973 ` 772` ``` (y = \ \ z \ \ \ x = -\)" ``` hoelzl@41973 ` 773` ``` by (cases rule: extreal3_cases[of x y z]) auto ``` hoelzl@41973 ` 774` hoelzl@41973 ` 775` ```lemma extreal_eq_minus: ``` hoelzl@41973 ` 776` ``` fixes x y z :: extreal ``` hoelzl@41976 ` 777` ``` shows "\y\ \ \ \ x = z - y \ x + y = z" ``` hoelzl@41976 ` 778` ``` by (auto simp: extreal_eq_minus_iff) ``` hoelzl@41973 ` 779` hoelzl@41973 ` 780` ```lemma extreal_less_minus_iff: ``` hoelzl@41973 ` 781` ``` fixes x y z :: extreal ``` hoelzl@41973 ` 782` ``` shows "x < z - y \ ``` hoelzl@41973 ` 783` ``` (y = \ \ z = \ \ x \ \) \ ``` hoelzl@41973 ` 784` ``` (y = -\ \ x \ \) \ ``` hoelzl@41976 ` 785` ``` (\y\ \ \\ x + y < z)" ``` hoelzl@41973 ` 786` ``` by (cases rule: extreal3_cases[of x y z]) auto ``` hoelzl@41973 ` 787` hoelzl@41973 ` 788` ```lemma extreal_less_minus: ``` hoelzl@41973 ` 789` ``` fixes x y z :: extreal ``` hoelzl@41976 ` 790` ``` shows "\y\ \ \ \ x < z - y \ x + y < z" ``` hoelzl@41976 ` 791` ``` by (auto simp: extreal_less_minus_iff) ``` hoelzl@41973 ` 792` hoelzl@41973 ` 793` ```lemma extreal_le_minus_iff: ``` hoelzl@41973 ` 794` ``` fixes x y z :: extreal ``` hoelzl@41973 ` 795` ``` shows "x \ z - y \ ``` hoelzl@41973 ` 796` ``` (y = \ \ z \ \ \ x = -\) \ ``` hoelzl@41976 ` 797` ``` (\y\ \ \ \ x + y \ z)" ``` hoelzl@41973 ` 798` ``` by (cases rule: extreal3_cases[of x y z]) auto ``` hoelzl@41973 ` 799` hoelzl@41973 ` 800` ```lemma extreal_le_minus: ``` hoelzl@41973 ` 801` ``` fixes x y z :: extreal ``` hoelzl@41976 ` 802` ``` shows "\y\ \ \ \ x \ z - y \ x + y \ z" ``` hoelzl@41976 ` 803` ``` by (auto simp: extreal_le_minus_iff) ``` hoelzl@41973 ` 804` hoelzl@41973 ` 805` ```lemma extreal_minus_less_iff: ``` hoelzl@41973 ` 806` ``` fixes x y z :: extreal ``` hoelzl@41973 ` 807` ``` shows "x - y < z \ ``` hoelzl@41973 ` 808` ``` y \ -\ \ (y = \ \ x \ \ \ z \ -\) \ ``` hoelzl@41973 ` 809` ``` (y \ \ \ x < z + y)" ``` hoelzl@41973 ` 810` ``` by (cases rule: extreal3_cases[of x y z]) auto ``` hoelzl@41973 ` 811` hoelzl@41973 ` 812` ```lemma extreal_minus_less: ``` hoelzl@41973 ` 813` ``` fixes x y z :: extreal ``` hoelzl@41976 ` 814` ``` shows "\y\ \ \ \ x - y < z \ x < z + y" ``` hoelzl@41976 ` 815` ``` by (auto simp: extreal_minus_less_iff) ``` hoelzl@41973 ` 816` hoelzl@41973 ` 817` ```lemma extreal_minus_le_iff: ``` hoelzl@41973 ` 818` ``` fixes x y z :: extreal ``` hoelzl@41973 ` 819` ``` shows "x - y \ z \ ``` hoelzl@41973 ` 820` ``` (y = -\ \ z = \) \ ``` hoelzl@41973 ` 821` ``` (y = \ \ x = \ \ z = \) \ ``` hoelzl@41976 ` 822` ``` (\y\ \ \ \ x \ z + y)" ``` hoelzl@41973 ` 823` ``` by (cases rule: extreal3_cases[of x y z]) auto ``` hoelzl@41973 ` 824` hoelzl@41973 ` 825` ```lemma extreal_minus_le: ``` hoelzl@41973 ` 826` ``` fixes x y z :: extreal ``` hoelzl@41976 ` 827` ``` shows "\y\ \ \ \ x - y \ z \ x \ z + y" ``` hoelzl@41976 ` 828` ``` by (auto simp: extreal_minus_le_iff) ``` hoelzl@41973 ` 829` hoelzl@41973 ` 830` ```lemma extreal_minus_eq_minus_iff: ``` hoelzl@41973 ` 831` ``` fixes a b c :: extreal ``` hoelzl@41973 ` 832` ``` shows "a - b = a - c \ ``` hoelzl@41973 ` 833` ``` b = c \ a = \ \ (a = -\ \ b \ -\ \ c \ -\)" ``` hoelzl@41973 ` 834` ``` by (cases rule: extreal3_cases[of a b c]) auto ``` hoelzl@41973 ` 835` hoelzl@41973 ` 836` ```lemma extreal_add_le_add_iff: ``` hoelzl@41973 ` 837` ``` "c + a \ c + b \ ``` hoelzl@41973 ` 838` ``` a \ b \ c = \ \ (c = -\ \ a \ \ \ b \ \)" ``` hoelzl@41973 ` 839` ``` by (cases rule: extreal3_cases[of a b c]) (simp_all add: field_simps) ``` hoelzl@41973 ` 840` hoelzl@41973 ` 841` ```lemma extreal_mult_le_mult_iff: ``` hoelzl@41976 ` 842` ``` "\c\ \ \ \ c * a \ c * b \ (0 < c \ a \ b) \ (c < 0 \ b \ a)" ``` hoelzl@41973 ` 843` ``` by (cases rule: extreal3_cases[of a b c]) (simp_all add: mult_le_cancel_left) ``` hoelzl@41973 ` 844` hoelzl@41979 ` 845` ```lemma extreal_minus_mono: ``` hoelzl@41979 ` 846` ``` fixes A B C D :: extreal assumes "A \ B" "D \ C" ``` hoelzl@41979 ` 847` ``` shows "A - C \ B - D" ``` hoelzl@41979 ` 848` ``` using assms ``` hoelzl@41979 ` 849` ``` by (cases rule: extreal3_cases[case_product extreal_cases, of A B C D]) simp_all ``` hoelzl@41979 ` 850` hoelzl@41979 ` 851` ```lemma real_of_extreal_minus: ``` hoelzl@41979 ` 852` ``` "real (a - b) = (if \a\ = \ \ \b\ = \ then 0 else real a - real b)" ``` hoelzl@41979 ` 853` ``` by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@41979 ` 854` hoelzl@41979 ` 855` ```lemma extreal_diff_positive: ``` hoelzl@41979 ` 856` ``` fixes a b :: extreal shows "a \ b \ 0 \ b - a" ``` hoelzl@41979 ` 857` ``` by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@41979 ` 858` hoelzl@41973 ` 859` ```lemma extreal_between: ``` hoelzl@41973 ` 860` ``` fixes x e :: extreal ``` hoelzl@41976 ` 861` ``` assumes "\x\ \ \" "0 < e" ``` hoelzl@41973 ` 862` ``` shows "x - e < x" "x < x + e" ``` hoelzl@41973 ` 863` ```using assms apply (cases x, cases e) apply auto ``` hoelzl@41973 ` 864` ```using assms by (cases x, cases e) auto ``` hoelzl@41973 ` 865` hoelzl@41973 ` 866` ```subsubsection {* Division *} ``` hoelzl@41973 ` 867` hoelzl@41973 ` 868` ```instantiation extreal :: inverse ``` hoelzl@41973 ` 869` ```begin ``` hoelzl@41973 ` 870` hoelzl@41973 ` 871` ```function inverse_extreal where ``` hoelzl@41973 ` 872` ```"inverse (extreal r) = (if r = 0 then \ else extreal (inverse r))" | ``` hoelzl@41973 ` 873` ```"inverse \ = 0" | ``` hoelzl@41973 ` 874` ```"inverse (-\) = 0" ``` hoelzl@41973 ` 875` ``` by (auto intro: extreal_cases) ``` hoelzl@41973 ` 876` ```termination by (relation "{}") simp ``` hoelzl@41973 ` 877` hoelzl@41973 ` 878` ```definition "x / y = x * inverse (y :: extreal)" ``` hoelzl@41973 ` 879` hoelzl@41973 ` 880` ```instance proof qed ``` hoelzl@41973 ` 881` ```end ``` hoelzl@41973 ` 882` hoelzl@41973 ` 883` ```lemma extreal_inverse[simp]: ``` hoelzl@41973 ` 884` ``` "inverse 0 = \" ``` hoelzl@41973 ` 885` ``` "inverse (1::extreal) = 1" ``` hoelzl@41973 ` 886` ``` by (simp_all add: one_extreal_def zero_extreal_def) ``` hoelzl@41973 ` 887` hoelzl@41973 ` 888` ```lemma extreal_divide[simp]: ``` hoelzl@41973 ` 889` ``` "extreal r / extreal p = (if p = 0 then extreal r * \ else extreal (r / p))" ``` hoelzl@41973 ` 890` ``` unfolding divide_extreal_def by (auto simp: divide_real_def) ``` hoelzl@41973 ` 891` hoelzl@41973 ` 892` ```lemma extreal_divide_same[simp]: ``` hoelzl@41976 ` 893` ``` "x / x = (if \x\ = \ \ x = 0 then 0 else 1)" ``` hoelzl@41973 ` 894` ``` by (cases x) ``` hoelzl@41973 ` 895` ``` (simp_all add: divide_real_def divide_extreal_def one_extreal_def) ``` hoelzl@41973 ` 896` hoelzl@41973 ` 897` ```lemma extreal_inv_inv[simp]: ``` hoelzl@41973 ` 898` ``` "inverse (inverse x) = (if x \ -\ then x else \)" ``` hoelzl@41973 ` 899` ``` by (cases x) auto ``` hoelzl@41973 ` 900` hoelzl@41973 ` 901` ```lemma extreal_inverse_minus[simp]: ``` hoelzl@41973 ` 902` ``` "inverse (- x) = (if x = 0 then \ else -inverse x)" ``` hoelzl@41973 ` 903` ``` by (cases x) simp_all ``` hoelzl@41973 ` 904` hoelzl@41973 ` 905` ```lemma extreal_uminus_divide[simp]: ``` hoelzl@41973 ` 906` ``` fixes x y :: extreal shows "- x / y = - (x / y)" ``` hoelzl@41973 ` 907` ``` unfolding divide_extreal_def by simp ``` hoelzl@41973 ` 908` hoelzl@41973 ` 909` ```lemma extreal_divide_Infty[simp]: ``` hoelzl@41973 ` 910` ``` "x / \ = 0" "x / -\ = 0" ``` hoelzl@41973 ` 911` ``` unfolding divide_extreal_def by simp_all ``` hoelzl@41973 ` 912` hoelzl@41973 ` 913` ```lemma extreal_divide_one[simp]: ``` hoelzl@41973 ` 914` ``` "x / 1 = (x::extreal)" ``` hoelzl@41973 ` 915` ``` unfolding divide_extreal_def by simp ``` hoelzl@41973 ` 916` hoelzl@41973 ` 917` ```lemma extreal_divide_extreal[simp]: ``` hoelzl@41973 ` 918` ``` "\ / extreal r = (if 0 \ r then \ else -\)" ``` hoelzl@41973 ` 919` ``` unfolding divide_extreal_def by simp ``` hoelzl@41973 ` 920` hoelzl@41978 ` 921` ```lemma zero_le_divide_extreal[simp]: ``` hoelzl@41978 ` 922` ``` fixes a :: extreal assumes "0 \ a" "0 \ b" ``` hoelzl@41978 ` 923` ``` shows "0 \ a / b" ``` hoelzl@41978 ` 924` ``` using assms by (cases rule: extreal2_cases[of a b]) (auto simp: zero_le_divide_iff) ``` hoelzl@41978 ` 925` hoelzl@41973 ` 926` ```lemma extreal_le_divide_pos: ``` hoelzl@41973 ` 927` ``` "x > 0 \ x \ \ \ y \ z / x \ x * y \ z" ``` hoelzl@41973 ` 928` ``` by (cases rule: extreal3_cases[of x y z]) (auto simp: field_simps) ``` hoelzl@41973 ` 929` hoelzl@41973 ` 930` ```lemma extreal_divide_le_pos: ``` hoelzl@41973 ` 931` ``` "x > 0 \ x \ \ \ z / x \ y \ z \ x * y" ``` hoelzl@41973 ` 932` ``` by (cases rule: extreal3_cases[of x y z]) (auto simp: field_simps) ``` hoelzl@41973 ` 933` hoelzl@41973 ` 934` ```lemma extreal_le_divide_neg: ``` hoelzl@41973 ` 935` ``` "x < 0 \ x \ -\ \ y \ z / x \ z \ x * y" ``` hoelzl@41973 ` 936` ``` by (cases rule: extreal3_cases[of x y z]) (auto simp: field_simps) ``` hoelzl@41973 ` 937` hoelzl@41973 ` 938` ```lemma extreal_divide_le_neg: ``` hoelzl@41973 ` 939` ``` "x < 0 \ x \ -\ \ z / x \ y \ x * y \ z" ``` hoelzl@41973 ` 940` ``` by (cases rule: extreal3_cases[of x y z]) (auto simp: field_simps) ``` hoelzl@41973 ` 941` hoelzl@41973 ` 942` ```lemma extreal_inverse_antimono_strict: ``` hoelzl@41973 ` 943` ``` fixes x y :: extreal ``` hoelzl@41973 ` 944` ``` shows "0 \ x \ x < y \ inverse y < inverse x" ``` hoelzl@41973 ` 945` ``` by (cases rule: extreal2_cases[of x y]) auto ``` hoelzl@41973 ` 946` hoelzl@41973 ` 947` ```lemma extreal_inverse_antimono: ``` hoelzl@41973 ` 948` ``` fixes x y :: extreal ``` hoelzl@41973 ` 949` ``` shows "0 \ x \ x <= y \ inverse y <= inverse x" ``` hoelzl@41973 ` 950` ``` by (cases rule: extreal2_cases[of x y]) auto ``` hoelzl@41973 ` 951` hoelzl@41973 ` 952` ```lemma inverse_inverse_Pinfty_iff[simp]: ``` hoelzl@41973 ` 953` ``` "inverse x = \ \ x = 0" ``` hoelzl@41973 ` 954` ``` by (cases x) auto ``` hoelzl@41973 ` 955` hoelzl@41973 ` 956` ```lemma extreal_inverse_eq_0: ``` hoelzl@41973 ` 957` ``` "inverse x = 0 \ x = \ \ x = -\" ``` hoelzl@41973 ` 958` ``` by (cases x) auto ``` hoelzl@41973 ` 959` hoelzl@41979 ` 960` ```lemma extreal_0_gt_inverse: ``` hoelzl@41979 ` 961` ``` fixes x :: extreal shows "0 < inverse x \ x \ \ \ 0 \ x" ``` hoelzl@41979 ` 962` ``` by (cases x) auto ``` hoelzl@41979 ` 963` hoelzl@41973 ` 964` ```lemma extreal_mult_less_right: ``` hoelzl@41973 ` 965` ``` assumes "b * a < c * a" "0 < a" "a < \" ``` hoelzl@41973 ` 966` ``` shows "b < c" ``` hoelzl@41973 ` 967` ``` using assms ``` hoelzl@41973 ` 968` ``` by (cases rule: extreal3_cases[of a b c]) ``` hoelzl@41973 ` 969` ``` (auto split: split_if_asm simp: zero_less_mult_iff zero_le_mult_iff) ``` hoelzl@41973 ` 970` hoelzl@41979 ` 971` ```lemma extreal_power_divide: ``` hoelzl@41979 ` 972` ``` "y \ 0 \ (x / y :: extreal) ^ n = x^n / y^n" ``` hoelzl@41979 ` 973` ``` by (cases rule: extreal2_cases[of x y]) ``` hoelzl@41979 ` 974` ``` (auto simp: one_extreal_def zero_extreal_def power_divide not_le ``` hoelzl@41979 ` 975` ``` power_less_zero_eq zero_le_power_iff) ``` hoelzl@41979 ` 976` hoelzl@41979 ` 977` ```lemma extreal_le_mult_one_interval: ``` hoelzl@41979 ` 978` ``` fixes x y :: extreal ``` hoelzl@41979 ` 979` ``` assumes y: "y \ -\" ``` hoelzl@41979 ` 980` ``` assumes z: "\z. \ 0 < z ; z < 1 \ \ z * x \ y" ``` hoelzl@41979 ` 981` ``` shows "x \ y" ``` hoelzl@41979 ` 982` ```proof (cases x) ``` hoelzl@41979 ` 983` ``` case PInf with z[of "1 / 2"] show "x \ y" by (simp add: one_extreal_def) ``` hoelzl@41979 ` 984` ```next ``` hoelzl@41979 ` 985` ``` case (real r) note r = this ``` hoelzl@41979 ` 986` ``` show "x \ y" ``` hoelzl@41979 ` 987` ``` proof (cases y) ``` hoelzl@41979 ` 988` ``` case (real p) note p = this ``` hoelzl@41979 ` 989` ``` have "r \ p" ``` hoelzl@41979 ` 990` ``` proof (rule field_le_mult_one_interval) ``` hoelzl@41979 ` 991` ``` fix z :: real assume "0 < z" and "z < 1" ``` hoelzl@41979 ` 992` ``` with z[of "extreal z"] ``` hoelzl@41979 ` 993` ``` show "z * r \ p" using p r by (auto simp: zero_le_mult_iff one_extreal_def) ``` hoelzl@41979 ` 994` ``` qed ``` hoelzl@41979 ` 995` ``` then show "x \ y" using p r by simp ``` hoelzl@41979 ` 996` ``` qed (insert y, simp_all) ``` hoelzl@41979 ` 997` ```qed simp ``` hoelzl@41978 ` 998` hoelzl@41973 ` 999` ```subsection "Complete lattice" ``` hoelzl@41973 ` 1000` hoelzl@41973 ` 1001` ```instantiation extreal :: lattice ``` hoelzl@41973 ` 1002` ```begin ``` hoelzl@41973 ` 1003` ```definition [simp]: "sup x y = (max x y :: extreal)" ``` hoelzl@41973 ` 1004` ```definition [simp]: "inf x y = (min x y :: extreal)" ``` hoelzl@41973 ` 1005` ```instance proof qed simp_all ``` hoelzl@41973 ` 1006` ```end ``` hoelzl@41973 ` 1007` hoelzl@41973 ` 1008` ```instantiation extreal :: complete_lattice ``` hoelzl@41973 ` 1009` ```begin ``` hoelzl@41973 ` 1010` hoelzl@41976 ` 1011` ```definition "bot = -\" ``` hoelzl@41973 ` 1012` ```definition "top = \" ``` hoelzl@41973 ` 1013` hoelzl@41973 ` 1014` ```definition "Sup S = (LEAST z. ALL x:S. x <= z :: extreal)" ``` hoelzl@41973 ` 1015` ```definition "Inf S = (GREATEST z. ALL x:S. z <= x :: extreal)" ``` hoelzl@41973 ` 1016` hoelzl@41973 ` 1017` ```lemma extreal_complete_Sup: ``` hoelzl@41973 ` 1018` ``` fixes S :: "extreal set" assumes "S \ {}" ``` hoelzl@41973 ` 1019` ``` shows "\x. (\y\S. y \ x) \ (\z. (\y\S. y \ z) \ x \ z)" ``` hoelzl@41973 ` 1020` ```proof cases ``` hoelzl@41973 ` 1021` ``` assume "\x. \a\S. a \ extreal x" ``` hoelzl@41973 ` 1022` ``` then obtain y where y: "\a. a\S \ a \ extreal y" by auto ``` hoelzl@41973 ` 1023` ``` then have "\ \ S" by force ``` hoelzl@41973 ` 1024` ``` show ?thesis ``` hoelzl@41973 ` 1025` ``` proof cases ``` hoelzl@41973 ` 1026` ``` assume "S = {-\}" ``` hoelzl@41973 ` 1027` ``` then show ?thesis by (auto intro!: exI[of _ "-\"]) ``` hoelzl@41973 ` 1028` ``` next ``` hoelzl@41973 ` 1029` ``` assume "S \ {-\}" ``` hoelzl@41973 ` 1030` ``` with `S \ {}` `\ \ S` obtain x where "x \ S - {-\}" "x \ \" by auto ``` hoelzl@41973 ` 1031` ``` with y `\ \ S` have "\z\real ` (S - {-\}). z \ y" ``` hoelzl@41973 ` 1032` ``` by (auto simp: real_of_extreal_ord_simps) ``` hoelzl@41973 ` 1033` ``` with reals_complete2[of "real ` (S - {-\})"] `x \ S - {-\}` ``` hoelzl@41973 ` 1034` ``` obtain s where s: ``` hoelzl@41973 ` 1035` ``` "\y\S - {-\}. real y \ s" "\z. (\y\S - {-\}. real y \ z) \ s \ z" ``` hoelzl@41973 ` 1036` ``` by auto ``` hoelzl@41973 ` 1037` ``` show ?thesis ``` hoelzl@41973 ` 1038` ``` proof (safe intro!: exI[of _ "extreal s"]) ``` hoelzl@41973 ` 1039` ``` fix z assume "z \ S" with `\ \ S` show "z \ extreal s" ``` hoelzl@41973 ` 1040` ``` proof (cases z) ``` hoelzl@41973 ` 1041` ``` case (real r) ``` hoelzl@41973 ` 1042` ``` then show ?thesis ``` hoelzl@41973 ` 1043` ``` using s(1)[rule_format, of z] `z \ S` `z = extreal r` by auto ``` hoelzl@41973 ` 1044` ``` qed auto ``` hoelzl@41973 ` 1045` ``` next ``` hoelzl@41973 ` 1046` ``` fix z assume *: "\y\S. y \ z" ``` hoelzl@41973 ` 1047` ``` with `S \ {-\}` `S \ {}` show "extreal s \ z" ``` hoelzl@41973 ` 1048` ``` proof (cases z) ``` hoelzl@41973 ` 1049` ``` case (real u) ``` hoelzl@41973 ` 1050` ``` with * have "s \ u" ``` hoelzl@41973 ` 1051` ``` by (intro s(2)[of u]) (auto simp: real_of_extreal_ord_simps) ``` hoelzl@41973 ` 1052` ``` then show ?thesis using real by simp ``` hoelzl@41973 ` 1053` ``` qed auto ``` hoelzl@41973 ` 1054` ``` qed ``` hoelzl@41973 ` 1055` ``` qed ``` hoelzl@41973 ` 1056` ```next ``` hoelzl@41973 ` 1057` ``` assume *: "\ (\x. \a\S. a \ extreal x)" ``` hoelzl@41973 ` 1058` ``` show ?thesis ``` hoelzl@41973 ` 1059` ``` proof (safe intro!: exI[of _ \]) ``` hoelzl@41973 ` 1060` ``` fix y assume **: "\z\S. z \ y" ``` hoelzl@41973 ` 1061` ``` with * show "\ \ y" ``` hoelzl@41973 ` 1062` ``` proof (cases y) ``` hoelzl@41973 ` 1063` ``` case MInf with * ** show ?thesis by (force simp: not_le) ``` hoelzl@41973 ` 1064` ``` qed auto ``` hoelzl@41973 ` 1065` ``` qed simp ``` hoelzl@41973 ` 1066` ```qed ``` hoelzl@41973 ` 1067` hoelzl@41973 ` 1068` ```lemma extreal_complete_Inf: ``` hoelzl@41973 ` 1069` ``` fixes S :: "extreal set" assumes "S ~= {}" ``` hoelzl@41973 ` 1070` ``` shows "EX x. (ALL y:S. x <= y) & (ALL z. (ALL y:S. z <= y) --> z <= x)" ``` hoelzl@41973 ` 1071` ```proof- ``` hoelzl@41973 ` 1072` ```def S1 == "uminus ` S" ``` hoelzl@41973 ` 1073` ```hence "S1 ~= {}" using assms by auto ``` hoelzl@41973 ` 1074` ```from this obtain x where x_def: "(ALL y:S1. y <= x) & (ALL z. (ALL y:S1. y <= z) --> x <= z)" ``` hoelzl@41973 ` 1075` ``` using extreal_complete_Sup[of S1] by auto ``` hoelzl@41973 ` 1076` ```{ fix z assume "ALL y:S. z <= y" ``` hoelzl@41973 ` 1077` ``` hence "ALL y:S1. y <= -z" unfolding S1_def by auto ``` hoelzl@41973 ` 1078` ``` hence "x <= -z" using x_def by auto ``` hoelzl@41973 ` 1079` ``` hence "z <= -x" ``` hoelzl@41973 ` 1080` ``` apply (subst extreal_uminus_uminus[symmetric]) ``` hoelzl@41973 ` 1081` ``` unfolding extreal_minus_le_minus . } ``` hoelzl@41973 ` 1082` ```moreover have "(ALL y:S. -x <= y)" ``` hoelzl@41973 ` 1083` ``` using x_def unfolding S1_def ``` hoelzl@41973 ` 1084` ``` apply simp ``` hoelzl@41973 ` 1085` ``` apply (subst (3) extreal_uminus_uminus[symmetric]) ``` hoelzl@41973 ` 1086` ``` unfolding extreal_minus_le_minus by simp ``` hoelzl@41973 ` 1087` ```ultimately show ?thesis by auto ``` hoelzl@41973 ` 1088` ```qed ``` hoelzl@41973 ` 1089` hoelzl@41973 ` 1090` ```lemma extreal_complete_uminus_eq: ``` hoelzl@41973 ` 1091` ``` fixes S :: "extreal set" ``` hoelzl@41973 ` 1092` ``` shows "(\y\uminus`S. y \ x) \ (\z. (\y\uminus`S. y \ z) \ x \ z) ``` hoelzl@41973 ` 1093` ``` \ (\y\S. -x \ y) \ (\z. (\y\S. z \ y) \ z \ -x)" ``` hoelzl@41973 ` 1094` ``` by simp (metis extreal_minus_le_minus extreal_uminus_uminus) ``` hoelzl@41973 ` 1095` hoelzl@41973 ` 1096` ```lemma extreal_Sup_uminus_image_eq: ``` hoelzl@41973 ` 1097` ``` fixes S :: "extreal set" ``` hoelzl@41973 ` 1098` ``` shows "Sup (uminus ` S) = - Inf S" ``` hoelzl@41973 ` 1099` ```proof cases ``` hoelzl@41973 ` 1100` ``` assume "S = {}" ``` hoelzl@41973 ` 1101` ``` moreover have "(THE x. All (op \ x)) = (-\::extreal)" ``` hoelzl@41973 ` 1102` ``` by (rule the_equality) (auto intro!: extreal_bot) ``` hoelzl@41973 ` 1103` ``` moreover have "(SOME x. \y. y \ x) = (\::extreal)" ``` hoelzl@41973 ` 1104` ``` by (rule some_equality) (auto intro!: extreal_top) ``` hoelzl@41973 ` 1105` ``` ultimately show ?thesis unfolding Inf_extreal_def Sup_extreal_def ``` hoelzl@41973 ` 1106` ``` Least_def Greatest_def GreatestM_def by simp ``` hoelzl@41973 ` 1107` ```next ``` hoelzl@41973 ` 1108` ``` assume "S \ {}" ``` hoelzl@41973 ` 1109` ``` with extreal_complete_Sup[of "uminus`S"] ``` hoelzl@41973 ` 1110` ``` obtain x where x: "(\y\S. -x \ y) \ (\z. (\y\S. z \ y) \ z \ -x)" ``` hoelzl@41973 ` 1111` ``` unfolding extreal_complete_uminus_eq by auto ``` hoelzl@41973 ` 1112` ``` show "Sup (uminus ` S) = - Inf S" ``` hoelzl@41973 ` 1113` ``` unfolding Inf_extreal_def Greatest_def GreatestM_def ``` hoelzl@41973 ` 1114` ``` proof (intro someI2[of _ _ "\x. Sup (uminus`S) = - x"]) ``` hoelzl@41973 ` 1115` ``` show "(\y\S. -x \ y) \ (\y. (\z\S. y \ z) \ y \ -x)" ``` hoelzl@41973 ` 1116` ``` using x . ``` hoelzl@41973 ` 1117` ``` fix x' assume "(\y\S. x' \ y) \ (\y. (\z\S. y \ z) \ y \ x')" ``` hoelzl@41973 ` 1118` ``` then have "(\y\uminus`S. y \ - x') \ (\y. (\z\uminus`S. z \ y) \ - x' \ y)" ``` hoelzl@41973 ` 1119` ``` unfolding extreal_complete_uminus_eq by simp ``` hoelzl@41973 ` 1120` ``` then show "Sup (uminus ` S) = -x'" ``` hoelzl@41973 ` 1121` ``` unfolding Sup_extreal_def extreal_uminus_eq_iff ``` hoelzl@41973 ` 1122` ``` by (intro Least_equality) auto ``` hoelzl@41973 ` 1123` ``` qed ``` hoelzl@41973 ` 1124` ```qed ``` hoelzl@41973 ` 1125` hoelzl@41973 ` 1126` ```instance ``` hoelzl@41973 ` 1127` ```proof ``` hoelzl@41973 ` 1128` ``` { fix x :: extreal and A ``` hoelzl@41973 ` 1129` ``` show "bot <= x" by (cases x) (simp_all add: bot_extreal_def) ``` hoelzl@41973 ` 1130` ``` show "x <= top" by (simp add: top_extreal_def) } ``` hoelzl@41973 ` 1131` hoelzl@41973 ` 1132` ``` { fix x :: extreal and A assume "x : A" ``` hoelzl@41973 ` 1133` ``` with extreal_complete_Sup[of A] ``` hoelzl@41973 ` 1134` ``` obtain s where s: "\y\A. y <= s" "\z. (\y\A. y <= z) \ s <= z" by auto ``` hoelzl@41973 ` 1135` ``` hence "x <= s" using `x : A` by auto ``` hoelzl@41973 ` 1136` ``` also have "... = Sup A" using s unfolding Sup_extreal_def ``` hoelzl@41973 ` 1137` ``` by (auto intro!: Least_equality[symmetric]) ``` hoelzl@41973 ` 1138` ``` finally show "x <= Sup A" . } ``` hoelzl@41973 ` 1139` ``` note le_Sup = this ``` hoelzl@41973 ` 1140` hoelzl@41973 ` 1141` ``` { fix x :: extreal and A assume *: "!!z. (z : A ==> z <= x)" ``` hoelzl@41973 ` 1142` ``` show "Sup A <= x" ``` hoelzl@41973 ` 1143` ``` proof (cases "A = {}") ``` hoelzl@41973 ` 1144` ``` case True ``` hoelzl@41973 ` 1145` ``` hence "Sup A = -\" unfolding Sup_extreal_def ``` hoelzl@41973 ` 1146` ``` by (auto intro!: Least_equality) ``` hoelzl@41973 ` 1147` ``` thus "Sup A <= x" by simp ``` hoelzl@41973 ` 1148` ``` next ``` hoelzl@41973 ` 1149` ``` case False ``` hoelzl@41973 ` 1150` ``` with extreal_complete_Sup[of A] ``` hoelzl@41973 ` 1151` ``` obtain s where s: "\y\A. y <= s" "\z. (\y\A. y <= z) \ s <= z" by auto ``` hoelzl@41973 ` 1152` ``` hence "Sup A = s" ``` hoelzl@41973 ` 1153` ``` unfolding Sup_extreal_def by (auto intro!: Least_equality) ``` hoelzl@41973 ` 1154` ``` also have "s <= x" using * s by auto ``` hoelzl@41973 ` 1155` ``` finally show "Sup A <= x" . ``` hoelzl@41973 ` 1156` ``` qed } ``` hoelzl@41973 ` 1157` ``` note Sup_le = this ``` hoelzl@41973 ` 1158` hoelzl@41973 ` 1159` ``` { fix x :: extreal and A assume "x \ A" ``` hoelzl@41973 ` 1160` ``` with le_Sup[of "-x" "uminus`A"] show "Inf A \ x" ``` hoelzl@41973 ` 1161` ``` unfolding extreal_Sup_uminus_image_eq by simp } ``` hoelzl@41973 ` 1162` hoelzl@41973 ` 1163` ``` { fix x :: extreal and A assume *: "!!z. (z : A ==> x <= z)" ``` hoelzl@41973 ` 1164` ``` with Sup_le[of "uminus`A" "-x"] show "x \ Inf A" ``` hoelzl@41973 ` 1165` ``` unfolding extreal_Sup_uminus_image_eq by force } ``` hoelzl@41973 ` 1166` ```qed ``` hoelzl@41973 ` 1167` ```end ``` hoelzl@41973 ` 1168` hoelzl@41973 ` 1169` ```lemma extreal_SUPR_uminus: ``` hoelzl@41973 ` 1170` ``` fixes f :: "'a => extreal" ``` hoelzl@41973 ` 1171` ``` shows "(SUP i : R. -(f i)) = -(INF i : R. f i)" ``` hoelzl@41973 ` 1172` ``` unfolding SUPR_def INFI_def ``` hoelzl@41973 ` 1173` ``` using extreal_Sup_uminus_image_eq[of "f`R"] ``` hoelzl@41973 ` 1174` ``` by (simp add: image_image) ``` hoelzl@41973 ` 1175` hoelzl@41973 ` 1176` ```lemma extreal_INFI_uminus: ``` hoelzl@41973 ` 1177` ``` fixes f :: "'a => extreal" ``` hoelzl@41973 ` 1178` ``` shows "(INF i : R. -(f i)) = -(SUP i : R. f i)" ``` hoelzl@41973 ` 1179` ``` using extreal_SUPR_uminus[of _ "\x. - f x"] by simp ``` hoelzl@41973 ` 1180` hoelzl@41979 ` 1181` ```lemma extreal_Inf_uminus_image_eq: "Inf (uminus ` S) = - Sup (S::extreal set)" ``` hoelzl@41979 ` 1182` ``` using extreal_Sup_uminus_image_eq[of "uminus ` S"] by (simp add: image_image) ``` hoelzl@41979 ` 1183` hoelzl@41973 ` 1184` ```lemma extreal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: extreal set)" ``` hoelzl@41973 ` 1185` ``` by (auto intro!: inj_onI) ``` hoelzl@41973 ` 1186` hoelzl@41973 ` 1187` ```lemma extreal_image_uminus_shift: ``` hoelzl@41973 ` 1188` ``` fixes X Y :: "extreal set" shows "uminus ` X = Y \ X = uminus ` Y" ``` hoelzl@41973 ` 1189` ```proof ``` hoelzl@41973 ` 1190` ``` assume "uminus ` X = Y" ``` hoelzl@41973 ` 1191` ``` then have "uminus ` uminus ` X = uminus ` Y" ``` hoelzl@41973 ` 1192` ``` by (simp add: inj_image_eq_iff) ``` hoelzl@41973 ` 1193` ``` then show "X = uminus ` Y" by (simp add: image_image) ``` hoelzl@41973 ` 1194` ```qed (simp add: image_image) ``` hoelzl@41973 ` 1195` hoelzl@41973 ` 1196` ```lemma Inf_extreal_iff: ``` hoelzl@41973 ` 1197` ``` fixes z :: extreal ``` hoelzl@41973 ` 1198` ``` shows "(!!x. x:X ==> z <= x) ==> (EX x:X. x Inf X < y" ``` hoelzl@41973 ` 1199` ``` by (metis complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower less_le_not_le linear ``` hoelzl@41973 ` 1200` ``` order_less_le_trans) ``` hoelzl@41973 ` 1201` hoelzl@41973 ` 1202` ```lemma Sup_eq_MInfty: ``` hoelzl@41973 ` 1203` ``` fixes S :: "extreal set" shows "Sup S = -\ \ S = {} \ S = {-\}" ``` hoelzl@41973 ` 1204` ```proof ``` hoelzl@41973 ` 1205` ``` assume a: "Sup S = -\" ``` hoelzl@41973 ` 1206` ``` with complete_lattice_class.Sup_upper[of _ S] ``` hoelzl@41973 ` 1207` ``` show "S={} \ S={-\}" by auto ``` hoelzl@41973 ` 1208` ```next ``` hoelzl@41973 ` 1209` ``` assume "S={} \ S={-\}" then show "Sup S = -\" ``` hoelzl@41973 ` 1210` ``` unfolding Sup_extreal_def by (auto intro!: Least_equality) ``` hoelzl@41973 ` 1211` ```qed ``` hoelzl@41973 ` 1212` hoelzl@41973 ` 1213` ```lemma Inf_eq_PInfty: ``` hoelzl@41973 ` 1214` ``` fixes S :: "extreal set" shows "Inf S = \ \ S = {} \ S = {\}" ``` hoelzl@41973 ` 1215` ``` using Sup_eq_MInfty[of "uminus`S"] ``` hoelzl@41973 ` 1216` ``` unfolding extreal_Sup_uminus_image_eq extreal_image_uminus_shift by simp ``` hoelzl@41973 ` 1217` hoelzl@41973 ` 1218` ```lemma Inf_eq_MInfty: "-\ : S ==> Inf S = -\" ``` hoelzl@41973 ` 1219` ``` unfolding Inf_extreal_def ``` hoelzl@41973 ` 1220` ``` by (auto intro!: Greatest_equality) ``` hoelzl@41973 ` 1221` hoelzl@41973 ` 1222` ```lemma Sup_eq_PInfty: "\ : S ==> Sup S = \" ``` hoelzl@41973 ` 1223` ``` unfolding Sup_extreal_def ``` hoelzl@41973 ` 1224` ``` by (auto intro!: Least_equality) ``` hoelzl@41973 ` 1225` hoelzl@41973 ` 1226` ```lemma extreal_SUPI: ``` hoelzl@41973 ` 1227` ``` fixes x :: extreal ``` hoelzl@41973 ` 1228` ``` assumes "!!i. i : A ==> f i <= x" ``` hoelzl@41973 ` 1229` ``` assumes "!!y. (!!i. i : A ==> f i <= y) ==> x <= y" ``` hoelzl@41973 ` 1230` ``` shows "(SUP i:A. f i) = x" ``` hoelzl@41973 ` 1231` ``` unfolding SUPR_def Sup_extreal_def ``` hoelzl@41973 ` 1232` ``` using assms by (auto intro!: Least_equality) ``` hoelzl@41973 ` 1233` hoelzl@41973 ` 1234` ```lemma extreal_INFI: ``` hoelzl@41973 ` 1235` ``` fixes x :: extreal ``` hoelzl@41973 ` 1236` ``` assumes "!!i. i : A ==> f i >= x" ``` hoelzl@41973 ` 1237` ``` assumes "!!y. (!!i. i : A ==> f i >= y) ==> x >= y" ``` hoelzl@41973 ` 1238` ``` shows "(INF i:A. f i) = x" ``` hoelzl@41973 ` 1239` ``` unfolding INFI_def Inf_extreal_def ``` hoelzl@41973 ` 1240` ``` using assms by (auto intro!: Greatest_equality) ``` hoelzl@41973 ` 1241` hoelzl@41973 ` 1242` ```lemma Sup_extreal_close: ``` hoelzl@41973 ` 1243` ``` fixes e :: extreal ``` hoelzl@41976 ` 1244` ``` assumes "0 < e" and S: "\Sup S\ \ \" "S \ {}" ``` hoelzl@41973 ` 1245` ``` shows "\x\S. Sup S - e < x" ``` hoelzl@41976 ` 1246` ``` using assms by (cases e) (auto intro!: less_Sup_iff[THEN iffD1]) ``` hoelzl@41973 ` 1247` hoelzl@41973 ` 1248` ```lemma Inf_extreal_close: ``` hoelzl@41976 ` 1249` ``` fixes e :: extreal assumes "\Inf X\ \ \" "0 < e" ``` hoelzl@41973 ` 1250` ``` shows "\x\X. x < Inf X + e" ``` hoelzl@41973 ` 1251` ```proof (rule Inf_less_iff[THEN iffD1]) ``` hoelzl@41973 ` 1252` ``` show "Inf X < Inf X + e" using assms ``` hoelzl@41976 ` 1253` ``` by (cases e) auto ``` hoelzl@41973 ` 1254` ```qed ``` hoelzl@41973 ` 1255` hoelzl@41973 ` 1256` ```lemma Sup_eq_top_iff: ``` hoelzl@41973 ` 1257` ``` fixes A :: "'a::{complete_lattice, linorder} set" ``` hoelzl@41973 ` 1258` ``` shows "Sup A = top \ (\xi\A. x < i)" ``` hoelzl@41973 ` 1259` ```proof ``` hoelzl@41973 ` 1260` ``` assume *: "Sup A = top" ``` hoelzl@41973 ` 1261` ``` show "(\xi\A. x < i)" unfolding *[symmetric] ``` hoelzl@41973 ` 1262` ``` proof (intro allI impI) ``` hoelzl@41973 ` 1263` ``` fix x assume "x < Sup A" then show "\i\A. x < i" ``` hoelzl@41973 ` 1264` ``` unfolding less_Sup_iff by auto ``` hoelzl@41973 ` 1265` ``` qed ``` hoelzl@41973 ` 1266` ```next ``` hoelzl@41973 ` 1267` ``` assume *: "\xi\A. x < i" ``` hoelzl@41973 ` 1268` ``` show "Sup A = top" ``` hoelzl@41973 ` 1269` ``` proof (rule ccontr) ``` hoelzl@41973 ` 1270` ``` assume "Sup A \ top" ``` hoelzl@41973 ` 1271` ``` with top_greatest[of "Sup A"] ``` hoelzl@41973 ` 1272` ``` have "Sup A < top" unfolding le_less by auto ``` hoelzl@41973 ` 1273` ``` then have "Sup A < Sup A" ``` hoelzl@41973 ` 1274` ``` using * unfolding less_Sup_iff by auto ``` hoelzl@41973 ` 1275` ``` then show False by auto ``` hoelzl@41973 ` 1276` ``` qed ``` hoelzl@41973 ` 1277` ```qed ``` hoelzl@41973 ` 1278` hoelzl@41973 ` 1279` ```lemma SUP_eq_top_iff: ``` hoelzl@41973 ` 1280` ``` fixes f :: "'a \ 'b::{complete_lattice, linorder}" ``` hoelzl@41973 ` 1281` ``` shows "(SUP i:A. f i) = top \ (\xi\A. x < f i)" ``` hoelzl@41973 ` 1282` ``` unfolding SUPR_def Sup_eq_top_iff by auto ``` hoelzl@41973 ` 1283` hoelzl@41973 ` 1284` ```lemma SUP_nat_Infty: "(SUP i::nat. extreal (real i)) = \" ``` hoelzl@41973 ` 1285` ```proof - ``` hoelzl@41973 ` 1286` ``` { fix x assume "x \ \" ``` hoelzl@41973 ` 1287` ``` then have "\k::nat. x < extreal (real k)" ``` hoelzl@41973 ` 1288` ``` proof (cases x) ``` hoelzl@41973 ` 1289` ``` case MInf then show ?thesis by (intro exI[of _ 0]) auto ``` hoelzl@41973 ` 1290` ``` next ``` hoelzl@41973 ` 1291` ``` case (real r) ``` hoelzl@41973 ` 1292` ``` moreover obtain k :: nat where "r < real k" ``` hoelzl@41973 ` 1293` ``` using ex_less_of_nat by (auto simp: real_eq_of_nat) ``` hoelzl@41973 ` 1294` ``` ultimately show ?thesis by auto ``` hoelzl@41973 ` 1295` ``` qed simp } ``` hoelzl@41973 ` 1296` ``` then show ?thesis ``` hoelzl@41973 ` 1297` ``` using SUP_eq_top_iff[of UNIV "\n::nat. extreal (real n)"] ``` hoelzl@41973 ` 1298` ``` by (auto simp: top_extreal_def) ``` hoelzl@41973 ` 1299` ```qed ``` hoelzl@41973 ` 1300` hoelzl@41979 ` 1301` ```lemma extreal_le_Sup: ``` hoelzl@41973 ` 1302` ``` fixes x :: extreal ``` hoelzl@41973 ` 1303` ``` shows "(x <= (SUP i:A. f i)) <-> (ALL y. y < x --> (EX i. i : A & y <= f i))" ``` hoelzl@41973 ` 1304` ```(is "?lhs <-> ?rhs") ``` hoelzl@41973 ` 1305` ```proof- ``` hoelzl@41973 ` 1306` ```{ assume "?rhs" ``` hoelzl@41973 ` 1307` ``` { assume "~(x <= (SUP i:A. f i))" hence "(SUP i:A. f i) (ALL y. x < y --> (EX i. i : A & f i <= y))" ``` hoelzl@41973 ` 1324` ```(is "?lhs <-> ?rhs") ``` hoelzl@41973 ` 1325` ```proof- ``` hoelzl@41973 ` 1326` ```{ assume "?rhs" ``` hoelzl@41973 ` 1327` ``` { assume "~((INF i:A. f i) <= x)" hence "x < (INF i:A. f i)" by (simp add: not_le) ``` hoelzl@41973 ` 1328` ``` from this obtain y where y_def: "x x" by auto ``` hoelzl@41973 ` 1348` ``` hence "(INF i:A. f i) >= x" apply (subst le_INFI) by auto ``` hoelzl@41973 ` 1349` ``` thus False using assms by auto ``` hoelzl@41973 ` 1350` ```qed ``` hoelzl@41973 ` 1351` hoelzl@41973 ` 1352` ```lemma same_INF: ``` hoelzl@41973 ` 1353` ``` assumes "ALL e:A. f e = g e" ``` hoelzl@41973 ` 1354` ``` shows "(INF e:A. f e) = (INF e:A. g e)" ``` hoelzl@41973 ` 1355` ```proof- ``` hoelzl@41973 ` 1356` ```have "f ` A = g ` A" unfolding image_def using assms by auto ``` hoelzl@41973 ` 1357` ```thus ?thesis unfolding INFI_def by auto ``` hoelzl@41973 ` 1358` ```qed ``` hoelzl@41973 ` 1359` hoelzl@41973 ` 1360` ```lemma same_SUP: ``` hoelzl@41973 ` 1361` ``` assumes "ALL e:A. f e = g e" ``` hoelzl@41973 ` 1362` ``` shows "(SUP e:A. f e) = (SUP e:A. g e)" ``` hoelzl@41973 ` 1363` ```proof- ``` hoelzl@41973 ` 1364` ```have "f ` A = g ` A" unfolding image_def using assms by auto ``` hoelzl@41973 ` 1365` ```thus ?thesis unfolding SUPR_def by auto ``` hoelzl@41973 ` 1366` ```qed ``` hoelzl@41973 ` 1367` hoelzl@41979 ` 1368` ```lemma SUPR_eq: ``` hoelzl@41979 ` 1369` ``` assumes "\i\A. \j\B. f i \ g j" ``` hoelzl@41979 ` 1370` ``` assumes "\j\B. \i\A. g j \ f i" ``` hoelzl@41979 ` 1371` ``` shows "(SUP i:A. f i) = (SUP j:B. g j)" ``` hoelzl@41979 ` 1372` ```proof (intro antisym) ``` hoelzl@41979 ` 1373` ``` show "(SUP i:A. f i) \ (SUP j:B. g j)" ``` hoelzl@41979 ` 1374` ``` using assms by (metis SUP_leI le_SUPI_trans) ``` hoelzl@41979 ` 1375` ``` show "(SUP i:B. g i) \ (SUP j:A. f j)" ``` hoelzl@41979 ` 1376` ``` using assms by (metis SUP_leI le_SUPI_trans) ``` hoelzl@41979 ` 1377` ```qed ``` hoelzl@41979 ` 1378` hoelzl@41978 ` 1379` ```lemma SUP_extreal_le_addI: ``` hoelzl@41978 ` 1380` ``` assumes "\i. f i + y \ z" and "y \ -\" ``` hoelzl@41978 ` 1381` ``` shows "SUPR UNIV f + y \ z" ``` hoelzl@41978 ` 1382` ```proof (cases y) ``` hoelzl@41978 ` 1383` ``` case (real r) ``` hoelzl@41978 ` 1384` ``` then have "\i. f i \ z - y" using assms by (simp add: extreal_le_minus_iff) ``` hoelzl@41978 ` 1385` ``` then have "SUPR UNIV f \ z - y" by (rule SUP_leI) ``` hoelzl@41978 ` 1386` ``` then show ?thesis using real by (simp add: extreal_le_minus_iff) ``` hoelzl@41978 ` 1387` ```qed (insert assms, auto) ``` hoelzl@41978 ` 1388` hoelzl@41978 ` 1389` ```lemma SUPR_extreal_add: ``` hoelzl@41978 ` 1390` ``` fixes f g :: "nat \ extreal" ``` hoelzl@41979 ` 1391` ``` assumes "incseq f" "incseq g" and pos: "\i. f i \ -\" "\i. g i \ -\" ``` hoelzl@41978 ` 1392` ``` shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g" ``` hoelzl@41978 ` 1393` ```proof (rule extreal_SUPI) ``` hoelzl@41978 ` 1394` ``` fix y assume *: "\i. i \ UNIV \ f i + g i \ y" ``` hoelzl@41978 ` 1395` ``` have f: "SUPR UNIV f \ -\" using pos ``` hoelzl@41978 ` 1396` ``` unfolding SUPR_def Sup_eq_MInfty by (auto dest: image_eqD) ``` hoelzl@41978 ` 1397` ``` { fix j ``` hoelzl@41978 ` 1398` ``` { fix i ``` hoelzl@41978 ` 1399` ``` have "f i + g j \ f i + g (max i j)" ``` hoelzl@41978 ` 1400` ``` using `incseq g`[THEN incseqD] by (rule add_left_mono) auto ``` hoelzl@41978 ` 1401` ``` also have "\ \ f (max i j) + g (max i j)" ``` hoelzl@41978 ` 1402` ``` using `incseq f`[THEN incseqD] by (rule add_right_mono) auto ``` hoelzl@41978 ` 1403` ``` also have "\ \ y" using * by auto ``` hoelzl@41978 ` 1404` ``` finally have "f i + g j \ y" . } ``` hoelzl@41978 ` 1405` ``` then have "SUPR UNIV f + g j \ y" ``` hoelzl@41978 ` 1406` ``` using assms(4)[of j] by (intro SUP_extreal_le_addI) auto ``` hoelzl@41978 ` 1407` ``` then have "g j + SUPR UNIV f \ y" by (simp add: ac_simps) } ``` hoelzl@41978 ` 1408` ``` then have "SUPR UNIV g + SUPR UNIV f \ y" ``` hoelzl@41978 ` 1409` ``` using f by (rule SUP_extreal_le_addI) ``` hoelzl@41978 ` 1410` ``` then show "SUPR UNIV f + SUPR UNIV g \ y" by (simp add: ac_simps) ``` hoelzl@41978 ` 1411` ```qed (auto intro!: add_mono le_SUPI) ``` hoelzl@41978 ` 1412` hoelzl@41979 ` 1413` ```lemma SUPR_extreal_add_pos: ``` hoelzl@41979 ` 1414` ``` fixes f g :: "nat \ extreal" ``` hoelzl@41979 ` 1415` ``` assumes inc: "incseq f" "incseq g" and pos: "\i. 0 \ f i" "\i. 0 \ g i" ``` hoelzl@41979 ` 1416` ``` shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g" ``` hoelzl@41979 ` 1417` ```proof (intro SUPR_extreal_add inc) ``` hoelzl@41979 ` 1418` ``` fix i show "f i \ -\" "g i \ -\" using pos[of i] by auto ``` hoelzl@41979 ` 1419` ```qed ``` hoelzl@41979 ` 1420` hoelzl@41979 ` 1421` ```lemma SUPR_extreal_setsum: ``` hoelzl@41979 ` 1422` ``` fixes f g :: "'a \ nat \ extreal" ``` hoelzl@41979 ` 1423` ``` assumes "\n. n \ A \ incseq (f n)" and pos: "\n i. n \ A \ 0 \ f n i" ``` hoelzl@41979 ` 1424` ``` shows "(SUP i. \n\A. f n i) = (\n\A. SUPR UNIV (f n))" ``` hoelzl@41979 ` 1425` ```proof cases ``` hoelzl@41979 ` 1426` ``` assume "finite A" then show ?thesis using assms ``` hoelzl@41979 ` 1427` ``` by induct (auto simp: incseq_setsumI2 setsum_nonneg SUPR_extreal_add_pos) ``` hoelzl@41979 ` 1428` ```qed simp ``` hoelzl@41979 ` 1429` hoelzl@41978 ` 1430` ```lemma SUPR_extreal_cmult: ``` hoelzl@41978 ` 1431` ``` fixes f :: "nat \ extreal" assumes "\i. 0 \ f i" "0 \ c" ``` hoelzl@41978 ` 1432` ``` shows "(SUP i. c * f i) = c * SUPR UNIV f" ``` hoelzl@41978 ` 1433` ```proof (rule extreal_SUPI) ``` hoelzl@41978 ` 1434` ``` fix i have "f i \ SUPR UNIV f" by (rule le_SUPI) auto ``` hoelzl@41978 ` 1435` ``` then show "c * f i \ c * SUPR UNIV f" ``` hoelzl@41978 ` 1436` ``` using `0 \ c` by (rule extreal_mult_left_mono) ``` hoelzl@41978 ` 1437` ```next ``` hoelzl@41978 ` 1438` ``` fix y assume *: "\i. i \ UNIV \ c * f i \ y" ``` hoelzl@41978 ` 1439` ``` show "c * SUPR UNIV f \ y" ``` hoelzl@41978 ` 1440` ``` proof cases ``` hoelzl@41978 ` 1441` ``` assume c: "0 < c \ c \ \" ``` hoelzl@41978 ` 1442` ``` with * have "SUPR UNIV f \ y / c" ``` hoelzl@41978 ` 1443` ``` by (intro SUP_leI) (auto simp: extreal_le_divide_pos) ``` hoelzl@41978 ` 1444` ``` with c show ?thesis ``` hoelzl@41978 ` 1445` ``` by (auto simp: extreal_le_divide_pos) ``` hoelzl@41978 ` 1446` ``` next ``` hoelzl@41978 ` 1447` ``` { assume "c = \" have ?thesis ``` hoelzl@41978 ` 1448` ``` proof cases ``` hoelzl@41978 ` 1449` ``` assume "\i. f i = 0" ``` hoelzl@41978 ` 1450` ``` moreover then have "range f = {0}" by auto ``` hoelzl@41978 ` 1451` ``` ultimately show "c * SUPR UNIV f \ y" using * by (auto simp: SUPR_def) ``` hoelzl@41978 ` 1452` ``` next ``` hoelzl@41978 ` 1453` ``` assume "\ (\i. f i = 0)" ``` hoelzl@41978 ` 1454` ``` then obtain i where "f i \ 0" by auto ``` hoelzl@41978 ` 1455` ``` with *[of i] `c = \` `0 \ f i` show ?thesis by (auto split: split_if_asm) ``` hoelzl@41978 ` 1456` ``` qed } ``` hoelzl@41978 ` 1457` ``` moreover assume "\ (0 < c \ c \ \)" ``` hoelzl@41978 ` 1458` ``` ultimately show ?thesis using * `0 \ c` by auto ``` hoelzl@41978 ` 1459` ``` qed ``` hoelzl@41978 ` 1460` ```qed ``` hoelzl@41978 ` 1461` hoelzl@41979 ` 1462` ```lemma SUP_PInfty: ``` hoelzl@41979 ` 1463` ``` fixes f :: "'a \ extreal" ``` hoelzl@41979 ` 1464` ``` assumes "\n::nat. \i\A. extreal (real n) \ f i" ``` hoelzl@41979 ` 1465` ``` shows "(SUP i:A. f i) = \" ``` hoelzl@41979 ` 1466` ``` unfolding SUPR_def Sup_eq_top_iff[where 'a=extreal, unfolded top_extreal_def] ``` hoelzl@41979 ` 1467` ``` apply simp ``` hoelzl@41979 ` 1468` ```proof safe ``` hoelzl@41979 ` 1469` ``` fix x assume "x \ \" ``` hoelzl@41979 ` 1470` ``` show "\i\A. x < f i" ``` hoelzl@41979 ` 1471` ``` proof (cases x) ``` hoelzl@41979 ` 1472` ``` case PInf with `x \ \` show ?thesis by simp ``` hoelzl@41979 ` 1473` ``` next ``` hoelzl@41979 ` 1474` ``` case MInf with assms[of "0"] show ?thesis by force ``` hoelzl@41979 ` 1475` ``` next ``` hoelzl@41979 ` 1476` ``` case (real r) ``` hoelzl@41979 ` 1477` ``` with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < extreal (real n)" by auto ``` hoelzl@41979 ` 1478` ``` moreover from assms[of n] guess i .. ``` hoelzl@41979 ` 1479` ``` ultimately show ?thesis ``` hoelzl@41979 ` 1480` ``` by (auto intro!: bexI[of _ i]) ``` hoelzl@41979 ` 1481` ``` qed ``` hoelzl@41979 ` 1482` ```qed ``` hoelzl@41979 ` 1483` hoelzl@41979 ` 1484` ```lemma Sup_countable_SUPR: ``` hoelzl@41979 ` 1485` ``` assumes "A \ {}" ``` hoelzl@41979 ` 1486` ``` shows "\f::nat \ extreal. range f \ A \ Sup A = SUPR UNIV f" ``` hoelzl@41979 ` 1487` ```proof (cases "Sup A") ``` hoelzl@41979 ` 1488` ``` case (real r) ``` hoelzl@41979 ` 1489` ``` have "\n::nat. \x. x \ A \ Sup A < x + 1 / extreal (real n)" ``` hoelzl@41979 ` 1490` ``` proof ``` hoelzl@41979 ` 1491` ``` fix n ::nat have "\x\A. Sup A - 1 / extreal (real n) < x" ``` hoelzl@41979 ` 1492` ``` using assms real by (intro Sup_extreal_close) (auto simp: one_extreal_def) ``` hoelzl@41979 ` 1493` ``` then guess x .. ``` hoelzl@41979 ` 1494` ``` then show "\x. x \ A \ Sup A < x + 1 / extreal (real n)" ``` hoelzl@41979 ` 1495` ``` by (auto intro!: exI[of _ x] simp: extreal_minus_less_iff) ``` hoelzl@41979 ` 1496` ``` qed ``` hoelzl@41979 ` 1497` ``` from choice[OF this] guess f .. note f = this ``` hoelzl@41979 ` 1498` ``` have "SUPR UNIV f = Sup A" ``` hoelzl@41979 ` 1499` ``` proof (rule extreal_SUPI) ``` hoelzl@41979 ` 1500` ``` fix i show "f i \ Sup A" using f ``` hoelzl@41979 ` 1501` ``` by (auto intro!: complete_lattice_class.Sup_upper) ``` hoelzl@41979 ` 1502` ``` next ``` hoelzl@41979 ` 1503` ``` fix y assume bound: "\i. i \ UNIV \ f i \ y" ``` hoelzl@41979 ` 1504` ``` show "Sup A \ y" ``` hoelzl@41979 ` 1505` ``` proof (rule extreal_le_epsilon, intro allI impI) ``` hoelzl@41979 ` 1506` ``` fix e :: extreal assume "0 < e" ``` hoelzl@41979 ` 1507` ``` show "Sup A \ y + e" ``` hoelzl@41979 ` 1508` ``` proof (cases e) ``` hoelzl@41979 ` 1509` ``` case (real r) ``` hoelzl@41979 ` 1510` ``` hence "0 < r" using `0 < e` by auto ``` hoelzl@41979 ` 1511` ``` then obtain n ::nat where *: "1 / real n < r" "0 < n" ``` hoelzl@41979 ` 1512` ``` using ex_inverse_of_nat_less by (auto simp: real_eq_of_nat inverse_eq_divide) ``` hoelzl@41979 ` 1513` ``` have "Sup A \ f n + 1 / extreal (real n)" using f[THEN spec, of n] by auto ``` hoelzl@41979 ` 1514` ``` also have "1 / extreal (real n) \ e" using real * by (auto simp: one_extreal_def ) ``` hoelzl@41979 ` 1515` ``` with bound have "f n + 1 / extreal (real n) \ y + e" by (rule add_mono) simp ``` hoelzl@41979 ` 1516` ``` finally show "Sup A \ y + e" . ``` hoelzl@41979 ` 1517` ``` qed (insert `0 < e`, auto) ``` hoelzl@41979 ` 1518` ``` qed ``` hoelzl@41979 ` 1519` ``` qed ``` hoelzl@41979 ` 1520` ``` with f show ?thesis by (auto intro!: exI[of _ f]) ``` hoelzl@41979 ` 1521` ```next ``` hoelzl@41979 ` 1522` ``` case PInf ``` hoelzl@41979 ` 1523` ``` from `A \ {}` obtain x where "x \ A" by auto ``` hoelzl@41979 ` 1524` ``` show ?thesis ``` hoelzl@41979 ` 1525` ``` proof cases ``` hoelzl@41979 ` 1526` ``` assume "\ \ A" ``` hoelzl@41979 ` 1527` ``` moreover then have "\ \ Sup A" by (intro complete_lattice_class.Sup_upper) ``` hoelzl@41979 ` 1528` ``` ultimately show ?thesis by (auto intro!: exI[of _ "\x. \"]) ``` hoelzl@41979 ` 1529` ``` next ``` hoelzl@41979 ` 1530` ``` assume "\ \ A" ``` hoelzl@41979 ` 1531` ``` have "\x\A. 0 \ x" ``` hoelzl@41979 ` 1532` ``` by (metis Infty_neq_0 PInf complete_lattice_class.Sup_least extreal_infty_less_eq2 linorder_linear) ``` hoelzl@41979 ` 1533` ``` then obtain x where "x \ A" "0 \ x" by auto ``` hoelzl@41979 ` 1534` ``` have "\n::nat. \f. f \ A \ x + extreal (real n) \ f" ``` hoelzl@41979 ` 1535` ``` proof (rule ccontr) ``` hoelzl@41979 ` 1536` ``` assume "\ ?thesis" ``` hoelzl@41979 ` 1537` ``` then have "\n::nat. Sup A \ x + extreal (real n)" ``` hoelzl@41979 ` 1538` ``` by (simp add: Sup_le_iff not_le less_imp_le Ball_def) (metis less_imp_le) ``` hoelzl@41979 ` 1539` ``` then show False using `x \ A` `\ \ A` PInf ``` hoelzl@41979 ` 1540` ``` by(cases x) auto ``` hoelzl@41979 ` 1541` ``` qed ``` hoelzl@41979 ` 1542` ``` from choice[OF this] guess f .. note f = this ``` hoelzl@41979 ` 1543` ``` have "SUPR UNIV f = \" ``` hoelzl@41979 ` 1544` ``` proof (rule SUP_PInfty) ``` hoelzl@41979 ` 1545` ``` fix n :: nat show "\i\UNIV. extreal (real n) \ f i" ``` hoelzl@41979 ` 1546` ``` using f[THEN spec, of n] `0 \ x` ``` hoelzl@41979 ` 1547` ``` by (cases rule: extreal2_cases[of "f n" x]) (auto intro!: exI[of _ n]) ``` hoelzl@41979 ` 1548` ``` qed ``` hoelzl@41979 ` 1549` ``` then show ?thesis using f PInf by (auto intro!: exI[of _ f]) ``` hoelzl@41979 ` 1550` ``` qed ``` hoelzl@41979 ` 1551` ```next ``` hoelzl@41979 ` 1552` ``` case MInf ``` hoelzl@41979 ` 1553` ``` with `A \ {}` have "A = {-\}" by (auto simp: Sup_eq_MInfty) ``` hoelzl@41979 ` 1554` ``` then show ?thesis using MInf by (auto intro!: exI[of _ "\x. -\"]) ``` hoelzl@41979 ` 1555` ```qed ``` hoelzl@41979 ` 1556` hoelzl@41979 ` 1557` ```lemma SUPR_countable_SUPR: ``` hoelzl@41979 ` 1558` ``` "A \ {} \ \f::nat \ extreal. range f \ g`A \ SUPR A g = SUPR UNIV f" ``` hoelzl@41979 ` 1559` ``` using Sup_countable_SUPR[of "g`A"] by (auto simp: SUPR_def) ``` hoelzl@41979 ` 1560` hoelzl@41979 ` 1561` hoelzl@41979 ` 1562` ```lemma Sup_extreal_cadd: ``` hoelzl@41979 ` 1563` ``` fixes A :: "extreal set" assumes "A \ {}" and "a \ -\" ``` hoelzl@41979 ` 1564` ``` shows "Sup ((\x. a + x) ` A) = a + Sup A" ``` hoelzl@41979 ` 1565` ```proof (rule antisym) ``` hoelzl@41979 ` 1566` ``` have *: "\a::extreal. \A. Sup ((\x. a + x) ` A) \ a + Sup A" ``` hoelzl@41979 ` 1567` ``` by (auto intro!: add_mono complete_lattice_class.Sup_least complete_lattice_class.Sup_upper) ``` hoelzl@41979 ` 1568` ``` then show "Sup ((\x. a + x) ` A) \ a + Sup A" . ``` hoelzl@41979 ` 1569` ``` show "a + Sup A \ Sup ((\x. a + x) ` A)" ``` hoelzl@41979 ` 1570` ``` proof (cases a) ``` hoelzl@41979 ` 1571` ``` case PInf with `A \ {}` show ?thesis by (auto simp: image_constant) ``` hoelzl@41979 ` 1572` ``` next ``` hoelzl@41979 ` 1573` ``` case (real r) ``` hoelzl@41979 ` 1574` ``` then have **: "op + (- a) ` op + a ` A = A" ``` hoelzl@41979 ` 1575` ``` by (auto simp: image_iff ac_simps zero_extreal_def[symmetric]) ``` hoelzl@41979 ` 1576` ``` from *[of "-a" "(\x. a + x) ` A"] real show ?thesis unfolding ** ``` hoelzl@41979 ` 1577` ``` by (cases rule: extreal2_cases[of "Sup A" "Sup (op + a ` A)"]) auto ``` hoelzl@41979 ` 1578` ``` qed (insert `a \ -\`, auto) ``` hoelzl@41979 ` 1579` ```qed ``` hoelzl@41979 ` 1580` hoelzl@41979 ` 1581` ```lemma Sup_extreal_cminus: ``` hoelzl@41979 ` 1582` ``` fixes A :: "extreal set" assumes "A \ {}" and "a \ -\" ``` hoelzl@41979 ` 1583` ``` shows "Sup ((\x. a - x) ` A) = a - Inf A" ``` hoelzl@41979 ` 1584` ``` using Sup_extreal_cadd[of "uminus ` A" a] assms ``` hoelzl@41979 ` 1585` ``` by (simp add: comp_def image_image minus_extreal_def ``` hoelzl@41979 ` 1586` ``` extreal_Sup_uminus_image_eq) ``` hoelzl@41979 ` 1587` hoelzl@41979 ` 1588` ```lemma SUPR_extreal_cminus: ``` hoelzl@41979 ` 1589` ``` fixes A assumes "A \ {}" and "a \ -\" ``` hoelzl@41979 ` 1590` ``` shows "(SUP x:A. a - f x) = a - (INF x:A. f x)" ``` hoelzl@41979 ` 1591` ``` using Sup_extreal_cminus[of "f`A" a] assms ``` hoelzl@41979 ` 1592` ``` unfolding SUPR_def INFI_def image_image by auto ``` hoelzl@41979 ` 1593` hoelzl@41979 ` 1594` ```lemma Inf_extreal_cminus: ``` hoelzl@41979 ` 1595` ``` fixes A :: "extreal set" assumes "A \ {}" and "\a\ \ \" ``` hoelzl@41979 ` 1596` ``` shows "Inf ((\x. a - x) ` A) = a - Sup A" ``` hoelzl@41979 ` 1597` ```proof - ``` hoelzl@41979 ` 1598` ``` { fix x have "-a - -x = -(a - x)" using assms by (cases x) auto } ``` hoelzl@41979 ` 1599` ``` moreover then have "(\x. -a - x)`uminus`A = uminus ` (\x. a - x) ` A" ``` hoelzl@41979 ` 1600` ``` by (auto simp: image_image) ``` hoelzl@41979 ` 1601` ``` ultimately show ?thesis ``` hoelzl@41979 ` 1602` ``` using Sup_extreal_cminus[of "uminus ` A" "-a"] assms ``` hoelzl@41979 ` 1603` ``` by (auto simp add: extreal_Sup_uminus_image_eq extreal_Inf_uminus_image_eq) ``` hoelzl@41979 ` 1604` ```qed ``` hoelzl@41979 ` 1605` hoelzl@41979 ` 1606` ```lemma INFI_extreal_cminus: ``` hoelzl@41979 ` 1607` ``` fixes A assumes "A \ {}" and "\a\ \ \" ``` hoelzl@41979 ` 1608` ``` shows "(INF x:A. a - f x) = a - (SUP x:A. f x)" ``` hoelzl@41979 ` 1609` ``` using Inf_extreal_cminus[of "f`A" a] assms ``` hoelzl@41979 ` 1610` ``` unfolding SUPR_def INFI_def image_image ``` hoelzl@41979 ` 1611` ``` by auto ``` hoelzl@41979 ` 1612` hoelzl@41973 ` 1613` ```subsection "Limits on @{typ extreal}" ``` hoelzl@41973 ` 1614` hoelzl@41973 ` 1615` ```subsubsection "Topological space" ``` hoelzl@41973 ` 1616` hoelzl@41973 ` 1617` ```instantiation extreal :: topological_space ``` hoelzl@41973 ` 1618` ```begin ``` hoelzl@41973 ` 1619` hoelzl@41975 ` 1620` ```definition "open A \ open (extreal -` A) ``` hoelzl@41973 ` 1621` ``` \ (\ \ A \ (\x. {extreal x <..} \ A)) ``` hoelzl@41973 ` 1622` ``` \ (-\ \ A \ (\x. {.. A))" ``` hoelzl@41973 ` 1623` hoelzl@41975 ` 1624` ```lemma open_PInfty: "open A \ \ \ A \ (\x. {extreal x<..} \ A)" ``` hoelzl@41973 ` 1625` ``` unfolding open_extreal_def by auto ``` hoelzl@41973 ` 1626` hoelzl@41975 ` 1627` ```lemma open_MInfty: "open A \ -\ \ A \ (\x. {.. A)" ``` hoelzl@41973 ` 1628` ``` unfolding open_extreal_def by auto ``` hoelzl@41973 ` 1629` hoelzl@41975 ` 1630` ```lemma open_PInfty2: assumes "open A" "\ \ A" obtains x where "{extreal x<..} \ A" ``` hoelzl@41973 ` 1631` ``` using open_PInfty[OF assms] by auto ``` hoelzl@41973 ` 1632` hoelzl@41975 ` 1633` ```lemma open_MInfty2: assumes "open A" "-\ \ A" obtains x where "{.. A" ``` hoelzl@41973 ` 1634` ``` using open_MInfty[OF assms] by auto ``` hoelzl@41973 ` 1635` hoelzl@41975 ` 1636` ```lemma extreal_openE: assumes "open A" obtains x y where ``` hoelzl@41975 ` 1637` ``` "open (extreal -` A)" ``` hoelzl@41975 ` 1638` ``` "\ \ A \ {extreal x<..} \ A" ``` hoelzl@41975 ` 1639` ``` "-\ \ A \ {.. A" ``` hoelzl@41973 ` 1640` ``` using assms open_extreal_def by auto ``` hoelzl@41973 ` 1641` hoelzl@41973 ` 1642` ```instance ``` hoelzl@41973 ` 1643` ```proof ``` hoelzl@41973 ` 1644` ``` let ?U = "UNIV::extreal set" ``` hoelzl@41973 ` 1645` ``` show "open ?U" unfolding open_extreal_def ``` hoelzl@41975 ` 1646` ``` by (auto intro!: exI[of _ 0]) ``` hoelzl@41973 ` 1647` ```next ``` hoelzl@41973 ` 1648` ``` fix S T::"extreal set" assume "open S" and "open T" ``` hoelzl@41975 ` 1649` ``` from `open S`[THEN extreal_openE] guess xS yS . ``` hoelzl@41975 ` 1650` ``` moreover from `open T`[THEN extreal_openE] guess xT yT . ``` hoelzl@41975 ` 1651` ``` ultimately have ``` hoelzl@41975 ` 1652` ``` "open (extreal -` (S \ T))" ``` hoelzl@41975 ` 1653` ``` "\ \ S \ T \ {extreal (max xS xT) <..} \ S \ T" ``` hoelzl@41975 ` 1654` ``` "-\ \ S \ T \ {..< extreal (min yS yT)} \ S \ T" ``` hoelzl@41975 ` 1655` ``` by auto ``` hoelzl@41975 ` 1656` ``` then show "open (S Int T)" unfolding open_extreal_def by blast ``` hoelzl@41973 ` 1657` ```next ``` hoelzl@41975 ` 1658` ``` fix K :: "extreal set set" assume "\S\K. open S" ``` hoelzl@41975 ` 1659` ``` then have *: "\S. \x y. S \ K \ open (extreal -` S) \ ``` hoelzl@41975 ` 1660` ``` (\ \ S \ {extreal x <..} \ S) \ (-\ \ S \ {..< extreal y} \ S)" ``` hoelzl@41975 ` 1661` ``` by (auto simp: open_extreal_def) ``` hoelzl@41975 ` 1662` ``` then show "open (Union K)" unfolding open_extreal_def ``` hoelzl@41975 ` 1663` ``` proof (intro conjI impI) ``` hoelzl@41975 ` 1664` ``` show "open (extreal -` \K)" ``` hoelzl@41975 ` 1665` ``` using *[unfolded choice_iff] by (auto simp: vimage_Union) ``` hoelzl@41975 ` 1666` ``` qed ((metis UnionE Union_upper subset_trans *)+) ``` hoelzl@41973 ` 1667` ```qed ``` hoelzl@41973 ` 1668` ```end ``` hoelzl@41973 ` 1669` hoelzl@41976 ` 1670` ```lemma open_extreal: "open S \ open (extreal ` S)" ``` hoelzl@41976 ` 1671` ``` by (auto simp: inj_vimage_image_eq open_extreal_def) ``` hoelzl@41976 ` 1672` hoelzl@41976 ` 1673` ```lemma open_extreal_vimage: "open S \ open (extreal -` S)" ``` hoelzl@41976 ` 1674` ``` unfolding open_extreal_def by auto ``` hoelzl@41976 ` 1675` hoelzl@41975 ` 1676` ```lemma continuous_on_extreal[intro, simp]: "continuous_on A extreal" ``` hoelzl@41975 ` 1677` ``` unfolding continuous_on_topological open_extreal_def by auto ``` hoelzl@41975 ` 1678` hoelzl@41975 ` 1679` ```lemma continuous_at_extreal[intro, simp]: "continuous (at x) extreal" ``` hoelzl@41975 ` 1680` ``` using continuous_on_eq_continuous_at[of UNIV] by auto ``` hoelzl@41975 ` 1681` hoelzl@41975 ` 1682` ```lemma continuous_within_extreal[intro, simp]: "x \ A \ continuous (at x within A) extreal" ``` hoelzl@41975 ` 1683` ``` using continuous_on_eq_continuous_within[of A] by auto ``` hoelzl@41975 ` 1684` hoelzl@41975 ` 1685` ```lemma open_extreal_lessThan[intro, simp]: "open {..< a :: extreal}" ``` hoelzl@41975 ` 1686` ```proof - ``` hoelzl@41975 ` 1687` ``` have "\x. extreal -` {..} = UNIV" "extreal -` {..< -\} = {}" by auto ``` hoelzl@41975 ` 1689` ``` then show ?thesis by (cases a) (auto simp: open_extreal_def) ``` hoelzl@41975 ` 1690` ```qed ``` hoelzl@41975 ` 1691` hoelzl@41975 ` 1692` ```lemma open_extreal_greaterThan[intro, simp]: ``` hoelzl@41973 ` 1693` ``` "open {a :: extreal <..}" ``` hoelzl@41975 ` 1694` ```proof - ``` hoelzl@41975 ` 1695` ``` have "\x. extreal -` {extreal x<..} = {x<..}" ``` hoelzl@41975 ` 1696` ``` "extreal -` {\<..} = {}" "extreal -` {-\<..} = UNIV" by auto ``` hoelzl@41975 ` 1697` ``` then show ?thesis by (cases a) (auto simp: open_extreal_def) ``` hoelzl@41975 ` 1698` ```qed ``` hoelzl@41975 ` 1699` hoelzl@41975 ` 1700` ```lemma extreal_open_greaterThanLessThan[intro, simp]: "open {a::extreal <..< b}" ``` hoelzl@41973 ` 1701` ``` unfolding greaterThanLessThan_def by auto ``` hoelzl@41973 ` 1702` hoelzl@41973 ` 1703` ```lemma closed_extreal_atLeast[simp, intro]: "closed {a :: extreal ..}" ``` hoelzl@41973 ` 1704` ```proof - ``` hoelzl@41973 ` 1705` ``` have "- {a ..} = {..< a}" by auto ``` hoelzl@41973 ` 1706` ``` then show "closed {a ..}" ``` hoelzl@41973 ` 1707` ``` unfolding closed_def using open_extreal_lessThan by auto ``` hoelzl@41973 ` 1708` ```qed ``` hoelzl@41973 ` 1709` hoelzl@41973 ` 1710` ```lemma closed_extreal_atMost[simp, intro]: "closed {.. b :: extreal}" ``` hoelzl@41973 ` 1711` ```proof - ``` hoelzl@41973 ` 1712` ``` have "- {.. b} = {b <..}" by auto ``` hoelzl@41973 ` 1713` ``` then show "closed {.. b}" ``` hoelzl@41973 ` 1714` ``` unfolding closed_def using open_extreal_greaterThan by auto ``` hoelzl@41973 ` 1715` ```qed ``` hoelzl@41973 ` 1716` hoelzl@41973 ` 1717` ```lemma closed_extreal_atLeastAtMost[simp, intro]: ``` hoelzl@41973 ` 1718` ``` shows "closed {a :: extreal .. b}" ``` hoelzl@41973 ` 1719` ``` unfolding atLeastAtMost_def by auto ``` hoelzl@41973 ` 1720` hoelzl@41973 ` 1721` ```lemma closed_extreal_singleton: ``` hoelzl@41973 ` 1722` ``` "closed {a :: extreal}" ``` hoelzl@41973 ` 1723` ```by (metis atLeastAtMost_singleton closed_extreal_atLeastAtMost) ``` hoelzl@41973 ` 1724` hoelzl@41973 ` 1725` ```lemma extreal_open_cont_interval: ``` hoelzl@41976 ` 1726` ``` assumes "open S" "x \ S" "\x\ \ \" ``` hoelzl@41973 ` 1727` ``` obtains e where "e>0" "{x-e <..< x+e} \ S" ``` hoelzl@41973 ` 1728` ```proof- ``` hoelzl@41975 ` 1729` ``` from `open S` have "open (extreal -` S)" by (rule extreal_openE) ``` hoelzl@41976 ` 1730` ``` then obtain e where "0 < e" and e: "ball (real x) e \ extreal -` S" ``` hoelzl@41976 ` 1731` ``` using assms unfolding open_contains_ball by force ``` hoelzl@41975 ` 1732` ``` show thesis ``` hoelzl@41975 ` 1733` ``` proof (intro that subsetI) ``` hoelzl@41975 ` 1734` ``` show "0 < extreal e" using `0 < e` by auto ``` hoelzl@41975 ` 1735` ``` fix y assume "y \ {x - extreal e<.. ball (real x) e" ``` hoelzl@41976 ` 1737` ``` by (cases y) (auto simp: ball_def dist_real_def) ``` hoelzl@41975 ` 1738` ``` then show "y \ S" using e by auto ``` hoelzl@41975 ` 1739` ``` qed ``` hoelzl@41973 ` 1740` ```qed ``` hoelzl@41973 ` 1741` hoelzl@41973 ` 1742` ```lemma extreal_open_cont_interval2: ``` hoelzl@41976 ` 1743` ``` assumes "open S" "x \ S" and x: "\x\ \ \" ``` hoelzl@41973 ` 1744` ``` obtains a b where "a < x" "x < b" "{a <..< b} \ S" ``` hoelzl@41973 ` 1745` ```proof- ``` hoelzl@41973 ` 1746` ``` guess e using extreal_open_cont_interval[OF assms] . ``` hoelzl@41973 ` 1747` ``` with that[of "x-e" "x+e"] extreal_between[OF x, of e] ``` hoelzl@41973 ` 1748` ``` show thesis by auto ``` hoelzl@41973 ` 1749` ```qed ``` hoelzl@41973 ` 1750` hoelzl@41973 ` 1751` ```lemma extreal_open_uminus: ``` hoelzl@41973 ` 1752` ``` fixes S :: "extreal set" ``` hoelzl@41973 ` 1753` ``` assumes "open S" ``` hoelzl@41973 ` 1754` ``` shows "open (uminus ` S)" ``` hoelzl@41975 ` 1755` ``` unfolding open_extreal_def ``` hoelzl@41975 ` 1756` ```proof (intro conjI impI) ``` hoelzl@41975 ` 1757` ``` obtain x y where S: "open (extreal -` S)" ``` hoelzl@41975 ` 1758` ``` "\ \ S \ {extreal x<..} \ S" "-\ \ S \ {..< extreal y} \ S" ``` hoelzl@41975 ` 1759` ``` using `open S` unfolding open_extreal_def by auto ``` hoelzl@41975 ` 1760` ``` have "extreal -` uminus ` S = uminus ` (extreal -` S)" ``` hoelzl@41975 ` 1761` ``` proof safe ``` hoelzl@41975 ` 1762` ``` fix x y assume "extreal x = - y" "y \ S" ``` hoelzl@41975 ` 1763` ``` then show "x \ uminus ` extreal -` S" by (cases y) auto ``` hoelzl@41975 ` 1764` ``` next ``` hoelzl@41975 ` 1765` ``` fix x assume "extreal x \ S" ``` hoelzl@41975 ` 1766` ``` then show "- x \ extreal -` uminus ` S" ``` hoelzl@41975 ` 1767` ``` by (auto intro: image_eqI[of _ _ "extreal x"]) ``` hoelzl@41975 ` 1768` ``` qed ``` hoelzl@41975 ` 1769` ``` then show "open (extreal -` uminus ` S)" ``` hoelzl@41975 ` 1770` ``` using S by (auto intro: open_negations) ``` hoelzl@41975 ` 1771` ``` { assume "\ \ uminus ` S" ``` hoelzl@41975 ` 1772` ``` then have "-\ \ S" by (metis image_iff extreal_uminus_uminus) ``` hoelzl@41975 ` 1773` ``` then have "uminus ` {.. uminus ` S" using S by (intro image_mono) auto ``` hoelzl@41975 ` 1774` ``` then show "\x. {extreal x<..} \ uminus ` S" using extreal_uminus_lessThan by auto } ``` hoelzl@41975 ` 1775` ``` { assume "-\ \ uminus ` S" ``` hoelzl@41975 ` 1776` ``` then have "\ : S" by (metis image_iff extreal_uminus_uminus) ``` hoelzl@41975 ` 1777` ``` then have "uminus ` {extreal x<..} <= uminus ` S" using S by (intro image_mono) auto ``` hoelzl@41975 ` 1778` ``` then show "\y. {.. (open {a :: extreal})" ``` hoelzl@41973 ` 1795` ```proof(rule ccontr) ``` hoelzl@41976 ` 1796` ``` assume "\ \ open {a}" hence a: "open {a}" by auto ``` hoelzl@41976 ` 1797` ``` show False ``` hoelzl@41976 ` 1798` ``` proof (cases a) ``` hoelzl@41976 ` 1799` ``` case MInf ``` hoelzl@41973 ` 1800` ``` then obtain y where "{..)` by auto ``` hoelzl@41976 ` 1803` ``` next ``` hoelzl@41976 ` 1804` ``` case PInf ``` hoelzl@41973 ` 1805` ``` then obtain y where "{extreal y<..} <= {a}" using a open_PInfty2[of "{a}"] by auto ``` hoelzl@41973 ` 1806` ``` hence "extreal(y+1):{a}" apply (subst subsetD[of "{extreal y<..}"]) by auto ``` hoelzl@41976 ` 1807` ``` then show False using `a=\` by auto ``` hoelzl@41976 ` 1808` ``` next ``` hoelzl@41976 ` 1809` ``` case (real r) then have fin: "\a\ \ \" by simp ``` hoelzl@41976 ` 1810` ``` from extreal_open_cont_interval[OF a singletonI this] guess e . note e = this ``` hoelzl@41973 ` 1811` ``` then obtain b where b_def: "a S" hence a: "open (-S)" "Inf S:(- S)" using assms by auto ``` hoelzl@41976 ` 1824` ``` show False ``` hoelzl@41976 ` 1825` ``` proof (cases "Inf S") ``` hoelzl@41976 ` 1826` ``` case MInf hence "(-\) : - S" using a by auto ``` hoelzl@41976 ` 1827` ``` then obtain y where "{..}" by (metis Inf_eq_PInfty assms(2)) ``` hoelzl@41976 ` 1833` ``` then show False by (metis `Inf S ~: S` insert_code mem_def PInf) ``` hoelzl@41976 ` 1834` ``` next ``` hoelzl@41976 ` 1835` ``` case (real r) then have fin: "\Inf S\ \ \" by simp ``` hoelzl@41976 ` 1836` ``` from extreal_open_cont_interval[OF a this] guess e . note e = this ``` hoelzl@41976 ` 1837` ``` { fix x assume "x:S" hence "x>=Inf S" by (rule complete_lattice_class.Inf_lower) ``` hoelzl@41976 ` 1838` ``` hence *: "x>Inf S-e" using e by (metis fin extreal_between(1) order_less_le_trans) ``` hoelzl@41976 ` 1839` ``` { assume "x=Inf S+e" by (metis linorder_le_less_linear) ``` hoelzl@41976 ` 1842` ``` } hence "Inf S + e <= Inf S" by (metis le_Inf_iff) ``` hoelzl@41976 ` 1843` ``` then show False using real e by (cases e) auto ``` hoelzl@41976 ` 1844` ``` qed ``` hoelzl@41973 ` 1845` ```qed ``` hoelzl@41973 ` 1846` hoelzl@41973 ` 1847` ```lemma extreal_closed_contains_Sup: ``` hoelzl@41973 ` 1848` ``` fixes S :: "extreal set" ``` hoelzl@41973 ` 1849` ``` assumes "closed S" "S ~= {}" ``` hoelzl@41973 ` 1850` ``` shows "Sup S : S" ``` hoelzl@41973 ` 1851` ```proof- ``` hoelzl@41973 ` 1852` ``` have "closed (uminus ` S)" by (metis assms(1) extreal_closed_uminus) ``` hoelzl@41973 ` 1853` ``` hence "Inf (uminus ` S) : uminus ` S" using assms extreal_closed_contains_Inf[of "uminus ` S"] by auto ``` hoelzl@41973 ` 1854` ``` hence "- Sup S : uminus ` S" using extreal_Sup_uminus_image_eq[of "uminus ` S"] by (auto simp: image_image) ``` hoelzl@41973 ` 1855` ``` thus ?thesis by (metis imageI extreal_uminus_uminus extreal_minus_minus_image) ``` hoelzl@41973 ` 1856` ```qed ``` hoelzl@41973 ` 1857` hoelzl@41973 ` 1858` ```lemma extreal_open_closed_aux: ``` hoelzl@41973 ` 1859` ``` fixes S :: "extreal set" ``` hoelzl@41973 ` 1860` ``` assumes "open S" "closed S" ``` hoelzl@41973 ` 1861` ``` assumes S: "(-\) ~: S" ``` hoelzl@41973 ` 1862` ``` shows "S = {}" ``` hoelzl@41973 ` 1863` ```proof(rule ccontr) ``` hoelzl@41973 ` 1864` ``` assume "S ~= {}" ``` hoelzl@41973 ` 1865` ``` hence *: "(Inf S):S" by (metis assms(2) extreal_closed_contains_Inf) ``` hoelzl@41973 ` 1866` ``` { assume "Inf S=(-\)" hence False using * assms(3) by auto } ``` hoelzl@41973 ` 1867` ``` moreover ``` hoelzl@41973 ` 1868` ``` { assume "Inf S=\" hence "S={\}" by (metis Inf_eq_PInfty `S ~= {}`) ``` hoelzl@41973 ` 1869` ``` hence False by (metis assms(1) not_open_extreal_singleton) } ``` hoelzl@41973 ` 1870` ``` moreover ``` hoelzl@41976 ` 1871` ``` { assume fin: "\Inf S\ \ \" ``` hoelzl@41973 ` 1872` ``` from extreal_open_cont_interval[OF assms(1) * fin] guess e . note e = this ``` hoelzl@41973 ` 1873` ``` then obtain b where b_def: "Inf S-e (S = {} | S = UNIV)" ``` hoelzl@41973 ` 1885` ```proof- ``` hoelzl@41973 ` 1886` ```{ assume lhs: "open S & closed S" ``` hoelzl@41973 ` 1887` ``` { assume "(-\) ~: S" hence "S={}" using lhs extreal_open_closed_aux by auto } ``` hoelzl@41973 ` 1888` ``` moreover ``` hoelzl@41973 ` 1889` ``` { assume "(-\) : S" hence "(- S)={}" using lhs extreal_open_closed_aux[of "-S"] by auto } ``` hoelzl@41973 ` 1890` ``` ultimately have "S = {} | S = UNIV" by auto ``` hoelzl@41973 ` 1891` ```} thus ?thesis by auto ``` hoelzl@41973 ` 1892` ```qed ``` hoelzl@41973 ` 1893` hoelzl@41973 ` 1894` hoelzl@41973 ` 1895` ```instance extreal :: t2_space ``` hoelzl@41973 ` 1896` ```proof ``` hoelzl@41973 ` 1897` ``` fix x y :: extreal assume "x ~= y" ``` hoelzl@41973 ` 1898` ``` let "?P x (y::extreal)" = "EX U V. open U & open V & x : U & y : V & U Int V = {}" ``` hoelzl@41973 ` 1899` hoelzl@41973 ` 1900` ``` { fix x y :: extreal assume "x < y" ``` hoelzl@41973 ` 1901` ``` from extreal_dense[OF this] obtain z where z: "x < z" "z < y" by auto ``` hoelzl@41973 ` 1902` ``` have "?P x y" ``` hoelzl@41973 ` 1903` ``` apply (rule exI[of _ "{..n. extreal (f n)) ---> extreal x) net \ (f ---> x) net" (is "?l = ?r") ``` hoelzl@41973 ` 1921` ```proof (intro iffI topological_tendstoI) ``` hoelzl@41973 ` 1922` ``` fix S assume "?l" "open S" "x \ S" ``` hoelzl@41973 ` 1923` ``` then show "eventually (\x. f x \ S) net" ``` hoelzl@41973 ` 1924` ``` using `?l`[THEN topological_tendstoD, OF open_extreal, OF `open S`] ``` hoelzl@41973 ` 1925` ``` by (simp add: inj_image_mem_iff) ``` hoelzl@41973 ` 1926` ```next ``` hoelzl@41973 ` 1927` ``` fix S assume "?r" "open S" "extreal x \ S" ``` hoelzl@41973 ` 1928` ``` show "eventually (\x. extreal (f x) \ S) net" ``` hoelzl@41975 ` 1929` ``` using `?r`[THEN topological_tendstoD, OF open_extreal_vimage, OF `open S`] ``` hoelzl@41975 ` 1930` ``` using `extreal x \ S` by auto ``` hoelzl@41973 ` 1931` ```qed ``` hoelzl@41973 ` 1932` hoelzl@41973 ` 1933` ```lemma lim_real_of_extreal[simp]: ``` hoelzl@41973 ` 1934` ``` assumes lim: "(f ---> extreal x) net" ``` hoelzl@41973 ` 1935` ``` shows "((\x. real (f x)) ---> x) net" ``` hoelzl@41973 ` 1936` ```proof (intro topological_tendstoI) ``` hoelzl@41973 ` 1937` ``` fix S assume "open S" "x \ S" ``` hoelzl@41973 ` 1938` ``` then have S: "open S" "extreal x \ extreal ` S" ``` hoelzl@41973 ` 1939` ``` by (simp_all add: inj_image_mem_iff) ``` hoelzl@41973 ` 1940` ``` have "\x. f x \ extreal ` S \ real (f x) \ S" by auto ``` hoelzl@41973 ` 1941` ``` from this lim[THEN topological_tendstoD, OF open_extreal, OF S] ``` hoelzl@41973 ` 1942` ``` show "eventually (\x. real (f x) \ S) net" ``` hoelzl@41973 ` 1943` ``` by (rule eventually_mono) ``` hoelzl@41973 ` 1944` ```qed ``` hoelzl@41973 ` 1945` hoelzl@41973 ` 1946` ```lemma Lim_PInfty: "f ----> \ <-> (ALL B. EX N. ALL n>=N. f n >= extreal B)" (is "?l = ?r") ``` hoelzl@41973 ` 1947` ```proof assume ?r show ?l apply(rule topological_tendstoI) ``` hoelzl@41973 ` 1948` ``` unfolding eventually_sequentially ``` hoelzl@41973 ` 1949` ``` proof- fix S assume "open S" "\ : S" ``` hoelzl@41973 ` 1950` ``` from open_PInfty[OF this] guess B .. note B=this ``` hoelzl@41973 ` 1951` ``` from `?r`[rule_format,of "B+1"] guess N .. note N=this ``` hoelzl@41973 ` 1952` ``` show "EX N. ALL n>=N. f n : S" apply(rule_tac x=N in exI) ``` hoelzl@41973 ` 1953` ``` proof safe case goal1 ``` hoelzl@41973 ` 1954` ``` have "extreal B < extreal (B + 1)" by auto ``` hoelzl@41973 ` 1955` ``` also have "... <= f n" using goal1 N by auto ``` hoelzl@41973 ` 1956` ``` finally show ?case using B by fastsimp ``` hoelzl@41973 ` 1957` ``` qed ``` hoelzl@41973 ` 1958` ``` qed ``` hoelzl@41973 ` 1959` ```next assume ?l show ?r ``` hoelzl@41973 ` 1960` ``` proof fix B::real have "open {extreal B<..}" "\ : {extreal B<..}" by auto ``` hoelzl@41973 ` 1961` ``` from topological_tendstoD[OF `?l` this,unfolded eventually_sequentially] ``` hoelzl@41973 ` 1962` ``` guess N .. note N=this ``` hoelzl@41973 ` 1963` ``` show "EX N. ALL n>=N. extreal B <= f n" apply(rule_tac x=N in exI) using N by auto ``` hoelzl@41973 ` 1964` ``` qed ``` hoelzl@41973 ` 1965` ```qed ``` hoelzl@41973 ` 1966` hoelzl@41973 ` 1967` hoelzl@41973 ` 1968` ```lemma Lim_MInfty: "f ----> (-\) <-> (ALL B. EX N. ALL n>=N. f n <= extreal B)" (is "?l = ?r") ``` hoelzl@41973 ` 1969` ```proof assume ?r show ?l apply(rule topological_tendstoI) ``` hoelzl@41973 ` 1970` ``` unfolding eventually_sequentially ``` hoelzl@41973 ` 1971` ``` proof- fix S assume "open S" "(-\) : S" ``` hoelzl@41973 ` 1972` ``` from open_MInfty[OF this] guess B .. note B=this ``` hoelzl@41973 ` 1973` ``` from `?r`[rule_format,of "B-(1::real)"] guess N .. note N=this ``` hoelzl@41973 ` 1974` ``` show "EX N. ALL n>=N. f n : S" apply(rule_tac x=N in exI) ``` hoelzl@41973 ` 1975` ``` proof safe case goal1 ``` hoelzl@41973 ` 1976` ``` have "extreal (B - 1) >= f n" using goal1 N by auto ``` hoelzl@41973 ` 1977` ``` also have "... < extreal B" by auto ``` hoelzl@41973 ` 1978` ``` finally show ?case using B by fastsimp ``` hoelzl@41973 ` 1979` ``` qed ``` hoelzl@41973 ` 1980` ``` qed ``` hoelzl@41973 ` 1981` ```next assume ?l show ?r ``` hoelzl@41973 ` 1982` ``` proof fix B::real have "open {..) : {..=N. extreal B >= f n" apply(rule_tac x=N in exI) using N by auto ``` hoelzl@41973 ` 1986` ``` qed ``` hoelzl@41973 ` 1987` ```qed ``` hoelzl@41973 ` 1988` hoelzl@41973 ` 1989` hoelzl@41973 ` 1990` ```lemma Lim_bounded_PInfty: assumes lim:"f ----> l" and "!!n. f n <= extreal B" shows "l ~= \" ``` hoelzl@41973 ` 1991` ```proof(rule ccontr,unfold not_not) let ?B = "B + 1" assume as:"l=\" ``` hoelzl@41973 ` 1992` ``` from lim[unfolded this Lim_PInfty,rule_format,of "?B"] ``` hoelzl@41973 ` 1993` ``` guess N .. note N=this[rule_format,OF le_refl] ``` hoelzl@41973 ` 1994` ``` hence "extreal ?B <= extreal B" using assms(2)[of N] by(rule order_trans) ``` hoelzl@41973 ` 1995` ``` hence "extreal ?B < extreal ?B" apply (rule le_less_trans) by auto ``` hoelzl@41973 ` 1996` ``` thus False by auto ``` hoelzl@41973 ` 1997` ```qed ``` hoelzl@41973 ` 1998` hoelzl@41973 ` 1999` hoelzl@41973 ` 2000` ```lemma Lim_bounded_MInfty: assumes lim:"f ----> l" and "!!n. f n >= extreal B" shows "l ~= (-\)" ``` hoelzl@41973 ` 2001` ```proof(rule ccontr,unfold not_not) let ?B = "B - 1" assume as:"l=(-\)" ``` hoelzl@41973 ` 2002` ``` from lim[unfolded this Lim_MInfty,rule_format,of "?B"] ``` hoelzl@41973 ` 2003` ``` guess N .. note N=this[rule_format,OF le_refl] ``` hoelzl@41973 ` 2004` ``` hence "extreal B <= extreal ?B" using assms(2)[of N] order_trans[of "extreal B" "f N" "extreal(B - 1)"] by blast ``` hoelzl@41973 ` 2005` ``` thus False by auto ``` hoelzl@41973 ` 2006` ```qed ``` hoelzl@41973 ` 2007` hoelzl@41973 ` 2008` hoelzl@41973 ` 2009` ```lemma tendsto_explicit: ``` hoelzl@41973 ` 2010` ``` "f ----> f0 <-> (ALL S. open S --> f0 : S --> (EX N. ALL n>=N. f n : S))" ``` hoelzl@41973 ` 2011` ``` unfolding tendsto_def eventually_sequentially by auto ``` hoelzl@41973 ` 2012` hoelzl@41973 ` 2013` hoelzl@41973 ` 2014` ```lemma tendsto_obtains_N: ``` hoelzl@41973 ` 2015` ``` assumes "f ----> f0" ``` hoelzl@41973 ` 2016` ``` assumes "open S" "f0 : S" ``` hoelzl@41973 ` 2017` ``` obtains N where "ALL n>=N. f n : S" ``` hoelzl@41973 ` 2018` ``` using tendsto_explicit[of f f0] assms by auto ``` hoelzl@41973 ` 2019` hoelzl@41973 ` 2020` hoelzl@41973 ` 2021` ```lemma tail_same_limit: ``` hoelzl@41973 ` 2022` ``` fixes X Y N ``` hoelzl@41973 ` 2023` ``` assumes "X ----> L" "ALL n>=N. X n = Y n" ``` hoelzl@41973 ` 2024` ``` shows "Y ----> L" ``` hoelzl@41973 ` 2025` ```proof- ``` hoelzl@41973 ` 2026` ```{ fix S assume "open S" and "L:S" ``` hoelzl@41973 ` 2027` ``` from this obtain N1 where "ALL n>=N1. X n : S" ``` hoelzl@41973 ` 2028` ``` using assms unfolding tendsto_def eventually_sequentially by auto ``` hoelzl@41973 ` 2029` ``` hence "ALL n>=max N N1. Y n : S" using assms by auto ``` hoelzl@41973 ` 2030` ``` hence "EX N. ALL n>=N. Y n : S" apply(rule_tac x="max N N1" in exI) by auto ``` hoelzl@41973 ` 2031` ```} ``` hoelzl@41973 ` 2032` ```thus ?thesis using tendsto_explicit by auto ``` hoelzl@41973 ` 2033` ```qed ``` hoelzl@41973 ` 2034` hoelzl@41973 ` 2035` hoelzl@41973 ` 2036` ```lemma Lim_bounded_PInfty2: ``` hoelzl@41973 ` 2037` ```assumes lim:"f ----> l" and "ALL n>=N. f n <= extreal B" ``` hoelzl@41973 ` 2038` ```shows "l ~= \" ``` hoelzl@41973 ` 2039` ```proof- ``` hoelzl@41973 ` 2040` ``` def g == "(%n. if n>=N then f n else extreal B)" ``` hoelzl@41973 ` 2041` ``` hence "g ----> l" using tail_same_limit[of f l N g] lim by auto ``` hoelzl@41973 ` 2042` ``` moreover have "!!n. g n <= extreal B" using g_def assms by auto ``` hoelzl@41973 ` 2043` ``` ultimately show ?thesis using Lim_bounded_PInfty by auto ``` hoelzl@41973 ` 2044` ```qed ``` hoelzl@41973 ` 2045` hoelzl@41973 ` 2046` ```lemma Lim_bounded_extreal: ``` hoelzl@41973 ` 2047` ``` assumes lim:"f ----> (l :: extreal)" ``` hoelzl@41973 ` 2048` ``` and "ALL n>=M. f n <= C" ``` hoelzl@41973 ` 2049` ``` shows "l<=C" ``` hoelzl@41973 ` 2050` ```proof- ``` hoelzl@41973 ` 2051` ```{ assume "l=(-\)" hence ?thesis by auto } ``` hoelzl@41973 ` 2052` ```moreover ``` hoelzl@41973 ` 2053` ```{ assume "~(l=(-\))" ``` hoelzl@41973 ` 2054` ``` { assume "C=\" hence ?thesis by auto } ``` hoelzl@41973 ` 2055` ``` moreover ``` hoelzl@41973 ` 2056` ``` { assume "C=(-\)" hence "ALL n>=M. f n = (-\)" using assms by auto ``` hoelzl@41973 ` 2057` ``` hence "l=(-\)" using assms ``` hoelzl@41973 ` 2058` ``` Lim_unique[OF trivial_limit_sequentially] tail_same_limit[of "\n. -\" "-\" M f, OF tendsto_const] by auto ``` hoelzl@41973 ` 2059` ``` hence ?thesis by auto } ``` hoelzl@41973 ` 2060` ``` moreover ``` hoelzl@41973 ` 2061` ``` { assume "EX B. C = extreal B" ``` hoelzl@41973 ` 2062` ``` from this obtain B where B_def: "C=extreal B" by auto ``` hoelzl@41973 ` 2063` ``` hence "~(l=\)" using Lim_bounded_PInfty2 assms by auto ``` hoelzl@41973 ` 2064` ``` from this obtain m where m_def: "extreal m=l" using `~(l=(-\))` by (cases l) auto ``` hoelzl@41973 ` 2065` ``` from this obtain N where N_def: "ALL n>=N. f n : {extreal(m - 1) <..< extreal(m+1)}" ``` hoelzl@41973 ` 2066` ``` apply (subst tendsto_obtains_N[of f l "{extreal(m - 1) <..< extreal(m+1)}"]) using assms by auto ``` hoelzl@41973 ` 2067` ``` { fix n assume "n>=N" ``` hoelzl@41973 ` 2068` ``` hence "EX r. extreal r = f n" using N_def by (cases "f n") auto ``` hoelzl@41973 ` 2069` ``` } from this obtain g where g_def: "ALL n>=N. extreal (g n) = f n" by metis ``` hoelzl@41973 ` 2070` ``` hence "(%n. extreal (g n)) ----> l" using tail_same_limit[of f l N] assms by auto ``` hoelzl@41973 ` 2071` ``` hence *: "(%n. g n) ----> m" using m_def by auto ``` hoelzl@41973 ` 2072` ``` { fix n assume "n>=max N M" ``` hoelzl@41973 ` 2073` ``` hence "extreal (g n) <= extreal B" using assms g_def B_def by auto ``` hoelzl@41973 ` 2074` ``` hence "g n <= B" by auto ``` hoelzl@41973 ` 2075` ``` } hence "EX N. ALL n>=N. g n <= B" by blast ``` hoelzl@41973 ` 2076` ``` hence "m<=B" using * LIMSEQ_le_const2[of g m B] by auto ``` hoelzl@41973 ` 2077` ``` hence ?thesis using m_def B_def by auto ``` hoelzl@41973 ` 2078` ``` } ultimately have ?thesis by (cases C) auto ``` hoelzl@41973 ` 2079` ```} ultimately show ?thesis by blast ``` hoelzl@41973 ` 2080` ```qed ``` hoelzl@41973 ` 2081` hoelzl@41973 ` 2082` ```lemma real_of_extreal_0[simp]: "real (0::extreal) = 0" ``` hoelzl@41973 ` 2083` ``` unfolding real_of_extreal_def zero_extreal_def by simp ``` hoelzl@41973 ` 2084` hoelzl@41973 ` 2085` ```lemma real_of_extreal_mult[simp]: ``` hoelzl@41973 ` 2086` ``` fixes a b :: extreal shows "real (a * b) = real a * real b" ``` hoelzl@41973 ` 2087` ``` by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@41973 ` 2088` hoelzl@41973 ` 2089` ```lemma real_of_extreal_eq_0: ``` hoelzl@41973 ` 2090` ``` "real x = 0 \ x = \ \ x = -\ \ x = 0" ``` hoelzl@41973 ` 2091` ``` by (cases x) auto ``` hoelzl@41973 ` 2092` hoelzl@41973 ` 2093` ```lemma tendsto_extreal_realD: ``` hoelzl@41973 ` 2094` ``` fixes f :: "'a \ extreal" ``` hoelzl@41973 ` 2095` ``` assumes "x \ 0" and tendsto: "((\x. extreal (real (f x))) ---> x) net" ``` hoelzl@41973 ` 2096` ``` shows "(f ---> x) net" ``` hoelzl@41973 ` 2097` ```proof (intro topological_tendstoI) ``` hoelzl@41973 ` 2098` ``` fix S assume S: "open S" "x \ S" ``` hoelzl@41973 ` 2099` ``` with `x \ 0` have "open (S - {0})" "x \ S - {0}" by auto ``` hoelzl@41973 ` 2100` ``` from tendsto[THEN topological_tendstoD, OF this] ``` hoelzl@41973 ` 2101` ``` show "eventually (\x. f x \ S) net" ``` hoelzl@41973 ` 2102` ``` by (rule eventually_rev_mp) (auto simp: extreal_real real_of_extreal_0) ``` hoelzl@41973 ` 2103` ```qed ``` hoelzl@41973 ` 2104` hoelzl@41973 ` 2105` ```lemma tendsto_extreal_realI: ``` hoelzl@41973 ` 2106` ``` fixes f :: "'a \ extreal" ``` hoelzl@41976 ` 2107` ``` assumes x: "\x\ \ \" and tendsto: "(f ---> x) net" ``` hoelzl@41973 ` 2108` ``` shows "((\x. extreal (real (f x))) ---> x) net" ``` hoelzl@41973 ` 2109` ```proof (intro topological_tendstoI) ``` hoelzl@41973 ` 2110` ``` fix S assume "open S" "x \ S" ``` hoelzl@41973 ` 2111` ``` with x have "open (S - {\, -\})" "x \ S - {\, -\}" by auto ``` hoelzl@41973 ` 2112` ``` from tendsto[THEN topological_tendstoD, OF this] ``` hoelzl@41973 ` 2113` ``` show "eventually (\x. extreal (real (f x)) \ S) net" ``` hoelzl@41973 ` 2114` ``` by (elim eventually_elim1) (auto simp: extreal_real) ``` hoelzl@41973 ` 2115` ```qed ``` hoelzl@41973 ` 2116` hoelzl@41973 ` 2117` ```lemma extreal_mult_cancel_left: ``` hoelzl@41973 ` 2118` ``` fixes a b c :: extreal shows "a * b = a * c \ ``` hoelzl@41976 ` 2119` ``` ((\a\ = \ \ 0 < b * c) \ a = 0 \ b = c)" ``` hoelzl@41973 ` 2120` ``` by (cases rule: extreal3_cases[of a b c]) ``` hoelzl@41973 ` 2121` ``` (simp_all add: zero_less_mult_iff) ``` hoelzl@41973 ` 2122` hoelzl@41973 ` 2123` ```lemma extreal_inj_affinity: ``` hoelzl@41976 ` 2124` ``` assumes "\m\ \ \" "m \ 0" "\t\ \ \" ``` hoelzl@41973 ` 2125` ``` shows "inj_on (\x. m * x + t) A" ``` hoelzl@41973 ` 2126` ``` using assms ``` hoelzl@41973 ` 2127` ``` by (cases rule: extreal2_cases[of m t]) ``` hoelzl@41973 ` 2128` ``` (auto intro!: inj_onI simp: extreal_add_cancel_right extreal_mult_cancel_left) ``` hoelzl@41973 ` 2129` hoelzl@41973 ` 2130` ```lemma extreal_PInfty_eq_plus[simp]: ``` hoelzl@41973 ` 2131` ``` shows "\ = a + b \ a = \ \ b = \" ``` hoelzl@41973 ` 2132` ``` by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@41973 ` 2133` hoelzl@41973 ` 2134` ```lemma extreal_MInfty_eq_plus[simp]: ``` hoelzl@41973 ` 2135` ``` shows "-\ = a + b \ (a = -\ \ b \ \) \ (b = -\ \ a \ \)" ``` hoelzl@41973 ` 2136` ``` by (cases rule: extreal2_cases[of a b]) auto ``` hoelzl@41973 ` 2137` hoelzl@41973 ` 2138` ```lemma extreal_less_divide_pos: ``` hoelzl@41973 ` 2139` ``` "x > 0 \ x \ \ \ y < z / x \ x * y < z" ``` hoelzl@41973 ` 2140` ``` by (cases rule: extreal3_cases[of x y z]) (auto simp: field_simps) ``` hoelzl@41973 ` 2141` hoelzl@41973 ` 2142` ```lemma extreal_divide_less_pos: ``` hoelzl@41973 ` 2143` ``` "x > 0 \ x \ \ \ y / x < z \ y < x * z" ``` hoelzl@41973 ` 2144` ``` by (cases rule: extreal3_cases[of x y z]) (auto simp: field_simps) ``` hoelzl@41973 ` 2145` hoelzl@41973 ` 2146` ```lemma extreal_open_affinity_pos: ``` hoelzl@41976 ` 2147` ``` assumes "open S" and m: "m \ \" "0 < m" and t: "\t\ \ \" ``` hoelzl@41973 ` 2148` ``` shows "open ((\x. m * x + t) ` S)" ``` hoelzl@41973 ` 2149` ```proof - ``` hoelzl@41973 ` 2150` ``` obtain r where r[simp]: "m = extreal r" using m by (cases m) auto ``` hoelzl@41976 ` 2151` ``` obtain p where p[simp]: "t = extreal p" using t by auto ``` hoelzl@41973 ` 2152` ``` have "r \ 0" "0 < r" and m': "m \ \" "m \ -\" "m \ 0" using m by auto ``` hoelzl@41975 ` 2153` ``` from `open S`[THEN extreal_openE] guess l u . note T = this ``` hoelzl@41973 ` 2154` ``` let ?f = "(\x. m * x + t)" ``` hoelzl@41973 ` 2155` ``` show ?thesis unfolding open_extreal_def ``` hoelzl@41973 ` 2156` ``` proof (intro conjI impI exI subsetI) ``` hoelzl@41975 ` 2157` ``` have "extreal -` ?f ` S = (\x. r * x + p) ` (extreal -` S)" ``` hoelzl@41975 ` 2158` ``` proof safe ``` hoelzl@41975 ` 2159` ``` fix x y assume "extreal y = m * x + t" "x \ S" ``` hoelzl@41975 ` 2160` ``` then show "y \ (\x. r * x + p) ` extreal -` S" ``` hoelzl@41975 ` 2161` ``` using `r \ 0` by (cases x) (auto intro!: image_eqI[of _ _ "real x"] split: split_if_asm) ``` hoelzl@41975 ` 2162` ``` qed force ``` hoelzl@41975 ` 2163` ``` then show "open (extreal -` ?f ` S)" ``` hoelzl@41975 ` 2164` ``` using open_affinity[OF T(1) `r \ 0`] by (auto simp: ac_simps) ``` hoelzl@41973 ` 2165` ``` next ``` hoelzl@41973 ` 2166` ``` assume "\ \ ?f`S" with `0 < r` have "\ \ S" by auto ``` hoelzl@41973 ` 2167` ``` fix x assume "x \ {extreal (r * l + p)<..}" ``` hoelzl@41973 ` 2168` ``` then have [simp]: "extreal (r * l + p) < x" by auto ``` hoelzl@41973 ` 2169` ``` show "x \ ?f`S" ``` hoelzl@41973 ` 2170` ``` proof (rule image_eqI) ``` hoelzl@41973 ` 2171` ``` show "x = m * ((x - t) / m) + t" ``` hoelzl@41973 ` 2172` ``` using m t by (cases rule: extreal3_cases[of m x t]) auto ``` hoelzl@41973 ` 2173` ``` have "extreal l < (x - t)/m" ``` hoelzl@41973 ` 2174` ``` using m t by (simp add: extreal_less_divide_pos extreal_less_minus) ``` hoelzl@41975 ` 2175` ``` then show "(x - t)/m \ S" using T(2)[OF `\ \ S`] by auto ``` hoelzl@41973 ` 2176` ``` qed ``` hoelzl@41973 ` 2177` ``` next ``` hoelzl@41973 ` 2178` ``` assume "-\ \ ?f`S" with `0 < r` have "-\ \ S" by auto ``` hoelzl@41973 ` 2179` ``` fix x assume "x \ {.. ?f`S" ``` hoelzl@41973 ` 2182` ``` proof (rule image_eqI) ``` hoelzl@41973 ` 2183` ``` show "x = m * ((x - t) / m) + t" ``` hoelzl@41973 ` 2184` ``` using m t by (cases rule: extreal3_cases[of m x t]) auto ``` hoelzl@41973 ` 2185` ``` have "(x - t)/m < extreal u" ``` hoelzl@41973 ` 2186` ``` using m t by (simp add: extreal_divide_less_pos extreal_minus_less) ``` hoelzl@41975 ` 2187` ``` then show "(x - t)/m \ S" using T(3)[OF `-\ \ S`] by auto ``` hoelzl@41973 ` 2188` ``` qed ``` hoelzl@41973 ` 2189` ``` qed ``` hoelzl@41973 ` 2190` ```qed ``` hoelzl@41973 ` 2191` hoelzl@41973 ` 2192` ```lemma extreal_open_affinity: ``` hoelzl@41976 ` 2193` ``` assumes "open S" and m: "\m\ \ \" "m \ 0" and t: "\t\ \ \" ``` hoelzl@41973 ` 2194` ``` shows "open ((\x. m * x + t) ` S)" ``` hoelzl@41973 ` 2195` ```proof cases ``` hoelzl@41973 ` 2196` ``` assume "0 < m" then show ?thesis ``` hoelzl@41976 ` 2197` ``` using extreal_open_affinity_pos[OF `open S` _ _ t, of m] m by auto ``` hoelzl@41973 ` 2198` ```next ``` hoelzl@41973 ` 2199` ``` assume "\ 0 < m" then ``` hoelzl@41973 ` 2200` ``` have "0 < -m" using `m \ 0` by (cases m) auto ``` hoelzl@41976 ` 2201` ``` then have m: "-m \ \" "0 < -m" using `\m\ \ \` ``` hoelzl@41976 ` 2202` ``` by (auto simp: extreal_uminus_eq_reorder) ``` hoelzl@41973 ` 2203` ``` from extreal_open_affinity_pos[OF extreal_open_uminus[OF `open S`] m t] ``` hoelzl@41973 ` 2204` ``` show ?thesis unfolding image_image by simp ``` hoelzl@41973 ` 2205` ```qed ``` hoelzl@41973 ` 2206` hoelzl@41973 ` 2207` ```lemma extreal_divide_eq: ``` hoelzl@41976 ` 2208` ``` "b \ 0 \ \b\ \ \ \ a / b = c \ a = b * c" ``` hoelzl@41973 ` 2209` ``` by (cases rule: extreal3_cases[of a b c]) ``` hoelzl@41973 ` 2210` ``` (simp_all add: field_simps) ``` hoelzl@41973 ` 2211` hoelzl@41973 ` 2212` ```lemma extreal_inverse_not_MInfty[simp]: "inverse a \ -\" ``` hoelzl@41973 ` 2213` ``` by (cases a) auto ``` hoelzl@41973 ` 2214` hoelzl@41973 ` 2215` ```lemma extreal_lim_mult: ``` hoelzl@41973 ` 2216` ``` fixes X :: "'a \ extreal" ``` hoelzl@41976 ` 2217` ``` assumes lim: "(X ---> L) net" and a: "\a\ \ \" ``` hoelzl@41973 ` 2218` ``` shows "((\i. a * X i) ---> a * L) net" ``` hoelzl@41973 ` 2219` ```proof cases ``` hoelzl@41973 ` 2220` ``` assume "a \ 0" ``` hoelzl@41973 ` 2221` ``` show ?thesis ``` hoelzl@41973 ` 2222` ``` proof (rule topological_tendstoI) ``` hoelzl@41973 ` 2223` ``` fix S assume "open S" "a * L \ S" ``` hoelzl@41973 ` 2224` ``` have "a * L / a = L" ``` hoelzl@41973 ` 2225` ``` using `a \ 0` a by (cases rule: extreal2_cases[of a L]) auto ``` hoelzl@41973 ` 2226` ``` then have L: "L \ ((\x. x / a) ` S)" ``` hoelzl@41973 ` 2227` ``` using `a * L \ S` by (force simp: image_iff) ``` hoelzl@41973 ` 2228` ``` moreover have "open ((\x. x / a) ` S)" ``` hoelzl@41973 ` 2229` ``` using extreal_open_affinity[OF `open S`, of "inverse a" 0] `a \ 0` a ``` hoelzl@41976 ` 2230` ``` by (auto simp: extreal_divide_eq extreal_inverse_eq_0 divide_extreal_def ac_simps) ``` hoelzl@41973 ` 2231` ``` note * = lim[THEN topological_tendstoD, OF this L] ``` hoelzl@41973 ` 2232` ``` { fix x from a `a \ 0` have "a * (x / a) = x" ``` hoelzl@41973 ` 2233` ``` by (cases rule: extreal2_cases[of a x]) auto } ``` hoelzl@41973 ` 2234` ``` note this[simp] ``` hoelzl@41973 ` 2235` ``` show "eventually (\x. a * X x \ S) net" ``` hoelzl@41973 ` 2236` ``` by (rule eventually_mono[OF _ *]) auto ``` hoelzl@41973 ` 2237` ``` qed ``` hoelzl@41973 ` 2238` ```qed auto ``` hoelzl@41973 ` 2239` hoelzl@41973 ` 2240` ```lemma extreal_mult_m1[simp]: "x * extreal (-1) = -x" ``` hoelzl@41973 ` 2241` ``` by (cases x) auto ``` hoelzl@41973 ` 2242` hoelzl@41973 ` 2243` ```lemma extreal_lim_uminus: ``` hoelzl@41973 ` 2244` ``` fixes X :: "'a \ extreal" shows "((\i. - X i) ---> -L) net \ (X ---> L) net" ``` hoelzl@41973 ` 2245` ``` using extreal_lim_mult[of X L net "extreal (-1)"] ``` hoelzl@41973 ` 2246` ``` extreal_lim_mult[of "(\i. - X i)" "-L" net "extreal (-1)"] ``` hoelzl@41973 ` 2247` ``` by (auto simp add: algebra_simps) ``` hoelzl@41973 ` 2248` hoelzl@41973 ` 2249` ```lemma Lim_bounded2_extreal: ``` hoelzl@41973 ` 2250` ``` assumes lim:"f ----> (l :: extreal)" ``` hoelzl@41973 ` 2251` ``` and ge: "ALL n>=N. f n >= C" ``` hoelzl@41973 ` 2252` ``` shows "l>=C" ``` hoelzl@41973 ` 2253` ```proof- ``` hoelzl@41973 ` 2254` ```def g == "(%i. -(f i))" ``` hoelzl@41973 ` 2255` ```{ fix n assume "n>=N" hence "g n <= -C" using assms extreal_minus_le_minus g_def by auto } ``` hoelzl@41973 ` 2256` ```hence "ALL n>=N. g n <= -C" by auto ``` hoelzl@41973 ` 2257` ```moreover have limg: "g ----> (-l)" using g_def extreal_lim_uminus lim by auto ``` hoelzl@41973 ` 2258` ```ultimately have "-l <= -C" using Lim_bounded_extreal[of g "-l" _ "-C"] by auto ``` hoelzl@41973 ` 2259` ```from this show ?thesis using extreal_minus_le_minus by auto ``` hoelzl@41973 ` 2260` ```qed ``` hoelzl@41973 ` 2261` hoelzl@41973 ` 2262` hoelzl@41973 ` 2263` ```lemma extreal_LimI_finite: ``` hoelzl@41976 ` 2264` ``` assumes "\x\ \ \" ``` hoelzl@41973 ` 2265` ``` assumes "!!r. 0 < r ==> EX N. ALL n>=N. u n < x + r & x < u n + r" ``` hoelzl@41973 ` 2266` ``` shows "u ----> x" ``` hoelzl@41973 ` 2267` ```proof (rule topological_tendstoI, unfold eventually_sequentially) ``` hoelzl@41973 ` 2268` ``` obtain rx where rx_def: "x=extreal rx" using assms by (cases x) auto ``` hoelzl@41973 ` 2269` ``` fix S assume "open S" "x : S" ``` hoelzl@41975 ` 2270` ``` then have "open (extreal -` S)" unfolding open_extreal_def by auto ``` hoelzl@41975 ` 2271` ``` with `x \ S` obtain r where "0 < r" and dist: "!!y. dist y rx < r ==> extreal y \ S" ``` hoelzl@41975 ` 2272` ``` unfolding open_real_def rx_def by auto ``` hoelzl@41973 ` 2273` ``` then obtain n where ``` hoelzl@41973 ` 2274` ``` upper: "!!N. n <= N ==> u N < x + extreal r" and ``` hoelzl@41976 ` 2275` ``` lower: "!!N. n <= N ==> x < u N + extreal r" using assms(2)[of "extreal r"] by auto ``` hoelzl@41973 ` 2276` ``` show "EX N. ALL n>=N. u n : S" ``` hoelzl@41973 ` 2277` ``` proof (safe intro!: exI[of _ n]) ``` hoelzl@41973 ` 2278` ``` fix N assume "n <= N" ``` hoelzl@41973 ` 2279` ``` from upper[OF this] lower[OF this] assms `0 < r` ``` hoelzl@41973 ` 2280` ``` have "u N ~: {\,(-\)}" by auto ``` hoelzl@41973 ` 2281` ``` from this obtain ra where ra_def: "(u N) = extreal ra" by (cases "u N") auto ``` hoelzl@41973 ` 2282` ``` hence "rx < ra + r" and "ra < rx + r" ``` hoelzl@41973 ` 2283` ``` using rx_def assms `0 < r` lower[OF `n <= N`] upper[OF `n <= N`] by auto ``` hoelzl@41975 ` 2284` ``` hence "dist (real (u N)) rx < r" ``` hoelzl@41973 ` 2285` ``` using rx_def ra_def ``` hoelzl@41973 ` 2286` ``` by (auto simp: dist_real_def abs_diff_less_iff field_simps) ``` hoelzl@41976 ` 2287` ``` from dist[OF this] show "u N : S" using `u N ~: {\, -\}` ``` hoelzl@41976 ` 2288` ``` by (auto simp: extreal_real split: split_if_asm) ``` hoelzl@41973 ` 2289` ``` qed ``` hoelzl@41973 ` 2290` ```qed ``` hoelzl@41973 ` 2291` hoelzl@41973 ` 2292` ```lemma extreal_LimI_finite_iff: ``` hoelzl@41976 ` 2293` ``` assumes "\x\ \ \" ``` hoelzl@41973 ` 2294` ``` shows "u ----> x <-> (ALL r. 0 < r --> (EX N. ALL n>=N. u n < x + r & x < u n + r))" ``` hoelzl@41973 ` 2295` ``` (is "?lhs <-> ?rhs") ``` hoelzl@41976 ` 2296` ```proof ``` hoelzl@41976 ` 2297` ``` assume lim: "u ----> x" ``` hoelzl@41973 ` 2298` ``` { fix r assume "(r::extreal)>0" ``` hoelzl@41973 ` 2299` ``` from this obtain N where N_def: "ALL n>=N. u n : {x - r <..< x + r}" ``` hoelzl@41973 ` 2300` ``` apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"]) ``` hoelzl@41973 ` 2301` ``` using lim extreal_between[of x r] assms `r>0` by auto ``` hoelzl@41973 ` 2302` ``` hence "EX N. ALL n>=N. u n < x + r & x < u n + r" ``` hoelzl@41973 ` 2303` ``` using extreal_minus_less[of r x] by (cases r) auto ``` hoelzl@41976 ` 2304` ``` } then show "?rhs" by auto ``` hoelzl@41976 ` 2305` ```next ``` hoelzl@41976 ` 2306` ``` assume ?rhs then show "u ----> x" ``` hoelzl@41976 ` 2307` ``` using extreal_LimI_finite[of x] assms by auto ``` hoelzl@41973 ` 2308` ```qed ``` hoelzl@41973 ` 2309` hoelzl@41973 ` 2310` hoelzl@41973 ` 2311` ```subsubsection {* @{text Liminf} and @{text Limsup} *} ``` hoelzl@41973 ` 2312` hoelzl@41973 ` 2313` ```definition ``` hoelzl@41973 ` 2314` ``` "Liminf net f = (GREATEST l. \yx. y < f x) net)" ``` hoelzl@41973 ` 2315` hoelzl@41973 ` 2316` ```definition ``` hoelzl@41973 ` 2317` ``` "Limsup net f = (LEAST l. \y>l. eventually (\x. f x < y) net)" ``` hoelzl@41973 ` 2318` hoelzl@41973 ` 2319` ```lemma Liminf_Sup: ``` hoelzl@41973 ` 2320` ``` fixes f :: "'a => 'b::{complete_lattice, linorder}" ``` hoelzl@41973 ` 2321` ``` shows "Liminf net f = Sup {l. \yx. y < f x) net}" ``` hoelzl@41973 ` 2322` ``` by (auto intro!: Greatest_equality complete_lattice_class.Sup_upper simp: less_Sup_iff Liminf_def) ``` hoelzl@41973 ` 2323` hoelzl@41973 ` 2324` ```lemma Limsup_Inf: ``` hoelzl@41973 ` 2325` ``` fixes f :: "'a => 'b::{complete_lattice, linorder}" ``` hoelzl@41973 ` 2326` ``` shows "Limsup net f = Inf {l. \y>l. eventually (\x. f x < y) net}" ``` hoelzl@41973 ` 2327` ``` by (auto intro!: Least_equality complete_lattice_class.Inf_lower simp: Inf_less_iff Limsup_def) ``` hoelzl@41973 ` 2328` hoelzl@41973 ` 2329` ```lemma extreal_SupI: ``` hoelzl@41973 ` 2330` ``` fixes x :: extreal ``` hoelzl@41973 ` 2331` ``` assumes "\y. y \ A \ y \ x" ``` hoelzl@41973 ` 2332` ``` assumes "\y. (\z. z \ A \ z \ y) \ x \ y" ``` hoelzl@41973 ` 2333` ``` shows "Sup A = x" ``` hoelzl@41973 ` 2334` ``` unfolding Sup_extreal_def ``` hoelzl@41973 ` 2335` ``` using assms by (auto intro!: Least_equality) ``` hoelzl@41973 ` 2336` hoelzl@41973 ` 2337` ```lemma extreal_InfI: ``` hoelzl@41973 ` 2338` ``` fixes x :: extreal ``` hoelzl@41973 ` 2339` ``` assumes "\i. i \ A \ x \ i" ``` hoelzl@41973 ` 2340` ``` assumes "\y. (\i. i \ A \ y \ i) \ y \ x" ``` hoelzl@41973 ` 2341` ``` shows "Inf A = x" ``` hoelzl@41973 ` 2342` ``` unfolding Inf_extreal_def ``` hoelzl@41973 ` 2343` ``` using assms by (auto intro!: Greatest_equality) ``` hoelzl@41973 ` 2344` hoelzl@41973 ` 2345` ```lemma Limsup_const: ``` hoelzl@41973 ` 2346` ``` fixes c :: "'a::{complete_lattice, linorder}" ``` hoelzl@41973 ` 2347` ``` assumes ntriv: "\ trivial_limit net" ``` hoelzl@41973 ` 2348` ``` shows "Limsup net (\x. c) = c" ``` hoelzl@41973 ` 2349` ``` unfolding Limsup_Inf ``` hoelzl@41973 ` 2350` ```proof (safe intro!: antisym complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower) ``` hoelzl@41973 ` 2351` ``` fix x assume *: "\y>x. eventually (\_. c < y) net" ``` hoelzl@41973 ` 2352` ``` show "c \ x" ``` hoelzl@41973 ` 2353` ``` proof (rule ccontr) ``` hoelzl@41973 ` 2354` ``` assume "\ c \ x" then have "x < c" by auto ``` hoelzl@41973 ` 2355` ``` then show False using ntriv * by (auto simp: trivial_limit_def) ``` hoelzl@41973 ` 2356` ``` qed ``` hoelzl@41973 ` 2357` ```qed auto ``` hoelzl@41973 ` 2358` hoelzl@41973 ` 2359` ```lemma Liminf_const: ``` hoelzl@41973 ` 2360` ``` fixes c :: "'a::{complete_lattice, linorder}" ``` hoelzl@41973 ` 2361` ``` assumes ntriv: "\ trivial_limit net" ``` hoelzl@41973 ` 2362` ``` shows "Liminf net (\x. c) = c" ``` hoelzl@41973 ` 2363` ``` unfolding Liminf_Sup ``` hoelzl@41973 ` 2364` ```proof (safe intro!: antisym complete_lattice_class.Sup_least complete_lattice_class.Sup_upper) ``` hoelzl@41973 ` 2365` ``` fix x assume *: "\y_. y < c) net" ``` hoelzl@41973 ` 2366` ``` show "x \ c" ``` hoelzl@41973 ` 2367` ``` proof (rule ccontr) ``` hoelzl@41973 ` 2368` ``` assume "\ x \ c" then have "c < x" by auto ``` hoelzl@41973 ` 2369` ``` then show False using ntriv * by (auto simp: trivial_limit_def) ``` hoelzl@41973 ` 2370` ``` qed ``` hoelzl@41973 ` 2371` ```qed auto ``` hoelzl@41973 ` 2372` hoelzl@41973 ` 2373` ```lemma mono_set: ``` hoelzl@41973 ` 2374` ``` fixes S :: "('a::order) set" ``` hoelzl@41973 ` 2375` ``` shows "mono S \ (\x y. x \ y \ x \ S \ y \ S)" ``` hoelzl@41973 ` 2376` ``` by (auto simp: mono_def mem_def) ``` hoelzl@41973 ` 2377` hoelzl@41973 ` 2378` ```lemma mono_greaterThan[intro, simp]: "mono {B<..}" unfolding mono_set by auto ``` hoelzl@41973 ` 2379` ```lemma mono_atLeast[intro, simp]: "mono {B..}" unfolding mono_set by auto ``` hoelzl@41973 ` 2380` ```lemma mono_UNIV[intro, simp]: "mono UNIV" unfolding mono_set by auto ``` hoelzl@41973 ` 2381` ```lemma mono_empty[intro, simp]: "mono {}" unfolding mono_set by auto ``` hoelzl@41973 ` 2382` hoelzl@41973 ` 2383` ```lemma mono_set_iff: ``` hoelzl@41973 ` 2384` ``` fixes S :: "'a::{linorder,complete_lattice} set" ``` hoelzl@41973 ` 2385` ``` defines "a \ Inf S" ``` hoelzl@41973 ` 2386` ``` shows "mono S \ (S = {a <..} \ S = {a..})" (is "_ = ?c") ``` hoelzl@41973 ` 2387` ```proof ``` hoelzl@41973 ` 2388` ``` assume "mono S" ``` hoelzl@41973 ` 2389` ``` then have mono: "\x y. x \ y \ x \ S \ y \ S" by (auto simp: mono_set) ``` hoelzl@41973 ` 2390` ``` show ?c ``` hoelzl@41973 ` 2391` ``` proof cases ``` hoelzl@41973 ` 2392` ``` assume "a \ S" ``` hoelzl@41973 ` 2393` ``` show ?c ``` hoelzl@41973 ` 2394` ``` using mono[OF _ `a \ S`] ``` hoelzl@41973 ` 2395` ``` by (auto intro: complete_lattice_class.Inf_lower simp: a_def) ``` hoelzl@41973 ` 2396` ``` next ``` hoelzl@41973 ` 2397` ``` assume "a \ S" ``` hoelzl@41973 ` 2398` ``` have "S = {a <..}" ``` hoelzl@41973 ` 2399` ``` proof safe ``` hoelzl@41973 ` 2400` ``` fix x assume "x \ S" ``` hoelzl@41973 ` 2401` ``` then have "a \ x" unfolding a_def by (rule complete_lattice_class.Inf_lower) ``` hoelzl@41973 ` 2402` ``` then show "a < x" using `x \ S` `a \ S` by (cases "a = x") auto ``` hoelzl@41973 ` 2403` ``` next ``` hoelzl@41973 ` 2404` ``` fix x assume "a < x" ``` hoelzl@41973 ` 2405` ``` then obtain y where "y < x" "y \ S" unfolding a_def Inf_less_iff .. ``` hoelzl@41973 ` 2406` ``` with mono[of y x] show "x \ S" by auto ``` hoelzl@41973 ` 2407` ``` qed ``` hoelzl@41973 ` 2408` ``` then show ?c .. ``` hoelzl@41973 ` 2409` ``` qed ``` hoelzl@41973 ` 2410` ```qed auto ``` hoelzl@41973 ` 2411` hoelzl@41973 ` 2412` hoelzl@41973 ` 2413` ```lemma extreal_open_atLeast: "open {x..} \ x = -\" ``` hoelzl@41973 ` 2414` ```proof ``` hoelzl@41973 ` 2415` ``` assume "x = -\" then have "{x..} = UNIV" by auto ``` hoelzl@41973 ` 2416` ``` then show "open {x..}" by auto ``` hoelzl@41973 ` 2417` ```next ``` hoelzl@41973 ` 2418` ``` assume "open {x..}" ``` hoelzl@41973 ` 2419` ``` then have "open {x..} \ closed {x..}" by auto ``` hoelzl@41973 ` 2420` ``` then have "{x..} = UNIV" unfolding extreal_open_closed by auto ``` hoelzl@41973 ` 2421` ``` then show "x = -\" by (simp add: bot_extreal_def atLeast_eq_UNIV_iff) ``` hoelzl@41973 ` 2422` ```qed ``` hoelzl@41973 ` 2423` hoelzl@41973 ` 2424` ```lemma extreal_open_mono_set: ``` hoelzl@41973 ` 2425` ``` fixes S :: "extreal set" ``` hoelzl@41973 ` 2426` ``` defines "a \ Inf S" ``` hoelzl@41973 ` 2427` ``` shows "(open S \ mono S) \ (S = UNIV \ S = {a <..})" ```