1979 next |
1984 next |
1980 assume ?rhs then show "u ----> x" |
1985 assume ?rhs then show "u ----> x" |
1981 using ereal_LimI_finite[of x] assms by auto |
1986 using ereal_LimI_finite[of x] assms by auto |
1982 qed |
1987 qed |
1983 |
1988 |
1984 |
1989 lemma ereal_Limsup_uminus: |
1985 subsubsection {* @{text Liminf} and @{text Limsup} *} |
1990 fixes f :: "'a => ereal" |
1986 |
1991 shows "Limsup net (\<lambda>x. - (f x)) = -(Liminf net f)" |
1987 definition |
1992 unfolding Limsup_def Liminf_def ereal_SUPR_uminus ereal_INFI_uminus .. |
1988 "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)" |
1993 |
1989 |
1994 lemma liminf_bounded_iff: |
1990 definition |
1995 fixes x :: "nat \<Rightarrow> ereal" |
1991 "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)" |
1996 shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs") |
1992 |
1997 unfolding le_Liminf_iff eventually_sequentially .. |
1993 abbreviation "liminf \<equiv> Liminf sequentially" |
|
1994 |
|
1995 abbreviation "limsup \<equiv> Limsup sequentially" |
|
1996 |
|
1997 lemma Liminf_eqI: |
|
1998 "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow> |
|
1999 (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x" |
|
2000 unfolding Liminf_def by (auto intro!: SUP_eqI) |
|
2001 |
|
2002 lemma Limsup_eqI: |
|
2003 "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow> |
|
2004 (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x" |
|
2005 unfolding Limsup_def by (auto intro!: INF_eqI) |
|
2006 |
|
2007 lemma liminf_SUPR_INFI: |
|
2008 fixes f :: "nat \<Rightarrow> 'a :: complete_lattice" |
|
2009 shows "liminf f = (SUP n. INF m:{n..}. f m)" |
|
2010 unfolding Liminf_def eventually_sequentially |
|
2011 by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono) |
|
2012 |
|
2013 lemma limsup_INFI_SUPR: |
|
2014 fixes f :: "nat \<Rightarrow> 'a :: complete_lattice" |
|
2015 shows "limsup f = (INF n. SUP m:{n..}. f m)" |
|
2016 unfolding Limsup_def eventually_sequentially |
|
2017 by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono) |
|
2018 |
|
2019 lemma Limsup_const: |
|
2020 assumes ntriv: "\<not> trivial_limit F" |
|
2021 shows "Limsup F (\<lambda>x. c) = (c::'a::complete_lattice)" |
|
2022 proof - |
|
2023 have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto |
|
2024 have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c" |
|
2025 using ntriv by (intro SUP_const) (auto simp: eventually_False *) |
|
2026 then show ?thesis |
|
2027 unfolding Limsup_def using eventually_True |
|
2028 by (subst INF_cong[where D="\<lambda>x. c"]) |
|
2029 (auto intro!: INF_const simp del: eventually_True) |
|
2030 qed |
|
2031 |
|
2032 lemma Liminf_const: |
|
2033 assumes ntriv: "\<not> trivial_limit F" |
|
2034 shows "Liminf F (\<lambda>x. c) = (c::'a::complete_lattice)" |
|
2035 proof - |
|
2036 have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto |
|
2037 have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c" |
|
2038 using ntriv by (intro INF_const) (auto simp: eventually_False *) |
|
2039 then show ?thesis |
|
2040 unfolding Liminf_def using eventually_True |
|
2041 by (subst SUP_cong[where D="\<lambda>x. c"]) |
|
2042 (auto intro!: SUP_const simp del: eventually_True) |
|
2043 qed |
|
2044 |
|
2045 lemma Liminf_mono: |
|
2046 fixes f g :: "'a => 'b :: complete_lattice" |
|
2047 assumes ev: "eventually (\<lambda>x. f x \<le> g x) F" |
|
2048 shows "Liminf F f \<le> Liminf F g" |
|
2049 unfolding Liminf_def |
|
2050 proof (safe intro!: SUP_mono) |
|
2051 fix P assume "eventually P F" |
|
2052 with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj) |
|
2053 then show "\<exists>Q\<in>{P. eventually P F}. INFI (Collect P) f \<le> INFI (Collect Q) g" |
|
2054 by (intro bexI[of _ ?Q]) (auto intro!: INF_mono) |
|
2055 qed |
|
2056 |
|
2057 lemma Liminf_eq: |
|
2058 fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice" |
|
2059 assumes "eventually (\<lambda>x. f x = g x) F" |
|
2060 shows "Liminf F f = Liminf F g" |
|
2061 by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto |
|
2062 |
|
2063 lemma Limsup_mono: |
|
2064 fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice" |
|
2065 assumes ev: "eventually (\<lambda>x. f x \<le> g x) F" |
|
2066 shows "Limsup F f \<le> Limsup F g" |
|
2067 unfolding Limsup_def |
|
2068 proof (safe intro!: INF_mono) |
|
2069 fix P assume "eventually P F" |
|
2070 with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj) |
|
2071 then show "\<exists>Q\<in>{P. eventually P F}. SUPR (Collect Q) f \<le> SUPR (Collect P) g" |
|
2072 by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono) |
|
2073 qed |
|
2074 |
|
2075 lemma Limsup_eq: |
|
2076 fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice" |
|
2077 assumes "eventually (\<lambda>x. f x = g x) net" |
|
2078 shows "Limsup net f = Limsup net g" |
|
2079 by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto |
|
2080 |
|
2081 lemma Liminf_le_Limsup: |
|
2082 fixes f :: "'a \<Rightarrow> 'b::complete_lattice" |
|
2083 assumes ntriv: "\<not> trivial_limit F" |
|
2084 shows "Liminf F f \<le> Limsup F f" |
|
2085 unfolding Limsup_def Liminf_def |
|
2086 apply (rule complete_lattice_class.SUP_least) |
|
2087 apply (rule complete_lattice_class.INF_greatest) |
|
2088 proof safe |
|
2089 fix P Q assume "eventually P F" "eventually Q F" |
|
2090 then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj) |
|
2091 then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)" |
|
2092 using ntriv by (auto simp add: eventually_False) |
|
2093 have "INFI (Collect P) f \<le> INFI (Collect ?C) f" |
|
2094 by (rule INF_mono) auto |
|
2095 also have "\<dots> \<le> SUPR (Collect ?C) f" |
|
2096 using not_False by (intro INF_le_SUP) auto |
|
2097 also have "\<dots> \<le> SUPR (Collect Q) f" |
|
2098 by (rule SUP_mono) auto |
|
2099 finally show "INFI (Collect P) f \<le> SUPR (Collect Q) f" . |
|
2100 qed |
|
2101 |
1998 |
2102 lemma |
1999 lemma |
2103 fixes X :: "nat \<Rightarrow> ereal" |
2000 fixes X :: "nat \<Rightarrow> ereal" |
2104 shows ereal_incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X" |
2001 shows ereal_incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X" |
2105 and ereal_decseq_uminus[simp]: "decseq (\<lambda>i. - X i) = incseq X" |
2002 and ereal_decseq_uminus[simp]: "decseq (\<lambda>i. - X i) = incseq X" |
2106 unfolding incseq_def decseq_def by auto |
2003 unfolding incseq_def decseq_def by auto |
2107 |
2004 |
2108 lemma Liminf_bounded: |
|
2109 fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice" |
|
2110 assumes ntriv: "\<not> trivial_limit F" |
|
2111 assumes le: "eventually (\<lambda>n. C \<le> X n) F" |
|
2112 shows "C \<le> Liminf F X" |
|
2113 using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp |
|
2114 |
|
2115 lemma Limsup_bounded: |
|
2116 fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice" |
|
2117 assumes ntriv: "\<not> trivial_limit F" |
|
2118 assumes le: "eventually (\<lambda>n. X n \<le> C) F" |
|
2119 shows "Limsup F X \<le> C" |
|
2120 using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp |
|
2121 |
|
2122 lemma le_Liminf_iff: |
|
2123 fixes X :: "_ \<Rightarrow> _ :: complete_linorder" |
|
2124 shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)" |
|
2125 proof - |
|
2126 { fix y P assume "eventually P F" "y < INFI (Collect P) X" |
|
2127 then have "eventually (\<lambda>x. y < X x) F" |
|
2128 by (auto elim!: eventually_elim1 dest: less_INF_D) } |
|
2129 moreover |
|
2130 { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" |
|
2131 have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X" |
|
2132 proof cases |
|
2133 assume "\<exists>z. y < z \<and> z < C" |
|
2134 then guess z .. |
|
2135 moreover then have "z \<le> INFI {x. z < X x} X" |
|
2136 by (auto intro!: INF_greatest) |
|
2137 ultimately show ?thesis |
|
2138 using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto |
|
2139 next |
|
2140 assume "\<not> (\<exists>z. y < z \<and> z < C)" |
|
2141 then have "C \<le> INFI {x. y < X x} X" |
|
2142 by (intro INF_greatest) auto |
|
2143 with `y < C` show ?thesis |
|
2144 using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto |
|
2145 qed } |
|
2146 ultimately show ?thesis |
|
2147 unfolding Liminf_def le_SUP_iff by auto |
|
2148 qed |
|
2149 |
|
2150 lemma lim_imp_Liminf: |
|
2151 fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}" |
|
2152 assumes ntriv: "\<not> trivial_limit F" |
|
2153 assumes lim: "(f ---> f0) F" |
|
2154 shows "Liminf F f = f0" |
|
2155 proof (intro Liminf_eqI) |
|
2156 fix P assume P: "eventually P F" |
|
2157 then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F" |
|
2158 by eventually_elim (auto intro!: INF_lower) |
|
2159 then show "INFI (Collect P) f \<le> f0" |
|
2160 by (rule tendsto_le[OF ntriv lim tendsto_const]) |
|
2161 next |
|
2162 fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y" |
|
2163 show "f0 \<le> y" |
|
2164 proof cases |
|
2165 assume "\<exists>z. y < z \<and> z < f0" |
|
2166 then guess z .. |
|
2167 moreover have "z \<le> INFI {x. z < f x} f" |
|
2168 by (rule INF_greatest) simp |
|
2169 ultimately show ?thesis |
|
2170 using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto |
|
2171 next |
|
2172 assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)" |
|
2173 show ?thesis |
|
2174 proof (rule classical) |
|
2175 assume "\<not> f0 \<le> y" |
|
2176 then have "eventually (\<lambda>x. y < f x) F" |
|
2177 using lim[THEN topological_tendstoD, of "{y <..}"] by auto |
|
2178 then have "eventually (\<lambda>x. f0 \<le> f x) F" |
|
2179 using discrete by (auto elim!: eventually_elim1) |
|
2180 then have "INFI {x. f0 \<le> f x} f \<le> y" |
|
2181 by (rule upper) |
|
2182 moreover have "f0 \<le> INFI {x. f0 \<le> f x} f" |
|
2183 by (intro INF_greatest) simp |
|
2184 ultimately show "f0 \<le> y" by simp |
|
2185 qed |
|
2186 qed |
|
2187 qed |
|
2188 |
|
2189 lemma lim_imp_Limsup: |
|
2190 fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}" |
|
2191 assumes ntriv: "\<not> trivial_limit F" |
|
2192 assumes lim: "(f ---> f0) F" |
|
2193 shows "Limsup F f = f0" |
|
2194 proof (intro Limsup_eqI) |
|
2195 fix P assume P: "eventually P F" |
|
2196 then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F" |
|
2197 by eventually_elim (auto intro!: SUP_upper) |
|
2198 then show "f0 \<le> SUPR (Collect P) f" |
|
2199 by (rule tendsto_le[OF ntriv tendsto_const lim]) |
|
2200 next |
|
2201 fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f" |
|
2202 show "y \<le> f0" |
|
2203 proof cases |
|
2204 assume "\<exists>z. f0 < z \<and> z < y" |
|
2205 then guess z .. |
|
2206 moreover have "SUPR {x. f x < z} f \<le> z" |
|
2207 by (rule SUP_least) simp |
|
2208 ultimately show ?thesis |
|
2209 using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto |
|
2210 next |
|
2211 assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)" |
|
2212 show ?thesis |
|
2213 proof (rule classical) |
|
2214 assume "\<not> y \<le> f0" |
|
2215 then have "eventually (\<lambda>x. f x < y) F" |
|
2216 using lim[THEN topological_tendstoD, of "{..< y}"] by auto |
|
2217 then have "eventually (\<lambda>x. f x \<le> f0) F" |
|
2218 using discrete by (auto elim!: eventually_elim1 simp: not_less) |
|
2219 then have "y \<le> SUPR {x. f x \<le> f0} f" |
|
2220 by (rule lower) |
|
2221 moreover have "SUPR {x. f x \<le> f0} f \<le> f0" |
|
2222 by (intro SUP_least) simp |
|
2223 ultimately show "y \<le> f0" by simp |
|
2224 qed |
|
2225 qed |
|
2226 qed |
|
2227 |
|
2228 lemma Liminf_eq_Limsup: |
|
2229 fixes f0 :: "'a :: {complete_linorder, linorder_topology}" |
|
2230 assumes ntriv: "\<not> trivial_limit F" |
|
2231 and lim: "Liminf F f = f0" "Limsup F f = f0" |
|
2232 shows "(f ---> f0) F" |
|
2233 proof (rule order_tendstoI) |
|
2234 fix a assume "f0 < a" |
|
2235 with assms have "Limsup F f < a" by simp |
|
2236 then obtain P where "eventually P F" "SUPR (Collect P) f < a" |
|
2237 unfolding Limsup_def INF_less_iff by auto |
|
2238 then show "eventually (\<lambda>x. f x < a) F" |
|
2239 by (auto elim!: eventually_elim1 dest: SUP_lessD) |
|
2240 next |
|
2241 fix a assume "a < f0" |
|
2242 with assms have "a < Liminf F f" by simp |
|
2243 then obtain P where "eventually P F" "a < INFI (Collect P) f" |
|
2244 unfolding Liminf_def less_SUP_iff by auto |
|
2245 then show "eventually (\<lambda>x. a < f x) F" |
|
2246 by (auto elim!: eventually_elim1 dest: less_INF_D) |
|
2247 qed |
|
2248 |
|
2249 lemma tendsto_iff_Liminf_eq_Limsup: |
|
2250 fixes f0 :: "'a :: {complete_linorder, linorder_topology}" |
|
2251 shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)" |
|
2252 by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf) |
|
2253 |
|
2254 lemma liminf_bounded_iff: |
|
2255 fixes x :: "nat \<Rightarrow> ereal" |
|
2256 shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs") |
|
2257 unfolding le_Liminf_iff eventually_sequentially .. |
|
2258 |
|
2259 lemma liminf_subseq_mono: |
|
2260 fixes X :: "nat \<Rightarrow> 'a :: complete_linorder" |
|
2261 assumes "subseq r" |
|
2262 shows "liminf X \<le> liminf (X \<circ> r) " |
|
2263 proof- |
|
2264 have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)" |
|
2265 proof (safe intro!: INF_mono) |
|
2266 fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m" |
|
2267 using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto |
|
2268 qed |
|
2269 then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def) |
|
2270 qed |
|
2271 |
|
2272 lemma limsup_subseq_mono: |
|
2273 fixes X :: "nat \<Rightarrow> 'a :: complete_linorder" |
|
2274 assumes "subseq r" |
|
2275 shows "limsup (X \<circ> r) \<le> limsup X" |
|
2276 proof- |
|
2277 have "\<And>n. (SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)" |
|
2278 proof (safe intro!: SUP_mono) |
|
2279 fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma" |
|
2280 using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto |
|
2281 qed |
|
2282 then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def) |
|
2283 qed |
|
2284 |
|
2285 definition (in order) mono_set: |
|
2286 "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)" |
|
2287 |
|
2288 lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto |
|
2289 lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto |
|
2290 lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto |
|
2291 lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto |
|
2292 |
|
2293 lemma (in complete_linorder) mono_set_iff: |
|
2294 fixes S :: "'a set" |
|
2295 defines "a \<equiv> Inf S" |
|
2296 shows "mono_set S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c") |
|
2297 proof |
|
2298 assume "mono_set S" |
|
2299 then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set) |
|
2300 show ?c |
|
2301 proof cases |
|
2302 assume "a \<in> S" |
|
2303 show ?c |
|
2304 using mono[OF _ `a \<in> S`] |
|
2305 by (auto intro: Inf_lower simp: a_def) |
|
2306 next |
|
2307 assume "a \<notin> S" |
|
2308 have "S = {a <..}" |
|
2309 proof safe |
|
2310 fix x assume "x \<in> S" |
|
2311 then have "a \<le> x" unfolding a_def by (rule Inf_lower) |
|
2312 then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto |
|
2313 next |
|
2314 fix x assume "a < x" |
|
2315 then obtain y where "y < x" "y \<in> S" unfolding a_def Inf_less_iff .. |
|
2316 with mono[of y x] show "x \<in> S" by auto |
|
2317 qed |
|
2318 then show ?c .. |
|
2319 qed |
|
2320 qed auto |
|
2321 |
|
2322 subsubsection {* Tests for code generator *} |
2005 subsubsection {* Tests for code generator *} |
2323 |
2006 |
2324 (* A small list of simple arithmetic expressions *) |
2007 (* A small list of simple arithmetic expressions *) |
2325 |
2008 |
2326 value [code] "- \<infinity> :: ereal" |
2009 value [code] "- \<infinity> :: ereal" |