--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Thu Jul 23 14:25:05 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Thu Jul 23 16:39:10 2015 +0200
@@ -11,48 +11,6 @@
imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real" "~~/src/HOL/Library/Indicator_Function"
begin
-lemma convergent_limsup_cl:
- fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
- shows "convergent X \<Longrightarrow> limsup X = lim X"
- by (auto simp: convergent_def limI lim_imp_Limsup)
-
-lemma lim_increasing_cl:
- assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
- obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
-proof
- show "f ----> (SUP n. f n)"
- using assms
- by (intro increasing_tendsto)
- (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
-qed
-
-lemma lim_decreasing_cl:
- assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
- obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
-proof
- show "f ----> (INF n. f n)"
- using assms
- by (intro decreasing_tendsto)
- (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
-qed
-
-lemma compact_complete_linorder:
- fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
- shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
-proof -
- obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
- using seq_monosub[of X]
- unfolding comp_def
- by auto
- then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)"
- by (auto simp add: monoseq_def)
- then obtain l where "(X \<circ> r) ----> l"
- using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
- by auto
- then show ?thesis
- using \<open>subseq r\<close> by auto
-qed
-
lemma compact_UNIV:
"compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)"
using compact_complete_linorder
@@ -94,21 +52,6 @@
by simp
qed
-lemma ereal_dense3:
- fixes x y :: ereal
- shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y"
-proof (cases x y rule: ereal2_cases, simp_all)
- fix r q :: real
- assume "r < q"
- from Rats_dense_in_real[OF this] show "\<exists>x. r < real_of_rat x \<and> real_of_rat x < q"
- by (fastforce simp: Rats_def)
-next
- fix r :: real
- show "\<exists>x. r < real_of_rat x" "\<exists>x. real_of_rat x < r"
- using gt_ex[of r] lt_ex[of r] Rats_dense_in_real
- by (auto simp: Rats_def)
-qed
-
instance ereal :: second_countable_topology
proof (default, intro exI conjI)
let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)"
@@ -139,43 +82,6 @@
qed
qed
-lemma continuous_on_ereal[intro, simp]: "continuous_on A ereal"
- unfolding continuous_on_topological open_ereal_def
- by auto
-
-lemma continuous_at_ereal[intro, simp]: "continuous (at x) ereal"
- using continuous_on_eq_continuous_at[of UNIV]
- by auto
-
-lemma continuous_within_ereal[intro, simp]: "x \<in> A \<Longrightarrow> continuous (at x within A) ereal"
- using continuous_on_eq_continuous_within[of A]
- by auto
-
-lemma ereal_open_uminus:
- fixes S :: "ereal set"
- assumes "open S"
- shows "open (uminus ` S)"
- using \<open>open S\<close>[unfolded open_generated_order]
-proof induct
- have "range uminus = (UNIV :: ereal set)"
- by (auto simp: image_iff ereal_uminus_eq_reorder)
- then show "open (range uminus :: ereal set)"
- by simp
-qed (auto simp add: image_Union image_Int)
-
-lemma ereal_uminus_complement:
- fixes S :: "ereal set"
- shows "uminus ` (- S) = - uminus ` S"
- by (auto intro!: bij_image_Compl_eq surjI[of _ uminus] simp: bij_betw_def)
-
-lemma ereal_closed_uminus:
- fixes S :: "ereal set"
- assumes "closed S"
- shows "closed (uminus ` S)"
- using assms
- unfolding closed_def ereal_uminus_complement[symmetric]
- by (rule ereal_open_uminus)
-
lemma ereal_open_closed_aux:
fixes S :: "ereal set"
assumes "open S"
@@ -185,6 +91,7 @@
proof (rule ccontr)
assume "\<not> ?thesis"
then have *: "Inf S \<in> S"
+
by (metis assms(2) closed_contains_Inf_cl)
{
assume "Inf S = -\<infinity>"
@@ -243,54 +150,6 @@
by auto
qed
-lemma ereal_open_affinity_pos:
- fixes S :: "ereal set"
- assumes "open S"
- and m: "m \<noteq> \<infinity>" "0 < m"
- and t: "\<bar>t\<bar> \<noteq> \<infinity>"
- shows "open ((\<lambda>x. m * x + t) ` S)"
-proof -
- have "open ((\<lambda>x. inverse m * (x + -t)) -` S)"
- using m t
- apply (intro open_vimage \<open>open S\<close>)
- apply (intro continuous_at_imp_continuous_on ballI tendsto_cmult_ereal continuous_at[THEN iffD2]
- tendsto_ident_at tendsto_add_left_ereal)
- apply auto
- done
- also have "(\<lambda>x. inverse m * (x + -t)) -` S = (\<lambda>x. (x - t) / m) -` S"
- using m t by (auto simp: divide_ereal_def mult.commute uminus_ereal.simps[symmetric] minus_ereal_def
- simp del: uminus_ereal.simps)
- also have "(\<lambda>x. (x - t) / m) -` S = (\<lambda>x. m * x + t) ` S"
- using m t
- by (simp add: set_eq_iff image_iff)
- (metis abs_ereal_less0 abs_ereal_uminus ereal_divide_eq ereal_eq_minus ereal_minus(7,8)
- ereal_minus_less_minus ereal_mult_eq_PInfty ereal_uminus_uminus ereal_zero_mult)
- finally show ?thesis .
-qed
-
-lemma ereal_open_affinity:
- fixes S :: "ereal set"
- assumes "open S"
- and m: "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0"
- and t: "\<bar>t\<bar> \<noteq> \<infinity>"
- shows "open ((\<lambda>x. m * x + t) ` S)"
-proof cases
- assume "0 < m"
- then show ?thesis
- using ereal_open_affinity_pos[OF \<open>open S\<close> _ _ t, of m] m
- by auto
-next
- assume "\<not> 0 < m" then
- have "0 < -m"
- using \<open>m \<noteq> 0\<close>
- by (cases m) auto
- then have m: "-m \<noteq> \<infinity>" "0 < -m"
- using \<open>\<bar>m\<bar> \<noteq> \<infinity>\<close>
- by (auto simp: ereal_uminus_eq_reorder)
- from ereal_open_affinity_pos[OF ereal_open_uminus[OF \<open>open S\<close>] m t] show ?thesis
- unfolding image_image by simp
-qed
-
lemma ereal_open_atLeast:
fixes x :: ereal
shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
@@ -310,290 +169,6 @@
by (simp add: bot_ereal_def atLeast_eq_UNIV_iff)
qed
-lemma open_uminus_iff:
- fixes S :: "ereal set"
- shows "open (uminus ` S) \<longleftrightarrow> open S"
- using ereal_open_uminus[of S] ereal_open_uminus[of "uminus ` S"]
- by auto
-
-lemma ereal_Liminf_uminus:
- fixes f :: "'a \<Rightarrow> ereal"
- shows "Liminf net (\<lambda>x. - (f x)) = - Limsup net f"
- using ereal_Limsup_uminus[of _ "(\<lambda>x. - (f x))"] by auto
-
-lemma Liminf_PInfty:
- fixes f :: "'a \<Rightarrow> ereal"
- assumes "\<not> trivial_limit net"
- shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
- unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
- using Liminf_le_Limsup[OF assms, of f]
- by auto
-
-lemma Limsup_MInfty:
- fixes f :: "'a \<Rightarrow> ereal"
- assumes "\<not> trivial_limit net"
- shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>"
- unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
- using Liminf_le_Limsup[OF assms, of f]
- by auto
-
-lemma convergent_ereal:
- fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
- shows "convergent X \<longleftrightarrow> limsup X = liminf X"
- using tendsto_iff_Liminf_eq_Limsup[of sequentially]
- by (auto simp: convergent_def)
-
-lemma limsup_le_liminf_real:
- fixes X :: "nat \<Rightarrow> real" and L :: real
- assumes 1: "limsup X \<le> L" and 2: "L \<le> liminf X"
- shows "X ----> L"
-proof -
- from 1 2 have "limsup X \<le> liminf X" by auto
- hence 3: "limsup X = liminf X"
- apply (subst eq_iff, rule conjI)
- by (rule Liminf_le_Limsup, auto)
- hence 4: "convergent (\<lambda>n. ereal (X n))"
- by (subst convergent_ereal)
- hence "limsup X = lim (\<lambda>n. ereal(X n))"
- by (rule convergent_limsup_cl)
- also from 1 2 3 have "limsup X = L" by auto
- finally have "lim (\<lambda>n. ereal(X n)) = L" ..
- hence "(\<lambda>n. ereal (X n)) ----> L"
- apply (elim subst)
- by (subst convergent_LIMSEQ_iff [symmetric], rule 4)
- thus ?thesis by simp
-qed
-
-lemma liminf_PInfty:
- fixes X :: "nat \<Rightarrow> ereal"
- shows "X ----> \<infinity> \<longleftrightarrow> liminf X = \<infinity>"
- by (metis Liminf_PInfty trivial_limit_sequentially)
-
-lemma limsup_MInfty:
- fixes X :: "nat \<Rightarrow> ereal"
- shows "X ----> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
- by (metis Limsup_MInfty trivial_limit_sequentially)
-
-lemma ereal_lim_mono:
- fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
- assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
- and "X ----> x"
- and "Y ----> y"
- shows "x \<le> y"
- using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
-
-lemma incseq_le_ereal:
- fixes X :: "nat \<Rightarrow> 'a::linorder_topology"
- assumes inc: "incseq X"
- and lim: "X ----> L"
- shows "X N \<le> L"
- using inc
- by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
-
-lemma decseq_ge_ereal:
- assumes dec: "decseq X"
- and lim: "X ----> (L::'a::linorder_topology)"
- shows "X N \<ge> L"
- using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
-
-lemma bounded_abs:
- fixes a :: real
- assumes "a \<le> x"
- and "x \<le> b"
- shows "abs x \<le> max (abs a) (abs b)"
- by (metis abs_less_iff assms leI le_max_iff_disj
- less_eq_real_def less_le_not_le less_minus_iff minus_minus)
-
-lemma ereal_Sup_lim:
- fixes a :: "'a::{complete_linorder,linorder_topology}"
- assumes "\<And>n. b n \<in> s"
- and "b ----> a"
- shows "a \<le> Sup s"
- by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
-
-lemma ereal_Inf_lim:
- fixes a :: "'a::{complete_linorder,linorder_topology}"
- assumes "\<And>n. b n \<in> s"
- and "b ----> a"
- shows "Inf s \<le> a"
- by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
-
-lemma SUP_Lim_ereal:
- fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
- assumes inc: "incseq X"
- and l: "X ----> l"
- shows "(SUP n. X n) = l"
- using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
- by simp
-
-lemma INF_Lim_ereal:
- fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
- assumes dec: "decseq X"
- and l: "X ----> l"
- shows "(INF n. X n) = l"
- using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
- by simp
-
-lemma SUP_eq_LIMSEQ:
- assumes "mono f"
- shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f ----> x"
-proof
- have inc: "incseq (\<lambda>i. ereal (f i))"
- using \<open>mono f\<close> unfolding mono_def incseq_def by auto
- {
- assume "f ----> x"
- then have "(\<lambda>i. ereal (f i)) ----> ereal x"
- by auto
- from SUP_Lim_ereal[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
- next
- assume "(SUP n. ereal (f n)) = ereal x"
- with LIMSEQ_SUP[OF inc] show "f ----> x" by auto
- }
-qed
-
-lemma liminf_ereal_cminus:
- fixes f :: "nat \<Rightarrow> ereal"
- assumes "c \<noteq> -\<infinity>"
- shows "liminf (\<lambda>x. c - f x) = c - limsup f"
-proof (cases c)
- case PInf
- then show ?thesis
- by (simp add: Liminf_const)
-next
- case (real r)
- then show ?thesis
- unfolding liminf_SUP_INF limsup_INF_SUP
- apply (subst INF_ereal_minus_right)
- apply auto
- apply (subst SUP_ereal_minus_right)
- apply auto
- done
-qed (insert \<open>c \<noteq> -\<infinity>\<close>, simp)
-
-
-subsubsection \<open>Continuity\<close>
-
-lemma continuous_at_of_ereal:
- fixes x0 :: ereal
- assumes "\<bar>x0\<bar> \<noteq> \<infinity>"
- shows "continuous (at x0) real"
-proof -
- {
- fix T
- assume T: "open T" "real x0 \<in> T"
- def S \<equiv> "ereal ` T"
- then have "ereal (real x0) \<in> S"
- using T by auto
- then have "x0 \<in> S"
- using assms ereal_real by auto
- moreover have "open S"
- using open_ereal S_def T by auto
- moreover have "\<forall>y\<in>S. real y \<in> T"
- using S_def T by auto
- ultimately have "\<exists>S. x0 \<in> S \<and> open S \<and> (\<forall>y\<in>S. real y \<in> T)"
- by auto
- }
- then show ?thesis
- unfolding continuous_at_open by blast
-qed
-
-lemma nhds_ereal: "nhds (ereal r) = filtermap ereal (nhds r)"
- by (simp add: filtermap_nhds_open_map open_ereal continuous_at_of_ereal)
-
-lemma at_ereal: "at (ereal r) = filtermap ereal (at r)"
- by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
-
-lemma at_left_ereal: "at_left (ereal r) = filtermap ereal (at_left r)"
- by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
-
-lemma at_right_ereal: "at_right (ereal r) = filtermap ereal (at_right r)"
- by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)
-
-lemma
- shows at_left_PInf: "at_left \<infinity> = filtermap ereal at_top"
- and at_right_MInf: "at_right (-\<infinity>) = filtermap ereal at_bot"
- unfolding filter_eq_iff eventually_filtermap eventually_at_top_dense eventually_at_bot_dense
- eventually_at_left[OF ereal_less(5)] eventually_at_right[OF ereal_less(6)]
- by (auto simp add: ereal_all_split ereal_ex_split)
-
-lemma ereal_tendsto_simps1:
- "((f \<circ> real) ---> y) (at_left (ereal x)) \<longleftrightarrow> (f ---> y) (at_left x)"
- "((f \<circ> real) ---> y) (at_right (ereal x)) \<longleftrightarrow> (f ---> y) (at_right x)"
- "((f \<circ> real) ---> y) (at_left (\<infinity>::ereal)) \<longleftrightarrow> (f ---> y) at_top"
- "((f \<circ> real) ---> y) (at_right (-\<infinity>::ereal)) \<longleftrightarrow> (f ---> y) at_bot"
- unfolding tendsto_compose_filtermap at_left_ereal at_right_ereal at_left_PInf at_right_MInf
- by (auto simp: filtermap_filtermap filtermap_ident)
-
-lemma ereal_tendsto_simps2:
- "((ereal \<circ> f) ---> ereal a) F \<longleftrightarrow> (f ---> a) F"
- "((ereal \<circ> f) ---> \<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_top)"
- "((ereal \<circ> f) ---> -\<infinity>) F \<longleftrightarrow> (LIM x F. f x :> at_bot)"
- unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense
- using lim_ereal by (simp_all add: comp_def)
-
-lemmas ereal_tendsto_simps = ereal_tendsto_simps1 ereal_tendsto_simps2
-
-lemma continuous_at_iff_ereal:
- fixes f :: "'a::t2_space \<Rightarrow> real"
- shows "continuous (at x0 within s) f \<longleftrightarrow> continuous (at x0 within s) (ereal \<circ> f)"
- unfolding continuous_within comp_def lim_ereal ..
-
-lemma continuous_on_iff_ereal:
- fixes f :: "'a::t2_space => real"
- assumes "open A"
- shows "continuous_on A f \<longleftrightarrow> continuous_on A (ereal \<circ> f)"
- unfolding continuous_on_def comp_def lim_ereal ..
-
-lemma continuous_on_real: "continuous_on (UNIV - {\<infinity>, -\<infinity>::ereal}) real"
- using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal
- by auto
-
-lemma continuous_on_iff_real:
- fixes f :: "'a::t2_space \<Rightarrow> ereal"
- assumes *: "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
- shows "continuous_on A f \<longleftrightarrow> continuous_on A (real \<circ> f)"
-proof -
- have "f ` A \<subseteq> UNIV - {\<infinity>, -\<infinity>}"
- using assms by force
- then have *: "continuous_on (f ` A) real"
- using continuous_on_real by (simp add: continuous_on_subset)
- have **: "continuous_on ((real \<circ> f) ` A) ereal"
- using continuous_on_ereal continuous_on_subset[of "UNIV" "ereal" "(real \<circ> f) ` A"]
- by blast
- {
- assume "continuous_on A f"
- then have "continuous_on A (real \<circ> f)"
- apply (subst continuous_on_compose)
- using *
- apply auto
- done
- }
- moreover
- {
- assume "continuous_on A (real \<circ> f)"
- then have "continuous_on A (ereal \<circ> (real \<circ> f))"
- apply (subst continuous_on_compose)
- using **
- apply auto
- done
- then have "continuous_on A f"
- apply (subst continuous_on_eq[of A "ereal \<circ> (real \<circ> f)" f])
- using assms ereal_real
- apply auto
- done
- }
- ultimately show ?thesis
- by auto
-qed
-
-lemma continuous_at_const:
- fixes f :: "'a::t2_space \<Rightarrow> ereal"
- assumes "\<forall>x. f x = C"
- shows "\<forall>x. continuous (at x) f"
- unfolding continuous_at_open
- using assms t1_space
- by auto
-
lemma mono_closed_real:
fixes S :: "real set"
assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S"
@@ -675,313 +250,6 @@
using mono_closed_real[of S] assms by auto
qed
-
-subsection \<open>Sums\<close>
-
-lemma sums_ereal_positive:
- fixes f :: "nat \<Rightarrow> ereal"
- assumes "\<And>i. 0 \<le> f i"
- shows "f sums (SUP n. \<Sum>i<n. f i)"
-proof -
- have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
- using ereal_add_mono[OF _ assms]
- by (auto intro!: incseq_SucI)
- from LIMSEQ_SUP[OF this]
- show ?thesis unfolding sums_def
- by (simp add: atLeast0LessThan)
-qed
-
-lemma summable_ereal_pos:
- fixes f :: "nat \<Rightarrow> ereal"
- assumes "\<And>i. 0 \<le> f i"
- shows "summable f"
- using sums_ereal_positive[of f, OF assms]
- unfolding summable_def
- by auto
-
-lemma suminf_ereal_eq_SUP:
- fixes f :: "nat \<Rightarrow> ereal"
- assumes "\<And>i. 0 \<le> f i"
- shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)"
- using sums_ereal_positive[of f, OF assms, THEN sums_unique]
- by simp
-
-lemma sums_ereal: "(\<lambda>x. ereal (f x)) sums ereal x \<longleftrightarrow> f sums x"
- unfolding sums_def by simp
-
-lemma suminf_bound:
- fixes f :: "nat \<Rightarrow> ereal"
- assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x"
- and pos: "\<And>n. 0 \<le> f n"
- shows "suminf f \<le> x"
-proof (rule Lim_bounded_ereal)
- have "summable f" using pos[THEN summable_ereal_pos] .
- then show "(\<lambda>N. \<Sum>n<N. f n) ----> suminf f"
- by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
- show "\<forall>n\<ge>0. setsum f {..<n} \<le> x"
- using assms by auto
-qed
-
-lemma suminf_bound_add:
- fixes f :: "nat \<Rightarrow> ereal"
- assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x"
- and pos: "\<And>n. 0 \<le> f n"
- and "y \<noteq> -\<infinity>"
- shows "suminf f + y \<le> x"
-proof (cases y)
- case (real r)
- then have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y"
- using assms by (simp add: ereal_le_minus)
- then have "(\<Sum> n. f n) \<le> x - y"
- using pos by (rule suminf_bound)
- then show "(\<Sum> n. f n) + y \<le> x"
- using assms real by (simp add: ereal_le_minus)
-qed (insert assms, auto)
-
-lemma suminf_upper:
- fixes f :: "nat \<Rightarrow> ereal"
- assumes "\<And>n. 0 \<le> f n"
- shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
- unfolding suminf_ereal_eq_SUP [OF assms]
- by (auto intro: complete_lattice_class.SUP_upper)
-
-lemma suminf_0_le:
- fixes f :: "nat \<Rightarrow> ereal"
- assumes "\<And>n. 0 \<le> f n"
- shows "0 \<le> (\<Sum>n. f n)"
- using suminf_upper[of f 0, OF assms]
- by simp
-
-lemma suminf_le_pos:
- fixes f g :: "nat \<Rightarrow> ereal"
- assumes "\<And>N. f N \<le> g N"
- and "\<And>N. 0 \<le> f N"
- shows "suminf f \<le> suminf g"
-proof (safe intro!: suminf_bound)
- fix n
- {
- fix N
- have "0 \<le> g N"
- using assms(2,1)[of N] by auto
- }
- have "setsum f {..<n} \<le> setsum g {..<n}"
- using assms by (auto intro: setsum_mono)
- also have "\<dots> \<le> suminf g"
- using \<open>\<And>N. 0 \<le> g N\<close>
- by (rule suminf_upper)
- finally show "setsum f {..<n} \<le> suminf g" .
-qed (rule assms(2))
-
-lemma suminf_half_series_ereal: "(\<Sum>n. (1/2 :: ereal) ^ Suc n) = 1"
- using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric]
- by (simp add: one_ereal_def)
-
-lemma suminf_add_ereal:
- fixes f g :: "nat \<Rightarrow> ereal"
- assumes "\<And>i. 0 \<le> f i"
- and "\<And>i. 0 \<le> g i"
- shows "(\<Sum>i. f i + g i) = suminf f + suminf g"
- apply (subst (1 2 3) suminf_ereal_eq_SUP)
- unfolding setsum.distrib
- apply (intro assms ereal_add_nonneg_nonneg SUP_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
- done
-
-lemma suminf_cmult_ereal:
- fixes f g :: "nat \<Rightarrow> ereal"
- assumes "\<And>i. 0 \<le> f i"
- and "0 \<le> a"
- shows "(\<Sum>i. a * f i) = a * suminf f"
- by (auto simp: setsum_ereal_right_distrib[symmetric] assms
- ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUP
- intro!: SUP_ereal_mult_left)
-
-lemma suminf_PInfty:
- fixes f :: "nat \<Rightarrow> ereal"
- assumes "\<And>i. 0 \<le> f i"
- and "suminf f \<noteq> \<infinity>"
- shows "f i \<noteq> \<infinity>"
-proof -
- from suminf_upper[of f "Suc i", OF assms(1)] assms(2)
- have "(\<Sum>i<Suc i. f i) \<noteq> \<infinity>"
- by auto
- then show ?thesis
- unfolding setsum_Pinfty by simp
-qed
-
-lemma suminf_PInfty_fun:
- assumes "\<And>i. 0 \<le> f i"
- and "suminf f \<noteq> \<infinity>"
- shows "\<exists>f'. f = (\<lambda>x. ereal (f' x))"
-proof -
- have "\<forall>i. \<exists>r. f i = ereal r"
- proof
- fix i
- show "\<exists>r. f i = ereal r"
- using suminf_PInfty[OF assms] assms(1)[of i]
- by (cases "f i") auto
- qed
- from choice[OF this] show ?thesis
- by auto
-qed
-
-lemma summable_ereal:
- assumes "\<And>i. 0 \<le> f i"
- and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
- shows "summable f"
-proof -
- have "0 \<le> (\<Sum>i. ereal (f i))"
- using assms by (intro suminf_0_le) auto
- with assms obtain r where r: "(\<Sum>i. ereal (f i)) = ereal r"
- by (cases "\<Sum>i. ereal (f i)") auto
- from summable_ereal_pos[of "\<lambda>x. ereal (f x)"]
- have "summable (\<lambda>x. ereal (f x))"
- using assms by auto
- from summable_sums[OF this]
- have "(\<lambda>x. ereal (f x)) sums (\<Sum>x. ereal (f x))"
- by auto
- then show "summable f"
- unfolding r sums_ereal summable_def ..
-qed
-
-lemma suminf_ereal:
- assumes "\<And>i. 0 \<le> f i"
- and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
- shows "(\<Sum>i. ereal (f i)) = ereal (suminf f)"
-proof (rule sums_unique[symmetric])
- from summable_ereal[OF assms]
- show "(\<lambda>x. ereal (f x)) sums (ereal (suminf f))"
- unfolding sums_ereal
- using assms
- by (intro summable_sums summable_ereal)
-qed
-
-lemma suminf_ereal_minus:
- fixes f g :: "nat \<Rightarrow> ereal"
- assumes ord: "\<And>i. g i \<le> f i" "\<And>i. 0 \<le> g i"
- and fin: "suminf f \<noteq> \<infinity>" "suminf g \<noteq> \<infinity>"
- shows "(\<Sum>i. f i - g i) = suminf f - suminf g"
-proof -
- {
- fix i
- have "0 \<le> f i"
- using ord[of i] by auto
- }
- moreover
- from suminf_PInfty_fun[OF \<open>\<And>i. 0 \<le> f i\<close> fin(1)] obtain f' where [simp]: "f = (\<lambda>x. ereal (f' x))" ..
- from suminf_PInfty_fun[OF \<open>\<And>i. 0 \<le> g i\<close> fin(2)] obtain g' where [simp]: "g = (\<lambda>x. ereal (g' x))" ..
- {
- fix i
- have "0 \<le> f i - g i"
- using ord[of i] by (auto simp: ereal_le_minus_iff)
- }
- moreover
- have "suminf (\<lambda>i. f i - g i) \<le> suminf f"
- using assms by (auto intro!: suminf_le_pos simp: field_simps)
- then have "suminf (\<lambda>i. f i - g i) \<noteq> \<infinity>"
- using fin by auto
- ultimately show ?thesis
- using assms \<open>\<And>i. 0 \<le> f i\<close>
- apply simp
- apply (subst (1 2 3) suminf_ereal)
- apply (auto intro!: suminf_diff[symmetric] summable_ereal)
- done
-qed
-
-lemma suminf_ereal_PInf [simp]: "(\<Sum>x. \<infinity>::ereal) = \<infinity>"
-proof -
- have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>::ereal)"
- by (rule suminf_upper) auto
- then show ?thesis
- by simp
-qed
-
-lemma summable_real_of_ereal:
- fixes f :: "nat \<Rightarrow> ereal"
- assumes f: "\<And>i. 0 \<le> f i"
- and fin: "(\<Sum>i. f i) \<noteq> \<infinity>"
- shows "summable (\<lambda>i. real (f i))"
-proof (rule summable_def[THEN iffD2])
- have "0 \<le> (\<Sum>i. f i)"
- using assms by (auto intro: suminf_0_le)
- with fin obtain r where r: "ereal r = (\<Sum>i. f i)"
- by (cases "(\<Sum>i. f i)") auto
- {
- fix i
- have "f i \<noteq> \<infinity>"
- using f by (intro suminf_PInfty[OF _ fin]) auto
- then have "\<bar>f i\<bar> \<noteq> \<infinity>"
- using f[of i] by auto
- }
- note fin = this
- have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))"
- using f
- by (auto intro!: summable_ereal_pos simp: ereal_le_real_iff zero_ereal_def)
- also have "\<dots> = ereal r"
- using fin r by (auto simp: ereal_real)
- finally show "\<exists>r. (\<lambda>i. real (f i)) sums r"
- by (auto simp: sums_ereal)
-qed
-
-lemma suminf_SUP_eq:
- fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ereal"
- assumes "\<And>i. incseq (\<lambda>n. f n i)"
- and "\<And>n i. 0 \<le> f n i"
- shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
-proof -
- {
- fix n :: nat
- have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
- using assms
- by (auto intro!: SUP_ereal_setsum [symmetric])
- }
- note * = this
- show ?thesis
- using assms
- apply (subst (1 2) suminf_ereal_eq_SUP)
- unfolding *
- apply (auto intro!: SUP_upper2)
- apply (subst SUP_commute)
- apply rule
- done
-qed
-
-lemma suminf_setsum_ereal:
- fixes f :: "_ \<Rightarrow> _ \<Rightarrow> ereal"
- assumes nonneg: "\<And>i a. a \<in> A \<Longrightarrow> 0 \<le> f i a"
- shows "(\<Sum>i. \<Sum>a\<in>A. f i a) = (\<Sum>a\<in>A. \<Sum>i. f i a)"
-proof (cases "finite A")
- case True
- then show ?thesis
- using nonneg
- by induct (simp_all add: suminf_add_ereal setsum_nonneg)
-next
- case False
- then show ?thesis by simp
-qed
-
-lemma suminf_ereal_eq_0:
- fixes f :: "nat \<Rightarrow> ereal"
- assumes nneg: "\<And>i. 0 \<le> f i"
- shows "(\<Sum>i. f i) = 0 \<longleftrightarrow> (\<forall>i. f i = 0)"
-proof
- assume "(\<Sum>i. f i) = 0"
- {
- fix i
- assume "f i \<noteq> 0"
- with nneg have "0 < f i"
- by (auto simp: less_le)
- also have "f i = (\<Sum>j. if j = i then f i else 0)"
- by (subst suminf_finite[where N="{i}"]) auto
- also have "\<dots> \<le> (\<Sum>i. f i)"
- using nneg
- by (auto intro!: suminf_le_pos)
- finally have False
- using \<open>(\<Sum>i. f i) = 0\<close> by auto
- }
- then show "\<forall>i. f i = 0"
- by auto
-qed simp
-
lemma Liminf_within:
fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
@@ -1045,50 +313,6 @@
apply (metis INF_absorb centre_in_ball)
done
-
-lemma suminf_ereal_offset_le:
- fixes f :: "nat \<Rightarrow> ereal"
- assumes f: "\<And>i. 0 \<le> f i"
- shows "(\<Sum>i. f (i + k)) \<le> suminf f"
-proof -
- have "(\<lambda>n. \<Sum>i<n. f (i + k)) ----> (\<Sum>i. f (i + k))"
- using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
- moreover have "(\<lambda>n. \<Sum>i<n. f i) ----> (\<Sum>i. f i)"
- using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
- then have "(\<lambda>n. \<Sum>i<n + k. f i) ----> (\<Sum>i. f i)"
- by (rule LIMSEQ_ignore_initial_segment)
- ultimately show ?thesis
- proof (rule LIMSEQ_le, safe intro!: exI[of _ k])
- fix n assume "k \<le> n"
- have "(\<Sum>i<n. f (i + k)) = (\<Sum>i<n. (f \<circ> (\<lambda>i. i + k)) i)"
- by simp
- also have "\<dots> = (\<Sum>i\<in>(\<lambda>i. i + k) ` {..<n}. f i)"
- by (subst setsum.reindex) auto
- also have "\<dots> \<le> setsum f {..<n + k}"
- by (intro setsum_mono3) (auto simp: f)
- finally show "(\<Sum>i<n. f (i + k)) \<le> setsum f {..<n + k}" .
- qed
-qed
-
-lemma sums_suminf_ereal: "f sums x \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal x"
- by (metis sums_ereal sums_unique)
-
-lemma suminf_ereal': "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal (\<Sum>i. f i)"
- by (metis sums_ereal sums_unique summable_def)
-
-lemma suminf_ereal_finite: "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
- by (auto simp: sums_ereal[symmetric] summable_def sums_unique[symmetric])
-
-lemma suminf_ereal_finite_neg:
- assumes "summable f"
- shows "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>"
-proof-
- from assms obtain x where "f sums x" by blast
- hence "(\<lambda>x. ereal (f x)) sums ereal x" by (simp add: sums_ereal)
- from sums_unique[OF this] have "(\<Sum>x. ereal (f x)) = ereal x" ..
- thus "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>" by simp_all
-qed
-
subsection \<open>monoset\<close>
definition (in order) mono_set:
@@ -1281,5 +505,4 @@
lemma indicator_inter_arith_ereal: "indicator A x * indicator B x = (indicator (A \<inter> B) x :: ereal)"
by (simp split: split_indicator)
-
end