# HG changeset patch # User paulson # Date 1458137130 0 # Node ID 20288ba55e853a0e8c67554fdc5c6cc1be953ccb # Parent de25474ce728ef8e4824b87c9f6dbf39973725da# Parent 2d73385aa5f35b7a171756c38664a31517163678 Merge diff -r de25474ce728 -r 20288ba55e85 src/HOL/Library/Liminf_Limsup.thy --- a/src/HOL/Library/Liminf_Limsup.thy Wed Mar 16 13:57:06 2016 +0000 +++ b/src/HOL/Library/Liminf_Limsup.thy Wed Mar 16 14:05:30 2016 +0000 @@ -3,18 +3,58 @@ Author: Manuel Eberl, TU München *) -section \Liminf and Limsup on complete lattices\ +section \Liminf and Limsup on conditionally complete lattices\ theory Liminf_Limsup imports Complex_Main begin +lemma (in conditionally_complete_linorder) le_cSup_iff: + assumes "A \ {}" "bdd_above A" + shows "x \ Sup A \ (\ya\A. y < a)" +proof safe + fix y assume "x \ Sup A" "y < x" + then have "y < Sup A" by auto + then show "\a\A. y < a" + unfolding less_cSup_iff[OF assms] . +qed (auto elim!: allE[of _ "Sup A"] simp add: not_le[symmetric] cSup_upper assms) + +lemma (in conditionally_complete_linorder) le_cSUP_iff: + "A \ {} \ bdd_above (f`A) \ x \ SUPREMUM A f \ (\yi\A. y < f i)" + using le_cSup_iff [of "f ` A"] by simp + +lemma le_cSup_iff_less: + fixes x :: "'a :: {conditionally_complete_linorder, dense_linorder}" + shows "A \ {} \ bdd_above (f`A) \ x \ (SUP i:A. f i) \ (\yi\A. y \ f i)" + by (simp add: le_cSUP_iff) + (blast intro: less_imp_le less_trans less_le_trans dest: dense) + lemma le_Sup_iff_less: fixes x :: "'a :: {complete_linorder, dense_linorder}" shows "x \ (SUP i:A. f i) \ (\yi\A. y \ f i)" (is "?lhs = ?rhs") unfolding le_SUP_iff by (blast intro: less_imp_le less_trans less_le_trans dest: dense) +lemma (in conditionally_complete_linorder) cInf_le_iff: + assumes "A \ {}" "bdd_below A" + shows "Inf A \ x \ (\y>x. \a\A. y > a)" +proof safe + fix y assume "x \ Inf A" "y > x" + then have "y > Inf A" by auto + then show "\a\A. y > a" + unfolding cInf_less_iff[OF assms] . +qed (auto elim!: allE[of _ "Inf A"] simp add: not_le[symmetric] cInf_lower assms) + +lemma (in conditionally_complete_linorder) cINF_le_iff: + "A \ {} \ bdd_below (f`A) \ INFIMUM A f \ x \ (\y>x. \i\A. y > f i)" + using cInf_le_iff [of "f ` A"] by simp + +lemma cInf_le_iff_less: + fixes x :: "'a :: {conditionally_complete_linorder, dense_linorder}" + shows "A \ {} \ bdd_below (f`A) \ (INF i:A. f i) \ x \ (\y>x. \i\A. f i \ y)" + by (simp add: cINF_le_iff) + (blast intro: less_imp_le less_trans le_less_trans dest: dense) + lemma Inf_le_iff_less: fixes x :: "'a :: {complete_linorder, dense_linorder}" shows "(INF i:A. f i) \ x \ (\y>x. \i\A. f i \ y)" diff -r de25474ce728 -r 20288ba55e85 src/HOL/Probability/Borel_Space.thy --- a/src/HOL/Probability/Borel_Space.thy Wed Mar 16 13:57:06 2016 +0000 +++ b/src/HOL/Probability/Borel_Space.thy Wed Mar 16 14:05:30 2016 +0000 @@ -11,6 +11,30 @@ "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis" begin +lemma sets_Collect_eventually_sequentially[measurable]: + "(\i. {x\space M. P x i} \ sets M) \ {x\space M. eventually (P x) sequentially} \ sets M" + unfolding eventually_sequentially by simp + +lemma open_Collect_less: + fixes f g :: "'i::topological_space \ 'a :: {dense_linorder, linorder_topology}" + assumes "continuous_on UNIV f" + assumes "continuous_on UNIV g" + shows "open {x. f x < g x}" +proof - + have "open (\y. {x \ UNIV. f x \ {..< y}} \ {x \ UNIV. g x \ {y <..}})" (is "open ?X") + by (intro open_UN ballI open_Int continuous_open_preimage assms) auto + also have "?X = {x. f x < g x}" + by (auto intro: dense) + finally show ?thesis . +qed + +lemma closed_Collect_le: + fixes f g :: "'i::topological_space \ 'a :: {dense_linorder, linorder_topology}" + assumes f: "continuous_on UNIV f" + assumes g: "continuous_on UNIV g" + shows "closed {x. f x \ g x}" + using open_Collect_less[OF g f] unfolding not_less[symmetric] Collect_neg_eq open_closed . + lemma topological_basis_trivial: "topological_basis {A. open A}" by (auto simp: topological_basis_def) @@ -428,6 +452,64 @@ lemma borel_compact: "compact (A::'a::t2_space set) \ A \ sets borel" by (auto intro: borel_closed dest!: compact_imp_closed) +lemma borel_sigma_sets_subset: + "A \ sets borel \ sigma_sets UNIV A \ sets borel" + using sets.sigma_sets_subset[of A borel] by simp + +lemma borel_eq_sigmaI1: + fixes F :: "'i \ 'a::topological_space set" and X :: "'a::topological_space set set" + assumes borel_eq: "borel = sigma UNIV X" + assumes X: "\x. x \ X \ x \ sets (sigma UNIV (F ` A))" + assumes F: "\i. i \ A \ F i \ sets borel" + shows "borel = sigma UNIV (F ` A)" + unfolding borel_def +proof (intro sigma_eqI antisym) + have borel_rev_eq: "sigma_sets UNIV {S::'a set. open S} = sets borel" + unfolding borel_def by simp + also have "\ = sigma_sets UNIV X" + unfolding borel_eq by simp + also have "\ \ sigma_sets UNIV (F`A)" + using X by (intro sigma_algebra.sigma_sets_subset[OF sigma_algebra_sigma_sets]) auto + finally show "sigma_sets UNIV {S. open S} \ sigma_sets UNIV (F`A)" . + show "sigma_sets UNIV (F`A) \ sigma_sets UNIV {S. open S}" + unfolding borel_rev_eq using F by (intro borel_sigma_sets_subset) auto +qed auto + +lemma borel_eq_sigmaI2: + fixes F :: "'i \ 'j \ 'a::topological_space set" + and G :: "'l \ 'k \ 'a::topological_space set" + assumes borel_eq: "borel = sigma UNIV ((\(i, j). G i j)`B)" + assumes X: "\i j. (i, j) \ B \ G i j \ sets (sigma UNIV ((\(i, j). F i j) ` A))" + assumes F: "\i j. (i, j) \ A \ F i j \ sets borel" + shows "borel = sigma UNIV ((\(i, j). F i j) ` A)" + using assms + by (intro borel_eq_sigmaI1[where X="(\(i, j). G i j) ` B" and F="(\(i, j). F i j)"]) auto + +lemma borel_eq_sigmaI3: + fixes F :: "'i \ 'j \ 'a::topological_space set" and X :: "'a::topological_space set set" + assumes borel_eq: "borel = sigma UNIV X" + assumes X: "\x. x \ X \ x \ sets (sigma UNIV ((\(i, j). F i j) ` A))" + assumes F: "\i j. (i, j) \ A \ F i j \ sets borel" + shows "borel = sigma UNIV ((\(i, j). F i j) ` A)" + using assms by (intro borel_eq_sigmaI1[where X=X and F="(\(i, j). F i j)"]) auto + +lemma borel_eq_sigmaI4: + fixes F :: "'i \ 'a::topological_space set" + and G :: "'l \ 'k \ 'a::topological_space set" + assumes borel_eq: "borel = sigma UNIV ((\(i, j). G i j)`A)" + assumes X: "\i j. (i, j) \ A \ G i j \ sets (sigma UNIV (range F))" + assumes F: "\i. F i \ sets borel" + shows "borel = sigma UNIV (range F)" + using assms by (intro borel_eq_sigmaI1[where X="(\(i, j). G i j) ` A" and F=F]) auto + +lemma borel_eq_sigmaI5: + fixes F :: "'i \ 'j \ 'a::topological_space set" and G :: "'l \ 'a::topological_space set" + assumes borel_eq: "borel = sigma UNIV (range G)" + assumes X: "\i. G i \ sets (sigma UNIV (range (\(i, j). F i j)))" + assumes F: "\i j. F i j \ sets borel" + shows "borel = sigma UNIV (range (\(i, j). F i j))" + using assms by (intro borel_eq_sigmaI1[where X="range G" and F="(\(i, j). F i j)"]) auto + lemma second_countable_borel_measurable: fixes X :: "'a::second_countable_topology set set" assumes eq: "open = generate_topology X" @@ -472,6 +554,40 @@ qed auto qed (auto simp: eq intro: generate_topology.Basis) +lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)" + unfolding borel_def +proof (intro sigma_eqI sigma_sets_eqI, safe) + fix x :: "'a set" assume "open x" + hence "x = UNIV - (UNIV - x)" by auto + also have "\ \ sigma_sets UNIV (Collect closed)" + by (force intro: sigma_sets.Compl simp: \open x\) + finally show "x \ sigma_sets UNIV (Collect closed)" by simp +next + fix x :: "'a set" assume "closed x" + hence "x = UNIV - (UNIV - x)" by auto + also have "\ \ sigma_sets UNIV (Collect open)" + by (force intro: sigma_sets.Compl simp: \closed x\) + finally show "x \ sigma_sets UNIV (Collect open)" by simp +qed simp_all + +lemma borel_eq_countable_basis: + fixes B::"'a::topological_space set set" + assumes "countable B" + assumes "topological_basis B" + shows "borel = sigma UNIV B" + unfolding borel_def +proof (intro sigma_eqI sigma_sets_eqI, safe) + interpret countable_basis using assms by unfold_locales + fix X::"'a set" assume "open X" + from open_countable_basisE[OF this] guess B' . note B' = this + then show "X \ sigma_sets UNIV B" + by (blast intro: sigma_sets_UNION \countable B\ countable_subset) +next + fix b assume "b \ B" + hence "open b" by (rule topological_basis_open[OF assms(2)]) + thus "b \ sigma_sets UNIV (Collect open)" by auto +qed simp_all + lemma borel_measurable_continuous_on_restrict: fixes f :: "'a::topological_space \ 'b::topological_space" assumes f: "continuous_on A f" @@ -516,24 +632,6 @@ by (subst borel_measurable_restrict_space_iff[symmetric]) (auto intro: borel_measurable_continuous_on_restrict) -lemma borel_eq_countable_basis: - fixes B::"'a::topological_space set set" - assumes "countable B" - assumes "topological_basis B" - shows "borel = sigma UNIV B" - unfolding borel_def -proof (intro sigma_eqI sigma_sets_eqI, safe) - interpret countable_basis using assms by unfold_locales - fix X::"'a set" assume "open X" - from open_countable_basisE[OF this] guess B' . note B' = this - then show "X \ sigma_sets UNIV B" - by (blast intro: sigma_sets_UNION \countable B\ countable_subset) -next - fix b assume "b \ B" - hence "open b" by (rule topological_basis_open[OF assms(2)]) - thus "b \ sigma_sets UNIV (Collect open)" by auto -qed simp_all - lemma borel_measurable_Pair[measurable (raw)]: fixes f :: "'a \ 'b::second_countable_topology" and g :: "'a \ 'c::second_countable_topology" assumes f[measurable]: "f \ borel_measurable M" @@ -574,6 +672,19 @@ subsection \Borel spaces on order topologies\ +lemma [measurable]: + fixes a b :: "'a::linorder_topology" + shows lessThan_borel: "{..< a} \ sets borel" + and greaterThan_borel: "{a <..} \ sets borel" + and greaterThanLessThan_borel: "{a<.. sets borel" + and atMost_borel: "{..a} \ sets borel" + and atLeast_borel: "{a..} \ sets borel" + and atLeastAtMost_borel: "{a..b} \ sets borel" + and greaterThanAtMost_borel: "{a<..b} \ sets borel" + and atLeastLessThan_borel: "{a.. sets borel" + unfolding greaterThanAtMost_def atLeastLessThan_def + by (blast intro: borel_open borel_closed open_lessThan open_greaterThan open_greaterThanLessThan + closed_atMost closed_atLeast closed_atLeastAtMost)+ lemma borel_Iio: "borel = sigma UNIV (range lessThan :: 'a::{linorder_topology, second_countable_topology} set set)" @@ -663,6 +774,40 @@ unfolding borel_Ioi by (rule measurable_measure_of) (auto simp: Int_def conj_commute) +lemma borel_measurableI_le: + fixes f :: "'a \ 'b::{linorder_topology, second_countable_topology}" + shows "(\y. {x\space M. f x \ y} \ sets M) \ f \ borel_measurable M" + by (rule borel_measurableI_greater) (auto simp: not_le[symmetric]) + +lemma borel_measurableI_ge: + fixes f :: "'a \ 'b::{linorder_topology, second_countable_topology}" + shows "(\y. {x\space M. y \ f x} \ sets M) \ f \ borel_measurable M" + by (rule borel_measurableI_less) (auto simp: not_le[symmetric]) + +lemma borel_measurable_less[measurable]: + fixes f :: "'a \ 'b::{second_countable_topology, dense_linorder, linorder_topology}" + assumes "f \ borel_measurable M" + assumes "g \ borel_measurable M" + shows "{w \ space M. f w < g w} \ sets M" +proof - + have "{w \ space M. f w < g w} = (\x. (f x, g x)) -` {x. fst x < snd x} \ space M" + by auto + also have "\ \ sets M" + by (intro measurable_sets[OF borel_measurable_Pair borel_open, OF assms open_Collect_less] + continuous_intros) + finally show ?thesis . +qed + +lemma + fixes f :: "'a \ 'b::{second_countable_topology, dense_linorder, linorder_topology}" + assumes f[measurable]: "f \ borel_measurable M" + assumes g[measurable]: "g \ borel_measurable M" + shows borel_measurable_le[measurable]: "{w \ space M. f w \ g w} \ sets M" + and borel_measurable_eq[measurable]: "{w \ space M. f w = g w} \ sets M" + and borel_measurable_neq: "{w \ space M. f w \ g w} \ sets M" + unfolding eq_iff not_less[symmetric] + by measurable + lemma borel_measurable_SUP[measurable (raw)]: fixes F :: "_ \ _ \ _::{complete_linorder, linorder_topology, second_countable_topology}" assumes [simp]: "countable I" @@ -677,6 +822,50 @@ shows "(\x. INF i:I. F i x) \ borel_measurable M" by (rule borel_measurableI_less) (simp add: INF_less_iff) +lemma borel_measurable_cSUP[measurable (raw)]: + fixes F :: "_ \ _ \ 'a::{conditionally_complete_linorder, linorder_topology, second_countable_topology}" + assumes [simp]: "countable I" + assumes [measurable]: "\i. i \ I \ F i \ borel_measurable M" + assumes bdd: "\x. x \ space M \ bdd_above ((\i. F i x) ` I)" + shows "(\x. SUP i:I. F i x) \ borel_measurable M" +proof cases + assume "I = {}" then show ?thesis + unfolding \I = {}\ image_empty by simp +next + assume "I \ {}" + show ?thesis + proof (rule borel_measurableI_le) + fix y + have "{x \ space M. \i\I. F i x \ y} \ sets M" + by measurable + also have "{x \ space M. \i\I. F i x \ y} = {x \ space M. (SUP i:I. F i x) \ y}" + by (simp add: cSUP_le_iff \I \ {}\ bdd cong: conj_cong) + finally show "{x \ space M. (SUP i:I. F i x) \ y} \ sets M" . + qed +qed + +lemma borel_measurable_cINF[measurable (raw)]: + fixes F :: "_ \ _ \ 'a::{conditionally_complete_linorder, linorder_topology, second_countable_topology}" + assumes [simp]: "countable I" + assumes [measurable]: "\i. i \ I \ F i \ borel_measurable M" + assumes bdd: "\x. x \ space M \ bdd_below ((\i. F i x) ` I)" + shows "(\x. INF i:I. F i x) \ borel_measurable M" +proof cases + assume "I = {}" then show ?thesis + unfolding \I = {}\ image_empty by simp +next + assume "I \ {}" + show ?thesis + proof (rule borel_measurableI_ge) + fix y + have "{x \ space M. \i\I. y \ F i x} \ sets M" + by measurable + also have "{x \ space M. \i\I. y \ F i x} = {x \ space M. y \ (INF i:I. F i x)}" + by (simp add: le_cINF_iff \I \ {}\ bdd cong: conj_cong) + finally show "{x \ space M. y \ (INF i:I. F i x)} \ sets M" . + qed +qed + lemma borel_measurable_lfp[consumes 1, case_names continuity step]: fixes F :: "('a \ 'b) \ ('a \ 'b::{complete_linorder, linorder_topology, second_countable_topology})" assumes "sup_continuous F" @@ -711,7 +900,102 @@ finally show ?thesis . qed -subsection \Borel spaces on euclidean spaces\ +lemma borel_measurable_max[measurable (raw)]: + "f \ borel_measurable M \ g \ borel_measurable M \ (\x. max (g x) (f x) :: 'b::{second_countable_topology, linorder_topology}) \ borel_measurable M" + by (rule borel_measurableI_less) simp + +lemma borel_measurable_min[measurable (raw)]: + "f \ borel_measurable M \ g \ borel_measurable M \ (\x. min (g x) (f x) :: 'b::{second_countable_topology, linorder_topology}) \ borel_measurable M" + by (rule borel_measurableI_greater) simp + +lemma borel_measurable_Min[measurable (raw)]: + "finite I \ (\i. i \ I \ f i \ borel_measurable M) \ (\x. Min ((\i. f i x)`I) :: 'b::{second_countable_topology, linorder_topology}) \ borel_measurable M" +proof (induct I rule: finite_induct) + case (insert i I) then show ?case + by (cases "I = {}") auto +qed auto + +lemma borel_measurable_Max[measurable (raw)]: + "finite I \ (\i. i \ I \ f i \ borel_measurable M) \ (\x. Max ((\i. f i x)`I) :: 'b::{second_countable_topology, linorder_topology}) \ borel_measurable M" +proof (induct I rule: finite_induct) + case (insert i I) then show ?case + by (cases "I = {}") auto +qed auto + +lemma borel_measurable_sup[measurable (raw)]: + "f \ borel_measurable M \ g \ borel_measurable M \ (\x. sup (g x) (f x) :: 'b::{lattice, second_countable_topology, linorder_topology}) \ borel_measurable M" + unfolding sup_max by measurable + +lemma borel_measurable_inf[measurable (raw)]: + "f \ borel_measurable M \ g \ borel_measurable M \ (\x. inf (g x) (f x) :: 'b::{lattice, second_countable_topology, linorder_topology}) \ borel_measurable M" + unfolding inf_min by measurable + +lemma [measurable (raw)]: + fixes f :: "nat \ 'a \ 'b::{complete_linorder, second_countable_topology, linorder_topology}" + assumes "\i. f i \ borel_measurable M" + shows borel_measurable_liminf: "(\x. liminf (\i. f i x)) \ borel_measurable M" + and borel_measurable_limsup: "(\x. limsup (\i. f i x)) \ borel_measurable M" + unfolding liminf_SUP_INF limsup_INF_SUP using assms by auto + +lemma measurable_convergent[measurable (raw)]: + fixes f :: "nat \ 'a \ 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology}" + assumes [measurable]: "\i. f i \ borel_measurable M" + shows "Measurable.pred M (\x. convergent (\i. f i x))" + unfolding convergent_ereal by measurable + +lemma sets_Collect_convergent[measurable]: + fixes f :: "nat \ 'a \ 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology}" + assumes f[measurable]: "\i. f i \ borel_measurable M" + shows "{x\space M. convergent (\i. f i x)} \ sets M" + by measurable + +lemma borel_measurable_lim[measurable (raw)]: + fixes f :: "nat \ 'a \ 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology}" + assumes [measurable]: "\i. f i \ borel_measurable M" + shows "(\x. lim (\i. f i x)) \ borel_measurable M" +proof - + have "\x. lim (\i. f i x) = (if convergent (\i. f i x) then limsup (\i. f i x) else (THE i. False))" + by (simp add: lim_def convergent_def convergent_limsup_cl) + then show ?thesis + by simp +qed + +lemma borel_measurable_LIMSEQ_order: + fixes u :: "nat \ 'a \ 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology}" + assumes u': "\x. x \ space M \ (\i. u i x) \ u' x" + and u: "\i. u i \ borel_measurable M" + shows "u' \ borel_measurable M" +proof - + have "\x. x \ space M \ u' x = liminf (\n. u n x)" + using u' by (simp add: lim_imp_Liminf[symmetric]) + with u show ?thesis by (simp cong: measurable_cong) +qed + +subsection \Borel spaces on topological monoids\ + +lemma borel_measurable_add[measurable (raw)]: + fixes f g :: "'a \ 'b::{second_countable_topology, topological_monoid_add}" + assumes f: "f \ borel_measurable M" + assumes g: "g \ borel_measurable M" + shows "(\x. f x + g x) \ borel_measurable M" + using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) + +lemma borel_measurable_setsum[measurable (raw)]: + fixes f :: "'c \ 'a \ 'b::{second_countable_topology, topological_comm_monoid_add}" + assumes "\i. i \ S \ f i \ borel_measurable M" + shows "(\x. \i\S. f i x) \ borel_measurable M" +proof cases + assume "finite S" + thus ?thesis using assms by induct auto +qed simp + +lemma borel_measurable_suminf_order[measurable (raw)]: + fixes f :: "nat \ 'a \ 'b::{complete_linorder, second_countable_topology, dense_linorder, linorder_topology, topological_comm_monoid_add}" + assumes f[measurable]: "\i. f i \ borel_measurable M" + shows "(\x. suminf (\i. f i x)) \ borel_measurable M" + unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp + +subsection \Borel spaces on Euclidean spaces\ lemma borel_measurable_inner[measurable (raw)]: fixes f g :: "'a \ 'b::{second_countable_topology, real_inner}" @@ -721,20 +1005,6 @@ using assms by (rule borel_measurable_continuous_Pair) (intro continuous_intros) -lemma [measurable]: - fixes a b :: "'a::linorder_topology" - shows lessThan_borel: "{..< a} \ sets borel" - and greaterThan_borel: "{a <..} \ sets borel" - and greaterThanLessThan_borel: "{a<.. sets borel" - and atMost_borel: "{..a} \ sets borel" - and atLeast_borel: "{a..} \ sets borel" - and atLeastAtMost_borel: "{a..b} \ sets borel" - and greaterThanAtMost_borel: "{a<..b} \ sets borel" - and atLeastLessThan_borel: "{a.. sets borel" - unfolding greaterThanAtMost_def atLeastLessThan_def - by (blast intro: borel_open borel_closed open_lessThan open_greaterThan open_greaterThanLessThan - closed_atMost closed_atLeast closed_atLeastAtMost)+ - notation eucl_less (infix " 'a :: {dense_linorder, linorder_topology}" - assumes "continuous_on UNIV f" - assumes "continuous_on UNIV g" - shows "open {x. f x < g x}" -proof - - have "open (\y. {x \ UNIV. f x \ {..< y}} \ {x \ UNIV. g x \ {y <..}})" (is "open ?X") - by (intro open_UN ballI open_Int continuous_open_preimage assms) auto - also have "?X = {x. f x < g x}" - by (auto intro: dense) - finally show ?thesis . -qed - -lemma closed_Collect_le: - fixes f g :: "'i::topological_space \ 'a :: {dense_linorder, linorder_topology}" - assumes f: "continuous_on UNIV f" - assumes g: "continuous_on UNIV g" - shows "closed {x. f x \ g x}" - using open_Collect_less[OF g f] unfolding not_less[symmetric] Collect_neg_eq open_closed . - -lemma borel_measurable_less[measurable]: - fixes f :: "'a \ 'b::{second_countable_topology, dense_linorder, linorder_topology}" - assumes "f \ borel_measurable M" - assumes "g \ borel_measurable M" - shows "{w \ space M. f w < g w} \ sets M" -proof - - have "{w \ space M. f w < g w} = (\x. (f x, g x)) -` {x. fst x < snd x} \ space M" - by auto - also have "\ \ sets M" - by (intro measurable_sets[OF borel_measurable_Pair borel_open, OF assms open_Collect_less] - continuous_intros) - finally show ?thesis . -qed - -lemma - fixes f :: "'a \ 'b::{second_countable_topology, dense_linorder, linorder_topology}" - assumes f[measurable]: "f \ borel_measurable M" - assumes g[measurable]: "g \ borel_measurable M" - shows borel_measurable_le[measurable]: "{w \ space M. f w \ g w} \ sets M" - and borel_measurable_eq[measurable]: "{w \ space M. f w = g w} \ sets M" - and borel_measurable_neq: "{w \ space M. f w \ g w} \ sets M" - unfolding eq_iff not_less[symmetric] - by measurable - lemma fixes i :: "'a::{second_countable_topology, real_inner}" shows hafspace_less_borel: "{x. a < x \ i} \ sets borel" @@ -806,66 +1032,6 @@ and hafspace_greater_eq_borel: "{x. x \ i \ a} \ sets borel" by simp_all -subsection "Borel space equals sigma algebras over intervals" - -lemma borel_sigma_sets_subset: - "A \ sets borel \ sigma_sets UNIV A \ sets borel" - using sets.sigma_sets_subset[of A borel] by simp - -lemma borel_eq_sigmaI1: - fixes F :: "'i \ 'a::topological_space set" and X :: "'a::topological_space set set" - assumes borel_eq: "borel = sigma UNIV X" - assumes X: "\x. x \ X \ x \ sets (sigma UNIV (F ` A))" - assumes F: "\i. i \ A \ F i \ sets borel" - shows "borel = sigma UNIV (F ` A)" - unfolding borel_def -proof (intro sigma_eqI antisym) - have borel_rev_eq: "sigma_sets UNIV {S::'a set. open S} = sets borel" - unfolding borel_def by simp - also have "\ = sigma_sets UNIV X" - unfolding borel_eq by simp - also have "\ \ sigma_sets UNIV (F`A)" - using X by (intro sigma_algebra.sigma_sets_subset[OF sigma_algebra_sigma_sets]) auto - finally show "sigma_sets UNIV {S. open S} \ sigma_sets UNIV (F`A)" . - show "sigma_sets UNIV (F`A) \ sigma_sets UNIV {S. open S}" - unfolding borel_rev_eq using F by (intro borel_sigma_sets_subset) auto -qed auto - -lemma borel_eq_sigmaI2: - fixes F :: "'i \ 'j \ 'a::topological_space set" - and G :: "'l \ 'k \ 'a::topological_space set" - assumes borel_eq: "borel = sigma UNIV ((\(i, j). G i j)`B)" - assumes X: "\i j. (i, j) \ B \ G i j \ sets (sigma UNIV ((\(i, j). F i j) ` A))" - assumes F: "\i j. (i, j) \ A \ F i j \ sets borel" - shows "borel = sigma UNIV ((\(i, j). F i j) ` A)" - using assms - by (intro borel_eq_sigmaI1[where X="(\(i, j). G i j) ` B" and F="(\(i, j). F i j)"]) auto - -lemma borel_eq_sigmaI3: - fixes F :: "'i \ 'j \ 'a::topological_space set" and X :: "'a::topological_space set set" - assumes borel_eq: "borel = sigma UNIV X" - assumes X: "\x. x \ X \ x \ sets (sigma UNIV ((\(i, j). F i j) ` A))" - assumes F: "\i j. (i, j) \ A \ F i j \ sets borel" - shows "borel = sigma UNIV ((\(i, j). F i j) ` A)" - using assms by (intro borel_eq_sigmaI1[where X=X and F="(\(i, j). F i j)"]) auto - -lemma borel_eq_sigmaI4: - fixes F :: "'i \ 'a::topological_space set" - and G :: "'l \ 'k \ 'a::topological_space set" - assumes borel_eq: "borel = sigma UNIV ((\(i, j). G i j)`A)" - assumes X: "\i j. (i, j) \ A \ G i j \ sets (sigma UNIV (range F))" - assumes F: "\i. F i \ sets borel" - shows "borel = sigma UNIV (range F)" - using assms by (intro borel_eq_sigmaI1[where X="(\(i, j). G i j) ` A" and F=F]) auto - -lemma borel_eq_sigmaI5: - fixes F :: "'i \ 'j \ 'a::topological_space set" and G :: "'l \ 'a::topological_space set" - assumes borel_eq: "borel = sigma UNIV (range G)" - assumes X: "\i. G i \ sets (sigma UNIV (range (\(i, j). F i j)))" - assumes F: "\i j. F i j \ sets borel" - shows "borel = sigma UNIV (range (\(i, j). F i j))" - using assms by (intro borel_eq_sigmaI1[where X="range G" and F="(\(i, j). F i j)"]) auto - lemma borel_eq_box: "borel = sigma UNIV (range (\ (a, b). box a b :: 'a :: euclidean_space set))" (is "_ = ?SIGMA") @@ -1057,6 +1223,28 @@ (auto intro!: sigma_sets_top) qed auto +lemma borel_set_induct[consumes 1, case_names empty interval compl union]: + assumes "A \ sets borel" + assumes empty: "P {}" and int: "\a b. a \ b \ P {a..b}" and compl: "\A. A \ sets borel \ P A \ P (-A)" and + un: "\f. disjoint_family f \ (\i. f i \ sets borel) \ (\i. P (f i)) \ P (\i::nat. f i)" + shows "P (A::real set)" +proof- + let ?G = "range (\(a,b). {a..b::real})" + have "Int_stable ?G" "?G \ Pow UNIV" "A \ sigma_sets UNIV ?G" + using assms(1) by (auto simp add: borel_eq_atLeastAtMost Int_stable_def) + thus ?thesis + proof (induction rule: sigma_sets_induct_disjoint) + case (union f) + from union.hyps(2) have "\i. f i \ sets borel" by (auto simp: borel_eq_atLeastAtMost) + with union show ?case by (auto intro: un) + next + case (basic A) + then obtain a b where "A = {a .. b}" by auto + then show ?case + by (cases "a \ b") (auto intro: int empty) + qed (auto intro: empty compl simp: Compl_eq_Diff_UNIV[symmetric] borel_eq_atLeastAtMost) +qed + 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 @@ -1081,22 +1269,6 @@ by (auto intro: sigma_sets.intros(2-) simp: eucl_lessThan) qed auto -lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)" - unfolding borel_def -proof (intro sigma_eqI sigma_sets_eqI, safe) - fix x :: "'a set" assume "open x" - hence "x = UNIV - (UNIV - x)" by auto - also have "\ \ sigma_sets UNIV (Collect closed)" - by (force intro: sigma_sets.Compl simp: \open x\) - finally show "x \ sigma_sets UNIV (Collect closed)" by simp -next - fix x :: "'a set" assume "closed x" - hence "x = UNIV - (UNIV - x)" by auto - also have "\ \ sigma_sets UNIV (Collect open)" - by (force intro: sigma_sets.Compl simp: \closed x\) - finally show "x \ sigma_sets UNIV (Collect open)" by simp -qed simp_all - lemma borel_measurable_halfspacesI: fixes f :: "'a \ 'c::euclidean_space" assumes F: "borel = sigma UNIV (F ` (UNIV \ Basis))" @@ -1158,28 +1330,6 @@ by (subst borel_measurable_iff_halfspace_le) auto qed auto -lemma borel_set_induct[consumes 1, case_names empty interval compl union]: - assumes "A \ sets borel" - assumes empty: "P {}" and int: "\a b. a \ b \ P {a..b}" and compl: "\A. A \ sets borel \ P A \ P (-A)" and - un: "\f. disjoint_family f \ (\i. f i \ sets borel) \ (\i. P (f i)) \ P (\i::nat. f i)" - shows "P (A::real set)" -proof- - let ?G = "range (\(a,b). {a..b::real})" - have "Int_stable ?G" "?G \ Pow UNIV" "A \ sigma_sets UNIV ?G" - using assms(1) by (auto simp add: borel_eq_atLeastAtMost Int_stable_def) - thus ?thesis - proof (induction rule: sigma_sets_induct_disjoint) - case (union f) - from union.hyps(2) have "\i. f i \ sets borel" by (auto simp: borel_eq_atLeastAtMost) - with union show ?case by (auto intro: un) - next - case (basic A) - then obtain a b where "A = {a .. b}" by auto - then show ?case - by (cases "a \ b") (auto intro: int empty) - qed (auto intro: empty compl simp: Compl_eq_Diff_UNIV[symmetric] borel_eq_atLeastAtMost) -qed - subsection "Borel measurable operators" lemma borel_measurable_norm[measurable]: "norm \ borel_measurable borel" @@ -1195,22 +1345,6 @@ shows "(\x. - g x) \ borel_measurable M" by (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_intros) -lemma borel_measurable_add[measurable (raw)]: - fixes f g :: "'a \ 'b::{second_countable_topology, real_normed_vector}" - assumes f: "f \ borel_measurable M" - assumes g: "g \ borel_measurable M" - shows "(\x. f x + g x) \ borel_measurable M" - using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) - -lemma borel_measurable_setsum[measurable (raw)]: - fixes f :: "'c \ 'a \ 'b::{second_countable_topology, real_normed_vector}" - assumes "\i. i \ S \ f i \ borel_measurable M" - shows "(\x. \i\S. f i x) \ borel_measurable M" -proof cases - assume "finite S" - thus ?thesis using assms by induct auto -qed simp - lemma borel_measurable_diff[measurable (raw)]: fixes f :: "'a \ 'b::{second_countable_topology, real_normed_vector}" assumes f: "f \ borel_measurable M" @@ -1291,28 +1425,6 @@ (\x. f x / g x::'b::{second_countable_topology, real_normed_div_algebra}) \ borel_measurable M" by (simp add: divide_inverse) -lemma borel_measurable_max[measurable (raw)]: - "f \ borel_measurable M \ g \ borel_measurable M \ (\x. max (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \ borel_measurable M" - by (simp add: max_def) - -lemma borel_measurable_min[measurable (raw)]: - "f \ borel_measurable M \ g \ borel_measurable M \ (\x. min (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \ borel_measurable M" - by (simp add: min_def) - -lemma borel_measurable_Min[measurable (raw)]: - "finite I \ (\i. i \ I \ f i \ borel_measurable M) \ (\x. Min ((\i. f i x)`I) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \ borel_measurable M" -proof (induct I rule: finite_induct) - case (insert i I) then show ?case - by (cases "I = {}") auto -qed auto - -lemma borel_measurable_Max[measurable (raw)]: - "finite I \ (\i. i \ I \ f i \ borel_measurable M) \ (\x. Max ((\i. f i x)`I) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \ borel_measurable M" -proof (induct I rule: finite_induct) - case (insert i I) then show ?case - by (cases "I = {}") auto -qed auto - lemma borel_measurable_abs[measurable (raw)]: "f \ borel_measurable M \ (\x. \f x :: real\) \ borel_measurable M" unfolding abs_real_def by simp @@ -1538,9 +1650,7 @@ assumes [measurable]: "f \ borel_measurable M" "g \ borel_measurable M" shows borel_measurable_ereal_add: "(\x. f x + g x) \ borel_measurable M" and borel_measurable_ereal_times: "(\x. f x * g x) \ borel_measurable M" - and borel_measurable_ereal_min: "(\x. min (g x) (f x)) \ borel_measurable M" - and borel_measurable_ereal_max: "(\x. max (g x) (f x)) \ borel_measurable M" - by (simp_all add: borel_measurable_ereal2 min_def max_def) + by (simp_all add: borel_measurable_ereal2) lemma [measurable(raw)]: fixes f g :: "'a \ ereal" @@ -1562,54 +1672,67 @@ shows "(\x. \i\S. f i x) \ borel_measurable M" using assms by (induction S rule: infinite_finite_induct) auto -lemma [measurable (raw)]: - fixes f :: "nat \ 'a \ ereal" - assumes "\i. f i \ borel_measurable M" - shows borel_measurable_liminf: "(\x. liminf (\i. f i x)) \ borel_measurable M" - and borel_measurable_limsup: "(\x. limsup (\i. f i x)) \ borel_measurable M" - unfolding liminf_SUP_INF limsup_INF_SUP using assms by auto - -lemma sets_Collect_eventually_sequentially[measurable]: - "(\i. {x\space M. P x i} \ sets M) \ {x\space M. eventually (P x) sequentially} \ sets M" - unfolding eventually_sequentially by simp - -lemma sets_Collect_ereal_convergent[measurable]: - fixes f :: "nat \ 'a => ereal" - assumes f[measurable]: "\i. f i \ borel_measurable M" - shows "{x\space M. convergent (\i. f i x)} \ sets M" - unfolding convergent_ereal by auto - -lemma borel_measurable_extreal_lim[measurable (raw)]: - fixes f :: "nat \ 'a \ ereal" - assumes [measurable]: "\i. f i \ borel_measurable M" - shows "(\x. lim (\i. f i x)) \ borel_measurable M" -proof - - have "\x. lim (\i. f i x) = (if convergent (\i. f i x) then limsup (\i. f i x) else (THE i. False))" - by (simp add: lim_def convergent_def convergent_limsup_cl) - then show ?thesis - by simp -qed - -lemma borel_measurable_ereal_LIMSEQ: - fixes u :: "nat \ 'a \ ereal" - assumes u': "\x. x \ space M \ (\i. u i x) \ u' x" - and u: "\i. u i \ borel_measurable M" - shows "u' \ borel_measurable M" -proof - - have "\x. x \ space M \ u' x = liminf (\n. u n x)" - using u' by (simp add: lim_imp_Liminf[symmetric]) - with u show ?thesis by (simp cong: measurable_cong) -qed - lemma borel_measurable_extreal_suminf[measurable (raw)]: fixes f :: "nat \ 'a \ ereal" assumes [measurable]: "\i. f i \ borel_measurable M" shows "(\x. (\i. f i x)) \ borel_measurable M" unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp +subsection "Borel space on the extended non-negative reals" + +text \ @{type ennreal} is a topological monoid, so no rules for plus are required, also all order + statements are usually done on type classes. \ + +lemma measurable_enn2ereal[measurable]: "enn2ereal \ borel \\<^sub>M borel" + by (intro borel_measurable_continuous_on1 continuous_on_enn2ereal) + +lemma measurable_e2ennreal[measurable]: "e2ennreal \ borel \\<^sub>M borel" + by (intro borel_measurable_continuous_on1 continuous_on_e2ennreal) + +definition [simp]: "is_borel f M \ f \ borel_measurable M" + +lemma is_borel_transfer[transfer_rule]: "rel_fun (rel_fun op = pcr_ennreal) op = is_borel is_borel" + unfolding is_borel_def[abs_def] +proof (safe intro!: rel_funI ext dest!: rel_fun_eq_pcr_ennreal[THEN iffD1]) + fix f and M :: "'a measure" + show "f \ borel_measurable M" if f: "enn2ereal \ f \ borel_measurable M" + using measurable_compose[OF f measurable_e2ennreal] by simp +qed simp + +lemma measurable_ennreal[measurable]: "ennreal \ borel \\<^sub>M borel" + unfolding is_borel_def[symmetric] by transfer simp + +lemma borel_measurable_times_ennreal[measurable (raw)]: + fixes f g :: "'a \ ennreal" + shows "f \ M \\<^sub>M borel \ g \ M \\<^sub>M borel \ (\x. f x * g x) \ M \\<^sub>M borel" + unfolding is_borel_def[symmetric] by transfer simp + +lemma borel_measurable_inverse_ennreal[measurable (raw)]: + fixes f :: "'a \ ennreal" + shows "f \ M \\<^sub>M borel \ (\x. inverse (f x)) \ M \\<^sub>M borel" + unfolding is_borel_def[symmetric] by transfer simp + +lemma borel_measurable_divide_ennreal[measurable (raw)]: + fixes f :: "'a \ ennreal" + shows "f \ M \\<^sub>M borel \ g \ M \\<^sub>M borel \ (\x. f x / g x) \ M \\<^sub>M borel" + unfolding divide_ennreal_def by simp + +lemma borel_measurable_minus_ennreal[measurable (raw)]: + fixes f :: "'a \ ennreal" + shows "f \ M \\<^sub>M borel \ g \ M \\<^sub>M borel \ (\x. f x - g x) \ M \\<^sub>M borel" + unfolding is_borel_def[symmetric] by transfer simp + +lemma borel_measurable_setprod_ennreal[measurable (raw)]: + fixes f :: "'c \ 'a \ ennreal" + assumes "\i. i \ S \ f i \ borel_measurable M" + shows "(\x. \i\S. f i x) \ borel_measurable M" + using assms by (induction S rule: infinite_finite_induct) auto + +hide_const (open) is_borel + subsection \LIMSEQ is borel measurable\ -lemma borel_measurable_LIMSEQ: +lemma borel_measurable_LIMSEQ_real: fixes u :: "nat \ 'a \ real" assumes u': "\x. x \ space M \ (\i. u i x) \ u' x" and u: "\i. u i \ borel_measurable M" @@ -1632,7 +1755,7 @@ fix A :: "'b set" assume "closed A" have [measurable]: "(\x. infdist (g x) A) \ borel_measurable M" - proof (rule borel_measurable_LIMSEQ) + proof (rule borel_measurable_LIMSEQ_real) show "\x. x \ space M \ (\i. infdist (f i x) A) \ infdist (g x) A" by (intro tendsto_infdist lim) show "\i. (\x. infdist (f i x) A) \ borel_measurable M" @@ -1659,7 +1782,7 @@ shows "{x\space M. Cauchy (\i. f i x)} \ sets M" unfolding metric_Cauchy_iff2 using f by auto -lemma borel_measurable_lim[measurable (raw)]: +lemma borel_measurable_lim_metric[measurable (raw)]: fixes f :: "nat \ 'a \ 'b::{banach, second_countable_topology}" assumes f[measurable]: "\i. f i \ borel_measurable M" shows "(\x. lim (\i. f i x)) \ borel_measurable M" @@ -1687,11 +1810,6 @@ shows "(\x. suminf (\i. f i x)) \ borel_measurable M" unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp -lemma borel_measurable_sup[measurable (raw)]: - "f \ borel_measurable M \ g \ borel_measurable M \ - (\x. sup (f x) (g x)::ereal) \ borel_measurable M" - by simp - (* Proof by Jeremy Avigad and Luke Serafin *) lemma isCont_borel: fixes f :: "'b::metric_space \ 'a::metric_space" diff -r de25474ce728 -r 20288ba55e85 src/HOL/Probability/Set_Integral.thy --- a/src/HOL/Probability/Set_Integral.thy Wed Mar 16 13:57:06 2016 +0000 +++ b/src/HOL/Probability/Set_Integral.thy Wed Mar 16 14:05:30 2016 +0000 @@ -363,7 +363,7 @@ done qed auto } then show "(\x. indicator (\i. A i) x *\<^sub>R f x) \ borel_measurable M" - apply (rule borel_measurable_LIMSEQ) + apply (rule borel_measurable_LIMSEQ_real) apply assumption apply (intro borel_measurable_integrable intgbl) done