src/HOL/Probability/Borel_Space.thy

 lemma open_prod_generated: "open = generate_topology {A \<times> B | A B. open A \<and> open B}"
 proof -
   have "{A \<times> B :: ('a \<times> 'b) set | A B. open A \<and> open B} = ((\<lambda>(a, b). a \<times> b) ` ({A. open A} \<times> {A. open A}))"
     by auto
   then show ?thesis
-    by (auto intro: topological_basis_prod topological_basis_trivial topological_basis_imp_subbasis)  
+    by (auto intro: topological_basis_prod topological_basis_trivial topological_basis_imp_subbasis)
 qed
 
 definition "mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s"
 
 lemma mono_onI:

   shows "inj_on f A"
 proof (rule inj_onI)
   fix x y assume "x \<in> A" "y \<in> A" "f x = f y"
   thus "x = y"
     by (cases x y rule: linorder_cases)
-       (auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x]) 
+       (auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x])
 qed
 
 lemma strict_mono_on_leD:
   assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A" "x \<in> A" "y \<in> A" "x \<le> y"
   shows "f x \<le> f y"

       by (cases h rule: linorder_cases[of _ 0])
          (simp_all add: divide_nonpos_neg divide_nonneg_pos mono_onD field_simps)
   qed
 qed simp
 
-lemma strict_mono_on_imp_mono_on: 
+lemma strict_mono_on_imp_mono_on:
   "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A \<Longrightarrow> mono_on f A"
   by (rule mono_onI, rule strict_mono_on_leD)
 
 lemma mono_on_ctble_discont:
   fixes f :: "real \<Rightarrow> real"

         fix x assume "x \<in> A" "x < a"
         with q2 *[of "a - x"] show "f x < real_of_rat q2"
           apply (auto simp add: dist_real_def not_less)
           apply (subgoal_tac "f x \<le> f xa")
           by (auto intro: mono)
-      qed 
+      qed
       thus ?thesis by auto
     next
       fix u assume "u > f a"
       then obtain q2 where q2: "f a < of_rat q2" "of_rat q2 < u"
         using of_rat_dense by blast

         fix x assume "x \<in> A" "x > a"
         with q2 *[of "x - a"] show "f x > real_of_rat q2"
           apply (auto simp add: dist_real_def)
           apply (subgoal_tac "f x \<ge> f xa")
           by (auto intro: mono)
-      qed 
+      qed
       thus ?thesis by auto
     qed
   qed
-  hence "\<exists>g :: real \<Rightarrow> nat \<times> rat . \<forall>a \<in> {a\<in>A. \<not> continuous (at a within A) f}. 
+  hence "\<exists>g :: real \<Rightarrow> nat \<times> rat . \<forall>a \<in> {a\<in>A. \<not> continuous (at a within A) f}.
       (fst (g a) = 0 \<and> of_rat (snd (g a)) < f a \<and> (\<forall>x \<in> A. x < a \<longrightarrow> f x < of_rat (snd (g a)))) |
       (fst (g a) = 1 \<and> of_rat (snd (g a)) > f a \<and> (\<forall>x \<in> A. x > a \<longrightarrow> f x > of_rat (snd (g a))))"
     by (rule bchoice)
   then guess g ..
   hence g: "\<And>a x. a \<in> A \<Longrightarrow> \<not> continuous (at a within A) f \<Longrightarrow> x \<in> A \<Longrightarrow>

   proof (auto simp add: inj_on_def)
     fix w z
     assume 1: "w \<in> A" and 2: "\<not> continuous (at w within A) f" and
            3: "z \<in> A" and 4: "\<not> continuous (at z within A) f" and
            5: "g w = g z"
-    from g [OF 1 2 3] g [OF 3 4 1] 5 
+    from g [OF 1 2 3] g [OF 3 4 1] 5
     show "w = z" by auto
   qed
