# HG changeset patch # User hoelzl # Date 1404135921 -7200 # Node ID 87429bdecad513d8923e563a610038bb6f81e6d9 # Parent 06e195515deb7d490bdc85cc4afb772465f1541c import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure diff -r 06e195515deb -r 87429bdecad5 src/HOL/Conditionally_Complete_Lattices.thy --- 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 \ {} \ bdd_above A \ bdd_below A \ Inf A \ Sup A" + by (auto intro!: cSup_upper2[of "SOME a. a \ A"] intro: someI cInf_lower) + end instance complete_lattice \ conditionally_complete_lattice @@ -447,20 +451,20 @@ lemma cSup_lessThan[simp]: "Sup {.. Sup {y<.. Sup {y<.. Sup {y.. Sup {y.. 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 \ 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 \ Inf {y<.. Inf {y<..a b::'a. a \ b" diff -r 06e195515deb -r 87429bdecad5 src/HOL/Finite_Set.thy --- 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 "\ finite A" + shows "\B. finite B \ card B = n \ B \ A" +proof (induction n) + case 0 show ?case by (intro exI[of _ "{}"]) auto +next + case (Suc n) + then guess B .. note B = this + with `\ finite A` have "A \ B" by auto + with B have "B \ A" by auto + hence "\x. x \ A - B" by (elim psubset_imp_ex_mem) + then guess x .. note x = this + with B have "finite (insert x B) \ card (insert x B) = Suc n \ insert x B \ A" + by auto + thus "\B. finite B \ card B = Suc n \ B \ A" .. +qed subsubsection {* Cardinality of image *} diff -r 06e195515deb -r 87429bdecad5 src/HOL/Library/Extended_Real.thy --- 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: "\P. (\x::ereal. P x) \ P \ \ (\x. P (ereal x)) \ P (-\)" + by (metis ereal_cases) + +lemma ereal_ex_split: "\P. (\x::ereal. P x) \ P \ \ (\x. P (ereal x)) \ P (-\)" + by (metis ereal_cases) + lemma ereal_uminus_eq_iff[simp]: fixes a b :: ereal shows "-a = -b \ a = b" @@ -2121,7 +2127,6 @@ by auto qed - subsubsection {* Convergent sequences *} lemma lim_ereal[simp]: "((\n. ereal (f n)) ---> ereal x) net \ (f ---> x) net" diff -r 06e195515deb -r 87429bdecad5 src/HOL/Library/Indicator_Function.thy --- 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 \ B \ 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 "\i j. i \ j \ A i \ A j = {}" + shows "(\i. indicator (A i) x::real) sums indicator (\i. A i) x" +proof cases + assume "\i. x \ A i" + then obtain i where i: "x \ A i" .. + with assms have "(\i. indicator (A i) x::real) sums (\i\{i}. indicator (A i) x)" + by (intro sums_finite) (auto split: split_indicator) + also have "(\i\{i}. indicator (A i) x) = indicator (\i. A i) x" + using i by (auto split: split_indicator) + finally show ?thesis . +qed simp + end diff -r 06e195515deb -r 87429bdecad5 src/HOL/Limits.thy --- 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 \ real" + defines "S \ {a..b}" + assumes "a \ b" and f: "continuous_on S f" + shows "\c d. f`S = {c..d} \ c \ d" +proof - + have S: "compact S" "S \ {}" + using `a \ b` by (auto simp: S_def) + obtain c where "c \ S" "\d\S. f d \ f c" + using continuous_attains_sup[OF S f] by auto + moreover obtain d where "d \ S" "\c\S. f d \ 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} \ f d \ 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*} diff -r 06e195515deb -r 87429bdecad5 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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 \ \Basis" - shows "cbox (0::'a::euclidean_space) One = convex hull {x. \i\Basis. (x\i = 0) \ (x\i = 1)}" + "cbox (0::'a::euclidean_space) One = convex hull {x. \i\Basis. (x\i = 0) \ (x\i = 1)}" (is "?int = convex hull ?points") proof - have One[simp]: "\i. i \ Basis \ One \ i = 1" diff -r 06e195515deb -r 87429bdecad5 src/HOL/Multivariate_Analysis/Derivative.thy --- 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 \ (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) \ t \ s \ (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]: "((\x. c) has_vector_derivative 0) net" by (auto simp: has_vector_derivative_def) diff -r 06e195515deb -r 87429bdecad5 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy --- 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 \ real" and L :: real + assumes 1: "limsup X \ L" and 2: "L \ liminf X" + shows "X ----> L" +proof - + from 1 2 have "limsup X \ 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 (\n. ereal (X n))" + by (subst convergent_ereal) + hence "limsup X = lim (\n. ereal(X n))" + by (rule convergent_limsup_cl) + also from 1 2 3 have "limsup X = L" by auto + finally have "lim (\n. ereal(X n)) = L" .. + hence "(\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 \ ereal" shows "X ----> \ \ liminf X = \" @@ -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 \ = filtermap ereal at_top" + and at_right_MInf: "at_right (-\) = 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 \ real) ---> y) (at_left (ereal x)) \ (f ---> y) (at_left x)" + "((f \ real) ---> y) (at_right (ereal x)) \ (f ---> y) (at_right x)" + "((f \ real) ---> y) (at_left (\::ereal)) \ (f ---> y) at_top" + "((f \ real) ---> y) (at_right (-\::ereal)) \ (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 \ f) ---> ereal a) F \ (f ---> a) F" + "((ereal \ f) ---> \) F \ (LIM x F. f x :> at_top)" + "((ereal \ f) ---> -\) F \ (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 \ real" - shows "continuous (at x0) f \ continuous (at x0) (ereal \ f)" -proof - - { - assume "continuous (at x0) f" - then have "continuous (at x0) (ereal \ f)" - using continuous_at_ereal continuous_at_compose[of x0 f ereal] - by auto - } - moreover - { - assume "continuous (at x0) (ereal \ f)" - then have "continuous (at x0) (real \ (ereal \ f))" - using continuous_at_of_ereal - by (intro continuous_at_compose[of x0 "ereal \ f"]) auto - moreover have "real \ (ereal \ 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 \ continuous (at x0 within s) (ereal \ 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 \ continuous_on A (ereal \ 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 - {\, -\::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 \ ereal" - assumes "\x. x \ A \ \f x\ \ \" + assumes *: "\x. x \ A \ \f x\ \ \" shows "continuous_on A f \ continuous_on A (real \ f)" proof - have "f ` A \ UNIV - {\, -\}" diff -r 06e195515deb -r 87429bdecad5 src/HOL/Multivariate_Analysis/Integration.thy --- 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 \ \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 \ ((\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 \ ((\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 \ ((\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 \ 'a::euclidean_space \ real" + assumes f: "\k. (f k has_integral x k) s" + assumes "\k x. x \ s \ f k x \ f (Suc k) x" + assumes "\x. x \ s \ (\k. f k x) ----> g x" + assumes "x ----> x'" + shows "(g has_integral x') s" +proof - + have x_eq: "x = (\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 \ (\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 \ 'n::euclidean_space \ real" assumes "\k. (f k) integrable_on s" @@ -12383,6 +12413,8 @@ subsection {* Dominated convergence *} +(* GENERALIZE the following theorems *) + lemma dominated_convergence: fixes f :: "nat \ 'n::euclidean_space \ real" assumes "\k. (f k) integrable_on s" "h integrable_on s" @@ -12657,4 +12689,26 @@ qed qed +lemma has_integral_dominated_convergence: + fixes f :: "nat \ 'n::euclidean_space \ real" + assumes "\k. (f k has_integral y k) s" "h integrable_on s" + "\k. \x\s. norm (f k x) \ h x" "\x\s. (\k. f k x) ----> g x" + and x: "y ----> x" + shows "(g has_integral x) s" +proof - + have int_f: "\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 "(\i. integral s (f i)) ----> x" + using integral_unique[OF assms(1)] x by simp + show "(\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 diff -r 06e195515deb -r 87429bdecad5 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- 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 \ \Basis" + definition (in euclidean_space) eucl_less (infix " (\i\Basis. a \ i < b \ 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 \ box c d = + box (\i\Basis. max (a\i) (c\i) *\<^sub>R i) (\i\Basis. min (b\i) (d\i) *\<^sub>R i)" + unfolding set_eq_iff and Int_iff and mem_box by auto + lemma rational_boxes: fixes x :: "'a\euclidean_space" assumes "e > 0" @@ -1142,6 +1151,24 @@ show ?th4 unfolding * by (intro **) auto qed +lemma UN_box_eq_UNIV: "(\i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One)) = UNIV" +proof - + { fix x b :: 'a assume [simp]: "b \ Basis" + have "\x \ b\ \ real (natceiling \x \ b\)" + by (rule real_natceiling_ge) + also have "\ \ real (natceiling (Max ((\b. \x \ b\)`Basis)))" + by (auto intro!: natceiling_mono) + also have "\ < real (natceiling (Max ((\b. \x \ b\)`Basis)) + 1)" + by simp + finally have "\x \ b\ < real (natceiling (Max ((\b. \x \ b\)`Basis)) + 1)" . } + then have "\x::'a. \n::nat. \b\Basis. \x \ b\ < real n" + by auto + moreover have "\x b::'a. \n::nat. \x \ b\ < real n \ - real n < x \ b \ x \ 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) \ @@ -4588,6 +4615,43 @@ "continuous (at x) f \ (\e > 0. \d > 0. \x'. dist x' x < d \ 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: "\ x y. x \ y \ f x \ ((f y) :: real)" + shows "(continuous (at_right (a :: real)) f) = (\e > 0. \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: "\ x y. x \ y \ f x \ ((f y) :: real)" + shows "(continuous (at_left (a :: real)) f) = (\e > 0. \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: diff -r 06e195515deb -r 87429bdecad5 src/HOL/Orderings.thy --- 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 \ P) \ (x = y \ P) \ (y < x \ P) \ P" using less_linear by blast +lemma linorder_wlog[case_names le sym]: + "(\a b. a \ b \ P a b) \ (\a b. P b a \ P a b) \ P a b" + by (cases rule: le_cases[of a b]) blast+ + lemma not_less: "\ x < y \ y \ x" apply (simp add: less_le) using linear apply (blast intro: antisym) @@ -360,7 +364,6 @@ lemma not_leE: "\ y \ x \ x < y" unfolding not_le . - text {* Dual order *} lemma dual_linorder: diff -r 06e195515deb -r 87429bdecad5 src/HOL/Probability/Binary_Product_Measure.thy --- 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 \ P: sigma_finite_measure "M1 \\<^sub>M M2" proof - from sigma_finite_up_in_pair_measure_generator guess F :: "nat \ ('a \ 'b) set" .. note F = this - show "\F::nat \ ('a \ 'b) set. range F \ sets (M1 \\<^sub>M M2) \ (\i. F i) = space (M1 \\<^sub>M M2) \ (\i. emeasure (M1 \\<^sub>M M2) (F i) \ \)" - proof (rule exI[of _ F], intro conjI) - show "range F \ sets (M1 \\<^sub>M M2)" using F by (auto simp: pair_measure_def) - show "(\i. F i) = space (M1 \\<^sub>M M2)" - using F by (auto simp: space_pair_measure) - show "\i. emeasure (M1 \\<^sub>M M2) (F i) \ \" using F by auto - qed + from M1.sigma_finite_countable guess F1 .. + moreover from M2.sigma_finite_countable guess F2 .. + ultimately show + "\A. countable A \ A \ sets (M1 \\<^sub>M M2) \ \A = space (M1 \\<^sub>M M2) \ (\a\A. emeasure (M1 \\<^sub>M M2) a \ \)" + by (intro exI[of _ "(\(a, b). a \ b) ` (F1 \ 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 (\i. f -` A i \ space M) \ sets M" - using A f by auto - show "(\i. f -` A i \ 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 \ space M) \ \" - using f A(1,2) A(3)[of i] by (simp add: emeasure_distr subset_eq) + proof + show "\A. countable A \ A \ sets M \ \A = space M \ (\a\A. emeasure M a \ \)" + using A f + by (intro exI[of _ "(\a. f -` a \ 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 \ '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 _ "\_. UNIV"]) + proof qed (intro exI[of _ "{UNIV}"], auto simp: borel_def emeasure_sigma) fix X :: "('a \ 'b) set" assume asm: "X \ sets (borel \\<^sub>M borel)" have "UNIV \ UNIV \ sets (borel \\<^sub>M borel :: ('a \ 'b) measure)" by (simp add: borel_prod) diff -r 06e195515deb -r 87429bdecad5 src/HOL/Probability/Bochner_Integration.thy --- 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 \ borel_measurable M" "AE x in M. 0 \ f x" + assumes "(\\<^sup>+x. f x \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 \ 'b::{banach, second_countable_topology}" shows "simple_bochner_integrable M f \ integrable M f" diff -r 06e195515deb -r 87429bdecad5 src/HOL/Probability/Borel_Space.thy --- 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 \ sets borel" by (auto intro: borel_closed) +lemma box_borel[measurable]: "box a b \ sets borel" + by (auto intro: borel_open) + lemma borel_compact: "compact (A::'a::t2_space set) \ A \ sets borel" by (auto intro: borel_closed dest!: compact_imp_closed) @@ -293,7 +296,6 @@ fixes a b :: "'a\ordered_euclidean_space" shows "{x. x sets borel" and "{x. a sets borel" - and "box a b \ sets borel" and "{..a} \ sets borel" and "{a..} \ sets borel" and "{a..b} \ sets borel" @@ -605,6 +607,16 @@ (auto intro!: sigma_sets_top) qed auto +lemma borel_sigma_sets_Ioc: "borel = sigma UNIV (range (\(a, b). {a <.. b::real}))" +proof (rule borel_eq_sigmaI5[OF borel_eq_atMost]) + fix i :: real + have "{..i} = (\j::nat. {-j <.. i})" + by (auto simp: minus_less_iff reals_Archimedean2) + also have "\ \ sets (sigma UNIV (range (\(i, j). {i<..j})))" + by (intro sets.countable_nat_UN) auto + finally show "{..i} \ sets (sigma UNIV (range (\(i, j). {i<..j})))" . +qed simp + lemma eucl_lessThan: "{x::real. x x. suminf (\i. f i x)) \ 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 \ 'a::metric_space" + shows "{x. isCont f x} \ sets borel" +proof - + let ?I = "\j. inverse(real (Suc j))" + + { fix x + have "isCont f x = (\i. \j. \y z. dist x y < ?I j \ dist x z < ?I j \ dist (f y) (f z) \ ?I i)" + unfolding continuous_at_eps_delta + proof safe + fix i assume "\e>0. \d>0. \y. dist y x < d \ dist (f y) (f x) < e" + moreover have "0 < ?I i / 2" + by simp + ultimately obtain d where d: "0 < d" "\y. dist x y < d \ 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 "\j. \y z. dist x y < ?I j \ dist x z < ?I j \ dist (f y) (f z) \ ?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) \ dist (f y) (f x) + dist (f z) (f x)" + by (rule dist_triangle2) + also have "\ < ?I i / 2 + ?I i / 2" + by (intro add_strict_mono d less_trans[OF _ j] *) + also have "\ \ ?I i" + by (simp add: field_simps real_of_nat_Suc) + finally show "dist (f y) (f z) \ ?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 "\i. \j. \y z. dist x y < ?I j \ dist x z < ?I j \ dist (f y) (f z) \ ?I i" + from this[THEN spec, of "Suc n"] + obtain j where j: "\y z. dist x y < ?I j \ dist x z < ?I j \ dist (f y) (f z) \ ?I (Suc n)" + by auto + + show "\d>0. \y. dist y x < d \ 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) \ ?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 **: "\e y. open {x. dist x y < e}" + using open_ball by (simp_all add: ball_def dist_commute) + + have "{x\space borel. isCont f x } \ 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 "']) (auto intro: generated_ringI_Basic) qed +lemma extend_measure_caratheodory: + fixes G :: "'i \ 'a set" + assumes M: "M = extend_measure \ I G \" + assumes "i \ I" + assumes "semiring_of_sets \ (G ` I)" + assumes empty: "\i. i \ I \ G i = {} \ \ i = 0" + assumes inj: "\i j. i \ I \ j \ I \ G i = G j \ \ i = \ j" + assumes nonneg: "\i. i \ I \ 0 \ \ i" + assumes add: "\A::nat \ 'i. \j. A \ UNIV \ I \ j \ I \ disjoint_family (G \ A) \ + (\i. G (A i)) = G j \ (\n. \ (A n)) = \ j" + shows "emeasure M (G i) = \ i" +proof - + interpret semiring_of_sets \ "G ` I" + by fact + have "\g\G`I. \i\I. g = G i" + by auto + then obtain sel where sel: "\g. g \ G ` I \ sel g \ I" "\g. g \ G ` I \ G (sel g) = g" + by metis + + have "\\'. (\s\G ` I. \' s = \ (sel s)) \ measure_space \ (sigma_sets \ (G ` I)) \'" + proof (rule caratheodory) + show "positive (G ` I) (\s. \ (sel s))" + by (auto simp: positive_def intro!: empty sel nonneg) + show "countably_additive (G ` I) (\s. \ (sel s))" + proof (rule countably_additiveI) + fix A :: "nat \ 'a set" assume "range A \ G ` I" "disjoint_family A" "(\i. A i) \ G ` I" + then show "(\i. \ (sel (A i))) = \ (sel (\i. A i))" + by (intro add) (auto simp: sel image_subset_iff_funcset comp_def Pi_iff intro!: sel) + qed + qed + then obtain \' where \': "\s\G ` I. \' s = \ (sel s)" "measure_space \ (sigma_sets \ (G ` I)) \'" + by metis + + show ?thesis + proof (rule emeasure_extend_measure[OF M]) + { fix i assume "i \ I" then show "\' (G i) = \ i" + using \' by (auto intro!: inj sel) } + show "G ` I \ Pow \" + by fact + then show "positive (sets M) \'" "countably_additive (sets M) \'" + using \' by (simp_all add: M sets_extend_measure measure_space_def) + qed fact +qed + +lemma extend_measure_caratheodory_pair: + fixes G :: "'i \ 'j \ 'a set" + assumes M: "M = extend_measure \ {(a, b). P a b} (\(a, b). G a b) (\(a, b). \ a b)" + assumes "P i j" + assumes semiring: "semiring_of_sets \ {G a b | a b. P a b}" + assumes empty: "\i j. P i j \ G i j = {} \ \ i j = 0" + assumes inj: "\i j k l. P i j \ P k l \ G i j = G k l \ \ i j = \ k l" + assumes nonneg: "\i j. P i j \ 0 \ \ i j" + assumes add: "\A::nat \ 'i. \B::nat \ 'j. \j k. + (\n. P (A n) (B n)) \ P j k \ disjoint_family (\n. G (A n) (B n)) \ + (\i. G (A i) (B i)) = G j k \ (\n. \ (A n) (B n)) = \ j k" + shows "emeasure M (G i j) = \ i j" +proof - + have "emeasure M ((\(a, b). G a b) (i, j)) = (\(a, b). \ a b) (i, j)" + proof (rule extend_measure_caratheodory[OF M]) + show "semiring_of_sets \ ((\(a, b). G a b) ` {(a, b). P a b})" + using semiring by (simp add: image_def conj_commute) + next + fix A :: "nat \ ('i \ 'j)" and j assume "A \ UNIV \ {(a, b). P a b}" "j \ {(a, b). P a b}" + "disjoint_family ((\(a, b). G a b) \ A)" + "(\i. case A i of (a, b) \ G a b) = (case j of (a, b) \ G a b)" + then show "(\n. case A n of (a, b) \ \ a b) = (case j of (a, b) \ \ a b)" + using add[of "\i. fst (A i)" "\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 diff -r 06e195515deb -r 87429bdecad5 src/HOL/Probability/Distributions.thy --- 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 \ b then b - a else 0)" - by (auto simp: measure_def) - -lemma integral_power: - "a \ b \ (\x. x^k * indicator {a..b} x \lborel) = (b^Suc k - a^Suc k) / Suc k" -proof (subst integral_FTC_atLeastAtMost) - fix x show "DERIV (\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 \ borel_measurable M" "AE x in M. 0 \ f x" - assumes "(\\<^sup>+x. f x \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)) \ (AE x in N. 0 < f x \ P x)" @@ -104,8 +84,8 @@ by (intro nn_integral_multc[symmetric]) auto also have "\ = (\\<^sup>+x. ereal (?f k x) * indicator {0 .. a} x \lborel)" by (intro nn_integral_cong) (simp add: field_simps) - also have "\ = ereal (?F k a) - (?F k 0)" - proof (rule nn_integral_FTC_atLeastAtMost) + also have "\ = ereal (?F k a - ?F k 0)" + proof (rule nn_integral_FTC_Icc) fix x assume "x \ {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 @@ (\ x. (x / measure lborel {a .. b}) * indicator {a .. b} x \lborel)" by (intro integral_cong) auto also have "(\ x. (x / measure lborel {a .. b}) * indicator {a .. b} x \lborel) = (a + b) / 2" - proof (subst integral_FTC_atLeastAtMost) + proof (subst integral_FTC_Icc_real) fix x show "DERIV (\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 "(\x. x\<^sup>2 * (?D x) \lborel) = (\x. x\<^sup>2 * (indicator {a - ?\ .. b - ?\} x) / measure lborel {a .. b} \lborel)" by (intro integral_cong) (auto split: split_indicator) also have "\ = (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 "(\x. x\<^sup>2 * ?D x \lborel) = (b - a)\<^sup>2 / 12" . qed fact diff -r 06e195515deb -r 87429bdecad5 src/HOL/Probability/Finite_Product_Measure.thy --- 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: "(\f\PiE I F. \i\I. P i (f i)) \ (\i\I. \x\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: "(\(i, j). c) = (\_. 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 \ nat \ 'a set" .. - then have F: "\j. j \ I \ range (F j) \ sets (M j)" - "incseq (\k. \\<^sub>E j \ I. F j k)" - "(\k. \\<^sub>E j \ I. F j k) = space (Pi\<^sub>M I M)" - "\k. \j. j \ I \ emeasure (M j) (F j k) \ \" - by blast+ - let ?F = "\k. \\<^sub>E j \ I. F j k" - - show ?thesis - proof (unfold_locales, intro exI[of _ ?F] conjI allI) - show "range ?F \ sets (Pi\<^sub>M I M)" using F(1) `finite I` by auto - next - from F(3) show "(\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 (\\<^sub>M i\I. M i) (?F j) \ \" - by (subst emeasure_PiM) auto - qed + obtain F where F: "\j. countable (F j)" "\j f. f \ F j \ f \ sets (M j)" + "\j f. f \ F j \ emeasure (M j) f \ \" and + in_space: "\j. space (M j) = (\F j)" + using sigma_finite_countable by (metis subset_eq) + moreover have "(\(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 "\A. countable A \ A \ sets (Pi\<^sub>M I M) \ \A = space (Pi\<^sub>M I M) \ (\a\A. emeasure (Pi\<^sub>M I M) a \ \)" + 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 \ sigma_finite_measure "Pi\<^sub>M I M" diff -r 06e195515deb -r 87429bdecad5 src/HOL/Probability/Independent_Family.thy --- 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: "\i. i \ I \ Y i \ measurable (M' i) (N i)" + shows "indep_vars N (\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 \ measurable M1 N1" "Y2 \ measurable M2 N2" shows "indep_var N1 (Y1 \ X1) N2 (Y2 \ X2)" diff -r 06e195515deb -r 87429bdecad5 src/HOL/Probability/Lebesgue_Measure.thy --- 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 :: _ \ real) absolutely_integrable_on X) \ - (indicator A :: _ \ 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 \ real) \ real measure" where + "interval_measure F = extend_measure UNIV {(a, b). a \ b} (\(a, b). {a <.. b}) (\(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 \ A) :: 'a\real) has_integral x) UNIV = ((indicator s :: _\real) has_integral x) A" -proof - - have "(\x. if x \ A then indicator s x else 0) = (indicator (s \ A) :: _\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 \ b" + assumes mono_F: "\x y. x \ y \ F x \ F y" + assumes right_cont_F : "\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 \ b`]) + show "semiring_of_sets UNIV {{a<..b} |a b :: real. a \ b}" + proof (unfold_locales, safe) + fix a b c d :: real assume *: "a \ b" "c \ d" + then show "\C\{{a<..b} |a b. a \ b}. finite C \ disjoint C \ {a<..b} - {c<..d} = \C" + proof cases + let ?C = "{{a<..b}}" + assume "b < c \ d \ a \ d \ c" + with * have "?C \ {{a<..b} |a b. a \ b} \ finite ?C \ disjoint ?C \ {a<..b} - {c<..d} = \?C" + by (auto simp add: disjoint_def) + thus ?thesis .. + next + let ?C = "{{a<..c}, {d<..b}}" + assume "\ (b < c \ d \ a \ d \ c)" + with * have "?C \ {{a<..b} |a b. a \ b} \ finite ?C \ disjoint ?C \ {a<..b} - {c<..d} = \?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 \ real" and a b :: real + assume l_r[simp]: "\n. l n \ r n" and "a \ b" and disj: "disjoint_family (\n. {l n<..r n})" + assume lr_eq_ab: "(\i. {l i<..r i}) = {a<..b}" + + have [intro, simp]: "\a b. a \ b \ 0 \ 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 \ b` + moreover have "\i. i \ S \ {l i <.. r i} \ {a <.. b}" + unfolding lr_eq_ab[symmetric] by auto + ultimately have "(\i\S. F (r i) - F (l i)) \ F b - F a" + proof (induction S arbitrary: a rule: finite_psubset_induct) + case (psubset S) + show ?case + proof cases + assume "\i\S. l i < r i" + with `finite S` have "Min (l ` {i\S. l i < r i}) \ l ` {i\S. l i < r i}" + by (intro Min_in) auto + then obtain m where m: "m \ S" "l m < r m" "l m = Min (l ` {i\S. l i < r i})" + by fastforce -lemma - fixes s a :: "'a::ordered_euclidean_space set" - shows integral_indicator_UNIV: - "integral UNIV (indicator (s \ A) :: 'a\real) = integral A (indicator s :: _\real)" - and integrable_indicator_UNIV: - "(indicator (s \ A) :: 'a\real) integrable_on UNIV \ (indicator s :: 'a\real) integrable_on A" - unfolding integral_def integrable_on_def has_integral_indicator_UNIV by auto + have "(\i\S. F (r i) - F (l i)) = (F (r m) - F (l m)) + (\i\S - {m}. F (r i) - F (l i))" + using m psubset by (intro setsum.remove) auto + also have "(\i\S - {m}. F (r i) - F (l i)) \ F b - F (r m)" + proof (intro psubset.IH) + show "S - {m} \ S" + using `m\S` by auto + show "r m \ b" + using psubset.prems(2)[OF `m\S`] `l m < r m` by auto + next + fix i assume "i \ S - {m}" + then have i: "i \ S" "i \ m" by auto + { assume i': "l i < r i" "l i < r m" + moreover with `finite S` i m have "l m \ l i" + by auto + ultimately have "{l i <.. r i} \ {l m <.. r m} \ {}" + by auto + then have False + using disjoint_family_onD[OF disj, of i m] i by auto } + then have "l i \ r i \ r m \ l i" + unfolding not_less[symmetric] using l_r[of i] by auto + then show "{l i <.. r i} \ {r m <.. b}" + using psubset.prems(2)[OF `i\S`] by auto + qed + also have "F (r m) - F (l m) \ F (r m) - F a" + using psubset.prems(2)[OF `m \ 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 \ 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 \ real" + assume "finite S" "\i. i\S \ l i < r i" "{u..v} \ (\i\S. {l i<..< r i})" + then have "F v - F u \ (\i\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 \ {}" + then obtain j where "j \ S" + by auto -subsection {* Standard Cubes *} - -definition cube :: "nat \ 'a::ordered_euclidean_space set" where - "cube n \ {\i\Basis. - n *\<^sub>R i .. \i\Basis. n *\<^sub>R i}" + let ?R = "r j < u \ l j > v \ (\i\S-{j}. l i \ l j \ r j \ r i)" + show ?case + proof cases + assume "?R" + with `j \ S` psubset.prems have "{u..v} \ (\i\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 \ S` have "F v - F u \ (\i\S - {j}. F (r i) - F (l i))" + by (intro psubset) auto + also have "\ \ (\i\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 "\ ?R" + then have j: "u \ r j" "l j \ v" "\i. i \ S - {j} \ r i < r j \ l i > l j" + by (auto simp: not_less) + let ?S1 = "{i \ S. l i < l j}" + let ?S2 = "{i \ S. r i > r j}" -lemma borel_cube[intro]: "cube n \ sets borel" - unfolding cube_def by auto + have "(\i\S. F (r i) - F (l i)) \ (\i\?S1 \ ?S2 \ {j}. F (r i) - F (l i))" + using `j \ S` `finite S` psubset.prems j + by (intro setsum_mono2) (auto intro: less_imp_le) + also have "(\i\?S1 \ ?S2 \ {j}. F (r i) - F (l i)) = + (\i\?S1. F (r i) - F (l i)) + (\i\?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 "(\i\?S1. F (r i) - F (l i)) \ F (l j) - F u" + using `j \ 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 "(\i\?S2. F (r i) - F (l i)) \ F v - F (r j)" + using `j \ 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 \ N \ cube n \ cube N" - by (fastforce simp: eucl_le[where 'a='a] cube_def setsum_negf) + { fix epsilon :: real assume egt0: "epsilon > 0" + have "\i. \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 "\d. d > 0 \ 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: "\i. delta i > 0" and + deltai_prop: "\i. F (r i + delta i) < F (r i) + epsilon / 2^(i+2)" + by metis + have "\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' \ "{i. l i < r i}" + obtain S :: "nat set" where + "S \ S'" and finS: "finite S" and + Sprop: "{a'..b} \ (\i \ S. {l i<..i \ S'. open ({l i<.. {a <.. b}" + by auto + also have "{a <.. b} = (\i\S'. {l i<..r i})" + unfolding lr_eq_ab[symmetric] by (fastforce simp add: S'_def intro: less_le_trans) + also have "\ \ (\i \ S'. {l i<.. (\i \ S'. {l i<..i. i \ S \ l i < r i" by auto + from finS have "\n. \i \ S. i \ n" + by (subst finite_nat_set_iff_bounded_le [symmetric]) + then obtain n where Sbound [rule_format]: "\i \ S. i \ n" .. + have "F b - F a' \ (\i\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 "... \ (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 "... \ ?t + (epsilon / 4) * (\ 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 "... \ ?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' \ (\i\S. F (r i) - F (l i)) + epsilon / 2" + by simp -lemma cube_subset_iff: "cube n \ cube N \ n \ 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 "... \ (F b - F a') + epsilon / 2" + using a_prop by (intro add_left_mono) simp + also have "... \ (\i\S. F (r i) - F (l i)) + epsilon / 2 + epsilon / 2" + apply (intro add_right_mono) + apply (rule aux2) + done + also have "... = (\i\S. F (r i) - F (l i)) + epsilon" + by auto + also have "... \ (\i\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) \ (\i\n. ereal (F (r i) - F (l i))) + epsilon" + by simp + then have "ereal (F b - F a) \ (\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) \ (\i. ereal (F (r i) - F (l i)))" + by (auto intro: ereal_le_epsilon2) + moreover + have "(\i. ereal (F (r i) - F (l i))) \ ereal (F b - F a)" + by (auto simp add: claim1 intro!: suminf_bound) + ultimately show "(\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) \ 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 \ ball 0 (real n)" and i: "i \ Basis" - thus "- real n \ x \ i" "real n \ x \ i" - using Basis_le_norm[OF i, of x] by(auto simp: dist_norm) -qed +lemma measure_interval_measure_Ioc: + assumes "a \ b" + assumes mono_F: "\x y. x \ y \ F x \ F y" + assumes right_cont_F : "\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: + "(\x y. x \ y \ F x \ F y) \ (\a. continuous (at_right a) F) \ + emeasure (interval_measure F) {a <.. b} = (if a \ 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 \ 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 \ b" + assumes mono_F: "\x y. x \ y \ F x \ 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 \ 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 \ cube n" + let ?F = "interval_measure F" + show "((\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 "\n. X n < a" "incseq X" "X ----> a" + with `a \ b` have "(\n. emeasure ?F {X n<..b}) ----> emeasure ?F (\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 "(\n. {X n <..b}) = {a..b}" + using `\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 "(\n. emeasure ?F {X n<..b}) = (\n. F b - F (X n))" + using `\n. X n < a` `a \ b` by (subst *) (auto intro: less_imp_le less_le_trans) + finally show "(\n. F b - F (X n)) ----> emeasure ?F {a..b}" . + qed + show "((\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: "\x y. x \ y \ F x \ F y" + assumes right_cont_F : "\a. continuous (at_right a) F" + shows "sigma_finite_measure (interval_measure F)" + apply unfold_locales + apply (intro exI[of _ "(\(a, b). {a <.. b}) ` (\ \ \)"]) + 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 (\\<^sub>M b\Basis. interval_measure (\x. x)) borel (\f. \b\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 (\x. x)" + by (rule sigma_finite_interval_measure) auto +interpretation finite_product_sigma_finite "\_. interval_measure (\x. x)" Basis + proof qed simp + +lemma lborel_eq_real: "lborel = interval_measure (\x. x)" + unfolding lborel_def Basis_real_def + using distr_id[of "interval_measure (\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 (\\<^sub>M b\Basis. lborel) borel (\f. \b\Basis. f b *\<^sub>R b)" + by (subst lborel_def) (simp add: lborel_eq_real) + +lemma nn_integral_lborel_setprod: + assumes [measurable]: "\b. b \ Basis \ f b \ borel_measurable borel" + assumes nn[simp]: "\b x. b \ Basis \ 0 \ f b x" + shows "(\\<^sup>+x. (\b\Basis. f b (x \ b)) \lborel) = (\b\Basis. (\\<^sup>+x. f b x \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 \ 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 \ 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} \ cube n)) (cube n)" - (is "(?I has_integral content ?R) (cube n)") -proof - - have [simp]: "(\x. if x \ 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) \ (indicator ?R has_integral content ?R) UNIV" - unfolding has_integral_restrict_univ[where s="cube n", symmetric] by simp - also have "\ \ ((\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 "((\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 "((\f. f 1) -` {l..u} \ space (Pi\<^sub>M {1} (\b. interval_measure (\x. x)))) = {1::real} \\<^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. \n. (indicator A :: 'a \ real) integrable_on cube n} - (\A. SUP n. ereal (integral (cube n) (indicator A)))" - -lemma space_lebesgue[simp]: "space lebesgue = UNIV" - unfolding lebesgue_def by simp - -lemma lebesgueI: "(\n. (indicator A :: _ \ real) integrable_on cube n) \ A \ sets lebesgue" - unfolding lebesgue_def by simp - -lemma sigma_algebra_lebesgue: - defines "leb \ {A. \n. (indicator A :: 'a::ordered_euclidean_space \ real) integrable_on cube n}" - shows "sigma_algebra UNIV leb" -proof (safe intro!: sigma_algebra_iff2[THEN iffD2]) - fix A assume A: "A \ leb" - moreover have "indicator (UNIV - A) = (\x. 1 - indicator A x :: real)" - by (auto simp: fun_eq_iff indicator_def) - ultimately show "UNIV - A \ leb" - using A by (auto intro!: integrable_sub simp: cube_def leb_def) -next - fix n show "{} \ leb" - by (auto simp: cube_def indicator_def[abs_def] leb_def) -next - fix A :: "nat \ _" assume A: "range A \ leb" - have "\n. (indicator (\i. A i) :: _ \ real) integrable_on cube n" (is "\n. ?g integrable_on _") - proof (intro dominated_convergence[where g="?g"] ballI allI) - fix k n show "(indicator (\i real) integrable_on cube n" - proof (induct k) - case (Suc k) - have *: "(\ i i A k" - unfolding lessThan_Suc UN_insert by auto - have *: "(\x. max (indicator (\ i ix. 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 "(\i. A i) \ leb" by (auto simp: leb_def) -qed simp - -lemma sets_lebesgue: "sets lebesgue = {A. \n. (indicator A :: _ \ real) integrable_on cube n}" - unfolding lebesgue_def sigma_algebra.sets_measure_of_eq[OF sigma_algebra_lebesgue] .. - -lemma lebesgueD: "A \ sets lebesgue \ (indicator A :: _ \ real) integrable_on cube n" - unfolding sets_lebesgue by simp +lemma emeasure_lborel_Icc_eq: "emeasure lborel {l .. u} = ereal (if l \ u then u - l else 0)" + by simp -lemma emeasure_lebesgue: - assumes "A \ sets lebesgue" - shows "emeasure lebesgue A = (SUP n. ereal (integral (cube n) (indicator A)))" - (is "_ = ?\ A") -proof (rule emeasure_measure_of[OF lebesgue_def]) - have *: "indicator {} = (\x. 0 :: real)" by (simp add: fun_eq_iff) - show "positive (sets lebesgue) ?\" - proof (unfold positive_def, intro conjI ballI) - show "?\ {} = 0" by (simp add: integral_0 *) - fix A :: "'a set" assume "A \ sets lebesgue" then show "0 \ ?\ A" - by (auto intro!: SUP_upper2 Integration.integral_nonneg simp: sets_lebesgue) - qed -next - show "countably_additive (sets lebesgue) ?\" - proof (intro countably_additive_def[THEN iffD2] allI impI) - fix A :: "nat \ 'a set" assume rA: "range A \ sets lebesgue" "disjoint_family A" - then have A[simp, intro]: "\i n. (indicator (A i) :: _ \ real) integrable_on cube n" - by (auto dest: lebesgueD) - let ?m = "\n i. integral (cube n) (indicator (A i) :: _\real)" - let ?M = "\n I. integral (cube n) (indicator (\i\I. A i) :: _\real)" - have nn[simp, intro]: "\i n. 0 \ ?m n i" by (auto intro!: Integration.integral_nonneg) - assume "(\i. A i) \ sets lebesgue" - then have UN_A[simp, intro]: "\i n. (indicator (\i. A i) :: _ \ real) integrable_on cube n" - by (auto simp: sets_lebesgue) - show "(\n. ?\ (A n)) = ?\ (\i. A i)" - proof (subst suminf_SUP_eq, safe intro!: incseq_SucI) - fix i n show "ereal (?m n i) \ 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 \ ereal (?m n i)" - using rA unfolding lebesgue_def - by (auto intro!: SUP_upper2 integral_nonneg) - next - show "(SUP n. \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 "\m. (UNION {.. sets lebesgue" using rA by auto - from lebesgueD[OF this] - have "(\m. ?M n {..< m}) ----> ?M n UNIV" - (is "(\m. integral _ (?A m)) ----> ?I") - by (intro dominated_convergence(2)[where f="?A" and h="\x. 1::real"]) - (auto intro: LIMSEQ_indicator_UN simp: cube_def) - moreover - { fix m have *: "(\xi sets lebesgue" using rA by auto - then have "(indicator (\ireal) integrable_on (cube n)" - by (auto dest!: lebesgueD) - moreover - have "(\i A m = {}" - using rA(2)[unfolded disjoint_family_on_def, THEN bspec, of m] - by auto - then have "\x. indicator (\iim. \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 \ sets borel" shows "s \ sets lebesgue" +lemma emeasure_lborel_cbox[simp]: + assumes [simp]: "\b. b \ Basis \ l \ b \ u \ b" + shows "emeasure lborel (cbox l u) = (\b\Basis. (u - l) \ b)" proof - - have "s \ sigma_sets (space lebesgue) (range (\(a, b). {a .. (b :: 'a\ordered_euclidean_space)}))" - using assms by (simp add: borel_eq_atLeastAtMost) - also have "\ \ sets lebesgue" - proof (safe intro!: sets.sigma_sets_subset lebesgueI) - fix n :: nat and a b :: 'a - show "(indicator {a..b} :: 'a\real) integrable_on cube n" - unfolding integrable_on_def using has_integral_interval_cube[of a b] by auto - qed + have "(\x. \b\Basis. indicator {l\b .. u\b} (x \ 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) = (\\<^sup>+x. (\b\Basis. indicator {l\b .. u\b} (x \ b)) \lborel)" + by simp + also have "\ = (\b\Basis. (u - l) \ b)" + by (subst nn_integral_lborel_setprod) (simp_all add: setprod_ereal inner_diff_left) finally show ?thesis . qed -lemma borel_measurable_lebesgueI: - "f \ borel_measurable borel \ f \ borel_measurable lebesgue" - unfolding measurable_def by simp +lemma AE_lborel_singleton: "AE x in lborel::'a::euclidean_space measure. x \ 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 \ 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 \ u" + shows "emeasure lborel {l <..< u} = ereal (u - l)" proof - - have "\n. integral (cube n) (indicator S :: 'a\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 \ sets lebesgue" and "0 \ m" - shows "emeasure lebesgue A = ereal m \ (\n. integral (cube n) (indicator A :: _ \ real)) ----> m" -proof (subst emeasure_lebesgue[OF A], intro SUP_eq_LIMSEQ) - show "mono (\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 \ sets lebesgue" "emeasure lebesgue s = ereal m" - shows "(indicator s has_integral m) UNIV" +lemma emeasure_lborel_Ioc[simp]: + assumes [simp]: "l \ u" + shows "emeasure lborel {l <.. u} = ereal (u - l)" proof - - let ?I = "indicator :: 'a set \ 'a \ real" - have "0 \ m" - using emeasure_nonneg[of lebesgue s] `emeasure lebesgue s = ereal m` by simp - have **: "(?I s) integrable_on UNIV \ (\k. integral UNIV (?I (s \ cube k))) ----> integral UNIV (?I s)" - proof (intro monotone_convergence_increasing allI ballI) - have LIMSEQ: "(\n. integral (cube n) (?I s)) ----> m" - using assms(2) unfolding lmeasure_iff_LIMSEQ[OF assms(1) `0 \ m`] . - { fix n have "integral (cube n) (?I s) \ 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 \ integral (cube n) (?I s)" - using assms by (auto dest!: lebesgueD intro!: Integration.integral_nonneg) } - ultimately - show "bounded {integral UNIV (?I (s \ 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 \ cube k) integrable_on UNIV" - unfolding integrable_indicator_UNIV using assms by (auto dest!: lebesgueD) - fix x show "?I (s \ cube k) x \ ?I (s \ 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 \ cube k" . - { fix n have "?I (s \ cube (n + k)) x = ?I s x" - using k cube_subset[of k "n + k"] by (auto simp: indicator_def) } - note * = this - show "(\k. ?I (s \ 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 \ 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 \ sets lebesgue" and "emeasure lebesgue s \ \" - shows "(indicator s :: _ \ real) integrable_on UNIV" -proof (cases "emeasure lebesgue s") - case (real m) - with lmeasure_finite_has_integral[OF `s \ 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 :: _\real) has_integral m) UNIV" - shows "s \ sets lebesgue" -proof (intro lebesgueI) - let ?I = "indicator :: 'a set \ 'a \ 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 \ 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 :: _\real) has_integral m) UNIV" - shows "emeasure lebesgue s = ereal m" -proof (intro lmeasure_iff_LIMSEQ[THEN iffD2]) - let ?I = "indicator :: 'a set \ 'a \ real" - show "s \ sets lebesgue" using has_integral_lebesgue[OF assms] . - show "0 \ m" using assms by (rule has_integral_nonneg) auto - have "(\n. integral UNIV (?I (s \ 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 \ cube n) integrable_on UNIV" - unfolding integrable_indicator_UNIV using `s \ sets lebesgue` by (auto dest: lebesgueD) - fix x show "norm (?I (s \ cube n) x) \ ?I s x" by (auto simp: indicator_def) - next - fix x :: 'a - from mem_big_cube obtain k where k: "x \ cube k" . - { fix n have "?I (s \ cube (n + k)) x = ?I s x" - using k cube_subset[of k "n + k"] by (auto simp: indicator_def) } - note * = this - show "(\k. ?I (s \ cube k) x) ----> ?I s x" - by (rule LIMSEQ_offset[where k=k]) (auto simp: *) - qed - then show "(\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 \ (A \ sets lebesgue \ 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 \ sets lebesgue \ emeasure lebesgue A = ereal m" - by (auto intro: has_integral_nonneg) -next - assume "A \ sets lebesgue \ 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::_\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]: "\b. b \ Basis \ l \ b \ u \ b" + shows "emeasure lborel (box l u) = (\b\Basis. (u - l) \ b)" +proof - + have "(\x. \b\Basis. indicator {l\b <..< u\b} (x \ 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) = (\\<^sup>+x. (\b\Basis. indicator {l\b <..< u\b} (x \ b)) \lborel)" + by simp + also have "\ = (\b\Basis. (u - l) \ 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 \ ereal" - assumes f:"simple_function lebesgue f" - shows "f = (\x. (\y \ f ` UNIV. y * indicator (f -` {y}) x))" - by (rule, subst simple_function_indicator_representation[OF f]) auto - -lemma integral_eq_lmeasure: - "(indicator s::_\real) integrable_on UNIV \ integral UNIV (indicator s) = real (emeasure lebesgue s)" - by (subst lmeasure_eq_integral) (auto intro!: integral_nonneg) - -lemma lmeasure_finite: assumes "(indicator s::_\real) integrable_on UNIV" shows "emeasure lebesgue s \ \" - using lmeasure_eq_integral[OF assms] by auto - -lemma negligible_iff_lebesgue_null_sets: - "negligible A \ A \ null_sets lebesgue" -proof - assume "negligible A" - from this[THEN lebesgueI_negligible] this[THEN lmeasure_eq_0] - show "A \ null_sets lebesgue" by auto -next - assume A: "A \ 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 :: _\real) integrable_on cbox a b" - by (intro integrable_on_subcbox has_integral_integrable) (auto intro: *) - then have "integral (cbox a b) (indicator A) \ (integral UNIV (indicator A) :: real)" - using * by (auto intro!: integral_subset_le) - moreover have "(0::real) \ 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 \b\Basis. l \ b \ u \ b then \b\Basis. (u - l) \ 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) = \" -proof (simp add: emeasure_lebesgue, intro SUP_PInfty bexI) - fix n :: nat - have "indicator UNIV = (\x::'a. 1 :: real)" by auto - moreover - { have "real n \ (2 * real n) ^ DIM('a)" - proof (cases n) - case 0 then show ?thesis by auto - next - case (Suc n') - have "real n \ (2 * real n)^1" by auto - also have "(2 * real n)^1 \ (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) \ ereal (integral (cube n) (indicator UNIV::'a\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 \ B \ B \ null_sets lebesgue \ A \ 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 \ {a..b})::_\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 \ {a..b})::_\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 \ a" - by (rule AE_I[where N="{a}"]) auto - -declare content_real[simp] +lemma emeasure_lborel_box_eq: + "emeasure lborel (box l u) = (if \b\Basis. l \ b \ u \ b then \b\Basis. (u - l) \ 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 \ 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 \ 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 \ 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]: "\b. b \ Basis \ l \ b \ u \ b" + shows measure_lborel_box[simp]: "measure lborel (box l u) = (\b\Basis. (u - l) \ b)" + and measure_lborel_cbox[simp]: "measure lborel (cbox l u) = (\b\Basis. (u - l) \ b)" + by (simp_all add: measure_def) -lemma - fixes a b :: real - shows lmeasure_real_greaterThanLessThan[simp]: - "emeasure lebesgue {a <..< b} = ereal (if a \ 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 "\A::'a set set. countable A \ A \ sets lborel \ \A = space lborel \ (\a\A. emeasure lborel a \ \)" + by (intro exI[of _ "range (\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 \ sets borel \ 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) = \" + 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 \ sets borel \ 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 _ "\n. cube n"]) - show "range cube \ sets lborel" by (auto intro: borel_closed) - { fix x :: 'a have "\n. x\cube n" using mem_big_cube by auto } - then show "(\i. cube i) = (space lborel :: 'a set)" using mem_big_cube by auto - show "\i. emeasure lborel (cube i) \ \" by (simp add: cube_def) -qed - -interpretation lebesgue: sigma_finite_measure lebesgue -proof - from lborel.sigma_finite guess A :: "nat \ 'a set" .. - then show "\A::nat \ 'a set. range A \ sets lebesgue \ (\i. A i) = space lebesgue \ (\i. emeasure lebesgue (A i) \ \)" - 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 \ (\i. {from_nat_into A i})" using from_nat_into_surj assms by force + moreover have "emeasure lborel (\i. {from_nat_into A i}) = 0" + by (rule emeasure_UN_eq_0) auto + ultimately have "emeasure lborel A \ 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 (\(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: "\a b. emeasure M {a .. b} = content {a .. b}" + fixes M :: "'a::euclidean_space measure" + assumes emeasure_eq: "\l u. (\b. b \ Basis \ l \ b \ u \ b) \ emeasure M (box l u) = (\b\Basis. (u - l) \ b)" assumes sets_eq: "sets M = sets borel" shows "lborel = M" -proof (rule measure_eqI_generator_eq[OF Int_stable_atLeastAtMost]) - let ?P = "\\<^sub>M i\{.. 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 \ ?E" unfolding cube_def [abs_def] by auto - { fix x :: 'a have "\n. x \ cube n" using mem_big_cube[of x] by fastforce } - then show "(\i. cube i :: 'a set) = UNIV" by auto + let ?A = "\n::nat. box (- (real n *\<^sub>R One)) (real n *\<^sub>R One) :: 'a set" + show "range ?A \ ?E" "(\i. ?A i) = UNIV" + unfolding UN_box_eq_UNIV by auto - { fix i show "emeasure lborel (cube i) \ \" unfolding cube_def by auto } + { fix i show "emeasure lborel (?A i) \ \" by auto } { fix X assume "X \ ?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 \ 0" - shows "lborel = density (distr lborel borel (\x. t + c * x)) (\_. \c\)" (is "_ = ?D") +lemma lborel_affine: + fixes t :: "'a::euclidean_space" assumes "c \ 0" + shows "lborel = density (distr lborel borel (\x. t + c *\<^sub>R x)) (\_. \c\^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: "\b. b \ ?B \ l \ b \ u \ b" + show "emeasure ?D (box l u) = (\b\?B. (u - l) \ b)" proof cases assume "0 < c" - then have "(\x. t + c * x) -` {a..b} = {(a - t) / c .. (b - t) / c}" - by (auto simp: field_simps) + then have "(\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 \ 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 "\ 0 < c" with `c \ 0` have "c < 0" by auto - then have *: "(\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 \ 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) = (\x. t + c *\<^sub>R x) -` box l u" + by (auto simp: field_simps box_def inner_simps) + then have "\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 * (\x\?B. l \ x - u \ x) = + (-1 * c) ^ card ?B * (\x\?B. -1 * (u \ x - l \ x))" + by simp + also have "\ = (-1 * -1)^card ?B * c ^ card ?B * (\x\?B. u \ x - l \ x)" + unfolding setprod.distrib power_mult_distrib by (simp add: setprod_constant) + finally have "(- c) ^ card ?B * (\x\?B. l \ x - u \ x) = c ^ card ?B * (\b\?B. u \ b - l \ 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 \ 0 \ lborel = density (distr lborel borel (\x. t + c * x)) (\_. \c\)" + using lborel_affine[of c t] by simp + +lemma AE_borel_affine: + fixes P :: "real \ bool" + shows "c \ 0 \ Measurable.pred borel P \ AE x in lborel. P x \ 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 \ borel_measurable borel" and c: "c \ 0" shows "(\\<^sup>+x. f x \lborel) = \c\ * (\\<^sup>+x. f (t + c * x) \lborel)" @@ -576,7 +611,7 @@ (simp add: nn_integral_density nn_integral_distr nn_integral_cmult) lemma lborel_integrable_real_affine: - fixes f :: "real \ _ :: {banach, second_countable_topology}" + fixes f :: "real \ 'a :: {banach, second_countable_topology}" assumes f: "integrable lborel f" shows "c \ 0 \ integrable lborel (\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 "\ 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 \ 0 \ y = x /\<^sub>R r \ 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 "(\x. c * f x) integrable_on s \ c = 0 \ f integrable_on s" - using integrable_cmul[of "\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 \ 0 \ @@ -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\space borel. P x} \ sets borel \ {x\space lborel. P x} \ sets lborel" by simp +lemma lborelD[measurable (raw)]: "A \ sets borel \ A \ sets lborel" by simp + +subsection {* Equivalence Lebesgue integral on @{const lborel} and HK-integral *} -lemma has_integral_scaleR_left: - "(f has_integral y) s \ ((\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 \ sets borel" and finite: "emeasure lborel A < \" + shows "((\x. 1) has_integral measure lborel A) A" +proof - + { fix l u :: 'a + have "((\x. 1) has_integral measure lborel (box l u)) (box l u)" + proof cases + assume "\b\Basis. l \ b \ u \ 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="\_. 1"]) + using has_integral_const[of "1::real" l u] + apply (simp_all add: inner_diff_left[symmetric] content_cbox_cases) + done + next + assume "\ (\b\Basis. l \ b \ u \ 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 \ ((\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 = "\A. measure lborel (A \ box a b)" + have "Int_stable (range (\(a, b). box a b))" + by (auto simp: Int_stable_def box_Int_box) + moreover have "(range (\(a, b). box a b)) \ Pow UNIV" + by auto + moreover have "A \ sigma_sets UNIV (range (\(a, b). box a b))" + using A unfolding borel_eq_box by simp + ultimately have "((\x. 1) has_integral ?M A) (A \ 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 \ 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 \ 'n::ordered_euclidean_space \ real" - assumes "\k. (f k has_integral y k) s" "h integrable_on s" - "\k. \x\s. norm (f k x) \ h x" "\x\s. (\k. f k x) ----> g x" - and x: "y ----> x" - shows "(g has_integral x) s" -proof - - have int_f: "\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 "(\i. integral s (f i)) ----> x" - using integral_unique[OF assms(1)] x by simp - show "(\i. integral s (f i)) ----> integral s g" - by (intro dominated_convergence[OF int_f assms(2)]) fact+ + have "((\x. 1) has_integral ?M (box a b)) (box a b)" + by (simp add: has_integral_box) + moreover have "((\x. if x \ A \ box a b then 1 else 0) has_integral ?M A) (box a b)" + by (subst has_integral_restrict) (auto intro: compl) + ultimately have "((\x. 1 - (if x \ A \ 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 "((\x. (if x \ (UNIV - A) \ 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 "((\x. 1) has_integral ?M (box a b) - ?M A) ((UNIV - A) \ 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]: "\i. F i \ sets borel" + by (simp add: borel_eq_box subset_eq) + have "((\x. if x \ UNION UNIV F \ box a b then 1 else 0) has_integral ?M (\i. F i)) (box a b)" + proof (rule has_integral_monotone_convergence_increasing) + let ?f = "\k x. \i F i \ box a b then 1 else 0 :: real" + show "\k. (?f k has_integral (\ik x. ?f k x \ ?f (Suc k) x" + by (intro setsum_mono2) auto + from union(1) have *: "\x i j. x \ F i \ x \ F j \ j = i" + by (auto simp add: disjoint_family_on_def) + show "\x. (\k. ?f k x) ----> (if x \ UNION UNIV F \ 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 ((\x. F x) \ box a b) \ emeasure lborel (box a b)" + by (intro emeasure_mono) auto + + with union(1) show "(\k. \i ?M (\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 = "\n::nat. box (- real n *\<^sub>R One) (real n *\<^sub>R One) :: 'a set" + let ?f = "\n::nat. \x. if x \ A \ ?B n then 1 else 0 :: real" + let ?M = "\n. measure lborel (A \ ?B n)" + + show "\n::nat. (?f n has_integral ?M n) A" + using * by (subst has_integral_restrict) simp_all + show "\k x. ?f k x \ ?f (Suc k) x" + by (auto simp: box_def) + { fix x assume "x \ A" + moreover have "(\k. indicator (A \ ?B k) x :: real) ----> indicator (\k::nat. A \ ?B k) x" + by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def box_def) + ultimately show "(\k. if x \ A \ ?B k then 1 else 0::real) ----> 1" + by (simp add: indicator_def UN_box_eq_UNIV) } + + have "(\n. emeasure lborel (A \ ?B n)) ----> emeasure lborel (\n::nat. A \ ?B n)" + by (intro Lim_emeasure_incseq) (auto simp: incseq_def box_def) + also have "(\n. emeasure lborel (A \ ?B n)) = (\n. measure lborel (A \ ?B n))" + proof (intro ext emeasure_eq_ereal_measure) + fix n have "emeasure lborel (A \ ?B n) \ emeasure lborel (?B n)" + by (intro emeasure_mono) auto + then show "emeasure lborel (A \ ?B n) \ \" + by auto + qed + finally show "(\n. measure lborel (A \ ?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 \ real" - assumes f: "f \ borel_measurable lebesgue" "\x. 0 \ f x" "(\\<^sup>+x. f x \lebesgue) = ereal r" + fixes f::"'a::euclidean_space \ real" + assumes f: "f \ borel_measurable borel" "\x. 0 \ f x" "(\\<^sup>+x. f x \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 "((\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 * (\\<^sup>+ x. g x \lebesgue) = ereal r" + then have "ereal c * (\\<^sup>+ x. g x \lborel) = ereal r" by (subst nn_integral_cmult[symmetric]) auto - then obtain r' where "(c = 0 \ r = 0) \ ((\\<^sup>+ x. ereal (g x) \lebesgue) = ereal r' \ r = c * r')" - by (cases "\\<^sup>+ x. ereal (g x) \lebesgue") (auto split: split_if_asm) + then obtain r' where "(c = 0 \ r = 0) \ ((\\<^sup>+ x. ereal (g x) \lborel) = ereal r' \ r = c * r')" + by (cases "\\<^sup>+ x. ereal (g x) \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 "(\\<^sup>+ x. h x + g x \lebesgue) = (\\<^sup>+ x. h x \lebesgue) + (\\<^sup>+ x. g x \lebesgue)" + then have "(\\<^sup>+ x. h x + g x \lborel) = (\\<^sup>+ x. h x \lborel) + (\\<^sup>+ x. g x \lborel)" unfolding plus_ereal.simps[symmetric] by (subst nn_integral_add) auto - with add obtain a b where "(\\<^sup>+ x. h x \lebesgue) = ereal a" "(\\<^sup>+ x. g x \lebesgue) = ereal b" "r = a + b" - by (cases "\\<^sup>+ x. h x \lebesgue" "\\<^sup>+ x. g x \lebesgue" rule: ereal2_cases) auto + with add obtain a b where "(\\<^sup>+ x. h x \lborel) = ereal a" "(\\<^sup>+ x. g x \lborel) = ereal b" "r = a + b" + by (cases "\\<^sup>+ x. h x \lborel" "\\<^sup>+ x. g x \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 "(\\<^sup>+x. ereal (U i x) \lebesgue) \ (\\<^sup>+x. ereal (f x) \lebesgue)" + have "(\\<^sup>+x. ereal (U i x) \lborel) \ (\\<^sup>+x. ereal (f x) \lborel)" using U_le_f by (intro nn_integral_mono) simp - then obtain p where "(\\<^sup>+x. U i x \lebesgue) = ereal p" "p \ r" - using seq(6) by (cases "\\<^sup>+x. U i x \lebesgue") auto + then obtain p where "(\\<^sup>+x. U i x \lborel) = ereal p" "p \ r" + using seq(6) by (cases "\\<^sup>+x. U i x \lborel") auto moreover then have "0 \ p" by (metis ereal_less_eq(5) nn_integral_nonneg) moreover note seq - ultimately have "\p. (\\<^sup>+x. U i x \lebesgue) = ereal p \ 0 \ p \ p \ r \ (U i has_integral p) UNIV" + ultimately have "\p. (\\<^sup>+x. U i x \lborel) = ereal p \ 0 \ p \ p \ r \ (U i has_integral p) UNIV" by auto } - then obtain p where p: "\i. (\\<^sup>+x. ereal (U i x) \lebesgue) = ereal (p i)" + then obtain p where p: "\i. (\\<^sup>+x. ereal (U i x) \lborel) = ereal (p i)" and bnd: "\i. p i \ r" "\i. 0 \ p i" and U_int: "\i.(U i has_integral (p i)) UNIV" by metis @@ -717,7 +845,7 @@ show "\x\UNIV. (\k. U k x) ----> f x" using seq by auto qed - moreover have "(\i. (\\<^sup>+x. U i x \lebesgue)) ----> (\\<^sup>+x. f x \lebesgue)" + moreover have "(\i. (\\<^sup>+x. U i x \lborel)) ----> (\\<^sup>+x. f x \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 \ real" - assumes f: "integrable lebesgue f" "\x. 0 \ f x" - shows "(f has_integral integral\<^sup>L lebesgue f) UNIV" -proof (rule nn_integral_has_integral) - show "(\\<^sup>+ x. ereal (f x) \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 \ real" + assumes f: "f \ borel_measurable borel" "\x. 0 \ f x" "(\\<^sup>+x. f x \lborel) < \" + shows "(\\<^sup>+x. f x \lborel) = integral UNIV f" +proof - + from f(3) obtain r where r: "(\\<^sup>+x. f x \lborel) = ereal r" + by (cases "\\<^sup>+x. f x \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 \ real" + assumes f: "f \ borel_measurable borel" "\x. 0 \ f x" "(\\<^sup>+x. f x \lborel) < \" + shows "f integrable_on UNIV" +proof - + from f(3) obtain r where r: "(\\<^sup>+x. f x \lborel) = ereal r" + by (cases "\\<^sup>+x. f x \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 \ real" + assumes f_borel: "f \ borel_measurable borel" and nonneg: "\x. 0 \ f x" + assumes I: "(f has_integral I) UNIV" + shows "integral\<^sup>N lborel f = I" +proof - + from f_borel have "(\x. ereal (f x)) \ borel_measurable lborel" by auto + from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this + let ?B = "\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) \ 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 \] max_def intro: SUP_upper split: split_if_asm) } + note F_le_f = this + let ?F = "\i x. F i x * indicator (?B i) x" + have "(\\<^sup>+ x. ereal (f x) \lborel) = (SUP i. integral\<^sup>N lborel (\x. ?F i x))" + proof (subst nn_integral_monotone_convergence_SUP[symmetric]) + { fix x + obtain j where j: "x \ ?B j" + using UN_box_eq_UNIV by auto -lemma has_integral_lebesgue_integral_lebesgue: - fixes f::"'a::ordered_euclidean_space \ 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 "\ = (SUP i. ?F i x)" + proof (rule SUP_eq) + fix i show "\j\UNIV. F i x \ ?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 "(\\<^sup>+ x. ereal (f x) \lborel) = (\\<^sup>+ x. (SUP i. ?F i x) \lborel)" + by simp + qed (insert F, auto simp: incseq_def le_fun_def box_def split: split_indicator) + also have "\ \ ereal I" + proof (rule SUP_least) + fix i :: nat + have finite_F: "(\\<^sup>+ x. ereal (real (F i x) * indicator (?B i) x) \lborel) < \" + proof (rule nn_integral_bound_simple_function) + have "emeasure lborel {x \ space lborel. ereal (real (F i x) * indicator (?B i) x) \ 0} \ + emeasure lborel (?B i)" + by (intro emeasure_mono) (auto split: split_indicator) + then show "emeasure lborel {x \ space lborel. ereal (real (F i x) * indicator (?B i) x) \ 0} < \" + 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: "(\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 "(\\<^sup>+ x. F i x * indicator (?B i) x \lborel) = + (\\<^sup>+ x. ereal (real (F i x) * indicator (?B i) x) \lborel)" + using F(3,5) + by (intro nn_integral_cong) (auto simp: image_iff ereal_real eq_commute split: split_indicator) + also have "\ = ereal (integral UNIV (\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 "\ \ ereal I" + by (auto intro!: has_integral_le[OF integrable_integral[OF int_F] I] nonneg F_le_f + split: split_indicator ) + finally show "(\\<^sup>+ x. F i x * indicator (?B i) x \lborel) \ ereal I" . + qed + finally have "(\\<^sup>+ x. ereal (f x) \lborel) < \" + 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 \ sets borel" + shows "((\x. 1) has_integral r) A \ emeasure lborel A = ereal r" +proof cases + assume emeasure_A: "emeasure lborel A = \" + have "\ (\x. 1::real) integrable_on A" + proof + assume int: "(\x. 1::real) integrable_on A" + then have "(indicator A::'a \ real) integrable_on UNIV" + unfolding indicator_def[abs_def] integrable_restrict_univ . + then obtain r where "((indicator A::'a\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 \ \" + moreover then have "((\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 \ 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 "\i. (s i has_integral integral\<^sup>L lebesgue (s i)) UNIV" by fact + show "\i. (s i has_integral integral\<^sup>L lborel (s i)) UNIV" by fact show "(\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 "\k. \x\UNIV. norm (s k x) \ norm (2 * f x)" using lim by (auto simp add: abs_mult) show "\x\UNIV. (\k. s k x) ----> f x" using lim by auto - show "(\k. integral\<^sup>L lebesgue (s k)) ----> integral\<^sup>L lebesgue f" - using lim by (intro integral_dominated_convergence[where w="\x. 2 * norm (f x)"]) auto + show "(\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="\x. 2 * norm (f x)"]) auto qed qed -lemma lebesgue_nn_integral_eq_borel: - assumes f: "f \ borel_measurable borel" - shows "integral\<^sup>N lebesgue f = integral\<^sup>N lborel f" -proof - - from f have "integral\<^sup>N lebesgue (\x. max 0 (f x)) = integral\<^sup>N lborel (\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 \ 'b::euclidean_space" +begin -lemma lebesgue_integral_eq_borel: - fixes f :: "_ \ _::{banach, second_countable_topology}" - assumes "f \ borel_measurable borel" - shows "integrable lebesgue f \ integrable lborel f" (is ?P) - and "integral\<^sup>L lebesgue f = integral\<^sup>L lborel f" (is ?I) -proof - - have "sets lborel \ 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 \ 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: "\x. x \ space M \ 0 \ f x" "\x. x \ space M \ f x < \" - assumes f[measurable]: "simple_function M f" - assumes supp: "emeasure M {x\space M. f x \ 0} < \" - shows "nn_integral M f < \" -proof cases - assume "space M = {}" - then have "nn_integral M f = (\\<^sup>+x. 0 \M)" - by (intro nn_integral_cong) auto - then show ?thesis by simp -next - assume "space M \ {}" - with simple_functionD(1)[OF f] bnd have bnd: "0 \ Max (f`space M) \ Max (f`space M) < \" - by (subst Max_less_iff) (auto simp: Max_ge_iff) - - have "nn_integral M f \ (\\<^sup>+x. Max (f`space M) * indicator {x\space M. f x \ 0} x \M)" - proof (rule nn_integral_mono) - fix x assume "x \ space M" - with f show "f x \ Max (f ` space M) * indicator {x \ space M. f x \ 0} x" - by (auto split: split_indicator intro!: Max_ge simple_functionD) - qed - also have "\ < \" - using bnd supp by (subst nn_integral_cmult) auto + have "((\x. \b\Basis. (f x \ b) *\<^sub>R b) has_integral (\b\Basis. integral\<^sup>L lborel (\x. f x \ 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: "(\x. \b\Basis. (f x \ b) *\<^sub>R b) = f" + by (simp add: fun_eq_iff euclidean_representation) + also have "(\b\Basis. integral\<^sup>L lborel (\x. f x \ 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 \ real" - assumes f_borel: "f \ borel_measurable lebesgue" and nonneg: "\x. 0 \ 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 "(\x. ereal (f x)) \ borel_measurable lebesgue" by auto - from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this - - have "(\\<^sup>+ x. ereal (f x) \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 "\ \ ereal I" - proof (rule SUP_least) - fix i :: nat - - { fix z - from F(4)[of z] have "F i z \ 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) \ f z" - by (cases "F i z") simp_all } - note F_bound = this - - { fix x :: ereal assume x: "x \ 0" "x \ range (F i)" - with F(3,5)[of i] have [simp]: "real x \ 0" - by (metis image_iff order_eq_iff real_of_ereal_le_0) - let ?s = "(\n z. real x * indicator (F i -` {x} \ cube n) z) :: nat \ 'a \ real" - have "(\z::'a. real x * indicator (F i -` {x}) z) integrable_on UNIV" - proof (rule dominated_convergence(1)) - fix n :: nat - have "(\z. indicator (F i -` {x} \ 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 "\x\UNIV. norm (?s n x) \ f x" - using nonneg F(5) by (auto split: split_indicator) - next - show "\z\UNIV. (\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 (\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 "(\n. ?s n z) ----> real x * indicator (F i -` {x}) z" - by (rule Lim_eventually) - qed - qed - then have "(indicator (F i -` {x}) :: 'a \ real) integrable_on UNIV" - by (simp add: integrable_on_cmult_iff) } - note F_finite = lmeasure_finite[OF this] - - have F_eq: "\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: "\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 (\x. real (F i x))" - unfolding integrable_iff_bounded - proof - have "(\\<^sup>+x. F i x \lebesgue) < \" - proof (rule nn_integral_bound_simple_function) - fix x::'a assume "x \ space lebesgue" then show "0 \ F i x" "F i x < \" - using F by (auto simp: image_iff eq_commute) - next - have eq: "{x \ space lebesgue. F i x \ 0} = (\x\F i ` space lebesgue - {0}. F i -` {x} \ space lebesgue)" - by auto - show "emeasure lebesgue {x \ space lebesgue. F i x \ 0} < \" - 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 "(\\<^sup>+x. norm (real (F i x)) \lebesgue) < \" by simp - qed (insert F(1), auto intro!: borel_measurable_real_of_ereal dest: borel_measurable_simple_function) - then have "((\x. real (F i x)) has_integral integral\<^sup>L lebesgue (\x. real (F i x))) UNIV" - by (rule has_integral_lebesgue_integral_lebesgue) - from this I have "integral\<^sup>L lebesgue (\x. real (F i x)) \ I" - by (rule has_integral_le) (intro ballI F_bound) - moreover have "integral\<^sup>N lebesgue (F i) = integral\<^sup>L lebesgue (\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) \ 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 \ real" - shows "f \ borel_measurable lebesgue \ (\x. 0 \ f x) \ - (f has_integral I) UNIV \ 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 \ real" - assumes "f \ borel_measurable borel" "\x. 0 \ 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 \ f integrable_on UNIV" + using has_integral_integral_lborel by (auto intro: has_integral_integrable) + +lemma integral_lborel: "integrable lborel f \ integral UNIV f = (\x. f x \lborel)" + using has_integral_integral_lborel by auto -subsection {* Equivalence between product spaces and euclidean spaces *} - -definition e2p :: "'a::ordered_euclidean_space \ ('a \ real)" where - "e2p x = (\i\Basis. x \ i)" - -definition p2e :: "('a \ real) \ 'a::ordered_euclidean_space" where - "p2e x = (\i\Basis. x i *\<^sub>R i)" - -lemma e2p_p2e[simp]: - "x \ extensional Basis \ 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 "\x. lborel::real measure" - by default - -interpretation lborel_space: finite_product_sigma_finite "\x. lborel::real measure" "Basis" - by default auto - -lemma sets_product_borel: - assumes I: "finite I" - shows "sets (\\<^sub>M i\I. lborel) = sigma_sets (\\<^sub>E i\I. UNIV) { \\<^sub>E i\I. {..< x i :: real} | x. True}" (is "_ = ?G") -proof (subst sigma_prod_algebra_sigma_eq[where S="\_ i::nat. {..M I (\i. lborel))) {Pi\<^sub>E I F |F. \i\I. F i \ 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 \ measurable (borel::'a::ordered_euclidean_space measure) (\\<^sub>M (i::'a)\Basis. (lborel :: real measure))" -proof (rule measurable_sigma_sets[OF sets_product_borel]) - fix A :: "('a \ real) set" assume "A \ {\\<^sub>E (i::'a)\Basis. {..\<^sub>E (i::'a)\Basis. {..i\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 \ space (borel::'a measure) \ sets borel" by simp -qed (auto simp: e2p_def) - -(* FIXME: conversion in measurable prover *) -lemma lborelD_Collect[measurable (raw)]: "{x\space borel. P x} \ sets borel \ {x\space lborel. P x} \ sets lborel" by simp -lemma lborelD[measurable (raw)]: "A \ sets borel \ A \ sets lborel" by simp - -lemma measurable_p2e[measurable]: - "p2e \ measurable (\\<^sub>M (i::'a)\Basis. (lborel :: real measure)) - (borel :: 'a::ordered_euclidean_space measure)" - (is "p2e \ measurable ?P _") -proof (safe intro!: borel_measurable_iff_halfspace_le[THEN iffD2]) - fix x and i :: 'a - let ?A = "{w \ space ?P. (p2e w :: 'a) \ i \ x}" - assume "i \ Basis" - then have "?A = (\\<^sub>E j\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 \ sets ?P" - by auto -qed - -lemma lborel_eq_lborel_space: - "(lborel :: 'a measure) = distr (\\<^sub>M (i::'a::ordered_euclidean_space)\Basis. lborel) borel p2e" - (is "?B = ?D") -proof (rule lborel_eqI) - show "sets ?D = sets borel" by simp - let ?P = "(\\<^sub>M (i::'a)\Basis. lborel)" - fix a b :: 'a - have *: "p2e -` {a .. b} \ space ?P = (\\<^sub>E i\Basis. {a \ i .. b \ i})" - by (auto simp: eucl_le[where 'a='a] p2e_def space_PiM PiE_def Pi_iff) - have "emeasure ?P (p2e -` {a..b} \ space ?P) = content {a..b}" - proof cases - assume "{a..b} \ {}" - then have "a \ b" - by (simp add: eucl_le[where 'a='a]) - then have "emeasure lborel {a..b} = (\x\Basis. emeasure lborel {a \ x .. b \ x})" - by (auto simp: eucl_le[where 'a='a] content_closed_interval - intro!: setprod_ereal[symmetric]) - also have "\ = emeasure ?P (p2e -` {a..b} \ 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 \ ereal" - assumes f: "f \ borel_measurable borel" - shows "integral\<^sup>N lborel f = \\<^sup>+x. f (p2e x) \(\\<^sub>M (i::'a)\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 \ _::{banach, second_countable_topology}" - shows "integrable lborel f \ integrable (\\<^sub>M (i::'a)\Basis. lborel) (\x. f (p2e x))" - unfolding integrable_iff_bounded -proof (intro conj_cong[symmetric]) - show "((\x. f (p2e x)) \ borel_measurable (Pi\<^sub>M Basis (\i. lborel))) = (f \ borel_measurable lborel)" - proof - assume "((\x. f (p2e x)) \ borel_measurable (Pi\<^sub>M Basis (\i. lborel)))" - then have "(\x. f (p2e (e2p x))) \ borel_measurable borel" - by measurable - then show "f \ borel_measurable lborel" - by simp - qed simp -qed (simp add: borel_fubini_positiv_integral) - -lemma borel_fubini: - fixes f :: "'a::ordered_euclidean_space \ _::{banach, second_countable_topology}" - shows "f \ borel_measurable borel \ - integral\<^sup>L lborel f = \x. f (p2e x) \((\\<^sub>M (i::'a)\Basis. lborel))" - by (subst lborel_eq_lborel_space) (simp add: integral_distr) - -lemma integrable_on_borel_integrable: - fixes f :: "'a::ordered_euclidean_space \ real" - shows "f \ borel_measurable borel \ (\x. 0 \ f x) \ f integrable_on UNIV \ 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 \ 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 \ emeasure lborel A < \" using emeasure_bounded_finite[of A] by (auto intro: compact_imp_bounded) lemma borel_integrable_compact: - fixes f :: "'a::ordered_euclidean_space \ 'b::{banach, second_countable_topology}" + fixes f :: "'a::euclidean_space \ 'b::{banach, second_countable_topology}" assumes "compact S" "continuous_on S f" shows "integrable lborel (\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) \ t \ s \ (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 \ b" - and F: "\x. a \ x \ x \ b \ DERIV F x :> f x" - and f: "\x. a \ x \ x \ b \ isCont f x" - shows "integral\<^sup>L lborel (\x. f x * indicator {a .. b} x) = F b - F a" -proof - - let ?f = "\x. f x * indicator {a .. b} x" - have "(?f has_integral (\x. ?f x \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 \ real" - assumes f_borel: "f \ borel_measurable borel" + assumes [measurable]: "f \ borel_measurable borel" assumes f: "\x. x \ {a..b} \ DERIV F x :> f x" "\x. x \ {a..b} \ 0 \ f x" and "a \ b" - shows integral_FTC_Icc_nonneg: "(\x. f x * indicator {a .. b} x \lborel) = F b - F a" (is ?eq) + shows nn_integral_FTC_Icc: "(\\<^sup>+x. ereal (f x) * indicator {a .. b} x \lborel) = F b - F a" (is ?nn) + and has_bochner_integral_FTC_Icc_nonneg: + "has_bochner_integral lborel (\x. f x * indicator {a .. b} x) (F b - F a)" (is ?has) + and integral_FTC_Icc_nonneg: "(\x. f x * indicator {a .. b} x \lborel) = F b - F a" (is ?eq) and integrable_FTC_Icc_nonneg: "integrable lborel (\x. f x * indicator {a .. b} x)" (is ?int) proof - - have i: "(f has_integral F b - F a) {a..b}" + have *: "(\x. f x * indicator {a..b} x) \ borel_measurable borel" "\x. 0 \ 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 \ b`) - have i: "((\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: "((\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: "((\x. f x * indicator {a .. b} x) has_integral F b - F a) UNIV" + unfolding indicator_def if_distrib[where f="\x. a * x" for a] + by (simp cong del: if_cong del: atLeastAtMost_iff) + then have nn: "(\\<^sup>+x. f x * indicator {a .. b} x \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 \ borel_measurable borel" "\x. x \ {a..b} \ DERIV F x :> f x" "\x. x \ {a..b} \ 0 \ f x" "a \ b" - shows "(\\<^sup>+x. f x * indicator {a .. b} x \lborel) = F b - F a" +lemma + fixes f :: "real \ 'a :: euclidean_space" + assumes "a \ b" + assumes "\x. a \ x \ x \ b \ (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 (\x. indicator {a .. b} x *\<^sub>R f x) (F b - F a)" (is ?has) + and integral_FTC_Icc: "(\x. indicator {a .. b} x *\<^sub>R f x \lborel) = F b - F a" (is ?eq) proof - - have "integrable lborel (\x. f x * indicator {a .. b} x)" - by (rule integrable_FTC_Icc_nonneg) fact+ - then have "(\\<^sup>+x. f x * indicator {a .. b} x \lborel) = (\x. f x * indicator {a .. b} x \lborel)" - using assms by (intro nn_integral_eq_integral) (auto simp: indicator_def) - also have "(\x. f x * indicator {a .. b} x \lborel) = F b - F a" - by (rule integral_FTC_Icc_nonneg) fact+ - finally show ?thesis - unfolding ereal_indicator[symmetric] by simp + let ?f = "\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="\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 \ real" + assumes "a \ b" + assumes deriv: "\x. a \ x \ x \ b \ DERIV F x :> f x" + assumes cont: "\x. a \ x \ x \ b \ isCont f x" + shows has_bochner_integral_FTC_Icc_real: + "has_bochner_integral lborel (\x. f x * indicator {a .. b} x) (F b - F a)" (is ?has) + and integral_FTC_Icc_real: "(\x. f x * indicator {a .. b} x \lborel) = F b - F a" (is ?eq) +proof - + have 1: "\x. a \ x \ x \ b \ (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 \ b` 1 2] integral_FTC_Icc[OF `a \ 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 "\ = (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 "\ = T - F a" proof (rule SUP_Lim_ereal) show "incseq (\n. ereal (F (a + real n) - F a))" @@ -1228,6 +1219,13 @@ finally show ?thesis . qed +lemma integral_power: + "a \ b \ (\x. x^k * indicator {a..b} x \lborel) = (b^Suc k - a^Suc k) / Suc k" +proof (subst integral_FTC_Icc_real) + fix x show "DERIV (\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 - \x. (f x * G x) * indicator {a .. b} x \lborel" proof- have 0: "(\x. (F x * g x + f x * G x) * indicator {a .. b} x \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 "(\x. (F x * g x + f x * G x) * indicator {a .. b} x \lborel) = @@ -1274,12 +1272,6 @@ = F b * G b - F a * G a - \x. indicator {a .. b} x *\<^sub>R (f x * G x) \lborel" using integral_by_parts[OF assms] by (simp add: mult_ac) -lemma AE_borel_affine: - fixes P :: "real \ bool" - shows "c \ 0 \ Measurable.pred borel P \ AE x in lborel. P x \ 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 \ 'a :: {banach, second_countable_topology}" assumes f: "has_bochner_integral lborel (\x. indicator {0..} x *\<^sub>R f x) x" @@ -1324,3 +1316,4 @@ qed end + diff -r 06e195515deb -r 87429bdecad5 src/HOL/Probability/Measure_Space.thy --- 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 \ (\i. F i \ sets M) \ (\i. emeasure M (F i)) sums emeasure M (\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 \ {} \ {x} \ sets M \ A \ sets M \ x \ A \ emeasure M (insert x A) = emeasure M {x} + emeasure M A" + by (rule emeasure_insert) + lemma emeasure_eq_setsum_singleton: assumes "finite S" "\x. x \ S \ {x} \ sets M" shows "emeasure M S = (\x\S. emeasure M {x})" @@ -1037,8 +1045,34 @@ locale sigma_finite_measure = fixes M :: "'a measure" - assumes sigma_finite: "\A::nat \ 'a set. - range A \ sets M \ (\i. A i) = space M \ (\i. emeasure M (A i) \ \)" + assumes sigma_finite_countable: + "\A::'a set set. countable A \ A \ sets M \ (\A) = space M \ (\a\A. emeasure M a \ \)" + +lemma (in sigma_finite_measure) sigma_finite: + obtains A :: "nat \ 'a set" + where "range A \ sets M" "(\i. A i) = space M" "\i. emeasure M (A i) \ \" +proof - + obtain A :: "'a set set" where + [simp]: "countable A" and + A: "A \ sets M" "(\A) = space M" "\a. a \ A \ emeasure M a \ \" + using sigma_finite_countable by metis + show thesis + proof cases + assume "A = {}" with `(\A) = space M` show thesis + by (intro that[of "\_. {}"]) auto + next + assume "A \ {}" + show thesis + proof + show "range (from_nat_into A) \ sets M" + using `A \ {}` A by auto + have "(\i. from_nat_into A i) = \A" + using range_from_nat_into[OF `A \ {}` `countable A`] by auto + with A show "(\i. from_nat_into A i) = space M" + by auto + qed (intro A from_nat_into `A \ {}`) + qed +qed lemma (in sigma_finite_measure) sigma_finite_disjoint: obtains A :: "nat \ 'a set" @@ -1135,6 +1169,16 @@ "f \ measurable M N \ S \ sets N \ measure (distr M N f) S = measure M (f -` S \ 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 \ measurable M N" and "g \ measurable K L" + shows "distr M N f = distr K L g" +proof (rule measure_eqI) + fix A assume "A \ 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 \ 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) \ \" lemma finite_measureI[Pure.intro!]: - assumes *: "emeasure M (space M) \ \" - shows "finite_measure M" -proof - show "\A. range A \ sets M \ (\i. A i) = space M \ (\i. emeasure M (A i) \ \)" - using * by (auto intro!: exI[of _ "\_. space M"]) -qed fact + "emeasure M (space M) \ \ \ finite_measure M" + proof qed (auto intro!: exI[of _ "{space M}"]) lemma (in finite_measure) emeasure_finite[simp, intro]: "emeasure M A \ \" 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 "\F::nat \ 'a set. range F \ sets (count_space A) \ (\i. F i) = space (count_space A) \ - (\i. emeasure (count_space A) (F i) \ \)" - using A - apply (intro exI[of _ "\i. {from_nat_into A i} \ A"]) - apply auto - apply (rule_tac x="to_nat_on A x" in exI) - apply simp - done -qed + proof qed (auto intro!: exI[of _ "(\a. {a}) ` A"] simp: A) lemma sigma_finite_measure_count_space: fixes A :: "'a::countable set" shows "sigma_finite_measure (count_space A)" diff -r 06e195515deb -r 87429bdecad5 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy --- 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: "\x. x \ space M \ 0 \ f x" "\x. x \ space M \ f x < \" + assumes f[measurable]: "simple_function M f" + assumes supp: "emeasure M {x\space M. f x \ 0} < \" + shows "nn_integral M f < \" +proof cases + assume "space M = {}" + then have "nn_integral M f = (\\<^sup>+x. 0 \M)" + by (intro nn_integral_cong) auto + then show ?thesis by simp +next + assume "space M \ {}" + with simple_functionD(1)[OF f] bnd have bnd: "0 \ Max (f`space M) \ Max (f`space M) < \" + by (subst Max_less_iff) (auto simp: Max_ge_iff) + + have "nn_integral M f \ (\\<^sup>+x. Max (f`space M) * indicator {x\space M. f x \ 0} x \M)" + proof (rule nn_integral_mono) + fix x assume "x \ space M" + with f show "f x \ Max (f ` space M) * indicator {x \ space M. f x \ 0} x" + by (auto split: split_indicator intro!: Max_ge simple_functionD) + qed + also have "\ < \" + using bnd supp by (subst nn_integral_cmult) auto + finally show ?thesis . +qed + lemma nn_integral_Markov_inequality: assumes u: "u \ borel_measurable M" "AE x in M. 0 \ u x" and "A \ sets M" and c: "0 \ c" shows "(emeasure M) ({x\space M. 1 \ c * u x} \ A) \ c * (\\<^sup>+ x. u x * indicator A x \M)" diff -r 06e195515deb -r 87429bdecad5 src/HOL/Probability/Probability_Measure.thy --- 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 \ integral\<^sup>L M" abbreviation (in prob_space) "variance X \ integral\<^sup>L M (\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 \ 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 \ variance (X::'a \ real)" by (intro integral_nonneg_AE) (auto intro!: integral_nonneg_AE) +lemma (in prob_space) variance_mean_zero: + "expectation X = 0 \ variance X = expectation (\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 \ P: prob_space "M1 \\<^sub>M M2" @@ -988,7 +995,7 @@ and M_eq: "\a. emeasure M {x\space M. X x \ 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) diff -r 06e195515deb -r 87429bdecad5 src/HOL/Probability/Projective_Family.thy --- 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 \ 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 \ {}" "finite K" "K \ I" "A = emb I K Y" "Y \ sets (Pi\<^sub>M K M)" have "emeasure (limP K M P) Y = emeasure (limP (K \ J) M P) (emb (K \ J) K Y)" - using K J by simp + using K J by (simp del: limP_finite) also have "emb (K \ J) K Y = emb (K \ J) J X" using K J by (simp add: prod_emb_injective[of "K \ J" I]) also have "emeasure (limP (K \ J) M P) (emb (K \ 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 \ {}" "finite J" "J \ I" "A = emb I J X" "X \ 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 "\ = emeasure (limP (J \ K) M P) (emb (J \ K) J X \ emb (J \ 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 "\ = \G A + \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 "\G (A \ B) = \G A + \G B" . qed qed @@ -334,19 +334,14 @@ end sublocale product_prob_space \ projective_family I "\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)) \ \" by simp - show "\A. range A \ sets (Pi\<^sub>M J M) \ - (\i. A i) = space (Pi\<^sub>M J M) \ - (\i. emeasure (Pi\<^sub>M J M) (A i) \ \)" 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 \ {}" "finite J" "J \ I" shows "limP J M (\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 diff -r 06e195515deb -r 87429bdecad5 src/HOL/Probability/Projective_Limit.thy --- 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 \ 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 \ (\ i\{1..n}. (Z i - Z' i))" using Z' Z `n \ 1` unfolding Y_def by (force simp: decseq_def) @@ -332,9 +332,7 @@ have "\G (Z i - Z' i) = \G (prod_emb I (\_. borel) (J i) (B i - K i))" unfolding Z'_def Z_eq by simp also have "\ = 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 "\ = P (J i) (B i) - P (J i) (K i)" apply (subst emeasure_Diff) using K_sets J `K _ \ B _` apply (auto simp: proj_sets) done @@ -585,7 +583,7 @@ moreover have "emb I {} {\x. undefined} = space (lim\<^sub>B I P)" by (auto simp: space_PiM prod_emb_def) moreover have "{\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 diff -r 06e195515deb -r 87429bdecad5 src/HOL/Probability/Radon_Nikodym.thy --- 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 \ \" - from sigma_finite guess Q .. note Q = this + from sigma_finite guess Q . note Q = this def A \ "\i. f -` (case i of 0 \ {\} | Suc n \ {.. ereal(of_nat (Suc n))}) \ space M" { fix i j have "A i \ Q j \ 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 = "\n. case prod_decode n of (i,j) \ A i \ Q j" + show "sigma_finite_measure ?N" - proof (default, intro exI conjI subsetI allI) - fix x assume "x \ range ?A" - then obtain n where n: "x = ?A n" by auto - then show "x \ sets ?N" using A_in_sets by (cases "prod_decode n") auto + proof (default, intro exI conjI ballI) + show "countable (range (\(i, j). A i \ Q j))" + by auto + show "range (\(i, j). A i \ Q j) \ sets (density M f)" + using A_in_sets by auto next - have "(\i. ?A i) = (\i j. A i \ Q j)" - proof safe - fix x i j assume "x \ A i" "x \ Q j" - then show "x \ (\i. case prod_decode i of (i, j) \ A i \ Q j)" - by (intro UN_I[of "prod_encode (i,j)"]) auto - qed auto + have "\range (\(i, j). A i \ Q j) = (\i j. A i \ Q j)" + by auto also have "\ = (\i. A i) \ space M" using Q by auto also have "(\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 "(\i. ?A i) = space ?N" by simp + finally show "\range (\(i, j). A i \ 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 \ range (\(i, j). A i \ Q j)" + then obtain i j where [simp]:"X = A i \ Q j" by auto have "(\\<^sup>+x. f x * indicator (A i \ Q j) x \M) \ \" 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) \ \" + then show "emeasure ?N X \ \" 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 "\A::nat \ 'b set. range A \ sets ?M' \ (\i. A i) = space ?M' \ (\i. emeasure ?M' (A i) \ \)" - proof (intro exI conjI allI) - show *: "range (\i. T' -` F i \ space ?M') \ sets ?M'" + from sigma_finite_countable guess F .. note F = this + show "\A. countable A \ A \ sets (distr M M' T) \ \A = space (distr M M' T) \ (\a\A. emeasure (distr M M' T) a \ \)" + proof (intro exI conjI ballI) + show *: "(\A. T' -` A \ space ?M') ` F \ sets ?M'" using F T' by (auto simp: measurable_def) - show "(\i. T' -` F i \ space ?M') = space ?M'" - using F T' by (force simp: measurable_def) - fix i - have "T' -` F i \ space M' \ sets M'" using * by auto + show "\((\A. T' -` A \ space ?M')`F) = space ?M'" + using F T'[THEN measurable_space] by (auto simp: set_eq_iff) + next + fix X assume "X \ (\A. T' -` A \ space ?M')`F" + then obtain A where [simp]: "X = T' -` A \ space ?M'" and "A \ F" by auto + have "X \ sets M'" using F T' `A\F` by auto moreover - have Fi: "F i \ sets M" using F by auto - ultimately show "emeasure ?M' (T' -` F i \ space ?M') \ \" - using F T T' by (simp add: emeasure_distr) - qed + have Fi: "A \ sets M" using F `A\F` by auto + ultimately show "emeasure ?M' X \ \" + using F T T' `A\F` by (simp add: emeasure_distr) + qed (insert F, auto) qed have "(RN_deriv ?M' ?N') \ T \ borel_measurable M" using T ac by measurable diff -r 06e195515deb -r 87429bdecad5 src/HOL/Probability/Sigma_Algebra.thy --- 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 \ B \ f i \ B" by blast +lemma disjoint_family_onD: "disjoint_family_on A I \ i \ I \ j \ I \ i \ j \ A i \ A j = {}" + by (auto simp: disjoint_family_on_def) + lemma Int_Diff_disjoint: "A \ B \ (A - B) = {}" by blast diff -r 06e195515deb -r 87429bdecad5 src/HOL/Real.thy --- 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 "\q :: rat. x < of_rat q \ 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: "\ q \ \. (x :: real) \ q" +lemma Rats_no_top_le: "\ q \ \. (x :: real) \ q" by (auto intro!: bexI[of _ "of_nat (natceiling x)"]) (metis real_natceiling_ge real_of_nat_def) +lemma Rats_no_bot_less: "\ q \ \. 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: diff -r 06e195515deb -r 87429bdecad5 src/HOL/Set_Interval.thy --- 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} \ a = c \ b = d" using atLeastLessThan_inj assms by auto +lemma (in linorder) Ioc_inj: "{a <.. b} = {c <.. d} \ (b \ a \ d \ c) \ a = c \ b = d" + by (metis eq_iff greaterThanAtMost_empty_iff2 greaterThanAtMost_iff le_cases not_le) + +lemma (in order) Iio_Int_singleton: "{.. {x} = (if x < k then {x} else {})" + by auto + +lemma (in linorder) Ioc_subset_iff: "{a<..b} \ {c<..d} \ (b \ a \ c \ a \ b \ d)" + by (auto simp: subset_eq Ball_def) (metis less_le not_less) + lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \ x = bot" by (auto simp: set_eq_iff intro: le_bot) @@ -588,6 +597,9 @@ lemma Int_atMost[simp]: "{..a} \ {..b} = {.. min a b}" by (auto simp: min_def) +lemma Ioc_disjoint: "{a<..b} \ {c<..d} = {} \ b \ a \ d \ c \ b \ c \ d \ a" + using assms by auto + end context complete_lattice diff -r 06e195515deb -r 87429bdecad5 src/HOL/Topological_Spaces.thy --- 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 \ closed (- S)" unfolding open_closed . +lemma open_Collect_neg: "closed {x. P x} \ open {x. \ 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 \ 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 \ Q x}" + using open_Un[OF assms] by (simp add: Un_def) + +lemma open_Collect_ex: "(\i. open {x. P i x}) \ open {x. \i. P i x}" + using open_UN[of UNIV "\i. {x. P i x}"] unfolding Collect_ex_eq by simp + +lemma open_Collect_imp: "closed {x. P x} \ open {x. Q x} \ open {x. P x \ 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} \ closed {x. \ 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 \ 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 \ Q x}" + using closed_Un[OF assms] by (simp add: Un_def) + +lemma closed_Collect_all: "(\i. closed {x. P i x}) \ closed {x. \i. P i x}" + using closed_INT[of UNIV "\i. {x. P i x}"] unfolding Collect_all_eq by simp + +lemma closed_Collect_imp: "open {x. P x} \ closed {x. Q x} \ closed {x. P x \ 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 (\i. R i) F" using assms by (auto elim!: eventually_rev_mp) +lemma not_eventually_impI: "eventually P F \ \ eventually Q F \ \ eventually (\x. P x \ Q x) F" + by (auto intro: eventually_mp) + +lemma not_eventuallyD: "\ eventually P F \ \x. \ P x" + by (metis always_eventually) + lemma eventually_subst: assumes "eventually (\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 \ filtermap f F \ filtermap f G \ F \ G" + apply (auto intro!: filtermap_mono) [] + apply (auto simp: le_filter_def eventually_filtermap) + apply (erule_tac x="\x. P (inv f x)" in allE) + apply auto + done + +lemma filtermap_eq_strong: "inj f \ filtermap f F = filtermap f G \ F = G" + by (simp add: filtermap_mono_strong eq_iff) + lemma filterlim_principal: "(LIM x F. f x :> principal S) \ (eventually (\x. f x \ S) F)" unfolding filterlim_def eventually_filtermap le_principal .. @@ -984,6 +1036,13 @@ "filterlim f F F1 \ filterlim f F F2 \ filterlim f F (sup F1 F2)" unfolding filterlim_def filtermap_sup by auto +lemma eventually_sequentially_Suc: "eventually (\i. P (Suc i)) sequentially \ 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) \ (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) \ (\Z. eventually (\x. f x \ Z) F)" by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1) +lemma filterlim_at_bot_dense: + fixes f :: "'a \ ('b::{dense_linorder, no_bot})" + shows "(LIM x F. f x :> at_bot) \ (\Z. eventually (\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 "\Z. eventually (\x. f x \ Z) F" + hence "eventually (\x. f x \ Z') F" by auto + thus "eventually (\x. f x < Z) F" + apply (rule eventually_mono[rotated]) + using 1 by auto + next + fix Z :: 'b + show "\Z. eventually (\x. f x < Z) F \ eventually (\x. f x \ 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 \ ('b::linorder)" and c :: "'b" shows "(LIM x F. f x :> at_bot) \ (\Z\c. eventually (\x. Z \ 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) \ (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) \ (\f. f ----> a \ eventually (\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 \ _" + shows "(f ---> a) (at x within s) \ (\X. (\i. X i \ s - {x}) \ X ----> x \ ((f \ 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 "(\x. g (f x)) -- a --> c" using g f inj by (rule tendsto_compose_eventually) +lemma tendsto_compose_filtermap: "((g \ f) ---> T) F \ (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 *: "\f. (\n. b < f n) \ (\n. f n < a) \ incseq f \ f ----> a \ eventually (\n. P (f n)) sequentially" shows "eventually P (at_left a)" proof (safe intro!: sequentially_imp_eventually_within) - fix X assume X: "\n. X n \ {.. X n \ a" "X ----> a" + fix X assume X: "\n. X n \ {..< a} \ X n \ a" "X ----> a" show "eventually (\n. P (X n)) sequentially" proof (rule ccontr) - - assume "\ eventually (\n. P (X n)) sequentially" - from not_eventually_sequentiallyD[OF this] - obtain r where "subseq r" "\n. \ P (X (r n))" - by auto - with X have "(X \ r) ----> a" - by (auto intro: LIMSEQ_subseq_LIMSEQ) - from order_tendstoD(1)[OF this] obtain s' where s': "\b i. b < a \ s' b \ i \ b < X (r i)" - unfolding eventually_sequentially comp_def by metis - def s \ "rec_nat (s' b) (\_ i. max (s' (X (r i))) (Suc i))" - then have [simp]: "s 0 = s' b" "\n. s (Suc n) = max (s' (X (r (s n)))) (Suc (s n))" - by auto - have "eventually (\n. P (((X \ r) \ s) n)) sequentially" - proof (rule *) - from X show inc: "incseq (X \ r \ s)" - unfolding incseq_Suc_iff comp_def by (intro allI s'[THEN less_imp_le]) auto - { fix n show "b < (X \ r \ s) n" - using inc[THEN incseqD, of 0 n] s'[OF b order_refl] by simp } - { fix n show "(X \ r \ s) n < a" - using X by simp } - from `(X \ r) ----> a` show "(X \ r \ s) ----> a" - by (rule LIMSEQ_subseq_LIMSEQ) (auto simp: subseq_Suc_iff) + assume neg: "\ eventually (\n. P (X n)) sequentially" + have "\s. \n. (\ P (X (s n)) \ b < X (s n)) \ (X (s n) \ X (s (Suc n)) \ Suc (s n) \ s (Suc n))" + proof (rule dependent_nat_choice) + have "\ eventually (\n. b < X n \ P (X n)) sequentially" + by (intro not_eventually_impI neg order_tendstoD(1) [OF X(2) b]) + then show "\x. \ P (X x) \ b < X x" + by (auto dest!: not_eventuallyD) + next + fix x n + have "\ eventually (\n. Suc x \ n \ b < X n \ X x < X n \ 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 "\n. (\ P (X n) \ b < X n) \ (X x \ X n \ Suc x \ n)" + by (auto dest!: not_eventuallyD) qed - with `\n. \ P (X (r n))` show False - by auto + then guess s .. + then have "\n. b < X (s n)" "\n. X (s n) < a" "incseq (\n. X (s n))" "(\n. X (s n)) ----> a" "\n. \ 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 *: "\f. (\n. a < f n) \ (\n. f n < b) \ decseq f \ f ----> a \ eventually (\n. P (f n)) sequentially" + shows "eventually P (at_right a)" +proof (safe intro!: sequentially_imp_eventually_within) + fix X assume X: "\n. X n \ {a <..} \ X n \ a" "X ----> a" + show "eventually (\n. P (X n)) sequentially" + proof (rule ccontr) + assume neg: "\ eventually (\n. P (X n)) sequentially" + have "\s. \n. (\ P (X (s n)) \ X (s n) < b) \ (X (s (Suc n)) \ X (s n) \ Suc (s n) \ s (Suc n))" + proof (rule dependent_nat_choice) + have "\ eventually (\n. X n < b \ P (X n)) sequentially" + by (intro not_eventually_impI neg order_tendstoD(2) [OF X(2) b]) + then show "\x. \ P (X x) \ X x < b" + by (auto dest!: not_eventuallyD) + next + fix x n + have "\ eventually (\n. Suc x \ n \ X n < b \ X n < X x \ 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 "\n. (\ P (X n) \ X n < b) \ (X n \ X x \ Suc x \ n)" + by (auto dest!: not_eventuallyD) + qed + then guess s .. + then have "\n. a < X (s n)" "\n. X (s n) < b" "decseq (\n. X (s n))" "(\n. X (s n)) ----> a" "\n. \ 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 *: "\S. (\n. a < S n) \ (\n. S n < b) \ decseq S \ S ----> a \ (\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) \ continuous (at x within s) f \ continuous (at x within s) (\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: "\S. open S \ 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 \ 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 \ s \ {} \ continuous_on s f \ (\x\s. \y\s. f x \ f y)" using compact_attains_inf[of "f ` s"] compact_continuous_image[of s f] by auto - subsection {* Connectedness *} context topological_space