import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
--- a/src/HOL/Conditionally_Complete_Lattices.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Mon Jun 30 15:45:21 2014 +0200
@@ -354,6 +354,10 @@
by (intro antisym le_supI cSUP_least cSUP_upper2)
(auto intro: le_supI1 le_supI2 cSUP_least cSUP_upper le_supI)
+lemma cInf_le_cSup:
+ "A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> bdd_below A \<Longrightarrow> Inf A \<le> Sup A"
+ by (auto intro!: cSup_upper2[of "SOME a. a \<in> A"] intro: someI cInf_lower)
+
end
instance complete_lattice \<subseteq> conditionally_complete_lattice
@@ -447,20 +451,20 @@
lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x"
by (auto intro!: cSup_eq_non_empty intro: dense_le)
-lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x"
- by (auto intro!: cSup_eq intro: dense_le_bounded)
+lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
+ by (auto intro!: cSup_eq_non_empty intro: dense_le_bounded)
-lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x"
- by (auto intro!: cSup_eq intro: dense_le_bounded)
+lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditionally_complete_linorder, dense_linorder}} = x"
+ by (auto intro!: cSup_eq_non_empty intro: dense_le_bounded)
lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditionally_complete_linorder, no_top, dense_linorder} <..} = x"
- by (auto intro!: cInf_eq intro: dense_ge)
+ by (auto intro!: cInf_eq_non_empty intro: dense_ge)
-lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, no_top, dense_linorder}} = y"
- by (auto intro!: cInf_eq intro: dense_ge_bounded)
+lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
+ by (auto intro!: cInf_eq_non_empty intro: dense_ge_bounded)
-lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, no_top, dense_linorder}} = y"
- by (auto intro!: cInf_eq intro: dense_ge_bounded)
+lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditionally_complete_linorder, dense_linorder}} = y"
+ by (auto intro!: cInf_eq_non_empty intro: dense_ge_bounded)
class linear_continuum = conditionally_complete_linorder + dense_linorder +
assumes UNIV_not_singleton: "\<exists>a b::'a. a \<noteq> b"
--- a/src/HOL/Finite_Set.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Finite_Set.thy Mon Jun 30 15:45:21 2014 +0200
@@ -1512,6 +1512,22 @@
lemma card_UNIV_unit [simp]: "card (UNIV :: unit set) = 1"
unfolding UNIV_unit by simp
+lemma infinite_arbitrarily_large:
+ assumes "\<not> finite A"
+ shows "\<exists>B. finite B \<and> card B = n \<and> B \<subseteq> A"
+proof (induction n)
+ case 0 show ?case by (intro exI[of _ "{}"]) auto
+next
+ case (Suc n)
+ then guess B .. note B = this
+ with `\<not> finite A` have "A \<noteq> B" by auto
+ with B have "B \<subset> A" by auto
+ hence "\<exists>x. x \<in> A - B" by (elim psubset_imp_ex_mem)
+ then guess x .. note x = this
+ with B have "finite (insert x B) \<and> card (insert x B) = Suc n \<and> insert x B \<subseteq> A"
+ by auto
+ thus "\<exists>B. finite B \<and> card B = Suc n \<and> B \<subseteq> A" ..
+qed
subsubsection {* Cardinality of image *}
--- a/src/HOL/Library/Extended_Real.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Library/Extended_Real.thy Mon Jun 30 15:45:21 2014 +0200
@@ -80,6 +80,12 @@
lemmas ereal2_cases = ereal_cases[case_product ereal_cases]
lemmas ereal3_cases = ereal2_cases[case_product ereal_cases]
+lemma ereal_all_split: "\<And>P. (\<forall>x::ereal. P x) \<longleftrightarrow> P \<infinity> \<and> (\<forall>x. P (ereal x)) \<and> P (-\<infinity>)"
+ by (metis ereal_cases)
+
+lemma ereal_ex_split: "\<And>P. (\<exists>x::ereal. P x) \<longleftrightarrow> P \<infinity> \<or> (\<exists>x. P (ereal x)) \<or> P (-\<infinity>)"
+ by (metis ereal_cases)
+
lemma ereal_uminus_eq_iff[simp]:
fixes a b :: ereal
shows "-a = -b \<longleftrightarrow> a = b"
@@ -2121,7 +2127,6 @@
by auto
qed
-
subsubsection {* Convergent sequences *}
lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
--- a/src/HOL/Library/Indicator_Function.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Library/Indicator_Function.thy Mon Jun 30 15:45:21 2014 +0200
@@ -142,4 +142,17 @@
"A \<subseteq> B \<Longrightarrow> indicator A x * indicator B x = (indicator A x :: 'a::{comm_semiring_1})"
by (auto split: split_indicator simp: fun_eq_iff)
+lemma indicator_sums:
+ assumes "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
+ shows "(\<lambda>i. indicator (A i) x::real) sums indicator (\<Union>i. A i) x"
+proof cases
+ assume "\<exists>i. x \<in> A i"
+ then obtain i where i: "x \<in> A i" ..
+ with assms have "(\<lambda>i. indicator (A i) x::real) sums (\<Sum>i\<in>{i}. indicator (A i) x)"
+ by (intro sums_finite) (auto split: split_indicator)
+ also have "(\<Sum>i\<in>{i}. indicator (A i) x) = indicator (\<Union>i. A i) x"
+ using i by (auto split: split_indicator)
+ finally show ?thesis .
+qed simp
+
end
--- a/src/HOL/Limits.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Limits.thy Mon Jun 30 15:45:21 2014 +0200
@@ -1820,6 +1820,26 @@
qed simp
+lemma continuous_image_closed_interval:
+ fixes a b and f :: "real \<Rightarrow> real"
+ defines "S \<equiv> {a..b}"
+ assumes "a \<le> b" and f: "continuous_on S f"
+ shows "\<exists>c d. f`S = {c..d} \<and> c \<le> d"
+proof -
+ have S: "compact S" "S \<noteq> {}"
+ using `a \<le> b` by (auto simp: S_def)
+ obtain c where "c \<in> S" "\<forall>d\<in>S. f d \<le> f c"
+ using continuous_attains_sup[OF S f] by auto
+ moreover obtain d where "d \<in> S" "\<forall>c\<in>S. f d \<le> f c"
+ using continuous_attains_inf[OF S f] by auto
+ moreover have "connected (f`S)"
+ using connected_continuous_image[OF f] connected_Icc by (auto simp: S_def)
+ ultimately have "f ` S = {f d .. f c} \<and> f d \<le> f c"
+ by (auto simp: connected_iff_interval)
+ then show ?thesis
+ by auto
+qed
+
subsection {* Boundedness of continuous functions *}
text{*By bisection, function continuous on closed interval is bounded above*}
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Jun 30 15:45:21 2014 +0200
@@ -5855,8 +5855,7 @@
qed
lemma unit_interval_convex_hull:
- defines "One \<equiv> \<Sum>Basis"
- shows "cbox (0::'a::euclidean_space) One = convex hull {x. \<forall>i\<in>Basis. (x\<bullet>i = 0) \<or> (x\<bullet>i = 1)}"
+ "cbox (0::'a::euclidean_space) One = convex hull {x. \<forall>i\<in>Basis. (x\<bullet>i = 0) \<or> (x\<bullet>i = 1)}"
(is "?int = convex hull ?points")
proof -
have One[simp]: "\<And>i. i \<in> Basis \<Longrightarrow> One \<bullet> i = 1"
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Jun 30 15:45:21 2014 +0200
@@ -1926,6 +1926,10 @@
"(f has_field_derivative y) F \<longleftrightarrow> (f has_vector_derivative y) F"
unfolding has_vector_derivative_def has_field_derivative_def real_scaleR_def mult_commute_abs ..
+lemma has_field_derivative_subset:
+ "(f has_field_derivative y) (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_field_derivative y) (at x within t)"
+ unfolding has_field_derivative_def by (rule has_derivative_subset)
+
lemma has_vector_derivative_const[simp, derivative_intros]: "((\<lambda>x. c) has_vector_derivative 0) net"
by (auto simp: has_vector_derivative_def)
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Mon Jun 30 15:45:21 2014 +0200
@@ -439,6 +439,27 @@
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>"
@@ -572,38 +593,52 @@
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) f \<longleftrightarrow> continuous (at x0) (ereal \<circ> f)"
-proof -
- {
- assume "continuous (at x0) f"
- then have "continuous (at x0) (ereal \<circ> f)"
- using continuous_at_ereal continuous_at_compose[of x0 f ereal]
- by auto
- }
- moreover
- {
- assume "continuous (at x0) (ereal \<circ> f)"
- then have "continuous (at x0) (real \<circ> (ereal \<circ> f))"
- using continuous_at_of_ereal
- by (intro continuous_at_compose[of x0 "ereal \<circ> f"]) auto
- moreover have "real \<circ> (ereal \<circ> f) = f"
- using real_ereal_id by (simp add: o_assoc)
- ultimately have "continuous (at x0) f"
- by auto
- }
- ultimately show ?thesis
- by auto
-qed
-
+ 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)"
- using continuous_at_iff_ereal assms
- by (auto simp add: continuous_on_eq_continuous_at cong del: continuous_on_cong)
+ 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
@@ -611,7 +646,7 @@
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>"
+ 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>}"
--- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Jun 30 15:45:21 2014 +0200
@@ -216,9 +216,6 @@
subsection {* Some useful lemmas about intervals. *}
-abbreviation One :: "'a::euclidean_space"
- where "One \<equiv> \<Sum>Basis"
-
lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
using nonempty_Basis
by (fastforce simp add: set_eq_iff mem_box)
@@ -2709,6 +2706,15 @@
qed
qed
+lemma has_integral_scaleR_left:
+ "(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x *\<^sub>R c) has_integral (y *\<^sub>R c)) s"
+ using has_integral_linear[OF _ bounded_linear_scaleR_left] by (simp add: comp_def)
+
+lemma has_integral_mult_left:
+ fixes c :: "_ :: {real_normed_algebra}"
+ shows "(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x * c) has_integral (y * c)) s"
+ using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def)
+
lemma has_integral_cmul: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s"
unfolding o_def[symmetric]
apply (rule has_integral_linear,assumption)
@@ -10961,6 +10967,30 @@
done
qed
+lemma has_integral_monotone_convergence_increasing:
+ fixes f :: "nat \<Rightarrow> 'a::euclidean_space \<Rightarrow> real"
+ assumes f: "\<And>k. (f k has_integral x k) s"
+ assumes "\<And>k x. x \<in> s \<Longrightarrow> f k x \<le> f (Suc k) x"
+ assumes "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>k. f k x) ----> g x"
+ assumes "x ----> x'"
+ shows "(g has_integral x') s"
+proof -
+ have x_eq: "x = (\<lambda>i. integral s (f i))"
+ by (simp add: integral_unique[OF f])
+ then have x: "{integral s (f k) |k. True} = range x"
+ by auto
+
+ have "g integrable_on s \<and> (\<lambda>k. integral s (f k)) ----> integral s g"
+ proof (intro monotone_convergence_increasing allI ballI assms)
+ show "bounded {integral s (f k) |k. True}"
+ unfolding x by (rule convergent_imp_bounded) fact
+ qed (auto intro: f)
+ moreover then have "integral s g = x'"
+ by (intro LIMSEQ_unique[OF _ `x ----> x'`]) (simp add: x_eq)
+ ultimately show ?thesis
+ by (simp add: has_integral_integral)
+qed
+
lemma monotone_convergence_decreasing:
fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
assumes "\<forall>k. (f k) integrable_on s"
@@ -12383,6 +12413,8 @@
subsection {* Dominated convergence *}
+(* GENERALIZE the following theorems *)
+
lemma dominated_convergence:
fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
assumes "\<And>k. (f k) integrable_on s" "h integrable_on s"
@@ -12657,4 +12689,26 @@
qed
qed
+lemma has_integral_dominated_convergence:
+ fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
+ assumes "\<And>k. (f k has_integral y k) s" "h integrable_on s"
+ "\<And>k. \<forall>x\<in>s. norm (f k x) \<le> h x" "\<forall>x\<in>s. (\<lambda>k. f k x) ----> g x"
+ and x: "y ----> x"
+ shows "(g has_integral x) s"
+proof -
+ have int_f: "\<And>k. (f k) integrable_on s"
+ using assms by (auto simp: integrable_on_def)
+ have "(g has_integral (integral s g)) s"
+ by (intro integrable_integral dominated_convergence[OF int_f assms(2)]) fact+
+ moreover have "integral s g = x"
+ proof (rule LIMSEQ_unique)
+ show "(\<lambda>i. integral s (f i)) ----> x"
+ using integral_unique[OF assms(1)] x by simp
+ show "(\<lambda>i. integral s (f i)) ----> integral s g"
+ by (intro dominated_convergence[OF int_f assms(2)]) fact+
+ qed
+ ultimately show ?thesis
+ by simp
+qed
+
end
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Jun 30 15:45:21 2014 +0200
@@ -825,6 +825,9 @@
subsection {* Boxes *}
+abbreviation One :: "'a::euclidean_space"
+ where "One \<equiv> \<Sum>Basis"
+
definition (in euclidean_space) eucl_less (infix "<e" 50)
where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
@@ -847,6 +850,12 @@
shows "box a b = {a <..< b}" "cbox a b = {a .. b}"
by auto
+lemma box_Int_box:
+ fixes a :: "'a::euclidean_space"
+ shows "box a b \<inter> box c d =
+ box (\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>R i)"
+ unfolding set_eq_iff and Int_iff and mem_box by auto
+
lemma rational_boxes:
fixes x :: "'a\<Colon>euclidean_space"
assumes "e > 0"
@@ -1142,6 +1151,24 @@
show ?th4 unfolding * by (intro **) auto
qed
+lemma UN_box_eq_UNIV: "(\<Union>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One)) = UNIV"
+proof -
+ { fix x b :: 'a assume [simp]: "b \<in> Basis"
+ have "\<bar>x \<bullet> b\<bar> \<le> real (natceiling \<bar>x \<bullet> b\<bar>)"
+ by (rule real_natceiling_ge)
+ also have "\<dots> \<le> real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)))"
+ by (auto intro!: natceiling_mono)
+ also have "\<dots> < real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)"
+ by simp
+ finally have "\<bar>x \<bullet> b\<bar> < real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)" . }
+ then have "\<And>x::'a. \<exists>n::nat. \<forall>b\<in>Basis. \<bar>x \<bullet> b\<bar> < real n"
+ by auto
+ moreover have "\<And>x b::'a. \<And>n::nat. \<bar>x \<bullet> b\<bar> < real n \<longleftrightarrow> - real n < x \<bullet> b \<and> x \<bullet> b < real n"
+ by auto
+ ultimately show ?thesis
+ by (auto simp: box_def inner_setsum_left inner_Basis setsum.If_cases)
+qed
+
text {* Intervals in general, including infinite and mixtures of open and closed. *}
definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
@@ -4588,6 +4615,43 @@
"continuous (at x) f \<longleftrightarrow> (\<forall>e > 0. \<exists>d > 0. \<forall>x'. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
using continuous_within_eps_delta [of x UNIV f] by simp
+lemma continuous_at_right_real_increasing:
+ assumes nondecF: "\<And> x y. x \<le> y \<Longrightarrow> f x \<le> ((f y) :: real)"
+ shows "(continuous (at_right (a :: real)) f) = (\<forall>e > 0. \<exists>delta > 0. f (a + delta) - f a < e)"
+ apply (auto simp add: continuous_within_eps_delta dist_real_def greaterThan_def)
+ apply (drule_tac x = e in spec, auto)
+ apply (drule_tac x = "a + d / 2" in spec)
+ apply (subst (asm) abs_of_nonneg)
+ apply (auto intro: nondecF simp add: field_simps)
+ apply (rule_tac x = "d / 2" in exI)
+ apply (auto simp add: field_simps)
+ apply (drule_tac x = e in spec, auto)
+ apply (rule_tac x = delta in exI, auto)
+ apply (subst abs_of_nonneg)
+ apply (auto intro: nondecF simp add: field_simps)
+ apply (rule le_less_trans)
+ prefer 2 apply assumption
+by (rule nondecF, auto)
+
+lemma continuous_at_left_real_increasing:
+ assumes nondecF: "\<And> x y. x \<le> y \<Longrightarrow> f x \<le> ((f y) :: real)"
+ shows "(continuous (at_left (a :: real)) f) = (\<forall>e > 0. \<exists>delta > 0. f a - f (a - delta) < e)"
+ apply (auto simp add: continuous_within_eps_delta dist_real_def lessThan_def)
+ apply (drule_tac x = e in spec, auto)
+ apply (drule_tac x = "a - d / 2" in spec)
+ apply (subst (asm) abs_of_nonpos)
+ apply (auto intro: nondecF simp add: field_simps)
+ apply (rule_tac x = "d / 2" in exI)
+ apply (auto simp add: field_simps)
+ apply (drule_tac x = e in spec, auto)
+ apply (rule_tac x = delta in exI, auto)
+ apply (subst abs_of_nonpos)
+ apply (auto intro: nondecF simp add: field_simps)
+ apply (rule less_le_trans)
+ apply assumption
+ apply auto
+by (rule nondecF, auto)
+
text{* Versions in terms of open balls. *}
lemma continuous_within_ball:
--- a/src/HOL/Orderings.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Orderings.thy Mon Jun 30 15:45:21 2014 +0200
@@ -319,6 +319,10 @@
"(x < y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y < x \<Longrightarrow> P) \<Longrightarrow> P"
using less_linear by blast
+lemma linorder_wlog[case_names le sym]:
+ "(\<And>a b. a \<le> b \<Longrightarrow> P a b) \<Longrightarrow> (\<And>a b. P b a \<Longrightarrow> P a b) \<Longrightarrow> P a b"
+ by (cases rule: le_cases[of a b]) blast+
+
lemma not_less: "\<not> x < y \<longleftrightarrow> y \<le> x"
apply (simp add: less_le)
using linear apply (blast intro: antisym)
@@ -360,7 +364,6 @@
lemma not_leE: "\<not> y \<le> x \<Longrightarrow> x < y"
unfolding not_le .
-
text {* Dual order *}
lemma dual_linorder:
--- a/src/HOL/Probability/Binary_Product_Measure.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Mon Jun 30 15:45:21 2014 +0200
@@ -343,14 +343,13 @@
sublocale pair_sigma_finite \<subseteq> P: sigma_finite_measure "M1 \<Otimes>\<^sub>M M2"
proof
- from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
- show "\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> sets (M1 \<Otimes>\<^sub>M M2) \<and> (\<Union>i. F i) = space (M1 \<Otimes>\<^sub>M M2) \<and> (\<forall>i. emeasure (M1 \<Otimes>\<^sub>M M2) (F i) \<noteq> \<infinity>)"
- proof (rule exI[of _ F], intro conjI)
- show "range F \<subseteq> sets (M1 \<Otimes>\<^sub>M M2)" using F by (auto simp: pair_measure_def)
- show "(\<Union>i. F i) = space (M1 \<Otimes>\<^sub>M M2)"
- using F by (auto simp: space_pair_measure)
- show "\<forall>i. emeasure (M1 \<Otimes>\<^sub>M M2) (F i) \<noteq> \<infinity>" using F by auto
- qed
+ from M1.sigma_finite_countable guess F1 ..
+ moreover from M2.sigma_finite_countable guess F2 ..
+ ultimately show
+ "\<exists>A. countable A \<and> A \<subseteq> sets (M1 \<Otimes>\<^sub>M M2) \<and> \<Union>A = space (M1 \<Otimes>\<^sub>M M2) \<and> (\<forall>a\<in>A. emeasure (M1 \<Otimes>\<^sub>M M2) a \<noteq> \<infinity>)"
+ by (intro exI[of _ "(\<lambda>(a, b). a \<times> b) ` (F1 \<times> F2)"] conjI)
+ (auto simp: M2.emeasure_pair_measure_Times space_pair_measure set_eq_iff subset_eq
+ dest: sets.sets_into_space)
qed
lemma sigma_finite_pair_measure:
@@ -644,15 +643,13 @@
shows "sigma_finite_measure M"
proof -
interpret sigma_finite_measure "distr M N f" by fact
- from sigma_finite_disjoint guess A . note A = this
+ from sigma_finite_countable guess A .. note A = this
show ?thesis
- proof (unfold_locales, intro conjI exI allI)
- show "range (\<lambda>i. f -` A i \<inter> space M) \<subseteq> sets M"
- using A f by auto
- show "(\<Union>i. f -` A i \<inter> space M) = space M"
- using A(1) A(2)[symmetric] f by (auto simp: measurable_def Pi_def)
- fix i show "emeasure M (f -` A i \<inter> space M) \<noteq> \<infinity>"
- using f A(1,2) A(3)[of i] by (simp add: emeasure_distr subset_eq)
+ proof
+ show "\<exists>A. countable A \<and> A \<subseteq> sets M \<and> \<Union>A = space M \<and> (\<forall>a\<in>A. emeasure M a \<noteq> \<infinity>)"
+ using A f
+ by (intro exI[of _ "(\<lambda>a. f -` a \<inter> space M) ` A"])
+ (auto simp: emeasure_distr set_eq_iff subset_eq intro: measurable_space)
qed
qed
@@ -825,7 +822,7 @@
('a::second_countable_topology \<times> 'b::second_countable_topology) measure)"
proof (rule measure_eqI[OF borel_prod])
interpret sigma_finite_measure "borel :: 'b measure"
- by (default) (auto simp: borel_def emeasure_sigma intro!: exI[of _ "\<lambda>_. UNIV"])
+ proof qed (intro exI[of _ "{UNIV}"], auto simp: borel_def emeasure_sigma)
fix X :: "('a \<times> 'b) set" assume asm: "X \<in> sets (borel \<Otimes>\<^sub>M borel)"
have "UNIV \<times> UNIV \<in> sets (borel \<Otimes>\<^sub>M borel :: ('a \<times> 'b) measure)"
by (simp add: borel_prod)
--- a/src/HOL/Probability/Bochner_Integration.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy Mon Jun 30 15:45:21 2014 +0200
@@ -1648,6 +1648,13 @@
by simp
qed
+lemma has_bochner_integral_nn_integral:
+ assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
+ assumes "(\<integral>\<^sup>+x. f x \<partial>M) = ereal x"
+ shows "has_bochner_integral M f x"
+ unfolding has_bochner_integral_iff
+ using assms by (auto simp: assms integral_eq_nn_integral intro: integrableI_nn_integral_finite)
+
lemma integrableI_simple_bochner_integrable:
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
shows "simple_bochner_integrable M f \<Longrightarrow> integrable M f"
--- a/src/HOL/Probability/Borel_Space.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Mon Jun 30 15:45:21 2014 +0200
@@ -141,6 +141,9 @@
lemma cbox_borel[measurable]: "cbox a b \<in> sets borel"
by (auto intro: borel_closed)
+lemma box_borel[measurable]: "box a b \<in> sets borel"
+ by (auto intro: borel_open)
+
lemma borel_compact: "compact (A::'a::t2_space set) \<Longrightarrow> A \<in> sets borel"
by (auto intro: borel_closed dest!: compact_imp_closed)
@@ -293,7 +296,6 @@
fixes a b :: "'a\<Colon>ordered_euclidean_space"
shows "{x. x <e a} \<in> sets borel"
and "{x. a <e x} \<in> sets borel"
- and "box a b \<in> sets borel"
and "{..a} \<in> sets borel"
and "{a..} \<in> sets borel"
and "{a..b} \<in> sets borel"
@@ -605,6 +607,16 @@
(auto intro!: sigma_sets_top)
qed auto
+lemma borel_sigma_sets_Ioc: "borel = sigma UNIV (range (\<lambda>(a, b). {a <.. b::real}))"
+proof (rule borel_eq_sigmaI5[OF borel_eq_atMost])
+ fix i :: real
+ have "{..i} = (\<Union>j::nat. {-j <.. i})"
+ by (auto simp: minus_less_iff reals_Archimedean2)
+ also have "\<dots> \<in> sets (sigma UNIV (range (\<lambda>(i, j). {i<..j})))"
+ by (intro sets.countable_nat_UN) auto
+ finally show "{..i} \<in> sets (sigma UNIV (range (\<lambda>(i, j). {i<..j})))" .
+qed simp
+
lemma eucl_lessThan: "{x::real. x <e a} = lessThan a"
by (simp add: eucl_less_def lessThan_def)
@@ -1307,6 +1319,73 @@
shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
+(* Proof by Jeremy Avigad and Luke Serafin *)
+lemma isCont_borel:
+ fixes f :: "'b::metric_space \<Rightarrow> 'a::metric_space"
+ shows "{x. isCont f x} \<in> sets borel"
+proof -
+ let ?I = "\<lambda>j. inverse(real (Suc j))"
+
+ { fix x
+ have "isCont f x = (\<forall>i. \<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i)"
+ unfolding continuous_at_eps_delta
+ proof safe
+ fix i assume "\<forall>e>0. \<exists>d>0. \<forall>y. dist y x < d \<longrightarrow> dist (f y) (f x) < e"
+ moreover have "0 < ?I i / 2"
+ by simp
+ ultimately obtain d where d: "0 < d" "\<And>y. dist x y < d \<Longrightarrow> dist (f y) (f x) < ?I i / 2"
+ by (metis dist_commute)
+ then obtain j where j: "?I j < d"
+ by (metis reals_Archimedean)
+
+ show "\<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i"
+ proof (safe intro!: exI[where x=j])
+ fix y z assume *: "dist x y < ?I j" "dist x z < ?I j"
+ have "dist (f y) (f z) \<le> dist (f y) (f x) + dist (f z) (f x)"
+ by (rule dist_triangle2)
+ also have "\<dots> < ?I i / 2 + ?I i / 2"
+ by (intro add_strict_mono d less_trans[OF _ j] *)
+ also have "\<dots> \<le> ?I i"
+ by (simp add: field_simps real_of_nat_Suc)
+ finally show "dist (f y) (f z) \<le> ?I i"
+ by simp
+ qed
+ next
+ fix e::real assume "0 < e"
+ then obtain n where n: "?I n < e"
+ by (metis reals_Archimedean)
+ assume "\<forall>i. \<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i"
+ from this[THEN spec, of "Suc n"]
+ obtain j where j: "\<And>y z. dist x y < ?I j \<Longrightarrow> dist x z < ?I j \<Longrightarrow> dist (f y) (f z) \<le> ?I (Suc n)"
+ by auto
+
+ show "\<exists>d>0. \<forall>y. dist y x < d \<longrightarrow> dist (f y) (f x) < e"
+ proof (safe intro!: exI[of _ "?I j"])
+ fix y assume "dist y x < ?I j"
+ then have "dist (f y) (f x) \<le> ?I (Suc n)"
+ by (intro j) (auto simp: dist_commute)
+ also have "?I (Suc n) < ?I n"
+ by simp
+ also note n
+ finally show "dist (f y) (f x) < e" .
+ qed simp
+ qed }
+ note * = this
+
+ have **: "\<And>e y. open {x. dist x y < e}"
+ using open_ball by (simp_all add: ball_def dist_commute)
+
+ have "{x\<in>space borel. isCont f x } \<in> sets borel"
+ unfolding *
+ apply (intro sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex)
+ apply (simp add: Collect_all_eq)
+ apply (intro borel_closed closed_INT ballI closed_Collect_imp open_Collect_conj **)
+ apply auto
+ done
+ then show ?thesis
+ by simp
+qed
+
no_notation
eucl_less (infix "<e" 50)
--- a/src/HOL/Probability/Caratheodory.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Probability/Caratheodory.thy Mon Jun 30 15:45:21 2014 +0200
@@ -998,4 +998,77 @@
by (intro exI[of _ \<mu>']) (auto intro: generated_ringI_Basic)
qed
+lemma extend_measure_caratheodory:
+ fixes G :: "'i \<Rightarrow> 'a set"
+ assumes M: "M = extend_measure \<Omega> I G \<mu>"
+ assumes "i \<in> I"
+ assumes "semiring_of_sets \<Omega> (G ` I)"
+ assumes empty: "\<And>i. i \<in> I \<Longrightarrow> G i = {} \<Longrightarrow> \<mu> i = 0"
+ assumes inj: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> G i = G j \<Longrightarrow> \<mu> i = \<mu> j"
+ assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> \<mu> i"
+ assumes add: "\<And>A::nat \<Rightarrow> 'i. \<And>j. A \<in> UNIV \<rightarrow> I \<Longrightarrow> j \<in> I \<Longrightarrow> disjoint_family (G \<circ> A) \<Longrightarrow>
+ (\<Union>i. G (A i)) = G j \<Longrightarrow> (\<Sum>n. \<mu> (A n)) = \<mu> j"
+ shows "emeasure M (G i) = \<mu> i"
+proof -
+ interpret semiring_of_sets \<Omega> "G ` I"
+ by fact
+ have "\<forall>g\<in>G`I. \<exists>i\<in>I. g = G i"
+ by auto
+ then obtain sel where sel: "\<And>g. g \<in> G ` I \<Longrightarrow> sel g \<in> I" "\<And>g. g \<in> G ` I \<Longrightarrow> G (sel g) = g"
+ by metis
+
+ have "\<exists>\<mu>'. (\<forall>s\<in>G ` I. \<mu>' s = \<mu> (sel s)) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G ` I)) \<mu>'"
+ proof (rule caratheodory)
+ show "positive (G ` I) (\<lambda>s. \<mu> (sel s))"
+ by (auto simp: positive_def intro!: empty sel nonneg)
+ show "countably_additive (G ` I) (\<lambda>s. \<mu> (sel s))"
+ proof (rule countably_additiveI)
+ fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> G ` I" "disjoint_family A" "(\<Union>i. A i) \<in> G ` I"
+ then show "(\<Sum>i. \<mu> (sel (A i))) = \<mu> (sel (\<Union>i. A i))"
+ by (intro add) (auto simp: sel image_subset_iff_funcset comp_def Pi_iff intro!: sel)
+ qed
+ qed
+ then obtain \<mu>' where \<mu>': "\<forall>s\<in>G ` I. \<mu>' s = \<mu> (sel s)" "measure_space \<Omega> (sigma_sets \<Omega> (G ` I)) \<mu>'"
+ by metis
+
+ show ?thesis
+ proof (rule emeasure_extend_measure[OF M])
+ { fix i assume "i \<in> I" then show "\<mu>' (G i) = \<mu> i"
+ using \<mu>' by (auto intro!: inj sel) }
+ show "G ` I \<subseteq> Pow \<Omega>"
+ by fact
+ then show "positive (sets M) \<mu>'" "countably_additive (sets M) \<mu>'"
+ using \<mu>' by (simp_all add: M sets_extend_measure measure_space_def)
+ qed fact
+qed
+
+lemma extend_measure_caratheodory_pair:
+ fixes G :: "'i \<Rightarrow> 'j \<Rightarrow> 'a set"
+ assumes M: "M = extend_measure \<Omega> {(a, b). P a b} (\<lambda>(a, b). G a b) (\<lambda>(a, b). \<mu> a b)"
+ assumes "P i j"
+ assumes semiring: "semiring_of_sets \<Omega> {G a b | a b. P a b}"
+ assumes empty: "\<And>i j. P i j \<Longrightarrow> G i j = {} \<Longrightarrow> \<mu> i j = 0"
+ assumes inj: "\<And>i j k l. P i j \<Longrightarrow> P k l \<Longrightarrow> G i j = G k l \<Longrightarrow> \<mu> i j = \<mu> k l"
+ assumes nonneg: "\<And>i j. P i j \<Longrightarrow> 0 \<le> \<mu> i j"
+ assumes add: "\<And>A::nat \<Rightarrow> 'i. \<And>B::nat \<Rightarrow> 'j. \<And>j k.
+ (\<And>n. P (A n) (B n)) \<Longrightarrow> P j k \<Longrightarrow> disjoint_family (\<lambda>n. G (A n) (B n)) \<Longrightarrow>
+ (\<Union>i. G (A i) (B i)) = G j k \<Longrightarrow> (\<Sum>n. \<mu> (A n) (B n)) = \<mu> j k"
+ shows "emeasure M (G i j) = \<mu> i j"
+proof -
+ have "emeasure M ((\<lambda>(a, b). G a b) (i, j)) = (\<lambda>(a, b). \<mu> a b) (i, j)"
+ proof (rule extend_measure_caratheodory[OF M])
+ show "semiring_of_sets \<Omega> ((\<lambda>(a, b). G a b) ` {(a, b). P a b})"
+ using semiring by (simp add: image_def conj_commute)
+ next
+ fix A :: "nat \<Rightarrow> ('i \<times> 'j)" and j assume "A \<in> UNIV \<rightarrow> {(a, b). P a b}" "j \<in> {(a, b). P a b}"
+ "disjoint_family ((\<lambda>(a, b). G a b) \<circ> A)"
+ "(\<Union>i. case A i of (a, b) \<Rightarrow> G a b) = (case j of (a, b) \<Rightarrow> G a b)"
+ then show "(\<Sum>n. case A n of (a, b) \<Rightarrow> \<mu> a b) = (case j of (a, b) \<Rightarrow> \<mu> a b)"
+ using add[of "\<lambda>i. fst (A i)" "\<lambda>i. snd (A i)" "fst j" "snd j"]
+ by (simp add: split_beta' comp_def Pi_iff)
+ qed (auto split: prod.splits intro: assms)
+ then show ?thesis by simp
+qed
+
+
end
--- a/src/HOL/Probability/Distributions.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Probability/Distributions.thy Mon Jun 30 15:45:21 2014 +0200
@@ -56,26 +56,6 @@
by (simp add: field_simps eq)
qed
-lemma measure_lebesgue_Icc: "measure lebesgue {a .. b} = (if a \<le> b then b - a else 0)"
- by (auto simp: measure_def)
-
-lemma integral_power:
- "a \<le> b \<Longrightarrow> (\<integral>x. x^k * indicator {a..b} x \<partial>lborel) = (b^Suc k - a^Suc k) / Suc k"
-proof (subst integral_FTC_atLeastAtMost)
- fix x show "DERIV (\<lambda>x. x^Suc k / Suc k) x :> x^k"
- by (intro derivative_eq_intros) auto
-qed (auto simp: field_simps)
-
-lemma has_bochner_integral_nn_integral:
- assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
- assumes "(\<integral>\<^sup>+x. f x \<partial>M) = ereal x"
- shows "has_bochner_integral M f x"
- unfolding has_bochner_integral_iff
-proof
- show "integrable M f"
- using assms by (rule integrableI_nn_integral_finite)
-qed (auto simp: assms integral_eq_nn_integral)
-
lemma (in prob_space) distributed_AE2:
assumes [measurable]: "distributed M N X f" "Measurable.pred N P"
shows "(AE x in M. P (X x)) \<longleftrightarrow> (AE x in N. 0 < f x \<longrightarrow> P x)"
@@ -104,8 +84,8 @@
by (intro nn_integral_multc[symmetric]) auto
also have "\<dots> = (\<integral>\<^sup>+x. ereal (?f k x) * indicator {0 .. a} x \<partial>lborel)"
by (intro nn_integral_cong) (simp add: field_simps)
- also have "\<dots> = ereal (?F k a) - (?F k 0)"
- proof (rule nn_integral_FTC_atLeastAtMost)
+ also have "\<dots> = ereal (?F k a - ?F k 0)"
+ proof (rule nn_integral_FTC_Icc)
fix x assume "x \<in> {0..a}"
show "DERIV (?F k) x :> ?f k x"
proof(induction k)
@@ -782,9 +762,7 @@
uniform_distributed_bounds[of X a b]
uniform_distributed_measure[of X a b]
distributed_measurable[of M lborel X]
- by (auto intro!: uniform_distrI_borel_atLeastAtMost
- simp: one_ereal_def emeasure_eq_measure
- simp del: measure_lborel)
+ by (auto intro!: uniform_distrI_borel_atLeastAtMost)
lemma (in prob_space) uniform_distributed_expectation:
fixes a b :: real
@@ -798,7 +776,7 @@
(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel)"
by (intro integral_cong) auto
also have "(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel) = (a + b) / 2"
- proof (subst integral_FTC_atLeastAtMost)
+ proof (subst integral_FTC_Icc_real)
fix x
show "DERIV (\<lambda>x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}"
using uniform_distributed_params[OF D]
@@ -827,7 +805,7 @@
have "(\<integral>x. x\<^sup>2 * (?D x) \<partial>lborel) = (\<integral>x. x\<^sup>2 * (indicator {a - ?\<mu> .. b - ?\<mu>} x) / measure lborel {a .. b} \<partial>lborel)"
by (intro integral_cong) (auto split: split_indicator)
also have "\<dots> = (b - a)\<^sup>2 / 12"
- by (simp add: integral_power measure_lebesgue_Icc uniform_distributed_expectation[OF D])
+ by (simp add: integral_power uniform_distributed_expectation[OF D])
(simp add: eval_nat_numeral field_simps )
finally show "(\<integral>x. x\<^sup>2 * ?D x \<partial>lborel) = (b - a)\<^sup>2 / 12" .
qed fact
--- a/src/HOL/Probability/Finite_Product_Measure.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Mon Jun 30 15:45:21 2014 +0200
@@ -8,6 +8,10 @@
imports Binary_Product_Measure
begin
+lemma PiE_choice: "(\<exists>f\<in>PiE I F. \<forall>i\<in>I. P i (f i)) \<longleftrightarrow> (\<forall>i\<in>I. \<exists>x\<in>F i. P i x)"
+ by (auto simp: Bex_def PiE_iff Ball_def dest!: choice_iff'[THEN iffD1])
+ (force intro: exI[of _ "restrict f I" for f])
+
lemma split_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
by auto
@@ -661,28 +665,19 @@
lemma (in product_sigma_finite) sigma_finite:
assumes "finite I"
shows "sigma_finite_measure (PiM I M)"
-proof -
+proof
interpret finite_product_sigma_finite M I by default fact
- from sigma_finite_pairs guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
- then have F: "\<And>j. j \<in> I \<Longrightarrow> range (F j) \<subseteq> sets (M j)"
- "incseq (\<lambda>k. \<Pi>\<^sub>E j \<in> I. F j k)"
- "(\<Union>k. \<Pi>\<^sub>E j \<in> I. F j k) = space (Pi\<^sub>M I M)"
- "\<And>k. \<And>j. j \<in> I \<Longrightarrow> emeasure (M j) (F j k) \<noteq> \<infinity>"
- by blast+
- let ?F = "\<lambda>k. \<Pi>\<^sub>E j \<in> I. F j k"
-
- show ?thesis
- proof (unfold_locales, intro exI[of _ ?F] conjI allI)
- show "range ?F \<subseteq> sets (Pi\<^sub>M I M)" using F(1) `finite I` by auto
- next
- from F(3) show "(\<Union>i. ?F i) = space (Pi\<^sub>M I M)" by simp
- next
- fix j
- from F `finite I` setprod_PInf[of I, OF emeasure_nonneg, of M]
- show "emeasure (\<Pi>\<^sub>M i\<in>I. M i) (?F j) \<noteq> \<infinity>"
- by (subst emeasure_PiM) auto
- qed
+ obtain F where F: "\<And>j. countable (F j)" "\<And>j f. f \<in> F j \<Longrightarrow> f \<in> sets (M j)"
+ "\<And>j f. f \<in> F j \<Longrightarrow> emeasure (M j) f \<noteq> \<infinity>" and
+ in_space: "\<And>j. space (M j) = (\<Union>F j)"
+ using sigma_finite_countable by (metis subset_eq)
+ moreover have "(\<Union>(PiE I ` PiE I F)) = space (Pi\<^sub>M I M)"
+ using in_space by (auto simp: space_PiM PiE_iff intro!: PiE_choice[THEN iffD2])
+ ultimately show "\<exists>A. countable A \<and> A \<subseteq> sets (Pi\<^sub>M I M) \<and> \<Union>A = space (Pi\<^sub>M I M) \<and> (\<forall>a\<in>A. emeasure (Pi\<^sub>M I M) a \<noteq> \<infinity>)"
+ by (intro exI[of _ "PiE I ` PiE I F"])
+ (auto intro!: countable_PiE sets_PiM_I_finite
+ simp: PiE_iff emeasure_PiM finite_index setprod_PInf emeasure_nonneg)
qed
sublocale finite_product_sigma_finite \<subseteq> sigma_finite_measure "Pi\<^sub>M I M"
--- a/src/HOL/Probability/Independent_Family.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Probability/Independent_Family.thy Mon Jun 30 15:45:21 2014 +0200
@@ -903,6 +903,12 @@
qed
qed
+lemma (in prob_space) indep_vars_compose2:
+ assumes "indep_vars M' X I"
+ assumes rv: "\<And>i. i \<in> I \<Longrightarrow> Y i \<in> measurable (M' i) (N i)"
+ shows "indep_vars N (\<lambda>i x. Y i (X i x)) I"
+ using indep_vars_compose [OF assms] by (simp add: comp_def)
+
lemma (in prob_space) indep_var_compose:
assumes "indep_var M1 X1 M2 X2" "Y1 \<in> measurable M1 N1" "Y2 \<in> measurable M2 N2"
shows "indep_var N1 (Y1 \<circ> X1) N2 (Y2 \<circ> X2)"
--- a/src/HOL/Probability/Lebesgue_Measure.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Mon Jun 30 15:45:21 2014 +0200
@@ -1,574 +1,609 @@
(* Title: HOL/Probability/Lebesgue_Measure.thy
Author: Johannes Hölzl, TU München
Author: Robert Himmelmann, TU München
+ Author: Jeremy Avigad
+ Author: Luke Serafin
*)
header {* Lebsegue measure *}
theory Lebesgue_Measure
- imports Finite_Product_Measure Bochner_Integration
+ imports Finite_Product_Measure Bochner_Integration Caratheodory
begin
-lemma absolutely_integrable_on_indicator[simp]:
- fixes A :: "'a::ordered_euclidean_space set"
- shows "((indicator A :: _ \<Rightarrow> real) absolutely_integrable_on X) \<longleftrightarrow>
- (indicator A :: _ \<Rightarrow> real) integrable_on X"
- unfolding absolutely_integrable_on_def by simp
+subsection {* Every right continuous and nondecreasing function gives rise to a measure *}
+
+definition interval_measure :: "(real \<Rightarrow> real) \<Rightarrow> real measure" where
+ "interval_measure F = extend_measure UNIV {(a, b). a \<le> b} (\<lambda>(a, b). {a <.. b}) (\<lambda>(a, b). ereal (F b - F a))"
-lemma has_integral_indicator_UNIV:
- fixes s A :: "'a::ordered_euclidean_space set" and x :: real
- shows "((indicator (s \<inter> A) :: 'a\<Rightarrow>real) has_integral x) UNIV = ((indicator s :: _\<Rightarrow>real) has_integral x) A"
-proof -
- have "(\<lambda>x. if x \<in> A then indicator s x else 0) = (indicator (s \<inter> A) :: _\<Rightarrow>real)"
- by (auto simp: fun_eq_iff indicator_def)
- then show ?thesis
- unfolding has_integral_restrict_univ[where s=A, symmetric] by simp
-qed
+lemma emeasure_interval_measure_Ioc:
+ assumes "a \<le> b"
+ assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y"
+ assumes right_cont_F : "\<And>a. continuous (at_right a) F"
+ shows "emeasure (interval_measure F) {a <.. b} = F b - F a"
+proof (rule extend_measure_caratheodory_pair[OF interval_measure_def `a \<le> b`])
+ show "semiring_of_sets UNIV {{a<..b} |a b :: real. a \<le> b}"
+ proof (unfold_locales, safe)
+ fix a b c d :: real assume *: "a \<le> b" "c \<le> d"
+ then show "\<exists>C\<subseteq>{{a<..b} |a b. a \<le> b}. finite C \<and> disjoint C \<and> {a<..b} - {c<..d} = \<Union>C"
+ proof cases
+ let ?C = "{{a<..b}}"
+ assume "b < c \<or> d \<le> a \<or> d \<le> c"
+ with * have "?C \<subseteq> {{a<..b} |a b. a \<le> b} \<and> finite ?C \<and> disjoint ?C \<and> {a<..b} - {c<..d} = \<Union>?C"
+ by (auto simp add: disjoint_def)
+ thus ?thesis ..
+ next
+ let ?C = "{{a<..c}, {d<..b}}"
+ assume "\<not> (b < c \<or> d \<le> a \<or> d \<le> c)"
+ with * have "?C \<subseteq> {{a<..b} |a b. a \<le> b} \<and> finite ?C \<and> disjoint ?C \<and> {a<..b} - {c<..d} = \<Union>?C"
+ by (auto simp add: disjoint_def Ioc_inj) (metis linear)+
+ thus ?thesis ..
+ qed
+ qed (auto simp: Ioc_inj, metis linear)
+
+next
+ fix l r :: "nat \<Rightarrow> real" and a b :: real
+ assume l_r[simp]: "\<And>n. l n \<le> r n" and "a \<le> b" and disj: "disjoint_family (\<lambda>n. {l n<..r n})"
+ assume lr_eq_ab: "(\<Union>i. {l i<..r i}) = {a<..b}"
+
+ have [intro, simp]: "\<And>a b. a \<le> b \<Longrightarrow> 0 \<le> F b - F a"
+ by (auto intro!: l_r mono_F simp: diff_le_iff)
+
+ { fix S :: "nat set" assume "finite S"
+ moreover note `a \<le> b`
+ moreover have "\<And>i. i \<in> S \<Longrightarrow> {l i <.. r i} \<subseteq> {a <.. b}"
+ unfolding lr_eq_ab[symmetric] by auto
+ ultimately have "(\<Sum>i\<in>S. F (r i) - F (l i)) \<le> F b - F a"
+ proof (induction S arbitrary: a rule: finite_psubset_induct)
+ case (psubset S)
+ show ?case
+ proof cases
+ assume "\<exists>i\<in>S. l i < r i"
+ with `finite S` have "Min (l ` {i\<in>S. l i < r i}) \<in> l ` {i\<in>S. l i < r i}"
+ by (intro Min_in) auto
+ then obtain m where m: "m \<in> S" "l m < r m" "l m = Min (l ` {i\<in>S. l i < r i})"
+ by fastforce
-lemma
- fixes s a :: "'a::ordered_euclidean_space set"
- shows integral_indicator_UNIV:
- "integral UNIV (indicator (s \<inter> A) :: 'a\<Rightarrow>real) = integral A (indicator s :: _\<Rightarrow>real)"
- and integrable_indicator_UNIV:
- "(indicator (s \<inter> A) :: 'a\<Rightarrow>real) integrable_on UNIV \<longleftrightarrow> (indicator s :: 'a\<Rightarrow>real) integrable_on A"
- unfolding integral_def integrable_on_def has_integral_indicator_UNIV by auto
+ have "(\<Sum>i\<in>S. F (r i) - F (l i)) = (F (r m) - F (l m)) + (\<Sum>i\<in>S - {m}. F (r i) - F (l i))"
+ using m psubset by (intro setsum.remove) auto
+ also have "(\<Sum>i\<in>S - {m}. F (r i) - F (l i)) \<le> F b - F (r m)"
+ proof (intro psubset.IH)
+ show "S - {m} \<subset> S"
+ using `m\<in>S` by auto
+ show "r m \<le> b"
+ using psubset.prems(2)[OF `m\<in>S`] `l m < r m` by auto
+ next
+ fix i assume "i \<in> S - {m}"
+ then have i: "i \<in> S" "i \<noteq> m" by auto
+ { assume i': "l i < r i" "l i < r m"
+ moreover with `finite S` i m have "l m \<le> l i"
+ by auto
+ ultimately have "{l i <.. r i} \<inter> {l m <.. r m} \<noteq> {}"
+ by auto
+ then have False
+ using disjoint_family_onD[OF disj, of i m] i by auto }
+ then have "l i \<noteq> r i \<Longrightarrow> r m \<le> l i"
+ unfolding not_less[symmetric] using l_r[of i] by auto
+ then show "{l i <.. r i} \<subseteq> {r m <.. b}"
+ using psubset.prems(2)[OF `i\<in>S`] by auto
+ qed
+ also have "F (r m) - F (l m) \<le> F (r m) - F a"
+ using psubset.prems(2)[OF `m \<in> S`] `l m < r m`
+ by (auto simp add: Ioc_subset_iff intro!: mono_F)
+ finally show ?case
+ by (auto intro: add_mono)
+ qed (simp add: `a \<le> b` less_le)
+ qed }
+ note claim1 = this
+
+ (* second key induction: a lower bound on the measures of any finite collection of Ai's
+ that cover an interval {u..v} *)
+
+ { fix S u v and l r :: "nat \<Rightarrow> real"
+ assume "finite S" "\<And>i. i\<in>S \<Longrightarrow> l i < r i" "{u..v} \<subseteq> (\<Union>i\<in>S. {l i<..< r i})"
+ then have "F v - F u \<le> (\<Sum>i\<in>S. F (r i) - F (l i))"
+ proof (induction arbitrary: v u rule: finite_psubset_induct)
+ case (psubset S)
+ show ?case
+ proof cases
+ assume "S = {}" then show ?case
+ using psubset by (simp add: mono_F)
+ next
+ assume "S \<noteq> {}"
+ then obtain j where "j \<in> S"
+ by auto
-subsection {* Standard Cubes *}
-
-definition cube :: "nat \<Rightarrow> 'a::ordered_euclidean_space set" where
- "cube n \<equiv> {\<Sum>i\<in>Basis. - n *\<^sub>R i .. \<Sum>i\<in>Basis. n *\<^sub>R i}"
+ let ?R = "r j < u \<or> l j > v \<or> (\<exists>i\<in>S-{j}. l i \<le> l j \<and> r j \<le> r i)"
+ show ?case
+ proof cases
+ assume "?R"
+ with `j \<in> S` psubset.prems have "{u..v} \<subseteq> (\<Union>i\<in>S-{j}. {l i<..< r i})"
+ apply (auto simp: subset_eq Ball_def)
+ apply (metis Diff_iff less_le_trans leD linear singletonD)
+ apply (metis Diff_iff less_le_trans leD linear singletonD)
+ apply (metis order_trans less_le_not_le linear)
+ done
+ with `j \<in> S` have "F v - F u \<le> (\<Sum>i\<in>S - {j}. F (r i) - F (l i))"
+ by (intro psubset) auto
+ also have "\<dots> \<le> (\<Sum>i\<in>S. F (r i) - F (l i))"
+ using psubset.prems
+ by (intro setsum_mono2 psubset) (auto intro: less_imp_le)
+ finally show ?thesis .
+ next
+ assume "\<not> ?R"
+ then have j: "u \<le> r j" "l j \<le> v" "\<And>i. i \<in> S - {j} \<Longrightarrow> r i < r j \<or> l i > l j"
+ by (auto simp: not_less)
+ let ?S1 = "{i \<in> S. l i < l j}"
+ let ?S2 = "{i \<in> S. r i > r j}"
-lemma borel_cube[intro]: "cube n \<in> sets borel"
- unfolding cube_def by auto
+ have "(\<Sum>i\<in>S. F (r i) - F (l i)) \<ge> (\<Sum>i\<in>?S1 \<union> ?S2 \<union> {j}. F (r i) - F (l i))"
+ using `j \<in> S` `finite S` psubset.prems j
+ by (intro setsum_mono2) (auto intro: less_imp_le)
+ also have "(\<Sum>i\<in>?S1 \<union> ?S2 \<union> {j}. F (r i) - F (l i)) =
+ (\<Sum>i\<in>?S1. F (r i) - F (l i)) + (\<Sum>i\<in>?S2 . F (r i) - F (l i)) + (F (r j) - F (l j))"
+ using psubset(1) psubset.prems(1) j
+ apply (subst setsum.union_disjoint)
+ apply simp_all
+ apply (subst setsum.union_disjoint)
+ apply auto
+ apply (metis less_le_not_le)
+ done
+ also (xtrans) have "(\<Sum>i\<in>?S1. F (r i) - F (l i)) \<ge> F (l j) - F u"
+ using `j \<in> S` `finite S` psubset.prems j
+ apply (intro psubset.IH psubset)
+ apply (auto simp: subset_eq Ball_def)
+ apply (metis less_le_trans not_le)
+ done
+ also (xtrans) have "(\<Sum>i\<in>?S2. F (r i) - F (l i)) \<ge> F v - F (r j)"
+ using `j \<in> S` `finite S` psubset.prems j
+ apply (intro psubset.IH psubset)
+ apply (auto simp: subset_eq Ball_def)
+ apply (metis le_less_trans not_le)
+ done
+ finally (xtrans) show ?case
+ by (auto simp: add_mono)
+ qed
+ qed
+ qed }
+ note claim2 = this
-lemma cube_closed[intro]: "closed (cube n)"
- unfolding cube_def by auto
+ (* now prove the inequality going the other way *)
-lemma cube_subset[intro]: "n \<le> N \<Longrightarrow> cube n \<subseteq> cube N"
- by (fastforce simp: eucl_le[where 'a='a] cube_def setsum_negf)
+ { fix epsilon :: real assume egt0: "epsilon > 0"
+ have "\<forall>i. \<exists>d. d > 0 & F (r i + d) < F (r i) + epsilon / 2^(i+2)"
+ proof
+ fix i
+ note right_cont_F [of "r i"]
+ thus "\<exists>d. d > 0 \<and> F (r i + d) < F (r i) + epsilon / 2^(i+2)"
+ apply -
+ apply (subst (asm) continuous_at_right_real_increasing)
+ apply (rule mono_F, assumption)
+ apply (drule_tac x = "epsilon / 2 ^ (i + 2)" in spec)
+ apply (erule impE)
+ using egt0 by (auto simp add: field_simps)
+ qed
+ then obtain delta where
+ deltai_gt0: "\<And>i. delta i > 0" and
+ deltai_prop: "\<And>i. F (r i + delta i) < F (r i) + epsilon / 2^(i+2)"
+ by metis
+ have "\<exists>a' > a. F a' - F a < epsilon / 2"
+ apply (insert right_cont_F [of a])
+ apply (subst (asm) continuous_at_right_real_increasing)
+ using mono_F apply force
+ apply (drule_tac x = "epsilon / 2" in spec)
+ using egt0 apply (auto simp add: field_simps)
+ by (metis add_less_cancel_left comm_monoid_add_class.add.right_neutral
+ comm_semiring_1_class.normalizing_semiring_rules(24) mult_2 mult_2_right)
+ then obtain a' where a'lea [arith]: "a' > a" and
+ a_prop: "F a' - F a < epsilon / 2"
+ by auto
+ def S' \<equiv> "{i. l i < r i}"
+ obtain S :: "nat set" where
+ "S \<subseteq> S'" and finS: "finite S" and
+ Sprop: "{a'..b} \<subseteq> (\<Union>i \<in> S. {l i<..<r i + delta i})"
+ proof (rule compactE_image)
+ show "compact {a'..b}"
+ by (rule compact_Icc)
+ show "\<forall>i \<in> S'. open ({l i<..<r i + delta i})" by auto
+ have "{a'..b} \<subseteq> {a <.. b}"
+ by auto
+ also have "{a <.. b} = (\<Union>i\<in>S'. {l i<..r i})"
+ unfolding lr_eq_ab[symmetric] by (fastforce simp add: S'_def intro: less_le_trans)
+ also have "\<dots> \<subseteq> (\<Union>i \<in> S'. {l i<..<r i + delta i})"
+ apply (intro UN_mono)
+ apply (auto simp: S'_def)
+ apply (cut_tac i=i in deltai_gt0)
+ apply simp
+ done
+ finally show "{a'..b} \<subseteq> (\<Union>i \<in> S'. {l i<..<r i + delta i})" .
+ qed
+ with S'_def have Sprop2: "\<And>i. i \<in> S \<Longrightarrow> l i < r i" by auto
+ from finS have "\<exists>n. \<forall>i \<in> S. i \<le> n"
+ by (subst finite_nat_set_iff_bounded_le [symmetric])
+ then obtain n where Sbound [rule_format]: "\<forall>i \<in> S. i \<le> n" ..
+ have "F b - F a' \<le> (\<Sum>i\<in>S. F (r i + delta i) - F (l i))"
+ apply (rule claim2 [rule_format])
+ using finS Sprop apply auto
+ apply (frule Sprop2)
+ apply (subgoal_tac "delta i > 0")
+ apply arith
+ by (rule deltai_gt0)
+ also have "... \<le> (SUM i : S. F(r i) - F(l i) + epsilon / 2^(i+2))"
+ apply (rule setsum_mono)
+ apply simp
+ apply (rule order_trans)
+ apply (rule less_imp_le)
+ apply (rule deltai_prop)
+ by auto
+ also have "... = (SUM i : S. F(r i) - F(l i)) +
+ (epsilon / 4) * (SUM i : S. (1 / 2)^i)" (is "_ = ?t + _")
+ by (subst setsum.distrib) (simp add: field_simps setsum_right_distrib)
+ also have "... \<le> ?t + (epsilon / 4) * (\<Sum> i < Suc n. (1 / 2)^i)"
+ apply (rule add_left_mono)
+ apply (rule mult_left_mono)
+ apply (rule setsum_mono2)
+ using egt0 apply auto
+ by (frule Sbound, auto)
+ also have "... \<le> ?t + (epsilon / 2)"
+ apply (rule add_left_mono)
+ apply (subst geometric_sum)
+ apply auto
+ apply (rule mult_left_mono)
+ using egt0 apply auto
+ done
+ finally have aux2: "F b - F a' \<le> (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon / 2"
+ by simp
-lemma cube_subset_iff: "cube n \<subseteq> cube N \<longleftrightarrow> n \<le> N"
- unfolding cube_def subset_box by (simp add: setsum_negf ex_in_conv eucl_le[where 'a='a])
+ have "F b - F a = (F b - F a') + (F a' - F a)"
+ by auto
+ also have "... \<le> (F b - F a') + epsilon / 2"
+ using a_prop by (intro add_left_mono) simp
+ also have "... \<le> (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon / 2 + epsilon / 2"
+ apply (intro add_right_mono)
+ apply (rule aux2)
+ done
+ also have "... = (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon"
+ by auto
+ also have "... \<le> (\<Sum>i\<le>n. F (r i) - F (l i)) + epsilon"
+ using finS Sbound Sprop by (auto intro!: add_right_mono setsum_mono3)
+ finally have "ereal (F b - F a) \<le> (\<Sum>i\<le>n. ereal (F (r i) - F (l i))) + epsilon"
+ by simp
+ then have "ereal (F b - F a) \<le> (\<Sum>i. ereal (F (r i) - F (l i))) + (epsilon :: real)"
+ apply (rule_tac order_trans)
+ prefer 2
+ apply (rule add_mono[where c="ereal epsilon"])
+ apply (rule suminf_upper[of _ "Suc n"])
+ apply (auto simp add: lessThan_Suc_atMost)
+ done }
+ hence "ereal (F b - F a) \<le> (\<Sum>i. ereal (F (r i) - F (l i)))"
+ by (auto intro: ereal_le_epsilon2)
+ moreover
+ have "(\<Sum>i. ereal (F (r i) - F (l i))) \<le> ereal (F b - F a)"
+ by (auto simp add: claim1 intro!: suminf_bound)
+ ultimately show "(\<Sum>n. ereal (F (r n) - F (l n))) = ereal (F b - F a)"
+ by simp
+qed (auto simp: Ioc_inj diff_le_iff mono_F)
-lemma ball_subset_cube: "ball (0::'a::ordered_euclidean_space) (real n) \<subseteq> cube n"
- apply (simp add: cube_def subset_eq mem_box setsum_negf eucl_le[where 'a='a])
-proof safe
- fix x i :: 'a assume x: "x \<in> ball 0 (real n)" and i: "i \<in> Basis"
- thus "- real n \<le> x \<bullet> i" "real n \<ge> x \<bullet> i"
- using Basis_le_norm[OF i, of x] by(auto simp: dist_norm)
-qed
+lemma measure_interval_measure_Ioc:
+ assumes "a \<le> b"
+ assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y"
+ assumes right_cont_F : "\<And>a. continuous (at_right a) F"
+ shows "measure (interval_measure F) {a <.. b} = F b - F a"
+ unfolding measure_def
+ apply (subst emeasure_interval_measure_Ioc)
+ apply fact+
+ apply simp
+ done
+
+lemma emeasure_interval_measure_Ioc_eq:
+ "(\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y) \<Longrightarrow> (\<And>a. continuous (at_right a) F) \<Longrightarrow>
+ emeasure (interval_measure F) {a <.. b} = (if a \<le> b then F b - F a else 0)"
+ using emeasure_interval_measure_Ioc[of a b F] by auto
+
+lemma sets_interval_measure [simp]: "sets (interval_measure F) = sets borel"
+ apply (simp add: sets_extend_measure interval_measure_def borel_sigma_sets_Ioc)
+ apply (rule sigma_sets_eqI)
+ apply auto
+ apply (case_tac "a \<le> ba")
+ apply (auto intro: sigma_sets.Empty)
+ done
+
+lemma space_interval_measure [simp]: "space (interval_measure F) = UNIV"
+ by (simp add: interval_measure_def space_extend_measure)
+
+lemma emeasure_interval_measure_Icc:
+ assumes "a \<le> b"
+ assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y"
+ assumes cont_F : "continuous_on UNIV F"
+ shows "emeasure (interval_measure F) {a .. b} = F b - F a"
+proof (rule tendsto_unique)
+ { fix a b :: real assume "a \<le> b" then have "emeasure (interval_measure F) {a <.. b} = F b - F a"
+ using cont_F
+ by (subst emeasure_interval_measure_Ioc)
+ (auto intro: mono_F continuous_within_subset simp: continuous_on_eq_continuous_within) }
+ note * = this
-lemma mem_big_cube: obtains n where "x \<in> cube n"
+ let ?F = "interval_measure F"
+ show "((\<lambda>a. F b - F a) ---> emeasure ?F {a..b}) (at_left a)"
+ proof (rule tendsto_at_left_sequentially)
+ show "a - 1 < a" by simp
+ fix X assume "\<And>n. X n < a" "incseq X" "X ----> a"
+ with `a \<le> b` have "(\<lambda>n. emeasure ?F {X n<..b}) ----> emeasure ?F (\<Inter>n. {X n <..b})"
+ apply (intro Lim_emeasure_decseq)
+ apply (auto simp: decseq_def incseq_def emeasure_interval_measure_Ioc *)
+ apply force
+ apply (subst (asm ) *)
+ apply (auto intro: less_le_trans less_imp_le)
+ done
+ also have "(\<Inter>n. {X n <..b}) = {a..b}"
+ using `\<And>n. X n < a`
+ apply auto
+ apply (rule LIMSEQ_le_const2[OF `X ----> a`])
+ apply (auto intro: less_imp_le)
+ apply (auto intro: less_le_trans)
+ done
+ also have "(\<lambda>n. emeasure ?F {X n<..b}) = (\<lambda>n. F b - F (X n))"
+ using `\<And>n. X n < a` `a \<le> b` by (subst *) (auto intro: less_imp_le less_le_trans)
+ finally show "(\<lambda>n. F b - F (X n)) ----> emeasure ?F {a..b}" .
+ qed
+ show "((\<lambda>a. ereal (F b - F a)) ---> F b - F a) (at_left a)"
+ using cont_F
+ by (intro lim_ereal[THEN iffD2] tendsto_intros )
+ (auto simp: continuous_on_def intro: tendsto_within_subset)
+qed (rule trivial_limit_at_left_real)
+
+lemma sigma_finite_interval_measure:
+ assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y"
+ assumes right_cont_F : "\<And>a. continuous (at_right a) F"
+ shows "sigma_finite_measure (interval_measure F)"
+ apply unfold_locales
+ apply (intro exI[of _ "(\<lambda>(a, b). {a <.. b}) ` (\<rat> \<times> \<rat>)"])
+ apply (auto intro!: Rats_no_top_le Rats_no_bot_less countable_rat simp: emeasure_interval_measure_Ioc_eq[OF assms])
+ done
+
+subsection {* Lebesgue-Borel measure *}
+
+definition lborel :: "('a :: euclidean_space) measure" where
+ "lborel = distr (\<Pi>\<^sub>M b\<in>Basis. interval_measure (\<lambda>x. x)) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)"
+
+lemma
+ shows sets_lborel[simp]: "sets lborel = sets borel"
+ and space_lborel[simp]: "space lborel = space borel"
+ and measurable_lborel1[simp]: "measurable M lborel = measurable M borel"
+ and measurable_lborel2[simp]: "measurable lborel M = measurable borel M"
+ by (simp_all add: lborel_def)
+
+context
+begin
+
+interpretation sigma_finite_measure "interval_measure (\<lambda>x. x)"
+ by (rule sigma_finite_interval_measure) auto
+interpretation finite_product_sigma_finite "\<lambda>_. interval_measure (\<lambda>x. x)" Basis
+ proof qed simp
+
+lemma lborel_eq_real: "lborel = interval_measure (\<lambda>x. x)"
+ unfolding lborel_def Basis_real_def
+ using distr_id[of "interval_measure (\<lambda>x. x)"]
+ by (subst distr_component[symmetric])
+ (simp_all add: distr_distr comp_def del: distr_id cong: distr_cong)
+
+lemma lborel_eq: "lborel = distr (\<Pi>\<^sub>M b\<in>Basis. lborel) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)"
+ by (subst lborel_def) (simp add: lborel_eq_real)
+
+lemma nn_integral_lborel_setprod:
+ assumes [measurable]: "\<And>b. b \<in> Basis \<Longrightarrow> f b \<in> borel_measurable borel"
+ assumes nn[simp]: "\<And>b x. b \<in> Basis \<Longrightarrow> 0 \<le> f b x"
+ shows "(\<integral>\<^sup>+x. (\<Prod>b\<in>Basis. f b (x \<bullet> b)) \<partial>lborel) = (\<Prod>b\<in>Basis. (\<integral>\<^sup>+x. f b x \<partial>lborel))"
+ by (simp add: lborel_def nn_integral_distr product_nn_integral_setprod
+ product_nn_integral_singleton)
+
+lemma emeasure_lborel_Icc[simp]:
+ fixes l u :: real
+ assumes [simp]: "l \<le> u"
+ shows "emeasure lborel {l .. u} = u - l"
proof -
- from reals_Archimedean2[of "norm x"] guess n ..
- with ball_subset_cube[unfolded subset_eq, of n]
- show ?thesis
- by (intro that[where n=n]) (auto simp add: dist_norm)
-qed
-
-lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)"
- unfolding cube_def cbox_interval[symmetric] subset_box by (simp add: setsum_negf)
-
-lemma has_integral_interval_cube:
- fixes a b :: "'a::ordered_euclidean_space"
- shows "(indicator {a .. b} has_integral content ({a .. b} \<inter> cube n)) (cube n)"
- (is "(?I has_integral content ?R) (cube n)")
-proof -
- have [simp]: "(\<lambda>x. if x \<in> cube n then ?I x else 0) = indicator ?R"
- by (auto simp: indicator_def cube_def fun_eq_iff eucl_le[where 'a='a])
- have "(?I has_integral content ?R) (cube n) \<longleftrightarrow> (indicator ?R has_integral content ?R) UNIV"
- unfolding has_integral_restrict_univ[where s="cube n", symmetric] by simp
- also have "\<dots> \<longleftrightarrow> ((\<lambda>x. 1::real) has_integral content ?R *\<^sub>R 1) ?R"
- unfolding indicator_def [abs_def] has_integral_restrict_univ real_scaleR_def mult_1_right ..
- also have "((\<lambda>x. 1) has_integral content ?R *\<^sub>R 1) ?R"
- unfolding cube_def inter_interval cbox_interval[symmetric] by (rule has_integral_const)
- finally show ?thesis .
+ have "((\<lambda>f. f 1) -` {l..u} \<inter> space (Pi\<^sub>M {1} (\<lambda>b. interval_measure (\<lambda>x. x)))) = {1::real} \<rightarrow>\<^sub>E {l..u}"
+ by (auto simp: space_PiM)
+ then show ?thesis
+ by (simp add: lborel_def emeasure_distr emeasure_PiM emeasure_interval_measure_Icc continuous_on_id)
qed
-subsection {* Lebesgue measure *}
-
-definition lebesgue :: "'a::ordered_euclidean_space measure" where
- "lebesgue = measure_of UNIV {A. \<forall>n. (indicator A :: 'a \<Rightarrow> real) integrable_on cube n}
- (\<lambda>A. SUP n. ereal (integral (cube n) (indicator A)))"
-
-lemma space_lebesgue[simp]: "space lebesgue = UNIV"
- unfolding lebesgue_def by simp
-
-lemma lebesgueI: "(\<And>n. (indicator A :: _ \<Rightarrow> real) integrable_on cube n) \<Longrightarrow> A \<in> sets lebesgue"
- unfolding lebesgue_def by simp
-
-lemma sigma_algebra_lebesgue:
- defines "leb \<equiv> {A. \<forall>n. (indicator A :: 'a::ordered_euclidean_space \<Rightarrow> real) integrable_on cube n}"
- shows "sigma_algebra UNIV leb"
-proof (safe intro!: sigma_algebra_iff2[THEN iffD2])
- fix A assume A: "A \<in> leb"
- moreover have "indicator (UNIV - A) = (\<lambda>x. 1 - indicator A x :: real)"
- by (auto simp: fun_eq_iff indicator_def)
- ultimately show "UNIV - A \<in> leb"
- using A by (auto intro!: integrable_sub simp: cube_def leb_def)
-next
- fix n show "{} \<in> leb"
- by (auto simp: cube_def indicator_def[abs_def] leb_def)
-next
- fix A :: "nat \<Rightarrow> _" assume A: "range A \<subseteq> leb"
- have "\<forall>n. (indicator (\<Union>i. A i) :: _ \<Rightarrow> real) integrable_on cube n" (is "\<forall>n. ?g integrable_on _")
- proof (intro dominated_convergence[where g="?g"] ballI allI)
- fix k n show "(indicator (\<Union>i<k. A i) :: _ \<Rightarrow> real) integrable_on cube n"
- proof (induct k)
- case (Suc k)
- have *: "(\<Union> i<Suc k. A i) = (\<Union> i<k. A i) \<union> A k"
- unfolding lessThan_Suc UN_insert by auto
- have *: "(\<lambda>x. max (indicator (\<Union> i<k. A i) x) (indicator (A k) x) :: real) =
- indicator (\<Union> i<Suc k. A i)" (is "(\<lambda>x. max (?f x) (?g x)) = _")
- by (auto simp: fun_eq_iff * indicator_def)
- show ?case
- using absolutely_integrable_max[of ?f "cube n" ?g] A Suc
- by (simp add: * leb_def subset_eq)
- qed auto
- qed (auto intro: LIMSEQ_indicator_UN simp: cube_def)
- then show "(\<Union>i. A i) \<in> leb" by (auto simp: leb_def)
-qed simp
-
-lemma sets_lebesgue: "sets lebesgue = {A. \<forall>n. (indicator A :: _ \<Rightarrow> real) integrable_on cube n}"
- unfolding lebesgue_def sigma_algebra.sets_measure_of_eq[OF sigma_algebra_lebesgue] ..
-
-lemma lebesgueD: "A \<in> sets lebesgue \<Longrightarrow> (indicator A :: _ \<Rightarrow> real) integrable_on cube n"
- unfolding sets_lebesgue by simp
+lemma emeasure_lborel_Icc_eq: "emeasure lborel {l .. u} = ereal (if l \<le> u then u - l else 0)"
+ by simp
-lemma emeasure_lebesgue:
- assumes "A \<in> sets lebesgue"
- shows "emeasure lebesgue A = (SUP n. ereal (integral (cube n) (indicator A)))"
- (is "_ = ?\<mu> A")
-proof (rule emeasure_measure_of[OF lebesgue_def])
- have *: "indicator {} = (\<lambda>x. 0 :: real)" by (simp add: fun_eq_iff)
- show "positive (sets lebesgue) ?\<mu>"
- proof (unfold positive_def, intro conjI ballI)
- show "?\<mu> {} = 0" by (simp add: integral_0 *)
- fix A :: "'a set" assume "A \<in> sets lebesgue" then show "0 \<le> ?\<mu> A"
- by (auto intro!: SUP_upper2 Integration.integral_nonneg simp: sets_lebesgue)
- qed
-next
- show "countably_additive (sets lebesgue) ?\<mu>"
- proof (intro countably_additive_def[THEN iffD2] allI impI)
- fix A :: "nat \<Rightarrow> 'a set" assume rA: "range A \<subseteq> sets lebesgue" "disjoint_family A"
- then have A[simp, intro]: "\<And>i n. (indicator (A i) :: _ \<Rightarrow> real) integrable_on cube n"
- by (auto dest: lebesgueD)
- let ?m = "\<lambda>n i. integral (cube n) (indicator (A i) :: _\<Rightarrow>real)"
- let ?M = "\<lambda>n I. integral (cube n) (indicator (\<Union>i\<in>I. A i) :: _\<Rightarrow>real)"
- have nn[simp, intro]: "\<And>i n. 0 \<le> ?m n i" by (auto intro!: Integration.integral_nonneg)
- assume "(\<Union>i. A i) \<in> sets lebesgue"
- then have UN_A[simp, intro]: "\<And>i n. (indicator (\<Union>i. A i) :: _ \<Rightarrow> real) integrable_on cube n"
- by (auto simp: sets_lebesgue)
- show "(\<Sum>n. ?\<mu> (A n)) = ?\<mu> (\<Union>i. A i)"
- proof (subst suminf_SUP_eq, safe intro!: incseq_SucI)
- fix i n show "ereal (?m n i) \<le> ereal (?m (Suc n) i)"
- using cube_subset[of n "Suc n"] by (auto intro!: integral_subset_le incseq_SucI)
- next
- fix i n show "0 \<le> ereal (?m n i)"
- using rA unfolding lebesgue_def
- by (auto intro!: SUP_upper2 integral_nonneg)
- next
- show "(SUP n. \<Sum>i. ereal (?m n i)) = (SUP n. ereal (?M n UNIV))"
- proof (intro arg_cong[where f="SUPREMUM UNIV"] ext sums_unique[symmetric] sums_ereal[THEN iffD2] sums_def[THEN iffD2])
- fix n
- have "\<And>m. (UNION {..<m} A) \<in> sets lebesgue" using rA by auto
- from lebesgueD[OF this]
- have "(\<lambda>m. ?M n {..< m}) ----> ?M n UNIV"
- (is "(\<lambda>m. integral _ (?A m)) ----> ?I")
- by (intro dominated_convergence(2)[where f="?A" and h="\<lambda>x. 1::real"])
- (auto intro: LIMSEQ_indicator_UN simp: cube_def)
- moreover
- { fix m have *: "(\<Sum>x<m. ?m n x) = ?M n {..< m}"
- proof (induct m)
- case (Suc m)
- have "(\<Union>i<m. A i) \<in> sets lebesgue" using rA by auto
- then have "(indicator (\<Union>i<m. A i) :: _\<Rightarrow>real) integrable_on (cube n)"
- by (auto dest!: lebesgueD)
- moreover
- have "(\<Union>i<m. A i) \<inter> A m = {}"
- using rA(2)[unfolded disjoint_family_on_def, THEN bspec, of m]
- by auto
- then have "\<And>x. indicator (\<Union>i<Suc m. A i) x =
- indicator (\<Union>i<m. A i) x + (indicator (A m) x :: real)"
- by (auto simp: indicator_add lessThan_Suc ac_simps)
- ultimately show ?case
- using Suc A by (simp add: Integration.integral_add[symmetric])
- qed auto }
- ultimately show "(\<lambda>m. \<Sum>x<m. ?m n x) ----> ?M n UNIV"
- by (simp add: atLeast0LessThan)
- qed
- qed
- qed
-qed (auto, fact)
-
-lemma lebesgueI_borel[intro, simp]:
- fixes s::"'a::ordered_euclidean_space set"
- assumes "s \<in> sets borel" shows "s \<in> sets lebesgue"
+lemma emeasure_lborel_cbox[simp]:
+ assumes [simp]: "\<And>b. b \<in> Basis \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b"
+ shows "emeasure lborel (cbox l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
proof -
- have "s \<in> sigma_sets (space lebesgue) (range (\<lambda>(a, b). {a .. (b :: 'a\<Colon>ordered_euclidean_space)}))"
- using assms by (simp add: borel_eq_atLeastAtMost)
- also have "\<dots> \<subseteq> sets lebesgue"
- proof (safe intro!: sets.sigma_sets_subset lebesgueI)
- fix n :: nat and a b :: 'a
- show "(indicator {a..b} :: 'a\<Rightarrow>real) integrable_on cube n"
- unfolding integrable_on_def using has_integral_interval_cube[of a b] by auto
- qed
+ have "(\<lambda>x. \<Prod>b\<in>Basis. indicator {l\<bullet>b .. u\<bullet>b} (x \<bullet> b) :: ereal) = indicator (cbox l u)"
+ by (auto simp: fun_eq_iff cbox_def setprod_ereal_0 split: split_indicator)
+ then have "emeasure lborel (cbox l u) = (\<integral>\<^sup>+x. (\<Prod>b\<in>Basis. indicator {l\<bullet>b .. u\<bullet>b} (x \<bullet> b)) \<partial>lborel)"
+ by simp
+ also have "\<dots> = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
+ by (subst nn_integral_lborel_setprod) (simp_all add: setprod_ereal inner_diff_left)
finally show ?thesis .
qed
-lemma borel_measurable_lebesgueI:
- "f \<in> borel_measurable borel \<Longrightarrow> f \<in> borel_measurable lebesgue"
- unfolding measurable_def by simp
+lemma AE_lborel_singleton: "AE x in lborel::'a::euclidean_space measure. x \<noteq> c"
+ using AE_discrete_difference[of "{c::'a}" lborel] emeasure_lborel_cbox[of c c]
+ by (auto simp del: emeasure_lborel_cbox simp add: cbox_sing setprod_constant)
-lemma lebesgueI_negligible[dest]: fixes s::"'a::ordered_euclidean_space set"
- assumes "negligible s" shows "s \<in> sets lebesgue"
- using assms by (force simp: cbox_interval[symmetric] cube_def integrable_on_def negligible_def intro!: lebesgueI)
-
-lemma lmeasure_eq_0:
- fixes S :: "'a::ordered_euclidean_space set"
- assumes "negligible S" shows "emeasure lebesgue S = 0"
+lemma emeasure_lborel_Ioo[simp]:
+ assumes [simp]: "l \<le> u"
+ shows "emeasure lborel {l <..< u} = ereal (u - l)"
proof -
- have "\<And>n. integral (cube n) (indicator S :: 'a\<Rightarrow>real) = 0"
- unfolding lebesgue_integral_def using assms
- by (intro integral_unique some1_equality ex_ex1I)
- (auto simp: cube_def negligible_def cbox_interval[symmetric])
+ have "emeasure lborel {l <..< u} = emeasure lborel {l .. u}"
+ using AE_lborel_singleton[of u] AE_lborel_singleton[of l] by (intro emeasure_eq_AE) auto
then show ?thesis
- using assms by (simp add: emeasure_lebesgue lebesgueI_negligible)
-qed
-
-lemma lmeasure_iff_LIMSEQ:
- assumes A: "A \<in> sets lebesgue" and "0 \<le> m"
- shows "emeasure lebesgue A = ereal m \<longleftrightarrow> (\<lambda>n. integral (cube n) (indicator A :: _ \<Rightarrow> real)) ----> m"
-proof (subst emeasure_lebesgue[OF A], intro SUP_eq_LIMSEQ)
- show "mono (\<lambda>n. integral (cube n) (indicator A::_=>real))"
- using cube_subset assms by (intro monoI integral_subset_le) (auto dest!: lebesgueD)
+ by simp
qed
-lemma lmeasure_finite_has_integral:
- fixes s :: "'a::ordered_euclidean_space set"
- assumes "s \<in> sets lebesgue" "emeasure lebesgue s = ereal m"
- shows "(indicator s has_integral m) UNIV"
+lemma emeasure_lborel_Ioc[simp]:
+ assumes [simp]: "l \<le> u"
+ shows "emeasure lborel {l <.. u} = ereal (u - l)"
proof -
- let ?I = "indicator :: 'a set \<Rightarrow> 'a \<Rightarrow> real"
- have "0 \<le> m"
- using emeasure_nonneg[of lebesgue s] `emeasure lebesgue s = ereal m` by simp
- have **: "(?I s) integrable_on UNIV \<and> (\<lambda>k. integral UNIV (?I (s \<inter> cube k))) ----> integral UNIV (?I s)"
- proof (intro monotone_convergence_increasing allI ballI)
- have LIMSEQ: "(\<lambda>n. integral (cube n) (?I s)) ----> m"
- using assms(2) unfolding lmeasure_iff_LIMSEQ[OF assms(1) `0 \<le> m`] .
- { fix n have "integral (cube n) (?I s) \<le> m"
- using cube_subset assms
- by (intro incseq_le[where L=m] LIMSEQ incseq_def[THEN iffD2] integral_subset_le allI impI)
- (auto dest!: lebesgueD) }
- moreover
- { fix n have "0 \<le> integral (cube n) (?I s)"
- using assms by (auto dest!: lebesgueD intro!: Integration.integral_nonneg) }
- ultimately
- show "bounded {integral UNIV (?I (s \<inter> cube k)) |k. True}"
- unfolding bounded_def
- apply (rule_tac exI[of _ 0])
- apply (rule_tac exI[of _ m])
- by (auto simp: dist_real_def integral_indicator_UNIV)
- fix k show "?I (s \<inter> cube k) integrable_on UNIV"
- unfolding integrable_indicator_UNIV using assms by (auto dest!: lebesgueD)
- fix x show "?I (s \<inter> cube k) x \<le> ?I (s \<inter> cube (Suc k)) x"
- using cube_subset[of k "Suc k"] by (auto simp: indicator_def)
- next
- fix x :: 'a
- from mem_big_cube obtain k where k: "x \<in> cube k" .
- { fix n have "?I (s \<inter> cube (n + k)) x = ?I s x"
- using k cube_subset[of k "n + k"] by (auto simp: indicator_def) }
- note * = this
- show "(\<lambda>k. ?I (s \<inter> cube k) x) ----> ?I s x"
- by (rule LIMSEQ_offset[where k=k]) (auto simp: *)
- qed
- note ** = conjunctD2[OF this]
- have m: "m = integral UNIV (?I s)"
- apply (intro LIMSEQ_unique[OF _ **(2)])
- using assms(2) unfolding lmeasure_iff_LIMSEQ[OF assms(1) `0 \<le> m`] integral_indicator_UNIV .
- show ?thesis
- unfolding m by (intro integrable_integral **)
+ have "emeasure lborel {l <.. u} = emeasure lborel {l .. u}"
+ using AE_lborel_singleton[of u] AE_lborel_singleton[of l] by (intro emeasure_eq_AE) auto
+ then show ?thesis
+ by simp
qed
-lemma lmeasure_finite_integrable: assumes s: "s \<in> sets lebesgue" and "emeasure lebesgue s \<noteq> \<infinity>"
- shows "(indicator s :: _ \<Rightarrow> real) integrable_on UNIV"
-proof (cases "emeasure lebesgue s")
- case (real m)
- with lmeasure_finite_has_integral[OF `s \<in> sets lebesgue` this] emeasure_nonneg[of lebesgue s]
- show ?thesis unfolding integrable_on_def by auto
-qed (insert assms emeasure_nonneg[of lebesgue s], auto)
-
-lemma has_integral_lebesgue: assumes "((indicator s :: _\<Rightarrow>real) has_integral m) UNIV"
- shows "s \<in> sets lebesgue"
-proof (intro lebesgueI)
- let ?I = "indicator :: 'a set \<Rightarrow> 'a \<Rightarrow> real"
- fix n show "(?I s) integrable_on cube n" unfolding cube_def
- proof (intro integrable_on_subinterval)
- show "(?I s) integrable_on UNIV"
- unfolding integrable_on_def using assms by auto
- qed auto
+lemma emeasure_lborel_Ico[simp]:
+ assumes [simp]: "l \<le> u"
+ shows "emeasure lborel {l ..< u} = ereal (u - l)"
+proof -
+ have "emeasure lborel {l ..< u} = emeasure lborel {l .. u}"
+ using AE_lborel_singleton[of u] AE_lborel_singleton[of l] by (intro emeasure_eq_AE) auto
+ then show ?thesis
+ by simp
qed
-lemma has_integral_lmeasure: assumes "((indicator s :: _\<Rightarrow>real) has_integral m) UNIV"
- shows "emeasure lebesgue s = ereal m"
-proof (intro lmeasure_iff_LIMSEQ[THEN iffD2])
- let ?I = "indicator :: 'a set \<Rightarrow> 'a \<Rightarrow> real"
- show "s \<in> sets lebesgue" using has_integral_lebesgue[OF assms] .
- show "0 \<le> m" using assms by (rule has_integral_nonneg) auto
- have "(\<lambda>n. integral UNIV (?I (s \<inter> cube n))) ----> integral UNIV (?I s)"
- proof (intro dominated_convergence(2) ballI)
- show "(?I s) integrable_on UNIV" unfolding integrable_on_def using assms by auto
- fix n show "?I (s \<inter> cube n) integrable_on UNIV"
- unfolding integrable_indicator_UNIV using `s \<in> sets lebesgue` by (auto dest: lebesgueD)
- fix x show "norm (?I (s \<inter> cube n) x) \<le> ?I s x" by (auto simp: indicator_def)
- next
- fix x :: 'a
- from mem_big_cube obtain k where k: "x \<in> cube k" .
- { fix n have "?I (s \<inter> cube (n + k)) x = ?I s x"
- using k cube_subset[of k "n + k"] by (auto simp: indicator_def) }
- note * = this
- show "(\<lambda>k. ?I (s \<inter> cube k) x) ----> ?I s x"
- by (rule LIMSEQ_offset[where k=k]) (auto simp: *)
- qed
- then show "(\<lambda>n. integral (cube n) (?I s)) ----> m"
- unfolding integral_unique[OF assms] integral_indicator_UNIV by simp
-qed
-
-lemma has_integral_iff_lmeasure:
- "(indicator A has_integral m) UNIV \<longleftrightarrow> (A \<in> sets lebesgue \<and> emeasure lebesgue A = ereal m)"
-proof
- assume "(indicator A has_integral m) UNIV"
- with has_integral_lmeasure[OF this] has_integral_lebesgue[OF this]
- show "A \<in> sets lebesgue \<and> emeasure lebesgue A = ereal m"
- by (auto intro: has_integral_nonneg)
-next
- assume "A \<in> sets lebesgue \<and> emeasure lebesgue A = ereal m"
- then show "(indicator A has_integral m) UNIV" by (intro lmeasure_finite_has_integral) auto
-qed
-
-lemma lmeasure_eq_integral: assumes "(indicator s::_\<Rightarrow>real) integrable_on UNIV"
- shows "emeasure lebesgue s = ereal (integral UNIV (indicator s))"
- using assms unfolding integrable_on_def
-proof safe
- fix y :: real assume "(indicator s has_integral y) UNIV"
- from this[unfolded has_integral_iff_lmeasure] integral_unique[OF this]
- show "emeasure lebesgue s = ereal (integral UNIV (indicator s))" by simp
+lemma emeasure_lborel_box[simp]:
+ assumes [simp]: "\<And>b. b \<in> Basis \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b"
+ shows "emeasure lborel (box l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
+proof -
+ have "(\<lambda>x. \<Prod>b\<in>Basis. indicator {l\<bullet>b <..< u\<bullet>b} (x \<bullet> b) :: ereal) = indicator (box l u)"
+ by (auto simp: fun_eq_iff box_def setprod_ereal_0 split: split_indicator)
+ then have "emeasure lborel (box l u) = (\<integral>\<^sup>+x. (\<Prod>b\<in>Basis. indicator {l\<bullet>b <..< u\<bullet>b} (x \<bullet> b)) \<partial>lborel)"
+ by simp
+ also have "\<dots> = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
+ by (subst nn_integral_lborel_setprod) (simp_all add: setprod_ereal inner_diff_left)
+ finally show ?thesis .
qed
-lemma lebesgue_simple_function_indicator:
- fixes f::"'a::ordered_euclidean_space \<Rightarrow> ereal"
- assumes f:"simple_function lebesgue f"
- shows "f = (\<lambda>x. (\<Sum>y \<in> f ` UNIV. y * indicator (f -` {y}) x))"
- by (rule, subst simple_function_indicator_representation[OF f]) auto
-
-lemma integral_eq_lmeasure:
- "(indicator s::_\<Rightarrow>real) integrable_on UNIV \<Longrightarrow> integral UNIV (indicator s) = real (emeasure lebesgue s)"
- by (subst lmeasure_eq_integral) (auto intro!: integral_nonneg)
-
-lemma lmeasure_finite: assumes "(indicator s::_\<Rightarrow>real) integrable_on UNIV" shows "emeasure lebesgue s \<noteq> \<infinity>"
- using lmeasure_eq_integral[OF assms] by auto
-
-lemma negligible_iff_lebesgue_null_sets:
- "negligible A \<longleftrightarrow> A \<in> null_sets lebesgue"
-proof
- assume "negligible A"
- from this[THEN lebesgueI_negligible] this[THEN lmeasure_eq_0]
- show "A \<in> null_sets lebesgue" by auto
-next
- assume A: "A \<in> null_sets lebesgue"
- then have *:"((indicator A) has_integral (0::real)) UNIV" using lmeasure_finite_has_integral[of A]
- by (auto simp: null_sets_def)
- show "negligible A" unfolding negligible_def
- proof (intro allI)
- fix a b :: 'a
- have integrable: "(indicator A :: _\<Rightarrow>real) integrable_on cbox a b"
- by (intro integrable_on_subcbox has_integral_integrable) (auto intro: *)
- then have "integral (cbox a b) (indicator A) \<le> (integral UNIV (indicator A) :: real)"
- using * by (auto intro!: integral_subset_le)
- moreover have "(0::real) \<le> integral (cbox a b) (indicator A)"
- using integrable by (auto intro!: integral_nonneg)
- ultimately have "integral (cbox a b) (indicator A) = (0::real)"
- using integral_unique[OF *] by auto
- then show "(indicator A has_integral (0::real)) (cbox a b)"
- using integrable_integral[OF integrable] by simp
- qed
-qed
+lemma emeasure_lborel_cbox_eq:
+ "emeasure lborel (cbox l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)"
+ using box_eq_empty(2)[THEN iffD2, of u l] by (auto simp: not_le)
-lemma lmeasure_UNIV[intro]: "emeasure lebesgue (UNIV::'a::ordered_euclidean_space set) = \<infinity>"
-proof (simp add: emeasure_lebesgue, intro SUP_PInfty bexI)
- fix n :: nat
- have "indicator UNIV = (\<lambda>x::'a. 1 :: real)" by auto
- moreover
- { have "real n \<le> (2 * real n) ^ DIM('a)"
- proof (cases n)
- case 0 then show ?thesis by auto
- next
- case (Suc n')
- have "real n \<le> (2 * real n)^1" by auto
- also have "(2 * real n)^1 \<le> (2 * real n) ^ DIM('a)"
- using Suc DIM_positive[where 'a='a]
- by (intro power_increasing) (auto simp: real_of_nat_Suc simp del: DIM_positive)
- finally show ?thesis .
- qed }
- ultimately show "ereal (real n) \<le> ereal (integral (cube n) (indicator UNIV::'a\<Rightarrow>real))"
- using integral_const DIM_positive[where 'a='a]
- by (auto simp: cube_def content_cbox_cases setprod_constant setsum_negf cbox_interval[symmetric])
-qed simp
-
-lemma lmeasure_complete: "A \<subseteq> B \<Longrightarrow> B \<in> null_sets lebesgue \<Longrightarrow> A \<in> null_sets lebesgue"
- unfolding negligible_iff_lebesgue_null_sets[symmetric] by (auto simp: negligible_subset)
-
-lemma
- fixes a b ::"'a::ordered_euclidean_space"
- shows lmeasure_atLeastAtMost[simp]: "emeasure lebesgue {a..b} = ereal (content {a..b})"
-proof -
- have "(indicator (UNIV \<inter> {a..b})::_\<Rightarrow>real) integrable_on UNIV"
- unfolding integrable_indicator_UNIV by (simp add: integrable_const indicator_def [abs_def] cbox_interval[symmetric])
- from lmeasure_eq_integral[OF this] show ?thesis unfolding integral_indicator_UNIV
- by (simp add: indicator_def [abs_def] cbox_interval[symmetric])
-qed
-
-lemma
- fixes a b ::"'a::ordered_euclidean_space"
- shows lmeasure_cbox[simp]: "emeasure lebesgue (cbox a b) = ereal (content (cbox a b))"
-proof -
- have "(indicator (UNIV \<inter> {a..b})::_\<Rightarrow>real) integrable_on UNIV"
- unfolding integrable_indicator_UNIV by (simp add: integrable_const indicator_def [abs_def] cbox_interval[symmetric])
- from lmeasure_eq_integral[OF this] show ?thesis unfolding integral_indicator_UNIV
- by (simp add: indicator_def [abs_def] cbox_interval[symmetric])
-qed
-
-lemma lmeasure_singleton[simp]:
- fixes a :: "'a::ordered_euclidean_space" shows "emeasure lebesgue {a} = 0"
- using lmeasure_atLeastAtMost[of a a] by simp
-
-lemma AE_lebesgue_singleton:
- fixes a :: "'a::ordered_euclidean_space" shows "AE x in lebesgue. x \<noteq> a"
- by (rule AE_I[where N="{a}"]) auto
-
-declare content_real[simp]
+lemma emeasure_lborel_box_eq:
+ "emeasure lborel (box l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)"
+ using box_eq_empty(1)[THEN iffD2, of u l] by (auto simp: not_le dest!: less_imp_le) force
lemma
- fixes a b :: real
- shows lmeasure_real_greaterThanAtMost[simp]:
- "emeasure lebesgue {a <.. b} = ereal (if a \<le> b then b - a else 0)"
-proof -
- have "emeasure lebesgue {a <.. b} = emeasure lebesgue {a .. b}"
- using AE_lebesgue_singleton[of a]
- by (intro emeasure_eq_AE) auto
- then show ?thesis by auto
-qed
+ fixes l u :: real
+ assumes [simp]: "l \<le> u"
+ shows measure_lborel_Icc[simp]: "measure lborel {l .. u} = u - l"
+ and measure_lborel_Ico[simp]: "measure lborel {l ..< u} = u - l"
+ and measure_lborel_Ioc[simp]: "measure lborel {l <.. u} = u - l"
+ and measure_lborel_Ioo[simp]: "measure lborel {l <..< u} = u - l"
+ by (simp_all add: measure_def)
-lemma
- fixes a b :: real
- shows lmeasure_real_atLeastLessThan[simp]:
- "emeasure lebesgue {a ..< b} = ereal (if a \<le> b then b - a else 0)"
-proof -
- have "emeasure lebesgue {a ..< b} = emeasure lebesgue {a .. b}"
- using AE_lebesgue_singleton[of b]
- by (intro emeasure_eq_AE) auto
- then show ?thesis by auto
-qed
+lemma
+ assumes [simp]: "\<And>b. b \<in> Basis \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b"
+ shows measure_lborel_box[simp]: "measure lborel (box l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
+ and measure_lborel_cbox[simp]: "measure lborel (cbox l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
+ by (simp_all add: measure_def)
-lemma
- fixes a b :: real
- shows lmeasure_real_greaterThanLessThan[simp]:
- "emeasure lebesgue {a <..< b} = ereal (if a \<le> b then b - a else 0)"
-proof -
- have "emeasure lebesgue {a <..< b} = emeasure lebesgue {a .. b}"
- using AE_lebesgue_singleton[of a] AE_lebesgue_singleton[of b]
- by (intro emeasure_eq_AE) auto
- then show ?thesis by auto
+lemma sigma_finite_lborel: "sigma_finite_measure lborel"
+proof
+ show "\<exists>A::'a set set. countable A \<and> A \<subseteq> sets lborel \<and> \<Union>A = space lborel \<and> (\<forall>a\<in>A. emeasure lborel a \<noteq> \<infinity>)"
+ by (intro exI[of _ "range (\<lambda>n::nat. box (- real n *\<^sub>R One) (real n *\<^sub>R One))"])
+ (auto simp: emeasure_lborel_cbox_eq UN_box_eq_UNIV)
qed
-subsection {* Lebesgue-Borel measure *}
-
-definition "lborel = measure_of UNIV (sets borel) (emeasure lebesgue)"
+end
-lemma
- shows space_lborel[simp]: "space lborel = UNIV"
- and sets_lborel[simp]: "sets lborel = sets borel"
- and measurable_lborel1[simp]: "measurable lborel = measurable borel"
- and measurable_lborel2[simp]: "measurable A lborel = measurable A borel"
- using sets.sigma_sets_eq[of borel]
- by (auto simp add: lborel_def measurable_def[abs_def])
-
-(* TODO: switch these rules! *)
-lemma emeasure_lborel[simp]: "A \<in> sets borel \<Longrightarrow> emeasure lborel A = emeasure lebesgue A"
- by (rule emeasure_measure_of[OF lborel_def])
- (auto simp: positive_def emeasure_nonneg countably_additive_def intro!: suminf_emeasure)
+lemma emeasure_lborel_UNIV: "emeasure lborel (UNIV::'a::euclidean_space set) = \<infinity>"
+ unfolding UN_box_eq_UNIV[symmetric]
+ apply (subst SUP_emeasure_incseq[symmetric])
+ apply (auto simp: incseq_def subset_box inner_add_left setprod_constant intro!: SUP_PInfty)
+ apply (rule_tac x="Suc n" in exI)
+ apply (rule order_trans[OF _ self_le_power])
+ apply (auto simp: card_gt_0_iff real_of_nat_Suc)
+ done
-lemma measure_lborel[simp]: "A \<in> sets borel \<Longrightarrow> measure lborel A = measure lebesgue A"
- unfolding measure_def by simp
+lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0"
+ using emeasure_lborel_cbox[of x x] nonempty_Basis
+ by (auto simp del: emeasure_lborel_cbox nonempty_Basis simp add: cbox_sing)
-interpretation lborel: sigma_finite_measure lborel
-proof (default, intro conjI exI[of _ "\<lambda>n. cube n"])
- show "range cube \<subseteq> sets lborel" by (auto intro: borel_closed)
- { fix x :: 'a have "\<exists>n. x\<in>cube n" using mem_big_cube by auto }
- then show "(\<Union>i. cube i) = (space lborel :: 'a set)" using mem_big_cube by auto
- show "\<forall>i. emeasure lborel (cube i) \<noteq> \<infinity>" by (simp add: cube_def)
-qed
-
-interpretation lebesgue: sigma_finite_measure lebesgue
-proof
- from lborel.sigma_finite guess A :: "nat \<Rightarrow> 'a set" ..
- then show "\<exists>A::nat \<Rightarrow> 'a set. range A \<subseteq> sets lebesgue \<and> (\<Union>i. A i) = space lebesgue \<and> (\<forall>i. emeasure lebesgue (A i) \<noteq> \<infinity>)"
- by (intro exI[of _ A]) (auto simp: subset_eq)
+lemma emeasure_lborel_countable:
+ fixes A :: "'a::euclidean_space set"
+ assumes "countable A"
+ shows "emeasure lborel A = 0"
+proof -
+ have "A \<subseteq> (\<Union>i. {from_nat_into A i})" using from_nat_into_surj assms by force
+ moreover have "emeasure lborel (\<Union>i. {from_nat_into A i}) = 0"
+ by (rule emeasure_UN_eq_0) auto
+ ultimately have "emeasure lborel A \<le> 0" using emeasure_mono
+ by (metis assms bot.extremum_unique emeasure_empty image_eq_UN range_from_nat_into sets.empty_sets)
+ thus ?thesis by (auto simp add: emeasure_le_0_iff)
qed
-interpretation lborel_pair: pair_sigma_finite lborel lborel ..
-
-lemma Int_stable_atLeastAtMost:
- fixes x::"'a::ordered_euclidean_space"
- shows "Int_stable (range (\<lambda>(a, b::'a). {a..b}))"
- by (auto simp: inter_interval Int_stable_def cbox_interval[symmetric])
+subsection {* Affine transformation on the Lebesgue-Borel *}
lemma lborel_eqI:
- fixes M :: "'a::ordered_euclidean_space measure"
- assumes emeasure_eq: "\<And>a b. emeasure M {a .. b} = content {a .. b}"
+ fixes M :: "'a::euclidean_space measure"
+ assumes emeasure_eq: "\<And>l u. (\<And>b. b \<in> Basis \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b) \<Longrightarrow> emeasure M (box l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
assumes sets_eq: "sets M = sets borel"
shows "lborel = M"
-proof (rule measure_eqI_generator_eq[OF Int_stable_atLeastAtMost])
- let ?P = "\<Pi>\<^sub>M i\<in>{..<DIM('a::ordered_euclidean_space)}. lborel"
- let ?E = "range (\<lambda>(a, b). {a..b} :: 'a set)"
+proof (rule measure_eqI_generator_eq)
+ let ?E = "range (\<lambda>(a, b). box a b::'a set)"
+ show "Int_stable ?E"
+ by (auto simp: Int_stable_def box_Int_box)
+
show "?E \<subseteq> Pow UNIV" "sets lborel = sigma_sets UNIV ?E" "sets M = sigma_sets UNIV ?E"
- by (simp_all add: borel_eq_atLeastAtMost sets_eq)
+ by (simp_all add: borel_eq_box sets_eq)
- show "range cube \<subseteq> ?E" unfolding cube_def [abs_def] by auto
- { fix x :: 'a have "\<exists>n. x \<in> cube n" using mem_big_cube[of x] by fastforce }
- then show "(\<Union>i. cube i :: 'a set) = UNIV" by auto
+ let ?A = "\<lambda>n::nat. box (- (real n *\<^sub>R One)) (real n *\<^sub>R One) :: 'a set"
+ show "range ?A \<subseteq> ?E" "(\<Union>i. ?A i) = UNIV"
+ unfolding UN_box_eq_UNIV by auto
- { fix i show "emeasure lborel (cube i) \<noteq> \<infinity>" unfolding cube_def by auto }
+ { fix i show "emeasure lborel (?A i) \<noteq> \<infinity>" by auto }
{ fix X assume "X \<in> ?E" then show "emeasure lborel X = emeasure M X"
- by (auto simp: emeasure_eq) }
+ apply (auto simp: emeasure_eq emeasure_lborel_box_eq )
+ apply (subst box_eq_empty(1)[THEN iffD2])
+ apply (auto intro: less_imp_le simp: not_le)
+ done }
qed
-
-(* GENEREALIZE to euclidean_spaces *)
-lemma lborel_real_affine:
- fixes c :: real assumes "c \<noteq> 0"
- shows "lborel = density (distr lborel borel (\<lambda>x. t + c * x)) (\<lambda>_. \<bar>c\<bar>)" (is "_ = ?D")
+lemma lborel_affine:
+ fixes t :: "'a::euclidean_space" assumes "c \<noteq> 0"
+ shows "lborel = density (distr lborel borel (\<lambda>x. t + c *\<^sub>R x)) (\<lambda>_. \<bar>c\<bar>^DIM('a))" (is "_ = ?D")
proof (rule lborel_eqI)
- fix a b show "emeasure ?D {a..b} = content {a .. b}"
+ let ?B = "Basis :: 'a set"
+ fix l u assume le: "\<And>b. b \<in> ?B \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b"
+ show "emeasure ?D (box l u) = (\<Prod>b\<in>?B. (u - l) \<bullet> b)"
proof cases
assume "0 < c"
- then have "(\<lambda>x. t + c * x) -` {a..b} = {(a - t) / c .. (b - t) / c}"
- by (auto simp: field_simps)
+ then have "(\<lambda>x. t + c *\<^sub>R x) -` box l u = box ((l - t) /\<^sub>R c) ((u - t) /\<^sub>R c)"
+ by (auto simp: field_simps box_def inner_simps)
with `0 < c` show ?thesis
- by (cases "a \<le> b")
- (auto simp: field_simps emeasure_density nn_integral_distr nn_integral_cmult
+ using le
+ by (auto simp: field_simps emeasure_density nn_integral_distr nn_integral_cmult
+ emeasure_lborel_box_eq inner_simps setprod_dividef setprod_constant
borel_measurable_indicator' emeasure_distr)
next
assume "\<not> 0 < c" with `c \<noteq> 0` have "c < 0" by auto
- then have *: "(\<lambda>x. t + c * x) -` {a..b} = {(b - t) / c .. (a - t) / c}"
- by (auto simp: field_simps)
- with `c < 0` show ?thesis
- by (cases "a \<le> b")
- (auto simp: field_simps emeasure_density nn_integral_distr
- nn_integral_cmult borel_measurable_indicator' emeasure_distr)
+ then have "box ((u - t) /\<^sub>R c) ((l - t) /\<^sub>R c) = (\<lambda>x. t + c *\<^sub>R x) -` box l u"
+ by (auto simp: field_simps box_def inner_simps)
+ then have "\<And>x. indicator (box l u) (t + c *\<^sub>R x) = (indicator (box ((u - t) /\<^sub>R c) ((l - t) /\<^sub>R c)) x :: ereal)"
+ by (auto split: split_indicator)
+ moreover
+ { have "(- c) ^ card ?B * (\<Prod>x\<in>?B. l \<bullet> x - u \<bullet> x) =
+ (-1 * c) ^ card ?B * (\<Prod>x\<in>?B. -1 * (u \<bullet> x - l \<bullet> x))"
+ by simp
+ also have "\<dots> = (-1 * -1)^card ?B * c ^ card ?B * (\<Prod>x\<in>?B. u \<bullet> x - l \<bullet> x)"
+ unfolding setprod.distrib power_mult_distrib by (simp add: setprod_constant)
+ finally have "(- c) ^ card ?B * (\<Prod>x\<in>?B. l \<bullet> x - u \<bullet> x) = c ^ card ?B * (\<Prod>b\<in>?B. u \<bullet> b - l \<bullet> b)"
+ by simp }
+ ultimately show ?thesis
+ using `c < 0` le
+ by (auto simp: field_simps emeasure_density nn_integral_distr nn_integral_cmult
+ emeasure_lborel_box_eq inner_simps setprod_dividef setprod_constant
+ borel_measurable_indicator' emeasure_distr)
qed
qed simp
+lemma lborel_real_affine:
+ "c \<noteq> 0 \<Longrightarrow> lborel = density (distr lborel borel (\<lambda>x. t + c * x)) (\<lambda>_. \<bar>c\<bar>)"
+ using lborel_affine[of c t] by simp
+
+lemma AE_borel_affine:
+ fixes P :: "real \<Rightarrow> bool"
+ shows "c \<noteq> 0 \<Longrightarrow> Measurable.pred borel P \<Longrightarrow> AE x in lborel. P x \<Longrightarrow> AE x in lborel. P (t + c * x)"
+ by (subst lborel_real_affine[where t="- t / c" and c="1 / c"])
+ (simp_all add: AE_density AE_distr_iff field_simps)
+
lemma nn_integral_real_affine:
fixes c :: real assumes [measurable]: "f \<in> borel_measurable borel" and c: "c \<noteq> 0"
shows "(\<integral>\<^sup>+x. f x \<partial>lborel) = \<bar>c\<bar> * (\<integral>\<^sup>+x. f (t + c * x) \<partial>lborel)"
@@ -576,7 +611,7 @@
(simp add: nn_integral_density nn_integral_distr nn_integral_cmult)
lemma lborel_integrable_real_affine:
- fixes f :: "real \<Rightarrow> _ :: {banach, second_countable_topology}"
+ fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
assumes f: "integrable lborel f"
shows "c \<noteq> 0 \<Longrightarrow> integrable lborel (\<lambda>x. f (t + c * x))"
using f f[THEN borel_measurable_integrable] unfolding integrable_iff_bounded
@@ -596,7 +631,8 @@
proof cases
assume f[measurable]: "integrable lborel f" then show ?thesis
using c f f[THEN borel_measurable_integrable] f[THEN lborel_integrable_real_affine, of c t]
- by (subst lborel_real_affine[OF c, of t]) (simp add: integral_density integral_distr)
+ by (subst lborel_real_affine[OF c, of t])
+ (simp add: integral_density integral_distr)
next
assume "\<not> integrable lborel f" with c show ?thesis
by (simp add: lborel_integrable_real_affine_iff not_integrable_integral_eq)
@@ -607,12 +643,6 @@
shows "r \<noteq> 0 \<Longrightarrow> y = x /\<^sub>R r \<longleftrightarrow> r *\<^sub>R y = x"
using scaleR_cancel_left[of r y "x /\<^sub>R r"] by simp
-lemma integrable_on_cmult_iff2:
- fixes c :: real
- shows "(\<lambda>x. c * f x) integrable_on s \<longleftrightarrow> c = 0 \<or> f integrable_on s"
- using integrable_cmul[of "\<lambda>x. c * f x" s "1 / c"] integrable_cmul[of f s c]
- by (cases "c = 0") auto
-
lemma lborel_has_bochner_integral_real_affine_iff:
fixes x :: "'a :: {banach, second_countable_topology}"
shows "c \<noteq> 0 \<Longrightarrow>
@@ -621,62 +651,160 @@
unfolding has_bochner_integral_iff lborel_integrable_real_affine_iff
by (simp_all add: lborel_integral_real_affine[symmetric] divideR_right cong: conj_cong)
-subsection {* Lebesgue integrable implies Gauge integrable *}
+interpretation lborel!: sigma_finite_measure lborel
+ by (rule sigma_finite_lborel)
+
+interpretation lborel_pair: pair_sigma_finite lborel lborel ..
+
+(* FIXME: conversion in measurable prover *)
+lemma lborelD_Collect[measurable (raw)]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" by simp
+lemma lborelD[measurable (raw)]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp
+
+subsection {* Equivalence Lebesgue integral on @{const lborel} and HK-integral *}
-lemma has_integral_scaleR_left:
- "(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x *\<^sub>R c) has_integral (y *\<^sub>R c)) s"
- using has_integral_linear[OF _ bounded_linear_scaleR_left] by (simp add: comp_def)
+lemma has_integral_measure_lborel:
+ fixes A :: "'a::euclidean_space set"
+ assumes A[measurable]: "A \<in> sets borel" and finite: "emeasure lborel A < \<infinity>"
+ shows "((\<lambda>x. 1) has_integral measure lborel A) A"
+proof -
+ { fix l u :: 'a
+ have "((\<lambda>x. 1) has_integral measure lborel (box l u)) (box l u)"
+ proof cases
+ assume "\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b"
+ then show ?thesis
+ apply simp
+ apply (subst has_integral_restrict[symmetric, OF box_subset_cbox])
+ apply (subst has_integral_spike_interior_eq[where g="\<lambda>_. 1"])
+ using has_integral_const[of "1::real" l u]
+ apply (simp_all add: inner_diff_left[symmetric] content_cbox_cases)
+ done
+ next
+ assume "\<not> (\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b)"
+ then have "box l u = {}"
+ unfolding box_eq_empty by (auto simp: not_le intro: less_imp_le)
+ then show ?thesis
+ by simp
+ qed }
+ note has_integral_box = this
-lemma has_integral_mult_left:
- fixes c :: "_ :: {real_normed_algebra}"
- shows "(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x * c) has_integral (y * c)) s"
- using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def)
+ { fix a b :: 'a let ?M = "\<lambda>A. measure lborel (A \<inter> box a b)"
+ have "Int_stable (range (\<lambda>(a, b). box a b))"
+ by (auto simp: Int_stable_def box_Int_box)
+ moreover have "(range (\<lambda>(a, b). box a b)) \<subseteq> Pow UNIV"
+ by auto
+ moreover have "A \<in> sigma_sets UNIV (range (\<lambda>(a, b). box a b))"
+ using A unfolding borel_eq_box by simp
+ ultimately have "((\<lambda>x. 1) has_integral ?M A) (A \<inter> box a b)"
+ proof (induction rule: sigma_sets_induct_disjoint)
+ case (basic A) then show ?case
+ by (auto simp: box_Int_box has_integral_box)
+ next
+ case empty then show ?case
+ by simp
+ next
+ case (compl A)
+ then have [measurable]: "A \<in> sets borel"
+ by (simp add: borel_eq_box)
-(* GENERALIZE Integration.dominated_convergence, then generalize the following theorems *)
-lemma has_integral_dominated_convergence:
- fixes f :: "nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
- assumes "\<And>k. (f k has_integral y k) s" "h integrable_on s"
- "\<And>k. \<forall>x\<in>s. norm (f k x) \<le> h x" "\<forall>x\<in>s. (\<lambda>k. f k x) ----> g x"
- and x: "y ----> x"
- shows "(g has_integral x) s"
-proof -
- have int_f: "\<And>k. (f k) integrable_on s"
- using assms by (auto simp: integrable_on_def)
- have "(g has_integral (integral s g)) s"
- by (intro integrable_integral dominated_convergence[OF int_f assms(2)]) fact+
- moreover have "integral s g = x"
- proof (rule LIMSEQ_unique)
- show "(\<lambda>i. integral s (f i)) ----> x"
- using integral_unique[OF assms(1)] x by simp
- show "(\<lambda>i. integral s (f i)) ----> integral s g"
- by (intro dominated_convergence[OF int_f assms(2)]) fact+
+ have "((\<lambda>x. 1) has_integral ?M (box a b)) (box a b)"
+ by (simp add: has_integral_box)
+ moreover have "((\<lambda>x. if x \<in> A \<inter> box a b then 1 else 0) has_integral ?M A) (box a b)"
+ by (subst has_integral_restrict) (auto intro: compl)
+ ultimately have "((\<lambda>x. 1 - (if x \<in> A \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
+ by (rule has_integral_sub)
+ then have "((\<lambda>x. (if x \<in> (UNIV - A) \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
+ by (rule has_integral_eq_eq[THEN iffD1, rotated 1]) auto
+ then have "((\<lambda>x. 1) has_integral ?M (box a b) - ?M A) ((UNIV - A) \<inter> box a b)"
+ by (subst (asm) has_integral_restrict) auto
+ also have "?M (box a b) - ?M A = ?M (UNIV - A)"
+ by (subst measure_Diff[symmetric]) (auto simp: emeasure_lborel_box_eq Diff_Int_distrib2)
+ finally show ?case .
+ next
+ case (union F)
+ then have [measurable]: "\<And>i. F i \<in> sets borel"
+ by (simp add: borel_eq_box subset_eq)
+ have "((\<lambda>x. if x \<in> UNION UNIV F \<inter> box a b then 1 else 0) has_integral ?M (\<Union>i. F i)) (box a b)"
+ proof (rule has_integral_monotone_convergence_increasing)
+ let ?f = "\<lambda>k x. \<Sum>i<k. if x \<in> F i \<inter> box a b then 1 else 0 :: real"
+ show "\<And>k. (?f k has_integral (\<Sum>i<k. ?M (F i))) (box a b)"
+ using union.IH by (auto intro!: has_integral_setsum simp del: Int_iff)
+ show "\<And>k x. ?f k x \<le> ?f (Suc k) x"
+ by (intro setsum_mono2) auto
+ from union(1) have *: "\<And>x i j. x \<in> F i \<Longrightarrow> x \<in> F j \<longleftrightarrow> j = i"
+ by (auto simp add: disjoint_family_on_def)
+ show "\<And>x. (\<lambda>k. ?f k x) ----> (if x \<in> UNION UNIV F \<inter> box a b then 1 else 0)"
+ apply (auto simp: * setsum.If_cases Iio_Int_singleton)
+ apply (rule_tac k="Suc xa" in LIMSEQ_offset)
+ apply (simp add: tendsto_const)
+ done
+ have *: "emeasure lborel ((\<Union>x. F x) \<inter> box a b) \<le> emeasure lborel (box a b)"
+ by (intro emeasure_mono) auto
+
+ with union(1) show "(\<lambda>k. \<Sum>i<k. ?M (F i)) ----> ?M (\<Union>i. F i)"
+ unfolding sums_def[symmetric] UN_extend_simps
+ by (intro measure_UNION) (auto simp: disjoint_family_on_def emeasure_lborel_box_eq)
+ qed
+ then show ?case
+ by (subst (asm) has_integral_restrict) auto
+ qed }
+ note * = this
+
+ show ?thesis
+ proof (rule has_integral_monotone_convergence_increasing)
+ let ?B = "\<lambda>n::nat. box (- real n *\<^sub>R One) (real n *\<^sub>R One) :: 'a set"
+ let ?f = "\<lambda>n::nat. \<lambda>x. if x \<in> A \<inter> ?B n then 1 else 0 :: real"
+ let ?M = "\<lambda>n. measure lborel (A \<inter> ?B n)"
+
+ show "\<And>n::nat. (?f n has_integral ?M n) A"
+ using * by (subst has_integral_restrict) simp_all
+ show "\<And>k x. ?f k x \<le> ?f (Suc k) x"
+ by (auto simp: box_def)
+ { fix x assume "x \<in> A"
+ moreover have "(\<lambda>k. indicator (A \<inter> ?B k) x :: real) ----> indicator (\<Union>k::nat. A \<inter> ?B k) x"
+ by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def box_def)
+ ultimately show "(\<lambda>k. if x \<in> A \<inter> ?B k then 1 else 0::real) ----> 1"
+ by (simp add: indicator_def UN_box_eq_UNIV) }
+
+ have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) ----> emeasure lborel (\<Union>n::nat. A \<inter> ?B n)"
+ by (intro Lim_emeasure_incseq) (auto simp: incseq_def box_def)
+ also have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) = (\<lambda>n. measure lborel (A \<inter> ?B n))"
+ proof (intro ext emeasure_eq_ereal_measure)
+ fix n have "emeasure lborel (A \<inter> ?B n) \<le> emeasure lborel (?B n)"
+ by (intro emeasure_mono) auto
+ then show "emeasure lborel (A \<inter> ?B n) \<noteq> \<infinity>"
+ by auto
+ qed
+ finally show "(\<lambda>n. measure lborel (A \<inter> ?B n)) ----> measure lborel A"
+ using emeasure_eq_ereal_measure[of lborel A] finite
+ by (simp add: UN_box_eq_UNIV)
qed
- ultimately show ?thesis
- by simp
qed
lemma nn_integral_has_integral:
- fixes f::"'a::ordered_euclidean_space \<Rightarrow> real"
- assumes f: "f \<in> borel_measurable lebesgue" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lebesgue) = ereal r"
+ fixes f::"'a::euclidean_space \<Rightarrow> real"
+ assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) = ereal r"
shows "(f has_integral r) UNIV"
using f proof (induct arbitrary: r rule: borel_measurable_induct_real)
- case (set A) then show ?case
- by (auto simp add: ereal_indicator has_integral_iff_lmeasure)
+ case (set A)
+ moreover then have "((\<lambda>x. 1) has_integral measure lborel A) A"
+ by (intro has_integral_measure_lborel) (auto simp: ereal_indicator)
+ ultimately show ?case
+ by (simp add: ereal_indicator measure_def) (simp add: indicator_def)
next
case (mult g c)
- then have "ereal c * (\<integral>\<^sup>+ x. g x \<partial>lebesgue) = ereal r"
+ then have "ereal c * (\<integral>\<^sup>+ x. g x \<partial>lborel) = ereal r"
by (subst nn_integral_cmult[symmetric]) auto
- then obtain r' where "(c = 0 \<and> r = 0) \<or> ((\<integral>\<^sup>+ x. ereal (g x) \<partial>lebesgue) = ereal r' \<and> r = c * r')"
- by (cases "\<integral>\<^sup>+ x. ereal (g x) \<partial>lebesgue") (auto split: split_if_asm)
+ then obtain r' where "(c = 0 \<and> r = 0) \<or> ((\<integral>\<^sup>+ x. ereal (g x) \<partial>lborel) = ereal r' \<and> r = c * r')"
+ by (cases "\<integral>\<^sup>+ x. ereal (g x) \<partial>lborel") (auto split: split_if_asm)
with mult show ?case
by (auto intro!: has_integral_cmult_real)
next
case (add g h)
moreover
- then have "(\<integral>\<^sup>+ x. h x + g x \<partial>lebesgue) = (\<integral>\<^sup>+ x. h x \<partial>lebesgue) + (\<integral>\<^sup>+ x. g x \<partial>lebesgue)"
+ then have "(\<integral>\<^sup>+ x. h x + g x \<partial>lborel) = (\<integral>\<^sup>+ x. h x \<partial>lborel) + (\<integral>\<^sup>+ x. g x \<partial>lborel)"
unfolding plus_ereal.simps[symmetric] by (subst nn_integral_add) auto
- with add obtain a b where "(\<integral>\<^sup>+ x. h x \<partial>lebesgue) = ereal a" "(\<integral>\<^sup>+ x. g x \<partial>lebesgue) = ereal b" "r = a + b"
- by (cases "\<integral>\<^sup>+ x. h x \<partial>lebesgue" "\<integral>\<^sup>+ x. g x \<partial>lebesgue" rule: ereal2_cases) auto
+ with add obtain a b where "(\<integral>\<^sup>+ x. h x \<partial>lborel) = ereal a" "(\<integral>\<^sup>+ x. g x \<partial>lborel) = ereal b" "r = a + b"
+ by (cases "\<integral>\<^sup>+ x. h x \<partial>lborel" "\<integral>\<^sup>+ x. g x \<partial>lborel" rule: ereal2_cases) auto
ultimately show ?case
by (auto intro!: has_integral_add)
next
@@ -693,16 +821,16 @@
note U_le_f = this
{ fix i
- have "(\<integral>\<^sup>+x. ereal (U i x) \<partial>lebesgue) \<le> (\<integral>\<^sup>+x. ereal (f x) \<partial>lebesgue)"
+ have "(\<integral>\<^sup>+x. ereal (U i x) \<partial>lborel) \<le> (\<integral>\<^sup>+x. ereal (f x) \<partial>lborel)"
using U_le_f by (intro nn_integral_mono) simp
- then obtain p where "(\<integral>\<^sup>+x. U i x \<partial>lebesgue) = ereal p" "p \<le> r"
- using seq(6) by (cases "\<integral>\<^sup>+x. U i x \<partial>lebesgue") auto
+ then obtain p where "(\<integral>\<^sup>+x. U i x \<partial>lborel) = ereal p" "p \<le> r"
+ using seq(6) by (cases "\<integral>\<^sup>+x. U i x \<partial>lborel") auto
moreover then have "0 \<le> p"
by (metis ereal_less_eq(5) nn_integral_nonneg)
moreover note seq
- ultimately have "\<exists>p. (\<integral>\<^sup>+x. U i x \<partial>lebesgue) = ereal p \<and> 0 \<le> p \<and> p \<le> r \<and> (U i has_integral p) UNIV"
+ ultimately have "\<exists>p. (\<integral>\<^sup>+x. U i x \<partial>lborel) = ereal p \<and> 0 \<le> p \<and> p \<le> r \<and> (U i has_integral p) UNIV"
by auto }
- then obtain p where p: "\<And>i. (\<integral>\<^sup>+x. ereal (U i x) \<partial>lebesgue) = ereal (p i)"
+ then obtain p where p: "\<And>i. (\<integral>\<^sup>+x. ereal (U i x) \<partial>lborel) = ereal (p i)"
and bnd: "\<And>i. p i \<le> r" "\<And>i. 0 \<le> p i"
and U_int: "\<And>i.(U i has_integral (p i)) UNIV" by metis
@@ -717,7 +845,7 @@
show "\<forall>x\<in>UNIV. (\<lambda>k. U k x) ----> f x"
using seq by auto
qed
- moreover have "(\<lambda>i. (\<integral>\<^sup>+x. U i x \<partial>lebesgue)) ----> (\<integral>\<^sup>+x. f x \<partial>lebesgue)"
+ moreover have "(\<lambda>i. (\<integral>\<^sup>+x. U i x \<partial>lborel)) ----> (\<integral>\<^sup>+x. f x \<partial>lborel)"
using seq U_le_f by (intro nn_integral_dominated_convergence[where w=f]) auto
ultimately have "integral UNIV f = r"
by (auto simp add: int_eq p seq intro: LIMSEQ_unique)
@@ -725,23 +853,135 @@
by (simp add: has_integral_integral)
qed
-lemma has_integral_integrable_lebesgue_nonneg:
- fixes f::"'a::ordered_euclidean_space \<Rightarrow> real"
- assumes f: "integrable lebesgue f" "\<And>x. 0 \<le> f x"
- shows "(f has_integral integral\<^sup>L lebesgue f) UNIV"
-proof (rule nn_integral_has_integral)
- show "(\<integral>\<^sup>+ x. ereal (f x) \<partial>lebesgue) = ereal (integral\<^sup>L lebesgue f)"
- using f by (intro nn_integral_eq_integral) auto
-qed (insert f, auto)
+lemma nn_integral_lborel_eq_integral:
+ fixes f::"'a::euclidean_space \<Rightarrow> real"
+ assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) < \<infinity>"
+ shows "(\<integral>\<^sup>+x. f x \<partial>lborel) = integral UNIV f"
+proof -
+ from f(3) obtain r where r: "(\<integral>\<^sup>+x. f x \<partial>lborel) = ereal r"
+ by (cases "\<integral>\<^sup>+x. f x \<partial>lborel") auto
+ then show ?thesis
+ using nn_integral_has_integral[OF f(1,2) r] by (simp add: integral_unique)
+qed
+
+lemma nn_integral_integrable_on:
+ fixes f::"'a::euclidean_space \<Rightarrow> real"
+ assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) < \<infinity>"
+ shows "f integrable_on UNIV"
+proof -
+ from f(3) obtain r where r: "(\<integral>\<^sup>+x. f x \<partial>lborel) = ereal r"
+ by (cases "\<integral>\<^sup>+x. f x \<partial>lborel") auto
+ then show ?thesis
+ by (intro has_integral_integrable[where i=r] nn_integral_has_integral[where r=r] f)
+qed
+
+lemma nn_integral_has_integral_lborel:
+ fixes f :: "'a::euclidean_space \<Rightarrow> real"
+ assumes f_borel: "f \<in> borel_measurable borel" and nonneg: "\<And>x. 0 \<le> f x"
+ assumes I: "(f has_integral I) UNIV"
+ shows "integral\<^sup>N lborel f = I"
+proof -
+ from f_borel have "(\<lambda>x. ereal (f x)) \<in> borel_measurable lborel" by auto
+ from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this
+ let ?B = "\<lambda>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One) :: 'a set"
+
+ note F(1)[THEN borel_measurable_simple_function, measurable]
+
+ { fix i x have "real (F i x) \<le> f x"
+ using F(3,5) F(4)[of x, symmetric] nonneg
+ unfolding real_le_ereal_iff
+ by (auto simp: image_iff eq_commute[of \<infinity>] max_def intro: SUP_upper split: split_if_asm) }
+ note F_le_f = this
+ let ?F = "\<lambda>i x. F i x * indicator (?B i) x"
+ have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>lborel) = (SUP i. integral\<^sup>N lborel (\<lambda>x. ?F i x))"
+ proof (subst nn_integral_monotone_convergence_SUP[symmetric])
+ { fix x
+ obtain j where j: "x \<in> ?B j"
+ using UN_box_eq_UNIV by auto
-lemma has_integral_lebesgue_integral_lebesgue:
- fixes f::"'a::ordered_euclidean_space \<Rightarrow> real"
- assumes f: "integrable lebesgue f"
- shows "(f has_integral (integral\<^sup>L lebesgue f)) UNIV"
+ have "ereal (f x) = (SUP i. F i x)"
+ using F(4)[of x] nonneg[of x] by (simp add: max_def)
+ also have "\<dots> = (SUP i. ?F i x)"
+ proof (rule SUP_eq)
+ fix i show "\<exists>j\<in>UNIV. F i x \<le> ?F j x"
+ using j F(2)
+ by (intro bexI[of _ "max i j"])
+ (auto split: split_max split_indicator simp: incseq_def le_fun_def box_def)
+ qed (auto intro!: F split: split_indicator)
+ finally have "ereal (f x) = (SUP i. ?F i x)" . }
+ then show "(\<integral>\<^sup>+ x. ereal (f x) \<partial>lborel) = (\<integral>\<^sup>+ x. (SUP i. ?F i x) \<partial>lborel)"
+ by simp
+ qed (insert F, auto simp: incseq_def le_fun_def box_def split: split_indicator)
+ also have "\<dots> \<le> ereal I"
+ proof (rule SUP_least)
+ fix i :: nat
+ have finite_F: "(\<integral>\<^sup>+ x. ereal (real (F i x) * indicator (?B i) x) \<partial>lborel) < \<infinity>"
+ proof (rule nn_integral_bound_simple_function)
+ have "emeasure lborel {x \<in> space lborel. ereal (real (F i x) * indicator (?B i) x) \<noteq> 0} \<le>
+ emeasure lborel (?B i)"
+ by (intro emeasure_mono) (auto split: split_indicator)
+ then show "emeasure lborel {x \<in> space lborel. ereal (real (F i x) * indicator (?B i) x) \<noteq> 0} < \<infinity>"
+ by auto
+ qed (auto split: split_indicator
+ intro!: real_of_ereal_pos F simple_function_compose1[where g="real"] simple_function_ereal)
+
+ have int_F: "(\<lambda>x. real (F i x) * indicator (?B i) x) integrable_on UNIV"
+ using F(5) finite_F
+ by (intro nn_integral_integrable_on) (auto split: split_indicator intro: real_of_ereal_pos)
+
+ have "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) =
+ (\<integral>\<^sup>+ x. ereal (real (F i x) * indicator (?B i) x) \<partial>lborel)"
+ using F(3,5)
+ by (intro nn_integral_cong) (auto simp: image_iff ereal_real eq_commute split: split_indicator)
+ also have "\<dots> = ereal (integral UNIV (\<lambda>x. real (F i x) * indicator (?B i) x))"
+ using F
+ by (intro nn_integral_lborel_eq_integral[OF _ _ finite_F])
+ (auto split: split_indicator intro: real_of_ereal_pos)
+ also have "\<dots> \<le> ereal I"
+ by (auto intro!: has_integral_le[OF integrable_integral[OF int_F] I] nonneg F_le_f
+ split: split_indicator )
+ finally show "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) \<le> ereal I" .
+ qed
+ finally have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>lborel) < \<infinity>"
+ by auto
+ from nn_integral_lborel_eq_integral[OF assms(1,2) this] I show ?thesis
+ by (simp add: integral_unique)
+qed
+
+lemma has_integral_iff_emeasure_lborel:
+ fixes A :: "'a::euclidean_space set"
+ assumes A[measurable]: "A \<in> sets borel"
+ shows "((\<lambda>x. 1) has_integral r) A \<longleftrightarrow> emeasure lborel A = ereal r"
+proof cases
+ assume emeasure_A: "emeasure lborel A = \<infinity>"
+ have "\<not> (\<lambda>x. 1::real) integrable_on A"
+ proof
+ assume int: "(\<lambda>x. 1::real) integrable_on A"
+ then have "(indicator A::'a \<Rightarrow> real) integrable_on UNIV"
+ unfolding indicator_def[abs_def] integrable_restrict_univ .
+ then obtain r where "((indicator A::'a\<Rightarrow>real) has_integral r) UNIV"
+ by auto
+ from nn_integral_has_integral_lborel[OF _ _ this] emeasure_A show False
+ by (simp add: ereal_indicator)
+ qed
+ with emeasure_A show ?thesis
+ by auto
+next
+ assume "emeasure lborel A \<noteq> \<infinity>"
+ moreover then have "((\<lambda>x. 1) has_integral measure lborel A) A"
+ by (simp add: has_integral_measure_lborel)
+ ultimately show ?thesis
+ by (auto simp: emeasure_eq_ereal_measure has_integral_unique)
+qed
+
+lemma has_integral_integral_real:
+ fixes f::"'a::euclidean_space \<Rightarrow> real"
+ assumes f: "integrable lborel f"
+ shows "(f has_integral (integral\<^sup>L lborel f)) UNIV"
using f proof induct
case (base A c) then show ?case
- by (auto intro!: has_integral_mult_left simp: has_integral_iff_lmeasure)
- (simp add: emeasure_eq_ereal_measure)
+ by (auto intro!: has_integral_mult_left simp: )
+ (simp add: emeasure_eq_ereal_measure indicator_def has_integral_measure_lborel)
next
case (add f g) then show ?case
by (auto intro!: has_integral_add)
@@ -749,306 +989,46 @@
case (lim f s)
show ?case
proof (rule has_integral_dominated_convergence)
- show "\<And>i. (s i has_integral integral\<^sup>L lebesgue (s i)) UNIV" by fact
+ show "\<And>i. (s i has_integral integral\<^sup>L lborel (s i)) UNIV" by fact
show "(\<lambda>x. norm (2 * f x)) integrable_on UNIV"
- using lim by (intro has_integral_integrable[OF has_integral_integrable_lebesgue_nonneg]) auto
+ using `integrable lborel f`
+ by (intro nn_integral_integrable_on)
+ (auto simp: integrable_iff_bounded abs_mult times_ereal.simps(1)[symmetric] nn_integral_cmult
+ simp del: times_ereal.simps)
show "\<And>k. \<forall>x\<in>UNIV. norm (s k x) \<le> norm (2 * f x)"
using lim by (auto simp add: abs_mult)
show "\<forall>x\<in>UNIV. (\<lambda>k. s k x) ----> f x"
using lim by auto
- show "(\<lambda>k. integral\<^sup>L lebesgue (s k)) ----> integral\<^sup>L lebesgue f"
- using lim by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) auto
+ show "(\<lambda>k. integral\<^sup>L lborel (s k)) ----> integral\<^sup>L lborel f"
+ using lim lim(1)[THEN borel_measurable_integrable]
+ by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) auto
qed
qed
-lemma lebesgue_nn_integral_eq_borel:
- assumes f: "f \<in> borel_measurable borel"
- shows "integral\<^sup>N lebesgue f = integral\<^sup>N lborel f"
-proof -
- from f have "integral\<^sup>N lebesgue (\<lambda>x. max 0 (f x)) = integral\<^sup>N lborel (\<lambda>x. max 0 (f x))"
- by (auto intro!: nn_integral_subalgebra[symmetric])
- then show ?thesis unfolding nn_integral_max_0 .
-qed
+context
+ fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+begin
-lemma lebesgue_integral_eq_borel:
- fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
- assumes "f \<in> borel_measurable borel"
- shows "integrable lebesgue f \<longleftrightarrow> integrable lborel f" (is ?P)
- and "integral\<^sup>L lebesgue f = integral\<^sup>L lborel f" (is ?I)
-proof -
- have "sets lborel \<subseteq> sets lebesgue" by auto
- from integral_subalgebra[of f lborel, OF _ this _ _]
- integrable_subalgebra[of f lborel, OF _ this _ _] assms
- show ?P ?I by auto
-qed
-
-lemma has_integral_lebesgue_integral:
- fixes f::"'a::ordered_euclidean_space => real"
- assumes f:"integrable lborel f"
+lemma has_integral_integral_lborel:
+ assumes f: "integrable lborel f"
shows "(f has_integral (integral\<^sup>L lborel f)) UNIV"
proof -
- have borel: "f \<in> borel_measurable borel"
- using f unfolding integrable_iff_bounded by auto
- from f show ?thesis
- using has_integral_lebesgue_integral_lebesgue[of f]
- unfolding lebesgue_integral_eq_borel[OF borel] by simp
-qed
-
-lemma nn_integral_bound_simple_function:
- assumes bnd: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x" "\<And>x. x \<in> space M \<Longrightarrow> f x < \<infinity>"
- assumes f[measurable]: "simple_function M f"
- assumes supp: "emeasure M {x\<in>space M. f x \<noteq> 0} < \<infinity>"
- shows "nn_integral M f < \<infinity>"
-proof cases
- assume "space M = {}"
- then have "nn_integral M f = (\<integral>\<^sup>+x. 0 \<partial>M)"
- by (intro nn_integral_cong) auto
- then show ?thesis by simp
-next
- assume "space M \<noteq> {}"
- with simple_functionD(1)[OF f] bnd have bnd: "0 \<le> Max (f`space M) \<and> Max (f`space M) < \<infinity>"
- by (subst Max_less_iff) (auto simp: Max_ge_iff)
-
- have "nn_integral M f \<le> (\<integral>\<^sup>+x. Max (f`space M) * indicator {x\<in>space M. f x \<noteq> 0} x \<partial>M)"
- proof (rule nn_integral_mono)
- fix x assume "x \<in> space M"
- with f show "f x \<le> Max (f ` space M) * indicator {x \<in> space M. f x \<noteq> 0} x"
- by (auto split: split_indicator intro!: Max_ge simple_functionD)
- qed
- also have "\<dots> < \<infinity>"
- using bnd supp by (subst nn_integral_cmult) auto
+ have "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. integral\<^sup>L lborel (\<lambda>x. f x \<bullet> b) *\<^sub>R b)) UNIV"
+ using f by (intro has_integral_setsum finite_Basis ballI has_integral_scaleR_left has_integral_integral_real) auto
+ also have eq_f: "(\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) = f"
+ by (simp add: fun_eq_iff euclidean_representation)
+ also have "(\<Sum>b\<in>Basis. integral\<^sup>L lborel (\<lambda>x. f x \<bullet> b) *\<^sub>R b) = integral\<^sup>L lborel f"
+ using f by (subst (2) eq_f[symmetric]) simp
finally show ?thesis .
qed
-
-lemma
- fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
- assumes f_borel: "f \<in> borel_measurable lebesgue" and nonneg: "\<And>x. 0 \<le> f x"
- assumes I: "(f has_integral I) UNIV"
- shows integrable_has_integral_lebesgue_nonneg: "integrable lebesgue f"
- and integral_has_integral_lebesgue_nonneg: "integral\<^sup>L lebesgue f = I"
-proof -
- from f_borel have "(\<lambda>x. ereal (f x)) \<in> borel_measurable lebesgue" by auto
- from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this
-
- have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>lebesgue) = (SUP i. integral\<^sup>N lebesgue (F i))"
- using F
- by (subst nn_integral_monotone_convergence_SUP[symmetric])
- (simp_all add: nn_integral_max_0 borel_measurable_simple_function)
- also have "\<dots> \<le> ereal I"
- proof (rule SUP_least)
- fix i :: nat
-
- { fix z
- from F(4)[of z] have "F i z \<le> ereal (f z)"
- by (metis SUP_upper UNIV_I ereal_max_0 max.absorb2 nonneg)
- with F(5)[of i z] have "real (F i z) \<le> f z"
- by (cases "F i z") simp_all }
- note F_bound = this
-
- { fix x :: ereal assume x: "x \<noteq> 0" "x \<in> range (F i)"
- with F(3,5)[of i] have [simp]: "real x \<noteq> 0"
- by (metis image_iff order_eq_iff real_of_ereal_le_0)
- let ?s = "(\<lambda>n z. real x * indicator (F i -` {x} \<inter> cube n) z) :: nat \<Rightarrow> 'a \<Rightarrow> real"
- have "(\<lambda>z::'a. real x * indicator (F i -` {x}) z) integrable_on UNIV"
- proof (rule dominated_convergence(1))
- fix n :: nat
- have "(\<lambda>z. indicator (F i -` {x} \<inter> cube n) z :: real) integrable_on cube n"
- using x F(1)[of i]
- by (intro lebesgueD) (auto simp: simple_function_def)
- then have cube: "?s n integrable_on cube n"
- by (simp add: integrable_on_cmult_iff)
- show "?s n integrable_on UNIV"
- by (rule integrable_on_superset[OF _ _ cube]) auto
- next
- show "f integrable_on UNIV"
- unfolding integrable_on_def using I by auto
- next
- fix n from F_bound show "\<forall>x\<in>UNIV. norm (?s n x) \<le> f x"
- using nonneg F(5) by (auto split: split_indicator)
- next
- show "\<forall>z\<in>UNIV. (\<lambda>n. ?s n z) ----> real x * indicator (F i -` {x}) z"
- proof
- fix z :: 'a
- from mem_big_cube[of z] guess j .
- then have x: "eventually (\<lambda>n. ?s n z = real x * indicator (F i -` {x}) z) sequentially"
- by (auto intro!: eventually_sequentiallyI[where c=j] dest!: cube_subset split: split_indicator)
- then show "(\<lambda>n. ?s n z) ----> real x * indicator (F i -` {x}) z"
- by (rule Lim_eventually)
- qed
- qed
- then have "(indicator (F i -` {x}) :: 'a \<Rightarrow> real) integrable_on UNIV"
- by (simp add: integrable_on_cmult_iff) }
- note F_finite = lmeasure_finite[OF this]
-
- have F_eq: "\<And>x. F i x = ereal (norm (real (F i x)))"
- using F(3,5) by (auto simp: fun_eq_iff ereal_real image_iff eq_commute)
- have F_eq2: "\<And>x. F i x = ereal (real (F i x))"
- using F(3,5) by (auto simp: fun_eq_iff ereal_real image_iff eq_commute)
-
- have int: "integrable lebesgue (\<lambda>x. real (F i x))"
- unfolding integrable_iff_bounded
- proof
- have "(\<integral>\<^sup>+x. F i x \<partial>lebesgue) < \<infinity>"
- proof (rule nn_integral_bound_simple_function)
- fix x::'a assume "x \<in> space lebesgue" then show "0 \<le> F i x" "F i x < \<infinity>"
- using F by (auto simp: image_iff eq_commute)
- next
- have eq: "{x \<in> space lebesgue. F i x \<noteq> 0} = (\<Union>x\<in>F i ` space lebesgue - {0}. F i -` {x} \<inter> space lebesgue)"
- by auto
- show "emeasure lebesgue {x \<in> space lebesgue. F i x \<noteq> 0} < \<infinity>"
- unfolding eq using simple_functionD[OF F(1)]
- by (subst setsum_emeasure[symmetric])
- (auto simp: disjoint_family_on_def setsum_Pinfty F_finite)
- qed fact
- with F_eq show "(\<integral>\<^sup>+x. norm (real (F i x)) \<partial>lebesgue) < \<infinity>" by simp
- qed (insert F(1), auto intro!: borel_measurable_real_of_ereal dest: borel_measurable_simple_function)
- then have "((\<lambda>x. real (F i x)) has_integral integral\<^sup>L lebesgue (\<lambda>x. real (F i x))) UNIV"
- by (rule has_integral_lebesgue_integral_lebesgue)
- from this I have "integral\<^sup>L lebesgue (\<lambda>x. real (F i x)) \<le> I"
- by (rule has_integral_le) (intro ballI F_bound)
- moreover have "integral\<^sup>N lebesgue (F i) = integral\<^sup>L lebesgue (\<lambda>x. real (F i x))"
- using int F by (subst nn_integral_eq_integral[symmetric]) (auto simp: F_eq2[symmetric] real_of_ereal_pos)
- ultimately show "integral\<^sup>N lebesgue (F i) \<le> ereal I"
- by simp
- qed
- finally show "integrable lebesgue f"
- using f_borel by (auto simp: integrable_iff_bounded nonneg)
- from has_integral_lebesgue_integral_lebesgue[OF this] I
- show "integral\<^sup>L lebesgue f = I"
- by (metis has_integral_unique)
-qed
-
-lemma has_integral_iff_has_bochner_integral_lebesgue_nonneg:
- fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
- shows "f \<in> borel_measurable lebesgue \<Longrightarrow> (\<And>x. 0 \<le> f x) \<Longrightarrow>
- (f has_integral I) UNIV \<longleftrightarrow> has_bochner_integral lebesgue f I"
- by (metis has_bochner_integral_iff has_integral_unique has_integral_lebesgue_integral_lebesgue
- integrable_has_integral_lebesgue_nonneg)
-
-lemma
- fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
- assumes "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(f has_integral I) UNIV"
- shows integrable_has_integral_nonneg: "integrable lborel f"
- and integral_has_integral_nonneg: "integral\<^sup>L lborel f = I"
- by (metis assms borel_measurable_lebesgueI integrable_has_integral_lebesgue_nonneg lebesgue_integral_eq_borel(1))
- (metis assms borel_measurable_lebesgueI has_integral_lebesgue_integral has_integral_unique integrable_has_integral_lebesgue_nonneg lebesgue_integral_eq_borel(1))
+lemma integrable_on_lborel: "integrable lborel f \<Longrightarrow> f integrable_on UNIV"
+ using has_integral_integral_lborel by (auto intro: has_integral_integrable)
+
+lemma integral_lborel: "integrable lborel f \<Longrightarrow> integral UNIV f = (\<integral>x. f x \<partial>lborel)"
+ using has_integral_integral_lborel by auto
-subsection {* Equivalence between product spaces and euclidean spaces *}
-
-definition e2p :: "'a::ordered_euclidean_space \<Rightarrow> ('a \<Rightarrow> real)" where
- "e2p x = (\<lambda>i\<in>Basis. x \<bullet> i)"
-
-definition p2e :: "('a \<Rightarrow> real) \<Rightarrow> 'a::ordered_euclidean_space" where
- "p2e x = (\<Sum>i\<in>Basis. x i *\<^sub>R i)"
-
-lemma e2p_p2e[simp]:
- "x \<in> extensional Basis \<Longrightarrow> e2p (p2e x::'a::ordered_euclidean_space) = x"
- by (auto simp: fun_eq_iff extensional_def p2e_def e2p_def)
-
-lemma p2e_e2p[simp]:
- "p2e (e2p x) = (x::'a::ordered_euclidean_space)"
- by (auto simp: euclidean_eq_iff[where 'a='a] p2e_def e2p_def)
-
-interpretation lborel_product: product_sigma_finite "\<lambda>x. lborel::real measure"
- by default
-
-interpretation lborel_space: finite_product_sigma_finite "\<lambda>x. lborel::real measure" "Basis"
- by default auto
-
-lemma sets_product_borel:
- assumes I: "finite I"
- shows "sets (\<Pi>\<^sub>M i\<in>I. lborel) = sigma_sets (\<Pi>\<^sub>E i\<in>I. UNIV) { \<Pi>\<^sub>E i\<in>I. {..< x i :: real} | x. True}" (is "_ = ?G")
-proof (subst sigma_prod_algebra_sigma_eq[where S="\<lambda>_ i::nat. {..<real i}" and E="\<lambda>_. range lessThan", OF I])
- show "sigma_sets (space (Pi\<^sub>M I (\<lambda>i. lborel))) {Pi\<^sub>E I F |F. \<forall>i\<in>I. F i \<in> range lessThan} = ?G"
- by (intro arg_cong2[where f=sigma_sets]) (auto simp: space_PiM image_iff bchoice_iff)
-qed (auto simp: borel_eq_lessThan eucl_lessThan reals_Archimedean2)
-
-lemma measurable_e2p[measurable]:
- "e2p \<in> measurable (borel::'a::ordered_euclidean_space measure) (\<Pi>\<^sub>M (i::'a)\<in>Basis. (lborel :: real measure))"
-proof (rule measurable_sigma_sets[OF sets_product_borel])
- fix A :: "('a \<Rightarrow> real) set" assume "A \<in> {\<Pi>\<^sub>E (i::'a)\<in>Basis. {..<x i} |x. True} "
- then obtain x where "A = (\<Pi>\<^sub>E (i::'a)\<in>Basis. {..<x i})" by auto
- then have "e2p -` A = {y :: 'a. eucl_less y (\<Sum>i\<in>Basis. x i *\<^sub>R i)}"
- using DIM_positive by (auto simp add: set_eq_iff e2p_def eucl_less_def)
- then show "e2p -` A \<inter> space (borel::'a measure) \<in> sets borel" by simp
-qed (auto simp: e2p_def)
-
-(* FIXME: conversion in measurable prover *)
-lemma lborelD_Collect[measurable (raw)]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" by simp
-lemma lborelD[measurable (raw)]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp
-
-lemma measurable_p2e[measurable]:
- "p2e \<in> measurable (\<Pi>\<^sub>M (i::'a)\<in>Basis. (lborel :: real measure))
- (borel :: 'a::ordered_euclidean_space measure)"
- (is "p2e \<in> measurable ?P _")
-proof (safe intro!: borel_measurable_iff_halfspace_le[THEN iffD2])
- fix x and i :: 'a
- let ?A = "{w \<in> space ?P. (p2e w :: 'a) \<bullet> i \<le> x}"
- assume "i \<in> Basis"
- then have "?A = (\<Pi>\<^sub>E j\<in>Basis. if i = j then {.. x} else UNIV)"
- using DIM_positive by (auto simp: space_PiM p2e_def PiE_def split: split_if_asm)
- then show "?A \<in> sets ?P"
- by auto
-qed
-
-lemma lborel_eq_lborel_space:
- "(lborel :: 'a measure) = distr (\<Pi>\<^sub>M (i::'a::ordered_euclidean_space)\<in>Basis. lborel) borel p2e"
- (is "?B = ?D")
-proof (rule lborel_eqI)
- show "sets ?D = sets borel" by simp
- let ?P = "(\<Pi>\<^sub>M (i::'a)\<in>Basis. lborel)"
- fix a b :: 'a
- have *: "p2e -` {a .. b} \<inter> space ?P = (\<Pi>\<^sub>E i\<in>Basis. {a \<bullet> i .. b \<bullet> i})"
- by (auto simp: eucl_le[where 'a='a] p2e_def space_PiM PiE_def Pi_iff)
- have "emeasure ?P (p2e -` {a..b} \<inter> space ?P) = content {a..b}"
- proof cases
- assume "{a..b} \<noteq> {}"
- then have "a \<le> b"
- by (simp add: eucl_le[where 'a='a])
- then have "emeasure lborel {a..b} = (\<Prod>x\<in>Basis. emeasure lborel {a \<bullet> x .. b \<bullet> x})"
- by (auto simp: eucl_le[where 'a='a] content_closed_interval
- intro!: setprod_ereal[symmetric])
- also have "\<dots> = emeasure ?P (p2e -` {a..b} \<inter> space ?P)"
- unfolding * by (subst lborel_space.measure_times) auto
- finally show ?thesis by simp
- qed simp
- then show "emeasure ?D {a .. b} = content {a .. b}"
- by (simp add: emeasure_distr measurable_p2e)
-qed
-
-lemma borel_fubini_positiv_integral:
- fixes f :: "'a::ordered_euclidean_space \<Rightarrow> ereal"
- assumes f: "f \<in> borel_measurable borel"
- shows "integral\<^sup>N lborel f = \<integral>\<^sup>+x. f (p2e x) \<partial>(\<Pi>\<^sub>M (i::'a)\<in>Basis. lborel)"
- by (subst lborel_eq_lborel_space) (simp add: nn_integral_distr measurable_p2e f)
-
-lemma borel_fubini_integrable:
- fixes f :: "'a::ordered_euclidean_space \<Rightarrow> _::{banach, second_countable_topology}"
- shows "integrable lborel f \<longleftrightarrow> integrable (\<Pi>\<^sub>M (i::'a)\<in>Basis. lborel) (\<lambda>x. f (p2e x))"
- unfolding integrable_iff_bounded
-proof (intro conj_cong[symmetric])
- show "((\<lambda>x. f (p2e x)) \<in> borel_measurable (Pi\<^sub>M Basis (\<lambda>i. lborel))) = (f \<in> borel_measurable lborel)"
- proof
- assume "((\<lambda>x. f (p2e x)) \<in> borel_measurable (Pi\<^sub>M Basis (\<lambda>i. lborel)))"
- then have "(\<lambda>x. f (p2e (e2p x))) \<in> borel_measurable borel"
- by measurable
- then show "f \<in> borel_measurable lborel"
- by simp
- qed simp
-qed (simp add: borel_fubini_positiv_integral)
-
-lemma borel_fubini:
- fixes f :: "'a::ordered_euclidean_space \<Rightarrow> _::{banach, second_countable_topology}"
- shows "f \<in> borel_measurable borel \<Longrightarrow>
- integral\<^sup>L lborel f = \<integral>x. f (p2e x) \<partial>((\<Pi>\<^sub>M (i::'a)\<in>Basis. lborel))"
- by (subst lborel_eq_lborel_space) (simp add: integral_distr)
-
-lemma integrable_on_borel_integrable:
- fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
- shows "f \<in> borel_measurable borel \<Longrightarrow> (\<And>x. 0 \<le> f x) \<Longrightarrow> f integrable_on UNIV \<Longrightarrow> integrable lborel f"
- by (metis borel_measurable_lebesgueI integrable_has_integral_nonneg integrable_on_def
- lebesgue_integral_eq_borel(1))
+end
subsection {* Fundamental Theorem of Calculus for the Lebesgue integral *}
@@ -1060,14 +1040,14 @@
then have "emeasure lborel A \<le> emeasure lborel (cbox a b)"
by (intro emeasure_mono) auto
then show ?thesis
- by auto
+ by (auto simp: emeasure_lborel_cbox_eq)
qed
lemma emeasure_compact_finite: "compact A \<Longrightarrow> emeasure lborel A < \<infinity>"
using emeasure_bounded_finite[of A] by (auto intro: compact_imp_bounded)
lemma borel_integrable_compact:
- fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}"
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}"
assumes "compact S" "continuous_on S f"
shows "integrable lborel (\<lambda>x. indicator S x *\<^sub>R f x)"
proof cases
@@ -1103,34 +1083,6 @@
by (auto simp: mult_commute)
qed
-lemma has_field_derivative_subset:
- "(f has_field_derivative y) (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_field_derivative y) (at x within t)"
- unfolding has_field_derivative_def by (rule has_derivative_subset)
-
-lemma integral_FTC_atLeastAtMost:
- fixes a b :: real
- assumes "a \<le> b"
- and F: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> DERIV F x :> f x"
- and f: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
- shows "integral\<^sup>L lborel (\<lambda>x. f x * indicator {a .. b} x) = F b - F a"
-proof -
- let ?f = "\<lambda>x. f x * indicator {a .. b} x"
- have "(?f has_integral (\<integral>x. ?f x \<partial>lborel)) UNIV"
- using borel_integrable_atLeastAtMost[OF f]
- by (rule has_integral_lebesgue_integral)
- moreover
- have "(f has_integral F b - F a) {a .. b}"
- by (intro fundamental_theorem_of_calculus)
- (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric]
- intro: has_field_derivative_subset[OF F] assms(1))
- then have "(?f has_integral F b - F a) {a .. b}"
- by (subst has_integral_eq_eq[where g=f]) auto
- then have "(?f has_integral F b - F a) UNIV"
- by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto
- ultimately show "integral\<^sup>L lborel ?f = F b - F a"
- by (rule has_integral_unique)
-qed
-
text {*
For the positive integral we replace continuity with Borel-measurability.
@@ -1139,37 +1091,76 @@
lemma
fixes f :: "real \<Rightarrow> real"
- assumes f_borel: "f \<in> borel_measurable borel"
+ assumes [measurable]: "f \<in> borel_measurable borel"
assumes f: "\<And>x. x \<in> {a..b} \<Longrightarrow> DERIV F x :> f x" "\<And>x. x \<in> {a..b} \<Longrightarrow> 0 \<le> f x" and "a \<le> b"
- shows integral_FTC_Icc_nonneg: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq)
+ shows nn_integral_FTC_Icc: "(\<integral>\<^sup>+x. ereal (f x) * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?nn)
+ and has_bochner_integral_FTC_Icc_nonneg:
+ "has_bochner_integral lborel (\<lambda>x. f x * indicator {a .. b} x) (F b - F a)" (is ?has)
+ and integral_FTC_Icc_nonneg: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq)
and integrable_FTC_Icc_nonneg: "integrable lborel (\<lambda>x. f x * indicator {a .. b} x)" (is ?int)
proof -
- have i: "(f has_integral F b - F a) {a..b}"
+ have *: "(\<lambda>x. f x * indicator {a..b} x) \<in> borel_measurable borel" "\<And>x. 0 \<le> f x * indicator {a..b} x"
+ using f(2) by (auto split: split_indicator)
+
+ have "(f has_integral F b - F a) {a..b}"
by (intro fundamental_theorem_of_calculus)
(auto simp: has_field_derivative_iff_has_vector_derivative[symmetric]
intro: has_field_derivative_subset[OF f(1)] `a \<le> b`)
- have i: "((\<lambda>x. f x * indicator {a..b} x) has_integral F b - F a) {a..b}"
- by (rule has_integral_eq[OF _ i]) auto
- have i: "((\<lambda>x. f x * indicator {a..b} x) has_integral F b - F a) UNIV"
- by (rule has_integral_on_superset[OF _ _ i]) auto
- from i f f_borel show ?eq
- by (intro integral_has_integral_nonneg) (auto split: split_indicator)
- from i f f_borel show ?int
- by (intro integrable_has_integral_nonneg) (auto split: split_indicator)
+ then have i: "((\<lambda>x. f x * indicator {a .. b} x) has_integral F b - F a) UNIV"
+ unfolding indicator_def if_distrib[where f="\<lambda>x. a * x" for a]
+ by (simp cong del: if_cong del: atLeastAtMost_iff)
+ then have nn: "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a"
+ by (rule nn_integral_has_integral_lborel[OF *])
+ then show ?has
+ by (rule has_bochner_integral_nn_integral[rotated 2]) (simp_all add: *)
+ then show ?eq ?int
+ unfolding has_bochner_integral_iff by auto
+ from nn show ?nn
+ by (simp add: ereal_mult_indicator)
qed
-lemma nn_integral_FTC_atLeastAtMost:
- assumes "f \<in> borel_measurable borel" "\<And>x. x \<in> {a..b} \<Longrightarrow> DERIV F x :> f x" "\<And>x. x \<in> {a..b} \<Longrightarrow> 0 \<le> f x" "a \<le> b"
- shows "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a"
+lemma
+ fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
+ assumes "a \<le> b"
+ assumes "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
+ assumes cont: "continuous_on {a .. b} f"
+ shows has_bochner_integral_FTC_Icc:
+ "has_bochner_integral lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) (F b - F a)" (is ?has)
+ and integral_FTC_Icc: "(\<integral>x. indicator {a .. b} x *\<^sub>R f x \<partial>lborel) = F b - F a" (is ?eq)
proof -
- have "integrable lborel (\<lambda>x. f x * indicator {a .. b} x)"
- by (rule integrable_FTC_Icc_nonneg) fact+
- then have "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = (\<integral>x. f x * indicator {a .. b} x \<partial>lborel)"
- using assms by (intro nn_integral_eq_integral) (auto simp: indicator_def)
- also have "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a"
- by (rule integral_FTC_Icc_nonneg) fact+
- finally show ?thesis
- unfolding ereal_indicator[symmetric] by simp
+ let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
+ have int: "integrable lborel ?f"
+ using borel_integrable_compact[OF _ cont] by auto
+ have "(f has_integral F b - F a) {a..b}"
+ using assms(1,2) by (intro fundamental_theorem_of_calculus) auto
+ moreover
+ have "(f has_integral integral\<^sup>L lborel ?f) {a..b}"
+ using has_integral_integral_lborel[OF int]
+ unfolding indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a]
+ by (simp cong del: if_cong del: atLeastAtMost_iff)
+ ultimately show ?eq
+ by (auto dest: has_integral_unique)
+ then show ?has
+ using int by (auto simp: has_bochner_integral_iff)
+qed
+
+lemma
+ fixes f :: "real \<Rightarrow> real"
+ assumes "a \<le> b"
+ assumes deriv: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> DERIV F x :> f x"
+ assumes cont: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
+ shows has_bochner_integral_FTC_Icc_real:
+ "has_bochner_integral lborel (\<lambda>x. f x * indicator {a .. b} x) (F b - F a)" (is ?has)
+ and integral_FTC_Icc_real: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq)
+proof -
+ have 1: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
+ unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
+ using deriv by (auto intro: DERIV_subset)
+ have 2: "continuous_on {a .. b} f"
+ using cont by (intro continuous_at_imp_continuous_on) auto
+ show ?has ?eq
+ using has_bochner_integral_FTC_Icc[OF `a \<le> b` 1 2] integral_FTC_Icc[OF `a \<le> b` 1 2]
+ by (auto simp: mult_commute)
qed
lemma nn_integral_FTC_atLeast:
@@ -1206,7 +1197,7 @@
using nonneg by (auto split: split_indicator)
qed
also have "\<dots> = (SUP i::nat. ereal (F (a + real i) - F a))"
- by (subst nn_integral_FTC_atLeastAtMost[OF f_borel f nonneg]) auto
+ by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto
also have "\<dots> = T - F a"
proof (rule SUP_Lim_ereal)
show "incseq (\<lambda>n. ereal (F (a + real n) - F a))"
@@ -1228,6 +1219,13 @@
finally show ?thesis .
qed
+lemma integral_power:
+ "a \<le> b \<Longrightarrow> (\<integral>x. x^k * indicator {a..b} x \<partial>lborel) = (b^Suc k - a^Suc k) / Suc k"
+proof (subst integral_FTC_Icc_real)
+ fix x show "DERIV (\<lambda>x. x^Suc k / Suc k) x :> x^k"
+ by (intro derivative_eq_intros) auto
+qed (auto simp: field_simps)
+
subsection {* Integration by parts *}
lemma integral_by_parts_integrable:
@@ -1251,7 +1249,7 @@
= F b * G b - F a * G a - \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
proof-
have 0: "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = F b * G b - F a * G a"
- by (rule integral_FTC_atLeastAtMost, auto intro!: derivative_eq_intros continuous_intros)
+ by (rule integral_FTC_Icc_real, auto intro!: derivative_eq_intros continuous_intros)
(auto intro!: DERIV_isCont)
have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) =
@@ -1274,12 +1272,6 @@
= F b * G b - F a * G a - \<integral>x. indicator {a .. b} x *\<^sub>R (f x * G x) \<partial>lborel"
using integral_by_parts[OF assms] by (simp add: mult_ac)
-lemma AE_borel_affine:
- fixes P :: "real \<Rightarrow> bool"
- shows "c \<noteq> 0 \<Longrightarrow> Measurable.pred borel P \<Longrightarrow> AE x in lborel. P x \<Longrightarrow> AE x in lborel. P (t + c * x)"
- by (subst lborel_real_affine[where t="- t / c" and c="1 / c"])
- (simp_all add: AE_density AE_distr_iff field_simps)
-
lemma has_bochner_integral_even_function:
fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
@@ -1324,3 +1316,4 @@
qed
end
+
--- a/src/HOL/Probability/Measure_Space.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Probability/Measure_Space.thy Mon Jun 30 15:45:21 2014 +0200
@@ -431,6 +431,10 @@
using sets.countable_UN[of A UNIV M] emeasure_countably_additive[of M]
by (simp add: countably_additive_def)
+lemma sums_emeasure:
+ "disjoint_family F \<Longrightarrow> (\<And>i. F i \<in> sets M) \<Longrightarrow> (\<lambda>i. emeasure M (F i)) sums emeasure M (\<Union>i. F i)"
+ unfolding sums_iff by (intro conjI summable_ereal_pos emeasure_nonneg suminf_emeasure) auto
+
lemma emeasure_additive: "additive (sets M) (emeasure M)"
by (metis sets.countably_additive_additive emeasure_positive emeasure_countably_additive)
@@ -591,6 +595,10 @@
from plus_emeasure[OF sets this] show ?thesis by simp
qed
+lemma emeasure_insert_ne:
+ "A \<noteq> {} \<Longrightarrow> {x} \<in> sets M \<Longrightarrow> A \<in> sets M \<Longrightarrow> x \<notin> A \<Longrightarrow> emeasure M (insert x A) = emeasure M {x} + emeasure M A"
+ by (rule emeasure_insert)
+
lemma emeasure_eq_setsum_singleton:
assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M"
shows "emeasure M S = (\<Sum>x\<in>S. emeasure M {x})"
@@ -1037,8 +1045,34 @@
locale sigma_finite_measure =
fixes M :: "'a measure"
- assumes sigma_finite: "\<exists>A::nat \<Rightarrow> 'a set.
- range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. emeasure M (A i) \<noteq> \<infinity>)"
+ assumes sigma_finite_countable:
+ "\<exists>A::'a set set. countable A \<and> A \<subseteq> sets M \<and> (\<Union>A) = space M \<and> (\<forall>a\<in>A. emeasure M a \<noteq> \<infinity>)"
+
+lemma (in sigma_finite_measure) sigma_finite:
+ obtains A :: "nat \<Rightarrow> 'a set"
+ where "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
+proof -
+ obtain A :: "'a set set" where
+ [simp]: "countable A" and
+ A: "A \<subseteq> sets M" "(\<Union>A) = space M" "\<And>a. a \<in> A \<Longrightarrow> emeasure M a \<noteq> \<infinity>"
+ using sigma_finite_countable by metis
+ show thesis
+ proof cases
+ assume "A = {}" with `(\<Union>A) = space M` show thesis
+ by (intro that[of "\<lambda>_. {}"]) auto
+ next
+ assume "A \<noteq> {}"
+ show thesis
+ proof
+ show "range (from_nat_into A) \<subseteq> sets M"
+ using `A \<noteq> {}` A by auto
+ have "(\<Union>i. from_nat_into A i) = \<Union>A"
+ using range_from_nat_into[OF `A \<noteq> {}` `countable A`] by auto
+ with A show "(\<Union>i. from_nat_into A i) = space M"
+ by auto
+ qed (intro A from_nat_into `A \<noteq> {}`)
+ qed
+qed
lemma (in sigma_finite_measure) sigma_finite_disjoint:
obtains A :: "nat \<Rightarrow> 'a set"
@@ -1135,6 +1169,16 @@
"f \<in> measurable M N \<Longrightarrow> S \<in> sets N \<Longrightarrow> measure (distr M N f) S = measure M (f -` S \<inter> space M)"
by (simp add: emeasure_distr measure_def)
+lemma distr_cong_AE:
+ assumes 1: "M = K" "sets N = sets L" and
+ 2: "(AE x in M. f x = g x)" and "f \<in> measurable M N" and "g \<in> measurable K L"
+ shows "distr M N f = distr K L g"
+proof (rule measure_eqI)
+ fix A assume "A \<in> sets (distr M N f)"
+ with assms show "emeasure (distr M N f) A = emeasure (distr K L g) A"
+ by (auto simp add: emeasure_distr intro!: emeasure_eq_AE measurable_sets)
+qed (insert 1, simp)
+
lemma AE_distrD:
assumes f: "f \<in> measurable M M'"
and AE: "AE x in distr M M' f. P x"
@@ -1311,12 +1355,8 @@
assumes finite_emeasure_space: "emeasure M (space M) \<noteq> \<infinity>"
lemma finite_measureI[Pure.intro!]:
- assumes *: "emeasure M (space M) \<noteq> \<infinity>"
- shows "finite_measure M"
-proof
- show "\<exists>A. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. emeasure M (A i) \<noteq> \<infinity>)"
- using * by (auto intro!: exI[of _ "\<lambda>_. space M"])
-qed fact
+ "emeasure M (space M) \<noteq> \<infinity> \<Longrightarrow> finite_measure M"
+ proof qed (auto intro!: exI[of _ "{space M}"])
lemma (in finite_measure) emeasure_finite[simp, intro]: "emeasure M A \<noteq> \<infinity>"
using finite_emeasure_space emeasure_space[of M A] by auto
@@ -1624,16 +1664,7 @@
lemma sigma_finite_measure_count_space_countable:
assumes A: "countable A"
shows "sigma_finite_measure (count_space A)"
-proof
- show "\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> sets (count_space A) \<and> (\<Union>i. F i) = space (count_space A) \<and>
- (\<forall>i. emeasure (count_space A) (F i) \<noteq> \<infinity>)"
- using A
- apply (intro exI[of _ "\<lambda>i. {from_nat_into A i} \<inter> A"])
- apply auto
- apply (rule_tac x="to_nat_on A x" in exI)
- apply simp
- done
-qed
+ proof qed (auto intro!: exI[of _ "(\<lambda>a. {a}) ` A"] simp: A)
lemma sigma_finite_measure_count_space:
fixes A :: "'a::countable set" shows "sigma_finite_measure (count_space A)"
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Mon Jun 30 15:45:21 2014 +0200
@@ -1187,6 +1187,32 @@
qed simp
qed simp
+lemma nn_integral_bound_simple_function:
+ assumes bnd: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x" "\<And>x. x \<in> space M \<Longrightarrow> f x < \<infinity>"
+ assumes f[measurable]: "simple_function M f"
+ assumes supp: "emeasure M {x\<in>space M. f x \<noteq> 0} < \<infinity>"
+ shows "nn_integral M f < \<infinity>"
+proof cases
+ assume "space M = {}"
+ then have "nn_integral M f = (\<integral>\<^sup>+x. 0 \<partial>M)"
+ by (intro nn_integral_cong) auto
+ then show ?thesis by simp
+next
+ assume "space M \<noteq> {}"
+ with simple_functionD(1)[OF f] bnd have bnd: "0 \<le> Max (f`space M) \<and> Max (f`space M) < \<infinity>"
+ by (subst Max_less_iff) (auto simp: Max_ge_iff)
+
+ have "nn_integral M f \<le> (\<integral>\<^sup>+x. Max (f`space M) * indicator {x\<in>space M. f x \<noteq> 0} x \<partial>M)"
+ proof (rule nn_integral_mono)
+ fix x assume "x \<in> space M"
+ with f show "f x \<le> Max (f ` space M) * indicator {x \<in> space M. f x \<noteq> 0} x"
+ by (auto split: split_indicator intro!: Max_ge simple_functionD)
+ qed
+ also have "\<dots> < \<infinity>"
+ using bnd supp by (subst nn_integral_cmult) auto
+ finally show ?thesis .
+qed
+
lemma nn_integral_Markov_inequality:
assumes u: "u \<in> borel_measurable M" "AE x in M. 0 \<le> u x" and "A \<in> sets M" and c: "0 \<le> c"
shows "(emeasure M) ({x\<in>space M. 1 \<le> c * u x} \<inter> A) \<le> c * (\<integral>\<^sup>+ x. u x * indicator A x \<partial>M)"
--- a/src/HOL/Probability/Probability_Measure.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy Mon Jun 30 15:45:21 2014 +0200
@@ -29,6 +29,9 @@
abbreviation (in prob_space) "expectation \<equiv> integral\<^sup>L M"
abbreviation (in prob_space) "variance X \<equiv> integral\<^sup>L M (\<lambda>x. (X x - expectation X)\<^sup>2)"
+lemma (in prob_space) finite_measure [simp]: "finite_measure M"
+ by unfold_locales
+
lemma (in prob_space) prob_space_distr:
assumes f: "f \<in> measurable M M'" shows "prob_space (distr M M' f)"
proof (rule prob_spaceI)
@@ -344,6 +347,10 @@
lemma (in prob_space) variance_positive: "0 \<le> variance (X::'a \<Rightarrow> real)"
by (intro integral_nonneg_AE) (auto intro!: integral_nonneg_AE)
+lemma (in prob_space) variance_mean_zero:
+ "expectation X = 0 \<Longrightarrow> variance X = expectation (\<lambda>x. (X x)^2)"
+ by simp
+
locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2
sublocale pair_prob_space \<subseteq> P: prob_space "M1 \<Otimes>\<^sub>M M2"
@@ -988,7 +995,7 @@
and M_eq: "\<And>a. emeasure M {x\<in>space M. X x \<le> a} = ereal (g a)"
shows "distributed M lborel X f"
proof (rule distributedI_real)
- show "sets lborel = sigma_sets (space lborel) (range atMost)"
+ show "sets (lborel::real measure) = sigma_sets (space lborel) (range atMost)"
by (simp add: borel_eq_atMost)
show "Int_stable (range atMost :: real set set)"
by (auto simp: Int_stable_def)
--- a/src/HOL/Probability/Projective_Family.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Probability/Projective_Family.thy Mon Jun 30 15:45:21 2014 +0200
@@ -118,7 +118,7 @@
finally show ?thesis .
qed
-lemma limP_finite:
+lemma limP_finite[simp]:
assumes "finite J"
assumes "J \<subseteq> I"
shows "limP J M P = P J" (is "?P = _")
@@ -237,11 +237,11 @@
proof (intro the_equality allI impI ballI)
fix K Y assume K: "K \<noteq> {}" "finite K" "K \<subseteq> I" "A = emb I K Y" "Y \<in> sets (Pi\<^sub>M K M)"
have "emeasure (limP K M P) Y = emeasure (limP (K \<union> J) M P) (emb (K \<union> J) K Y)"
- using K J by simp
+ using K J by (simp del: limP_finite)
also have "emb (K \<union> J) K Y = emb (K \<union> J) J X"
using K J by (simp add: prod_emb_injective[of "K \<union> J" I])
also have "emeasure (limP (K \<union> J) M P) (emb (K \<union> J) J X) = emeasure (limP J M P) X"
- using K J by simp
+ using K J by (simp del: limP_finite)
finally show "emeasure (limP J M P) X = emeasure (limP K M P) Y" ..
qed (insert J, force)
@@ -255,7 +255,7 @@
proof -
from * obtain J X where J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^sub>M J M)"
unfolding generator_def by auto
- with mu_G_spec[OF this] show ?thesis by auto
+ with mu_G_spec[OF this] show ?thesis by (auto simp del: limP_finite)
qed
lemma generatorE:
@@ -326,7 +326,7 @@
also have "\<dots> = emeasure (limP (J \<union> K) M P) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
using JK J(1, 4) K(1, 4) by (simp add: mu_G_eq sets.Un del: prod_emb_Un)
also have "\<dots> = \<mu>G A + \<mu>G B"
- using J K JK_disj by (simp add: plus_emeasure[symmetric])
+ using J K JK_disj by (simp add: plus_emeasure[symmetric] del: limP_finite)
finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" .
qed
qed
@@ -334,19 +334,14 @@
end
sublocale product_prob_space \<subseteq> projective_family I "\<lambda>J. PiM J M" M
-proof
- fix J::"'i set" assume "finite J"
+proof (simp add: projective_family_def, safe)
+ fix J::"'i set" assume [simp]: "finite J"
interpret f: finite_product_prob_space M J proof qed fact
- show "emeasure (Pi\<^sub>M J M) (space (Pi\<^sub>M J M)) \<noteq> \<infinity>" by simp
- show "\<exists>A. range A \<subseteq> sets (Pi\<^sub>M J M) \<and>
- (\<Union>i. A i) = space (Pi\<^sub>M J M) \<and>
- (\<forall>i. emeasure (Pi\<^sub>M J M) (A i) \<noteq> \<infinity>)" using sigma_finite[OF `finite J`]
- by (auto simp add: sigma_finite_measure_def)
- show "emeasure (Pi\<^sub>M J M) (space (Pi\<^sub>M J M)) = 1" by (rule f.emeasure_space_1)
-qed simp_all
-
-lemma (in product_prob_space) limP_PiM_finite[simp]:
- assumes "J \<noteq> {}" "finite J" "J \<subseteq> I" shows "limP J M (\<lambda>J. PiM J M) = PiM J M"
- using assms by (simp add: limP_finite)
+ show "prob_space (Pi\<^sub>M J M)"
+ proof
+ show "emeasure (Pi\<^sub>M J M) (space (Pi\<^sub>M J M)) = 1"
+ by (simp add: space_PiM emeasure_PiM emeasure_space_1)
+ qed
+qed
end
--- a/src/HOL/Probability/Projective_Limit.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Probability/Projective_Limit.thy Mon Jun 30 15:45:21 2014 +0200
@@ -315,7 +315,7 @@
using J J_mono K_sets `n \<ge> 1`
by (simp only: emeasure_eq_measure)
(auto dest!: bspec[where x=n]
- simp: extensional_restrict emeasure_eq_measure prod_emb_iff
+ simp: extensional_restrict emeasure_eq_measure prod_emb_iff simp del: limP_finite
intro!: measure_Diff[symmetric] set_mp[OF K_B])
also have subs: "Z n - Y n \<subseteq> (\<Union> i\<in>{1..n}. (Z i - Z' i))" using Z' Z `n \<ge> 1`
unfolding Y_def by (force simp: decseq_def)
@@ -332,9 +332,7 @@
have "\<mu>G (Z i - Z' i) = \<mu>G (prod_emb I (\<lambda>_. borel) (J i) (B i - K i))"
unfolding Z'_def Z_eq by simp
also have "\<dots> = P (J i) (B i - K i)"
- apply (subst mu_G_eq) using J K_sets apply auto
- apply (subst limP_finite) apply auto
- done
+ using J K_sets by (subst mu_G_eq) auto
also have "\<dots> = P (J i) (B i) - P (J i) (K i)"
apply (subst emeasure_Diff) using K_sets J `K _ \<subseteq> B _` apply (auto simp: proj_sets)
done
@@ -585,7 +583,7 @@
moreover have "emb I {} {\<lambda>x. undefined} = space (lim\<^sub>B I P)"
by (auto simp: space_PiM prod_emb_def)
moreover have "{\<lambda>x. undefined} = space (lim\<^sub>B {} P)"
- by (auto simp: space_PiM prod_emb_def)
+ by (auto simp: space_PiM prod_emb_def simp del: limP_finite)
ultimately show ?thesis
by (simp add: P.emeasure_space_1 limP_finite emeasure_space_1 del: space_limP)
next
--- a/src/HOL/Probability/Radon_Nikodym.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy Mon Jun 30 15:45:21 2014 +0200
@@ -991,26 +991,23 @@
using fin by (auto elim!: AE_Ball_mp)
next
assume AE: "AE x in M. f x \<noteq> \<infinity>"
- from sigma_finite guess Q .. note Q = this
+ from sigma_finite guess Q . note Q = this
def A \<equiv> "\<lambda>i. f -` (case i of 0 \<Rightarrow> {\<infinity>} | Suc n \<Rightarrow> {.. ereal(of_nat (Suc n))}) \<inter> space M"
{ fix i j have "A i \<inter> Q j \<in> sets M"
unfolding A_def using f Q
apply (rule_tac sets.Int)
by (cases i) (auto intro: measurable_sets[OF f(1)]) }
note A_in_sets = this
- let ?A = "\<lambda>n. case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j"
+
show "sigma_finite_measure ?N"
- proof (default, intro exI conjI subsetI allI)
- fix x assume "x \<in> range ?A"
- then obtain n where n: "x = ?A n" by auto
- then show "x \<in> sets ?N" using A_in_sets by (cases "prod_decode n") auto
+ proof (default, intro exI conjI ballI)
+ show "countable (range (\<lambda>(i, j). A i \<inter> Q j))"
+ by auto
+ show "range (\<lambda>(i, j). A i \<inter> Q j) \<subseteq> sets (density M f)"
+ using A_in_sets by auto
next
- have "(\<Union>i. ?A i) = (\<Union>i j. A i \<inter> Q j)"
- proof safe
- fix x i j assume "x \<in> A i" "x \<in> Q j"
- then show "x \<in> (\<Union>i. case prod_decode i of (i, j) \<Rightarrow> A i \<inter> Q j)"
- by (intro UN_I[of "prod_encode (i,j)"]) auto
- qed auto
+ have "\<Union>range (\<lambda>(i, j). A i \<inter> Q j) = (\<Union>i j. A i \<inter> Q j)"
+ by auto
also have "\<dots> = (\<Union>i. A i) \<inter> space M" using Q by auto
also have "(\<Union>i. A i) = space M"
proof safe
@@ -1027,10 +1024,10 @@
unfolding A_def by (auto intro!: exI[of _ "Suc 0"])
qed
qed (auto simp: A_def)
- finally show "(\<Union>i. ?A i) = space ?N" by simp
+ finally show "\<Union>range (\<lambda>(i, j). A i \<inter> Q j) = space ?N" by simp
next
- fix n obtain i j where
- [simp]: "prod_decode n = (i, j)" by (cases "prod_decode n") auto
+ fix X assume "X \<in> range (\<lambda>(i, j). A i \<inter> Q j)"
+ then obtain i j where [simp]:"X = A i \<inter> Q j" by auto
have "(\<integral>\<^sup>+x. f x * indicator (A i \<inter> Q j) x \<partial>M) \<noteq> \<infinity>"
proof (cases i)
case 0
@@ -1048,7 +1045,7 @@
using Q by (auto simp: real_eq_of_nat[symmetric])
finally show ?thesis by simp
qed
- then show "emeasure ?N (?A n) \<noteq> \<infinity>"
+ then show "emeasure ?N X \<noteq> \<infinity>"
using A_in_sets Q f by (auto simp: emeasure_density)
qed
qed
@@ -1164,20 +1161,22 @@
let ?M' = "distr M M' T" and ?N' = "distr N M' T"
interpret M': sigma_finite_measure ?M'
proof
- from sigma_finite guess F .. note F = this
- show "\<exists>A::nat \<Rightarrow> 'b set. range A \<subseteq> sets ?M' \<and> (\<Union>i. A i) = space ?M' \<and> (\<forall>i. emeasure ?M' (A i) \<noteq> \<infinity>)"
- proof (intro exI conjI allI)
- show *: "range (\<lambda>i. T' -` F i \<inter> space ?M') \<subseteq> sets ?M'"
+ from sigma_finite_countable guess F .. note F = this
+ show "\<exists>A. countable A \<and> A \<subseteq> sets (distr M M' T) \<and> \<Union>A = space (distr M M' T) \<and> (\<forall>a\<in>A. emeasure (distr M M' T) a \<noteq> \<infinity>)"
+ proof (intro exI conjI ballI)
+ show *: "(\<lambda>A. T' -` A \<inter> space ?M') ` F \<subseteq> sets ?M'"
using F T' by (auto simp: measurable_def)
- show "(\<Union>i. T' -` F i \<inter> space ?M') = space ?M'"
- using F T' by (force simp: measurable_def)
- fix i
- have "T' -` F i \<inter> space M' \<in> sets M'" using * by auto
+ show "\<Union>((\<lambda>A. T' -` A \<inter> space ?M')`F) = space ?M'"
+ using F T'[THEN measurable_space] by (auto simp: set_eq_iff)
+ next
+ fix X assume "X \<in> (\<lambda>A. T' -` A \<inter> space ?M')`F"
+ then obtain A where [simp]: "X = T' -` A \<inter> space ?M'" and "A \<in> F" by auto
+ have "X \<in> sets M'" using F T' `A\<in>F` by auto
moreover
- have Fi: "F i \<in> sets M" using F by auto
- ultimately show "emeasure ?M' (T' -` F i \<inter> space ?M') \<noteq> \<infinity>"
- using F T T' by (simp add: emeasure_distr)
- qed
+ have Fi: "A \<in> sets M" using F `A\<in>F` by auto
+ ultimately show "emeasure ?M' X \<noteq> \<infinity>"
+ using F T T' `A\<in>F` by (simp add: emeasure_distr)
+ qed (insert F, auto)
qed
have "(RN_deriv ?M' ?N') \<circ> T \<in> borel_measurable M"
using T ac by measurable
--- a/src/HOL/Probability/Sigma_Algebra.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Mon Jun 30 15:45:21 2014 +0200
@@ -796,6 +796,9 @@
lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
by blast
+lemma disjoint_family_onD: "disjoint_family_on A I \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
+ by (auto simp: disjoint_family_on_def)
+
lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
by blast
--- a/src/HOL/Real.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Real.thy Mon Jun 30 15:45:21 2014 +0200
@@ -1429,6 +1429,12 @@
ultimately show ?thesis by fast
qed
+lemma of_rat_dense:
+ fixes x y :: real
+ assumes "x < y"
+ shows "\<exists>q :: rat. x < of_rat q \<and> of_rat q < y"
+using Rats_dense_in_real [OF `x < y`]
+by (auto elim: Rats_cases)
subsection{*Numerals and Arithmetic*}
@@ -1444,7 +1450,7 @@
"real (- numeral v :: int) = - numeral v"
by (simp_all add: real_of_int_def)
-lemma real_of_nat_numeral [simp]:
+lemma real_of_nat_numeral [simp]:
"real (numeral v :: nat) = numeral v"
by (simp add: real_of_nat_def)
@@ -1995,9 +2001,15 @@
unfolding natceiling_def real_of_int_of_nat_eq [symmetric] ceiling_subtract
by simp
-lemma Rats_unbounded: "\<exists> q \<in> \<rat>. (x :: real) \<le> q"
+lemma Rats_no_top_le: "\<exists> q \<in> \<rat>. (x :: real) \<le> q"
by (auto intro!: bexI[of _ "of_nat (natceiling x)"]) (metis real_natceiling_ge real_of_nat_def)
+lemma Rats_no_bot_less: "\<exists> q \<in> \<rat>. q < (x :: real)"
+ apply (auto intro!: bexI[of _ "of_int (floor x - 1)"])
+ apply (rule less_le_trans[OF _ of_int_floor_le])
+ apply simp
+ done
+
subsection {* Exponentiation with floor *}
lemma floor_power:
--- a/src/HOL/Set_Interval.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Set_Interval.thy Mon Jun 30 15:45:21 2014 +0200
@@ -457,6 +457,15 @@
shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d"
using atLeastLessThan_inj assms by auto
+lemma (in linorder) Ioc_inj: "{a <.. b} = {c <.. d} \<longleftrightarrow> (b \<le> a \<and> d \<le> c) \<or> a = c \<and> b = d"
+ by (metis eq_iff greaterThanAtMost_empty_iff2 greaterThanAtMost_iff le_cases not_le)
+
+lemma (in order) Iio_Int_singleton: "{..<k} \<inter> {x} = (if x < k then {x} else {})"
+ by auto
+
+lemma (in linorder) Ioc_subset_iff: "{a<..b} \<subseteq> {c<..d} \<longleftrightarrow> (b \<le> a \<or> c \<le> a \<and> b \<le> d)"
+ by (auto simp: subset_eq Ball_def) (metis less_le not_less)
+
lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
by (auto simp: set_eq_iff intro: le_bot)
@@ -588,6 +597,9 @@
lemma Int_atMost[simp]: "{..a} \<inter> {..b} = {.. min a b}"
by (auto simp: min_def)
+lemma Ioc_disjoint: "{a<..b} \<inter> {c<..d} = {} \<longleftrightarrow> b \<le> a \<or> d \<le> c \<or> b \<le> c \<or> d \<le> a"
+ using assms by auto
+
end
context complete_lattice
--- a/src/HOL/Topological_Spaces.thy Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Topological_Spaces.thy Mon Jun 30 15:45:21 2014 +0200
@@ -102,6 +102,42 @@
lemma closed_Compl [continuous_intros, intro]: "open S \<Longrightarrow> closed (- S)"
unfolding open_closed .
+lemma open_Collect_neg: "closed {x. P x} \<Longrightarrow> open {x. \<not> P x}"
+ unfolding Collect_neg_eq by (rule open_Compl)
+
+lemma open_Collect_conj: assumes "open {x. P x}" "open {x. Q x}" shows "open {x. P x \<and> Q x}"
+ using open_Int[OF assms] by (simp add: Int_def)
+
+lemma open_Collect_disj: assumes "open {x. P x}" "open {x. Q x}" shows "open {x. P x \<or> Q x}"
+ using open_Un[OF assms] by (simp add: Un_def)
+
+lemma open_Collect_ex: "(\<And>i. open {x. P i x}) \<Longrightarrow> open {x. \<exists>i. P i x}"
+ using open_UN[of UNIV "\<lambda>i. {x. P i x}"] unfolding Collect_ex_eq by simp
+
+lemma open_Collect_imp: "closed {x. P x} \<Longrightarrow> open {x. Q x} \<Longrightarrow> open {x. P x \<longrightarrow> Q x}"
+ unfolding imp_conv_disj by (intro open_Collect_disj open_Collect_neg)
+
+lemma open_Collect_const: "open {x. P}"
+ by (cases P) auto
+
+lemma closed_Collect_neg: "open {x. P x} \<Longrightarrow> closed {x. \<not> P x}"
+ unfolding Collect_neg_eq by (rule closed_Compl)
+
+lemma closed_Collect_conj: assumes "closed {x. P x}" "closed {x. Q x}" shows "closed {x. P x \<and> Q x}"
+ using closed_Int[OF assms] by (simp add: Int_def)
+
+lemma closed_Collect_disj: assumes "closed {x. P x}" "closed {x. Q x}" shows "closed {x. P x \<or> Q x}"
+ using closed_Un[OF assms] by (simp add: Un_def)
+
+lemma closed_Collect_all: "(\<And>i. closed {x. P i x}) \<Longrightarrow> closed {x. \<forall>i. P i x}"
+ using closed_INT[of UNIV "\<lambda>i. {x. P i x}"] unfolding Collect_all_eq by simp
+
+lemma closed_Collect_imp: "open {x. P x} \<Longrightarrow> closed {x. Q x} \<Longrightarrow> closed {x. P x \<longrightarrow> Q x}"
+ unfolding imp_conv_disj by (intro closed_Collect_disj closed_Collect_neg)
+
+lemma closed_Collect_const: "closed {x. P}"
+ by (cases P) auto
+
end
subsection{* Hausdorff and other separation properties *}
@@ -374,6 +410,12 @@
shows "eventually (\<lambda>i. R i) F"
using assms by (auto elim!: eventually_rev_mp)
+lemma not_eventually_impI: "eventually P F \<Longrightarrow> \<not> eventually Q F \<Longrightarrow> \<not> eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
+ by (auto intro: eventually_mp)
+
+lemma not_eventuallyD: "\<not> eventually P F \<Longrightarrow> \<exists>x. \<not> P x"
+ by (metis always_eventually)
+
lemma eventually_subst:
assumes "eventually (\<lambda>n. P n = Q n) F"
shows "eventually P F = eventually Q F" (is "?L = ?R")
@@ -965,6 +1007,16 @@
apply fact
done
+lemma filtermap_mono_strong: "inj f \<Longrightarrow> filtermap f F \<le> filtermap f G \<longleftrightarrow> F \<le> G"
+ apply (auto intro!: filtermap_mono) []
+ apply (auto simp: le_filter_def eventually_filtermap)
+ apply (erule_tac x="\<lambda>x. P (inv f x)" in allE)
+ apply auto
+ done
+
+lemma filtermap_eq_strong: "inj f \<Longrightarrow> filtermap f F = filtermap f G \<longleftrightarrow> F = G"
+ by (simp add: filtermap_mono_strong eq_iff)
+
lemma filterlim_principal:
"(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
unfolding filterlim_def eventually_filtermap le_principal ..
@@ -984,6 +1036,13 @@
"filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
unfolding filterlim_def filtermap_sup by auto
+lemma eventually_sequentially_Suc: "eventually (\<lambda>i. P (Suc i)) sequentially \<longleftrightarrow> eventually P sequentially"
+ unfolding eventually_sequentially by (metis Suc_le_D Suc_le_mono le_Suc_eq)
+
+lemma filterlim_sequentially_Suc:
+ "(LIM x sequentially. f (Suc x) :> F) \<longleftrightarrow> (LIM x sequentially. f x :> F)"
+ unfolding filterlim_iff by (subst eventually_sequentially_Suc) simp
+
lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
@@ -1259,6 +1318,23 @@
shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)"
by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1)
+lemma filterlim_at_bot_dense:
+ fixes f :: "'a \<Rightarrow> ('b::{dense_linorder, no_bot})"
+ shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x < Z) F)"
+proof (auto simp add: filterlim_at_bot[of f F])
+ fix Z :: 'b
+ from lt_ex [of Z] obtain Z' where 1: "Z' < Z" ..
+ assume "\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F"
+ hence "eventually (\<lambda>x. f x \<le> Z') F" by auto
+ thus "eventually (\<lambda>x. f x < Z) F"
+ apply (rule eventually_mono[rotated])
+ using 1 by auto
+ next
+ fix Z :: 'b
+ show "\<forall>Z. eventually (\<lambda>x. f x < Z) F \<Longrightarrow> eventually (\<lambda>x. f x \<le> Z) F"
+ by (drule spec [of _ Z], erule eventually_mono[rotated], auto simp add: less_imp_le)
+qed
+
lemma filterlim_at_bot_le:
fixes f :: "'a \<Rightarrow> ('b::linorder)" and c :: "'b"
shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F)"
@@ -1343,6 +1419,11 @@
by (intro exI[of _ "{b <..}"]) auto
qed
+lemma tendsto_at_within_iff_tendsto_nhds:
+ "(g ---> g l) (at l within S) \<longleftrightarrow> (g ---> g l) (inf (nhds l) (principal S))"
+ unfolding tendsto_def eventually_at_filter eventually_inf_principal
+ by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
+
subsection {* Limits on sequences *}
abbreviation (in topological_space)
@@ -1742,6 +1823,12 @@
"eventually P (nhds a) \<longleftrightarrow> (\<forall>f. f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially)"
using eventually_nhds_within_iff_sequentially[of P a UNIV] by simp
+lemma tendsto_at_iff_sequentially:
+ fixes f :: "'a :: first_countable_topology \<Rightarrow> _"
+ shows "(f ---> a) (at x within s) \<longleftrightarrow> (\<forall>X. (\<forall>i. X i \<in> s - {x}) \<longrightarrow> X ----> x \<longrightarrow> ((f \<circ> X) ----> a))"
+ unfolding filterlim_def[of _ "nhds a"] le_filter_def eventually_filtermap at_within_def eventually_nhds_within_iff_sequentially comp_def
+ by metis
+
subsection {* Function limit at a point *}
abbreviation
@@ -1805,6 +1892,9 @@
shows "(\<lambda>x. g (f x)) -- a --> c"
using g f inj by (rule tendsto_compose_eventually)
+lemma tendsto_compose_filtermap: "((g \<circ> f) ---> T) F \<longleftrightarrow> (g ---> T) (filtermap f F)"
+ by (simp add: filterlim_def filtermap_filtermap comp_def)
+
subsubsection {* Relation of LIM and LIMSEQ *}
lemma (in first_countable_topology) sequentially_imp_eventually_within:
@@ -1840,34 +1930,27 @@
assumes *: "\<And>f. (\<And>n. b < f n) \<Longrightarrow> (\<And>n. f n < a) \<Longrightarrow> incseq f \<Longrightarrow> f ----> a \<Longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
shows "eventually P (at_left a)"
proof (safe intro!: sequentially_imp_eventually_within)
- fix X assume X: "\<forall>n. X n \<in> {..<a} \<and> X n \<noteq> a" "X ----> a"
+ fix X assume X: "\<forall>n. X n \<in> {..< a} \<and> X n \<noteq> a" "X ----> a"
show "eventually (\<lambda>n. P (X n)) sequentially"
proof (rule ccontr)
-
- assume "\<not> eventually (\<lambda>n. P (X n)) sequentially"
- from not_eventually_sequentiallyD[OF this]
- obtain r where "subseq r" "\<And>n. \<not> P (X (r n))"
- by auto
- with X have "(X \<circ> r) ----> a"
- by (auto intro: LIMSEQ_subseq_LIMSEQ)
- from order_tendstoD(1)[OF this] obtain s' where s': "\<And>b i. b < a \<Longrightarrow> s' b \<le> i \<Longrightarrow> b < X (r i)"
- unfolding eventually_sequentially comp_def by metis
- def s \<equiv> "rec_nat (s' b) (\<lambda>_ i. max (s' (X (r i))) (Suc i))"
- then have [simp]: "s 0 = s' b" "\<And>n. s (Suc n) = max (s' (X (r (s n)))) (Suc (s n))"
- by auto
- have "eventually (\<lambda>n. P (((X \<circ> r) \<circ> s) n)) sequentially"
- proof (rule *)
- from X show inc: "incseq (X \<circ> r \<circ> s)"
- unfolding incseq_Suc_iff comp_def by (intro allI s'[THEN less_imp_le]) auto
- { fix n show "b < (X \<circ> r \<circ> s) n"
- using inc[THEN incseqD, of 0 n] s'[OF b order_refl] by simp }
- { fix n show "(X \<circ> r \<circ> s) n < a"
- using X by simp }
- from `(X \<circ> r) ----> a` show "(X \<circ> r \<circ> s) ----> a"
- by (rule LIMSEQ_subseq_LIMSEQ) (auto simp: subseq_Suc_iff)
+ assume neg: "\<not> eventually (\<lambda>n. P (X n)) sequentially"
+ have "\<exists>s. \<forall>n. (\<not> P (X (s n)) \<and> b < X (s n)) \<and> (X (s n) \<le> X (s (Suc n)) \<and> Suc (s n) \<le> s (Suc n))"
+ proof (rule dependent_nat_choice)
+ have "\<not> eventually (\<lambda>n. b < X n \<longrightarrow> P (X n)) sequentially"
+ by (intro not_eventually_impI neg order_tendstoD(1) [OF X(2) b])
+ then show "\<exists>x. \<not> P (X x) \<and> b < X x"
+ by (auto dest!: not_eventuallyD)
+ next
+ fix x n
+ have "\<not> eventually (\<lambda>n. Suc x \<le> n \<longrightarrow> b < X n \<longrightarrow> X x < X n \<longrightarrow> P (X n)) sequentially"
+ using X by (intro not_eventually_impI order_tendstoD(1)[OF X(2)] eventually_ge_at_top neg) auto
+ then show "\<exists>n. (\<not> P (X n) \<and> b < X n) \<and> (X x \<le> X n \<and> Suc x \<le> n)"
+ by (auto dest!: not_eventuallyD)
qed
- with `\<And>n. \<not> P (X (r n))` show False
- by auto
+ then guess s ..
+ then have "\<And>n. b < X (s n)" "\<And>n. X (s n) < a" "incseq (\<lambda>n. X (s n))" "(\<lambda>n. X (s n)) ----> a" "\<And>n. \<not> P (X (s n))"
+ using X by (auto simp: subseq_Suc_iff Suc_le_eq incseq_Suc_iff intro!: LIMSEQ_subseq_LIMSEQ[OF `X ----> a`, unfolded comp_def])
+ from *[OF this(1,2,3,4)] this(5) show False by auto
qed
qed
@@ -1879,6 +1962,44 @@
using assms unfolding tendsto_def [where l=L]
by (simp add: sequentially_imp_eventually_at_left)
+lemma sequentially_imp_eventually_at_right:
+ fixes a :: "'a :: {dense_linorder, linorder_topology, first_countable_topology}"
+ assumes b[simp]: "a < b"
+ assumes *: "\<And>f. (\<And>n. a < f n) \<Longrightarrow> (\<And>n. f n < b) \<Longrightarrow> decseq f \<Longrightarrow> f ----> a \<Longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
+ shows "eventually P (at_right a)"
+proof (safe intro!: sequentially_imp_eventually_within)
+ fix X assume X: "\<forall>n. X n \<in> {a <..} \<and> X n \<noteq> a" "X ----> a"
+ show "eventually (\<lambda>n. P (X n)) sequentially"
+ proof (rule ccontr)
+ assume neg: "\<not> eventually (\<lambda>n. P (X n)) sequentially"
+ have "\<exists>s. \<forall>n. (\<not> P (X (s n)) \<and> X (s n) < b) \<and> (X (s (Suc n)) \<le> X (s n) \<and> Suc (s n) \<le> s (Suc n))"
+ proof (rule dependent_nat_choice)
+ have "\<not> eventually (\<lambda>n. X n < b \<longrightarrow> P (X n)) sequentially"
+ by (intro not_eventually_impI neg order_tendstoD(2) [OF X(2) b])
+ then show "\<exists>x. \<not> P (X x) \<and> X x < b"
+ by (auto dest!: not_eventuallyD)
+ next
+ fix x n
+ have "\<not> eventually (\<lambda>n. Suc x \<le> n \<longrightarrow> X n < b \<longrightarrow> X n < X x \<longrightarrow> P (X n)) sequentially"
+ using X by (intro not_eventually_impI order_tendstoD(2)[OF X(2)] eventually_ge_at_top neg) auto
+ then show "\<exists>n. (\<not> P (X n) \<and> X n < b) \<and> (X n \<le> X x \<and> Suc x \<le> n)"
+ by (auto dest!: not_eventuallyD)
+ qed
+ then guess s ..
+ then have "\<And>n. a < X (s n)" "\<And>n. X (s n) < b" "decseq (\<lambda>n. X (s n))" "(\<lambda>n. X (s n)) ----> a" "\<And>n. \<not> P (X (s n))"
+ using X by (auto simp: subseq_Suc_iff Suc_le_eq decseq_Suc_iff intro!: LIMSEQ_subseq_LIMSEQ[OF `X ----> a`, unfolded comp_def])
+ from *[OF this(1,2,3,4)] this(5) show False by auto
+ qed
+qed
+
+lemma tendsto_at_right_sequentially:
+ fixes a :: "_ :: {dense_linorder, linorder_topology, first_countable_topology}"
+ assumes "a < b"
+ assumes *: "\<And>S. (\<And>n. a < S n) \<Longrightarrow> (\<And>n. S n < b) \<Longrightarrow> decseq S \<Longrightarrow> S ----> a \<Longrightarrow> (\<lambda>n. X (S n)) ----> L"
+ shows "(X ---> L) (at_right a)"
+ using assms unfolding tendsto_def [where l=L]
+ by (simp add: sequentially_imp_eventually_at_right)
+
subsection {* Continuity *}
subsubsection {* Continuity on a set *}
@@ -2073,6 +2194,21 @@
"isCont g (f x) \<Longrightarrow> continuous (at x within s) f \<Longrightarrow> continuous (at x within s) (\<lambda>x. g (f x))"
using continuous_within_compose2[of x s f g] by (simp add: continuous_at_within)
+lemma filtermap_nhds_open_map:
+ assumes cont: "isCont f a" and open_map: "\<And>S. open S \<Longrightarrow> open (f`S)"
+ shows "filtermap f (nhds a) = nhds (f a)"
+ unfolding filter_eq_iff
+proof safe
+ fix P assume "eventually P (filtermap f (nhds a))"
+ then guess S unfolding eventually_filtermap eventually_nhds ..
+ then show "eventually P (nhds (f a))"
+ unfolding eventually_nhds by (intro exI[of _ "f`S"]) (auto intro!: open_map)
+qed (metis filterlim_iff tendsto_at_iff_tendsto_nhds isCont_def eventually_filtermap cont)
+
+lemma continuous_at_split:
+ "continuous (at (x::'a::linorder_topology)) f = (continuous (at_left x) f \<and> continuous (at_right x) f)"
+ by (simp add: continuous_within filterlim_at_split)
+
subsubsection{* Open-cover compactness *}
context topological_space
@@ -2301,7 +2437,6 @@
shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f \<Longrightarrow> (\<exists>x\<in>s. \<forall>y\<in>s. f x \<le> f y)"
using compact_attains_inf[of "f ` s"] compact_continuous_image[of s f] by auto
-
subsection {* Connectedness *}
context topological_space