-  thus ?thesis 
-    by (rule countableI') 
+  thus ?thesis
+    by (rule countableI')
 qed
 
 lemma mono_on_ctble_discont_open:
   fixes f :: "real \<Rightarrow> real"
   fixes A :: "real set"

 lemma closure_contains_Sup:
   fixes S :: "real set"
   assumes "S \<noteq> {}" "bdd_above S"
   shows "Sup S \<in> closure S"
 proof-
-  have "Inf (uminus ` S) \<in> closure (uminus ` S)" 
+  have "Inf (uminus ` S) \<in> closure (uminus ` S)"
       using assms by (intro closure_contains_Inf) auto
   also have "Inf (uminus ` S) = -Sup S" by (simp add: Inf_real_def)
   also have "closure (uminus ` S) = uminus ` closure S"
       by (rule sym, intro closure_injective_linear_image) (auto intro: linearI)
   finally show ?thesis by auto

   assumes ab: "a \<le> b"
   shows "g a \<le> g b"
 proof (cases "a < b")
   assume "a < b"
   from deriv have "\<forall>x. x \<ge> a \<and> x \<le> b \<longrightarrow> (g has_real_derivative g' x) (at x)" by simp
-  from MVT2[OF \<open>a < b\<close> this] and deriv 
+  from MVT2[OF \<open>a < b\<close> this] and deriv
     obtain \<xi> where \<xi>_ab: "\<xi> > a" "\<xi> < b" and g_ab: "g b - g a = (b - a) * g' \<xi>" by blast
   from \<xi>_ab ab nonneg have "(b - a) * g' \<xi> \<ge> 0" by simp
   with g_ab show ?thesis by simp
 qed (insert ab, simp)
 

   assumes "continuous_on {a::real..b} g" and mono: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
   assumes "a \<le> b" "(c::real) \<le> d" "{c..d} \<subseteq> {g a..g b}"
   obtains c' d' where "{a..b} \<inter> g -` {c..d} = {c'..d'}" "c' \<le> d'" "g c' = c" "g d' = d"
 proof-
     let ?A = "{a..b} \<inter> g -` {c..d}"
-    from IVT'[of g a c b, OF _ _ \<open>a \<le> b\<close> assms(1)] assms(4,5) 
+    from IVT'[of g a c b, OF _ _ \<open>a \<le> b\<close> assms(1)] assms(4,5)
          obtain c'' where c'': "c'' \<in> ?A" "g c'' = c" by auto
-    from IVT'[of g a d b, OF _ _ \<open>a \<le> b\<close> assms(1)] assms(4,5) 
+    from IVT'[of g a d b, OF _ _ \<open>a \<le> b\<close> assms(1)] assms(4,5)
          obtain d'' where d'': "d'' \<in> ?A" "g d'' = d" by auto
     hence [simp]: "?A \<noteq> {}" by blast
 
     def c' \<equiv> "Inf ?A" and d' \<equiv> "Sup ?A"
     have "?A \<subseteq> {c'..d'}" unfolding c'_def d'_def
         by (intro subsetI) (auto intro: cInf_lower cSup_upper)
-    moreover from assms have "closed ?A" 
+    moreover from assms have "closed ?A"
         using continuous_on_closed_vimage[of "{a..b}" g] by (subst Int_commute) simp
     hence c'd'_in_set: "c' \<in> ?A" "d' \<in> ?A" unfolding c'_def d'_def
         by ((intro closed_contains_Inf closed_contains_Sup, simp_all)[])+
-    hence "{c'..d'} \<subseteq> ?A" using assms 
+    hence "{c'..d'} \<subseteq> ?A" using assms
         by (intro subsetI)
-           (auto intro!: order_trans[of c "g c'" "g x" for x] order_trans[of "g x" "g d'" d for x] 
+           (auto intro!: order_trans[of c "g c'" "g x" for x] order_trans[of "g x" "g d'" d for x]
                  intro!: mono)
     moreover have "c' \<le> d'" using c'd'_in_set(2) unfolding c'_def by (intro cInf_lower) auto
     moreover have "g c' \<le> c" "g d' \<ge> d"
       apply (insert c'' d'' c'd'_in_set)
       apply (subst c''(2)[symmetric])

     ultimately show ?thesis using that by blast
 qed
 
 subsection \<open>Generic Borel spaces\<close>
 
-definition borel :: "'a::topological_space measure" where
+definition (in topological_space) borel :: "'a measure" where
   "borel = sigma UNIV {S. open S}"
 
 abbreviation "borel_measurable M \<equiv> measurable M borel"
 
 lemma in_borel_measurable:

     and borel_measurable_eq[measurable]: "{w \<in> space M. f w = g w} \<in> sets M"
     and borel_measurable_neq: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
   unfolding eq_iff not_less[symmetric]
   by measurable
 
-lemma 
+lemma
   fixes i :: "'a::{second_countable_topology, real_inner}"
   shows hafspace_less_borel: "{x. a < x \<bullet> i} \<in> sets borel"
     and hafspace_greater_borel: "{x. x \<bullet> i < a} \<in> sets borel"
     and hafspace_less_eq_borel: "{x. a \<le> x \<bullet> i} \<in> sets borel"
     and hafspace_greater_eq_borel: "{x. x \<bullet> i \<le> a} \<in> sets borel"

     done
 qed (auto simp: box_def)
 
 lemma halfspace_gt_in_halfspace:
   assumes i: "i \<in> A"
-  shows "{x::'a. a < x \<bullet> i} \<in> 
+  shows "{x::'a. a < x \<bullet> i} \<in>
     sigma_sets UNIV ((\<lambda> (a, i). {x::'a::euclidean_space. x \<bullet> i < a}) ` (UNIV \<times> A))"
   (is "?set \<in> ?SIGMA")
 proof -
   interpret sigma_algebra UNIV ?SIGMA
     by (intro sigma_algebra_sigma_sets) simp_all

 proof (rule borel_eq_sigmaI5[OF borel_eq_atMost])
   fix i :: real
   have "{..i} = (\<Union>j::nat. {-j <.. i})"
     by (auto simp: minus_less_iff reals_Archimedean2)
   also have "\<dots> \<in> sets (sigma UNIV (range (\<lambda>(i, j). {i<..j})))"
-    by (intro sets.countable_nat_UN) auto 
+    by (intro sets.countable_nat_UN) auto
   finally show "{..i} \<in> sets (sigma UNIV (range (\<lambda>(i, j). {i<..j})))" .
 qed simp
 
 lemma eucl_lessThan: "{x::real. x <e a} = lessThan a"
   by (simp add: eucl_less_def lessThan_def)

 qed simp_all
 
 lemma borel_measurable_halfspacesI:
   fixes f :: "'a \<Rightarrow> 'c::euclidean_space"
   assumes F: "borel = sigma UNIV (F ` (UNIV \<times> Basis))"
-  and S_eq: "\<And>a i. S a i = f -` F (a,i) \<inter> space M" 
+  and S_eq: "\<And>a i. S a i = f -` F (a,i) \<inter> space M"
   shows "f \<in> borel_measurable M = (\<forall>i\<in>Basis. \<forall>a::real. S a i \<in> sets M)"
 proof safe
   fix a :: real and i :: 'b assume i: "i \<in> Basis" and f: "f \<in> borel_measurable M"
   then show "S a i \<in> sets M" unfolding assms
     by (auto intro!: measurable_sets simp: assms(1))

   then show "f \<in> borel_measurable M"
     by (subst borel_measurable_iff_halfspace_le) auto
 qed auto
 
 lemma borel_set_induct[consumes 1, case_names empty interval compl union]:
-  assumes "A \<in> sets borel" 
+  assumes "A \<in> sets borel"
   assumes empty: "P {}" and int: "\<And>a b. a \<le> b \<Longrightarrow> P {a..b}" and compl: "\<And>A. A \<in> sets borel \<Longrightarrow> P A \<Longrightarrow> P (-A)" and
           un: "\<And>f. disjoint_family f \<Longrightarrow> (\<And>i. f i \<in> sets borel) \<Longrightarrow>  (\<And>i. P (f i)) \<Longrightarrow> P (\<Union>i::nat. f i)"
   shows "P (A::real set)"
 proof-
   let ?G = "range (\<lambda>(a,b). {a..b::real})"
-  have "Int_stable ?G" "?G \<subseteq> Pow UNIV" "A \<in> sigma_sets UNIV ?G" 
+  have "Int_stable ?G" "?G \<subseteq> Pow UNIV" "A \<in> 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) 
+  proof (induction rule: sigma_sets_induct_disjoint)
     case (union f)
       from union.hyps(2) have "\<And>i. f i \<in> sets borel" by (auto simp: borel_eq_atLeastAtMost)
       with union show ?case by (auto intro: un)
   next
     case (basic A)

   fixes g f :: "'a \<Rightarrow> 'b::{second_countable_topology, metric_space}"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. dist (f x) (g x)) \<in> borel_measurable M"
   using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
-  
+
 lemma borel_measurable_scaleR[measurable (raw)]:
   fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M"

   "(\<lambda>x::real^'n. x $ i) \<in> borel_measurable borel"
   by (simp add: cart_eq_inner_axis)
 
 lemma convex_measurable:
   fixes A :: "'a :: euclidean_space set"
-  shows "X \<in> borel_measurable M \<Longrightarrow> X ` space M \<subseteq> A \<Longrightarrow> open A \<Longrightarrow> convex_on A q \<Longrightarrow> 
+  shows "X \<in> borel_measurable M \<Longrightarrow> X ` space M \<subseteq> A \<Longrightarrow> open A \<Longrightarrow> convex_on A q \<Longrightarrow>
     (\<lambda>x. q (X x)) \<in> borel_measurable M"
   by (rule measurable_compose[where f=X and N="restrict_space borel A"])
      (auto intro!: borel_measurable_continuous_on_restrict convex_on_continuous measurable_restrict_space2)
 
 lemma borel_measurable_ln[measurable (raw)]:

 lemma borel_measurable_ereal[measurable (raw)]:
   assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
   using continuous_on_ereal f by (rule borel_measurable_continuous_on) (rule continuous_on_id)
 
 lemma borel_measurable_real_of_ereal[measurable (raw)]:
-  fixes f :: "'a \<Rightarrow> ereal" 
+  fixes f :: "'a \<Rightarrow> ereal"
   assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. real_of_ereal (f x)) \<in> borel_measurable M"
   apply (rule measurable_compose[OF f])
   apply (rule borel_measurable_continuous_countable_exceptions[of "{\<infinity>, -\<infinity> }"])
   apply (auto intro: continuous_on_real simp: Compl_eq_Diff_UNIV)
   done
 
 lemma borel_measurable_ereal_cases:
-  fixes f :: "'a \<Rightarrow> ereal" 
+  fixes f :: "'a \<Rightarrow> ereal"
   assumes f: "f \<in> borel_measurable M"
   assumes H: "(\<lambda>x. H (ereal (real_of_ereal (f x)))) \<in> borel_measurable M"
   shows "(\<lambda>x. H (f x)) \<in> borel_measurable M"
 proof -
   let ?F = "\<lambda>x. if f x = \<infinity> then H \<infinity> else if f x = - \<infinity> then H (-\<infinity>) else H (ereal (real_of_ereal (f x)))"

 proof
   assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp
 qed auto
 
 lemma set_Collect_ereal2:
-  fixes f g :: "'a \<Rightarrow> ereal" 
+  fixes f g :: "'a \<Rightarrow> ereal"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   assumes H: "{x \<in> space M. H (ereal (real_of_ereal (f x))) (ereal (real_of_ereal (g x)))} \<in> sets M"
     "{x \<in> space borel. H (-\<infinity>) (ereal x)} \<in> sets borel"
     "{x \<in> space borel. H (\<infinity>) (ereal x)} \<in> sets borel"

 lemma borel_measurable_iff_Ici_ereal:
   "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a..} \<inter> space M \<in> sets M)"
   unfolding borel_measurable_ereal_iff_Iio vimage_sets_compl_iff[where A="{..< a}" for a] by simp
 
 lemma borel_measurable_ereal2:
-  fixes f g :: "'a \<Rightarrow> ereal" 
+  fixes f g :: "'a \<Rightarrow> ereal"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   assumes H: "(\<lambda>x. H (ereal (real_of_ereal (f x))) (ereal (real_of_ereal (g x)))) \<in> borel_measurable M"
     "(\<lambda>x. H (-\<infinity>) (ereal (real_of_ereal (g x)))) \<in> borel_measurable M"
     "(\<lambda>x. H (\<infinity>) (ereal (real_of_ereal (g x)))) \<in> borel_measurable M"

 
 lemma sets_Collect_eventually_sequentially[measurable]:
   "(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"
   unfolding eventually_sequentially by simp
 
-lemma sets_Collect_ereal_convergent[measurable]: 
+lemma sets_Collect_ereal_convergent[measurable]:
   fixes f :: "nat \<Rightarrow> 'a => ereal"
   assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
   shows "{x\<in>space M. convergent (\<lambda>i. f i x)} \<in> sets M"
   unfolding convergent_ereal by auto
 

   assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
   assumes lim: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. f i x) \<longlonglongrightarrow> g x"
   shows "g \<in> borel_measurable M"
   unfolding borel_eq_closed
 proof (safe intro!: measurable_measure_of)
-  fix A :: "'b set" assume "closed A" 
+  fix A :: "'b set" assume "closed A"
 
   have [measurable]: "(\<lambda>x. infdist (g x) A) \<in> borel_measurable M"
   proof (rule borel_measurable_LIMSEQ)
     show "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. infdist (f i x) A) \<longlonglongrightarrow> infdist (g x) A"
       by (intro tendsto_infdist lim)

       by measurable
     finally show ?thesis .
   qed simp
 qed auto
 
-lemma sets_Collect_Cauchy[measurable]: 
+lemma sets_Collect_Cauchy[measurable]:
   fixes f :: "nat \<Rightarrow> 'a => 'b::{metric_space, second_countable_topology}"
   assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
   shows "{x\<in>space M. Cauchy (\<lambda>i. f i x)} \<in> sets M"
   unfolding metric_Cauchy_iff2 using f by auto
 

     fix x
     have "convergent (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
       by (cases "Cauchy (\<lambda>i. f i x)")
          (auto simp add: convergent_eq_cauchy[symmetric] convergent_def)
     then show "(\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0) \<longlonglongrightarrow> u' x"
-      unfolding u'_def 
+      unfolding u'_def
       by (rule convergent_LIMSEQ_iff[THEN iffD1])
   qed measurable
   then show ?thesis
     unfolding * by measurable
 qed

         by (metis reals_Archimedean)
       assume "\<forall>i. \<exists>j. \<forall>y z. dist x y < ?I j \<and> dist x z < ?I j \<longrightarrow> dist (f y) (f z) \<le> ?I i"
       from this[THEN spec, of "Suc n"]
       obtain j where j: "\<And>y z. dist x y < ?I j \<Longrightarrow> dist x z < ?I j \<Longrightarrow> dist (f y) (f z) \<le> ?I (Suc n)"
         by auto
-      
+
       show "\<exists>d>0. \<forall>y. dist y x < d \<longrightarrow> dist (f y) (f x) < e"
       proof (safe intro!: exI[of _ "?I j"])
         fix y assume "dist y x < ?I j"
         then have "dist (f y) (f x) \<le> ?I (Suc n)"
           by (intro j) (auto simp: dist_commute)

   assumes "mono_on f A"
   shows "f \<in> borel_measurable (restrict_space borel A)"
   apply (rule measurable_restrict_countable[OF mono_on_ctble_discont[OF assms]])
   apply (auto intro!: image_eqI[where x="{x}" for x] simp: sets_restrict_space)
   apply (auto simp add: sets_restrict_restrict_space continuous_on_eq_continuous_within
-              cong: measurable_cong_sets 
+              cong: measurable_cong_sets
               intro!: borel_measurable_continuous_on_restrict intro: continuous_within_subset)
   done
 
 lemma borel_measurable_mono:
   fixes f :: "real \<Rightarrow> real"