src/HOL/Probability/Borel.thy

Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.

(* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *)

header {*Borel spaces*}

theory Borel
  imports Sigma_Algebra Positive_Infinite_Real Multivariate_Analysis
begin

section "Generic Borel spaces"

definition "borel_space = sigma (UNIV::'a::topological_space set) open"
abbreviation "borel_measurable M \<equiv> measurable M borel_space"

interpretation borel_space: sigma_algebra borel_space
  using sigma_algebra_sigma by (auto simp: borel_space_def)

lemma in_borel_measurable:
   "f \<in> borel_measurable M \<longleftrightarrow>
    (\<forall>S \<in> sets (sigma UNIV open).
      f -` S \<inter> space M \<in> sets M)"
  by (auto simp add: measurable_def borel_space_def)

lemma in_borel_measurable_borel_space:
   "f \<in> borel_measurable M \<longleftrightarrow>
    (\<forall>S \<in> sets borel_space.
      f -` S \<inter> space M \<in> sets M)"
  by (auto simp add: measurable_def borel_space_def)

lemma space_borel_space[simp]: "space borel_space = UNIV"
  unfolding borel_space_def by auto

lemma borel_space_open[simp]:
  assumes "open A" shows "A \<in> sets borel_space"
proof -
  have "A \<in> open" unfolding mem_def using assms .
  thus ?thesis unfolding borel_space_def sigma_def by (auto intro!: sigma_sets.Basic)
qed

lemma borel_space_closed[simp]:
  assumes "closed A" shows "A \<in> sets borel_space"
proof -
  have "space borel_space - (- A) \<in> sets borel_space"
    using assms unfolding closed_def by (blast intro: borel_space_open)
  thus ?thesis by simp
qed

lemma (in sigma_algebra) borel_measurable_vimage:
  fixes f :: "'a \<Rightarrow> 'x::t2_space"
  assumes borel: "f \<in> borel_measurable M"
  shows "f -` {x} \<inter> space M \<in> sets M"
proof (cases "x \<in> f ` space M")
  case True then obtain y where "x = f y" by auto
  from closed_sing[of "f y"]
  have "{f y} \<in> sets borel_space" by (rule borel_space_closed)
  with assms show ?thesis
    unfolding in_borel_measurable_borel_space `x = f y` by auto
next
  case False hence "f -` {x} \<inter> space M = {}" by auto
  thus ?thesis by auto
qed

lemma (in sigma_algebra) borel_measurableI:
  fixes f :: "'a \<Rightarrow> 'x\<Colon>topological_space"
  assumes "\<And>S. open S \<Longrightarrow> f -` S \<inter> space M \<in> sets M"
  shows "f \<in> borel_measurable M"
  unfolding borel_space_def
proof (rule measurable_sigma)
  fix S :: "'x set" assume "S \<in> open" thus "f -` S \<inter> space M \<in> sets M"
    using assms[of S] by (simp add: mem_def)
qed simp_all

lemma borel_space_singleton[simp, intro]:
  fixes x :: "'a::t1_space"
  shows "A \<in> sets borel_space \<Longrightarrow> insert x A \<in> sets borel_space"
  proof (rule borel_space.insert_in_sets)
    show "{x} \<in> sets borel_space"
      using closed_sing[of x] by (rule borel_space_closed)
  qed simp

lemma (in sigma_algebra) borel_measurable_const[simp, intro]:
  "(\<lambda>x. c) \<in> borel_measurable M"
  by (auto intro!: measurable_const)

lemma (in sigma_algebra) borel_measurable_indicator:
  assumes A: "A \<in> sets M"
  shows "indicator A \<in> borel_measurable M"
  unfolding indicator_def_raw using A
  by (auto intro!: measurable_If_set borel_measurable_const)

lemma borel_measurable_translate:
  assumes "A \<in> sets borel_space" and trans: "\<And>B. open B \<Longrightarrow> f -` B \<in> sets borel_space"
  shows "f -` A \<in> sets borel_space"
proof -
  have "A \<in> sigma_sets UNIV open" using assms
    by (simp add: borel_space_def sigma_def)
  thus ?thesis
  proof (induct rule: sigma_sets.induct)
    case (Basic a) thus ?case using trans[of a] by (simp add: mem_def)
  next
    case (Compl a)
    moreover have "UNIV \<in> sets borel_space"
      by (metis borel_space.top borel_space_def_raw mem_def space_sigma)
    ultimately show ?case
      by (auto simp: vimage_Diff borel_space.Diff)
  qed (auto simp add: vimage_UN)
qed

section "Borel spaces on euclidean spaces"

lemma lessThan_borel[simp, intro]:
  fixes a :: "'a\<Colon>ordered_euclidean_space"
  shows "{..< a} \<in> sets borel_space"
  by (blast intro: borel_space_open)

lemma greaterThan_borel[simp, intro]:
  fixes a :: "'a\<Colon>ordered_euclidean_space"
  shows "{a <..} \<in> sets borel_space"
  by (blast intro: borel_space_open)

lemma greaterThanLessThan_borel[simp, intro]:
  fixes a b :: "'a\<Colon>ordered_euclidean_space"
  shows "{a<..<b} \<in> sets borel_space"
  by (blast intro: borel_space_open)

lemma atMost_borel[simp, intro]:
  fixes a :: "'a\<Colon>ordered_euclidean_space"
  shows "{..a} \<in> sets borel_space"
  by (blast intro: borel_space_closed)

lemma atLeast_borel[simp, intro]:
  fixes a :: "'a\<Colon>ordered_euclidean_space"
  shows "{a..} \<in> sets borel_space"
  by (blast intro: borel_space_closed)

lemma atLeastAtMost_borel[simp, intro]:
  fixes a b :: "'a\<Colon>ordered_euclidean_space"
  shows "{a..b} \<in> sets borel_space"
  by (blast intro: borel_space_closed)

lemma greaterThanAtMost_borel[simp, intro]:
  fixes a b :: "'a\<Colon>ordered_euclidean_space"
  shows "{a<..b} \<in> sets borel_space"
  unfolding greaterThanAtMost_def by blast

lemma atLeastLessThan_borel[simp, intro]:
  fixes a b :: "'a\<Colon>ordered_euclidean_space"
  shows "{a..<b} \<in> sets borel_space"
  unfolding atLeastLessThan_def by blast

lemma hafspace_less_borel[simp, intro]:
  fixes a :: real
  shows "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel_space"
  by (auto intro!: borel_space_open open_halfspace_component_gt)

lemma hafspace_greater_borel[simp, intro]:
  fixes a :: real
  shows "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel_space"
  by (auto intro!: borel_space_open open_halfspace_component_lt)

lemma hafspace_less_eq_borel[simp, intro]:
  fixes a :: real
  shows "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel_space"
  by (auto intro!: borel_space_closed closed_halfspace_component_ge)

lemma hafspace_greater_eq_borel[simp, intro]:
  fixes a :: real
  shows "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel_space"
  by (auto intro!: borel_space_closed closed_halfspace_component_le)

lemma (in sigma_algebra) borel_measurable_less[simp, intro]:
  fixes f :: "'a \<Rightarrow> real"
  assumes f: "f \<in> borel_measurable M"
  assumes g: "g \<in> borel_measurable M"
  shows "{w \<in> space M. f w < g w} \<in> sets M"
proof -
  have "{w \<in> space M. f w < g w} =
        (\<Union>r. (f -` {..< of_rat r} \<inter> space M) \<inter> (g -` {of_rat r <..} \<inter> space M))"
    using Rats_dense_in_real by (auto simp add: Rats_def)
  then show ?thesis using f g
    by simp (blast intro: measurable_sets)
qed

lemma (in sigma_algebra) borel_measurable_le[simp, intro]:
  fixes f :: "'a \<Rightarrow> real"
  assumes f: "f \<in> borel_measurable M"
  assumes g: "g \<in> borel_measurable M"
  shows "{w \<in> space M. f w \<le> g w} \<in> sets M"
proof -
  have "{w \<in> space M. f w \<le> g w} = space M - {w \<in> space M. g w < f w}"
    by auto
  thus ?thesis using f g
    by simp blast
qed

lemma (in sigma_algebra) borel_measurable_eq[simp, intro]:
  fixes f :: "'a \<Rightarrow> real"
  assumes f: "f \<in> borel_measurable M"
  assumes g: "g \<in> borel_measurable M"
  shows "{w \<in> space M. f w = g w} \<in> sets M"
proof -
  have "{w \<in> space M. f w = g w} =
        {w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
    by auto
  thus ?thesis using f g by auto
qed

lemma (in sigma_algebra) borel_measurable_neq[simp, intro]:
  fixes f :: "'a \<Rightarrow> real"
  assumes f: "f \<in> borel_measurable M"
  assumes g: "g \<in> borel_measurable M"
  shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
proof -
  have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}"
    by auto
  thus ?thesis using f g by auto
qed

subsection "Borel space equals sigma algebras over intervals"

lemma rational_boxes:
  fixes x :: "'a\<Colon>ordered_euclidean_space"
  assumes "0 < e"
  shows "\<exists>a b. (\<forall>i. a $$ i \<in> \<rat>) \<and> (\<forall>i. b $$ i \<in> \<rat>) \<and> x \<in> {a <..< b} \<and> {a <..< b} \<subseteq> ball x e"
proof -
  def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
  then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos)
  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x $$ i \<and> x $$ i - y < e'" (is "\<forall>i. ?th i")
  proof
    fix i from Rats_dense_in_real[of "x $$ i - e'" "x $$ i"] e
    show "?th i" by auto
  qed
  from choice[OF this] guess a .. note a = this
  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x $$ i < y \<and> y - x $$ i < e'" (is "\<forall>i. ?th i")
  proof
    fix i from Rats_dense_in_real[of "x $$ i" "x $$ i + e'"] e
    show "?th i" by auto
  qed
  from choice[OF this] guess b .. note b = this
  { fix y :: 'a assume *: "Chi a < y" "y < Chi b"
    have "dist x y = sqrt (\<Sum>i<DIM('a). (dist (x $$ i) (y $$ i))\<twosuperior>)"
      unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
    also have "\<dots> < sqrt (\<Sum>i<DIM('a). e^2 / real (DIM('a)))"
    proof (rule real_sqrt_less_mono, rule setsum_strict_mono)
      fix i assume i: "i \<in> {..<DIM('a)}"
      have "a i < y$$i \<and> y$$i < b i" using * i eucl_less[where 'a='a] by auto
      moreover have "a i < x$$i" "x$$i - a i < e'" using a by auto
      moreover have "x$$i < b i" "b i - x$$i < e'" using b by auto
      ultimately have "\<bar>x$$i - y$$i\<bar> < 2 * e'" by auto
      then have "dist (x $$ i) (y $$ i) < e/sqrt (real (DIM('a)))"
        unfolding e'_def by (auto simp: dist_real_def)
      then have "(dist (x $$ i) (y $$ i))\<twosuperior> < (e/sqrt (real (DIM('a))))\<twosuperior>"
        by (rule power_strict_mono) auto
      then show "(dist (x $$ i) (y $$ i))\<twosuperior> < e\<twosuperior> / real DIM('a)"
        by (simp add: power_divide)
    qed auto
    also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat DIM_positive)
    finally have "dist x y < e" . }
  with a b show ?thesis
    apply (rule_tac exI[of _ "Chi a"])
    apply (rule_tac exI[of _ "Chi b"])
    using eucl_less[where 'a='a] by auto
qed

lemma ex_rat_list:
  fixes x :: "'a\<Colon>ordered_euclidean_space"
  assumes "\<And> i. x $$ i \<in> \<rat>"
  shows "\<exists> r. length r = DIM('a) \<and> (\<forall> i < DIM('a). of_rat (r ! i) = x $$ i)"
proof -
  have "\<forall>i. \<exists>r. x $$ i = of_rat r" using assms unfolding Rats_def by blast
  from choice[OF this] guess r ..
  then show ?thesis by (auto intro!: exI[of _ "map r [0 ..< DIM('a)]"])
qed

lemma open_UNION:
  fixes M :: "'a\<Colon>ordered_euclidean_space set"
  assumes "open M"
  shows "M = UNION {(a, b) | a b. {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)} \<subseteq> M}
                   (\<lambda> (a, b). {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)})"
    (is "M = UNION ?idx ?box")
proof safe
  fix x assume "x \<in> M"
  obtain e where e: "e > 0" "ball x e \<subseteq> M"
    using openE[OF assms `x \<in> M`] by auto
  then obtain a b where ab: "x \<in> {a <..< b}" "\<And>i. a $$ i \<in> \<rat>" "\<And>i. b $$ i \<in> \<rat>" "{a <..< b} \<subseteq> ball x e"
    using rational_boxes[OF e(1)] by blast
  then obtain p q where pq: "length p = DIM ('a)"
                            "length q = DIM ('a)"
                            "\<forall> i < DIM ('a). of_rat (p ! i) = a $$ i \<and> of_rat (q ! i) = b $$ i"
    using ex_rat_list[OF ab(2)] ex_rat_list[OF ab(3)] by blast
  hence p: "Chi (of_rat \<circ> op ! p) = a"
    using euclidean_eq[of "Chi (of_rat \<circ> op ! p)" a]
    unfolding o_def by auto
  from pq have q: "Chi (of_rat \<circ> op ! q) = b"
    using euclidean_eq[of "Chi (of_rat \<circ> op ! q)" b]
    unfolding o_def by auto
  have "x \<in> ?box (p, q)"
    using p q ab by auto
  thus "x \<in> UNION ?idx ?box" using ab e p q exI[of _ p] exI[of _ q] by auto
qed auto

lemma halfspace_span_open:
  "sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})))
    \<subseteq> sets borel_space"
  by (auto intro!: borel_space.sigma_sets_subset[simplified] borel_space_open
                   open_halfspace_component_lt simp: sets_sigma)

lemma halfspace_lt_in_halfspace:
  "{x\<Colon>'a. x $$ i < a} \<in> sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})))"
  unfolding sets_sigma by (rule sigma_sets.Basic) auto

lemma halfspace_gt_in_halfspace:
  "{x\<Colon>'a. a < x $$ i} \<in> sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a})))"
    (is "?set \<in> sets ?SIGMA")
proof -
  interpret sigma_algebra ?SIGMA by (rule sigma_algebra_sigma) simp
  have *: "?set = (\<Union>n. space ?SIGMA - {x\<Colon>'a. x $$ i < a + 1 / real (Suc n)})"
  proof (safe, simp_all add: not_less)
    fix x assume "a < x $$ i"
    with reals_Archimedean[of "x $$ i - a"]
    obtain n where "a + 1 / real (Suc n) < x $$ i"
      by (auto simp: inverse_eq_divide field_simps)
    then show "\<exists>n. a + 1 / real (Suc n) \<le> x $$ i"
      by (blast intro: less_imp_le)
  next
    fix x n
    have "a < a + 1 / real (Suc n)" by auto
    also assume "\<dots> \<le> x"
    finally show "a < x" .
  qed
  show "?set \<in> sets ?SIGMA" unfolding *
    by (safe intro!: countable_UN Diff halfspace_lt_in_halfspace)
qed

lemma (in sigma_algebra) sets_sigma_subset:
  assumes "A = space M"
  assumes "B \<subseteq> sets M"
  shows "sets (sigma A B) \<subseteq> sets M"
  by (unfold assms sets_sigma, rule sigma_sets_subset, rule assms)

lemma open_span_halfspace:
  "sets borel_space \<subseteq> sets (sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x $$ i < a})))"
    (is "_ \<subseteq> sets ?SIGMA")
proof (unfold borel_space_def, rule sigma_algebra.sets_sigma_subset, safe)
  show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) simp
  then interpret sigma_algebra ?SIGMA .
  fix S :: "'a set" assume "S \<in> open" then have "open S" unfolding mem_def .
  from open_UNION[OF this]
  obtain I where *: "S =
    (\<Union>(a, b)\<in>I.
        (\<Inter> i<DIM('a). {x. (Chi (real_of_rat \<circ> op ! a)::'a) $$ i < x $$ i}) \<inter>
        (\<Inter> i<DIM('a). {x. x $$ i < (Chi (real_of_rat \<circ> op ! b)::'a) $$ i}))"
    unfolding greaterThanLessThan_def
    unfolding eucl_greaterThan_eq_halfspaces[where 'a='a]
    unfolding eucl_lessThan_eq_halfspaces[where 'a='a]
    by blast
  show "S \<in> sets ?SIGMA"
    unfolding *
    by (auto intro!: countable_UN Int countable_INT halfspace_lt_in_halfspace halfspace_gt_in_halfspace)
qed auto

lemma halfspace_span_halfspace_le:
  "sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a}))) \<subseteq>
   sets (sigma UNIV (range (\<lambda> (a, i). {x. x $$ i \<le> a})))"
  (is "_ \<subseteq> sets ?SIGMA")
proof (rule sigma_algebra.sets_sigma_subset, safe)
  show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
  then interpret sigma_algebra ?SIGMA .
  fix a i
  have *: "{x::'a. x$$i < a} = (\<Union>n. {x. x$$i \<le> a - 1/real (Suc n)})"
  proof (safe, simp_all)
    fix x::'a assume *: "x$$i < a"
    with reals_Archimedean[of "a - x$$i"]
    obtain n where "x $$ i < a - 1 / (real (Suc n))"
      by (auto simp: field_simps inverse_eq_divide)
    then show "\<exists>n. x $$ i \<le> a - 1 / (real (Suc n))"
      by (blast intro: less_imp_le)
  next
    fix x::'a and n
    assume "x$$i \<le> a - 1 / real (Suc n)"
    also have "\<dots> < a" by auto
    finally show "x$$i < a" .
  qed
  show "{x. x$$i < a} \<in> sets ?SIGMA" unfolding *
    by (safe intro!: countable_UN)
       (auto simp: sets_sigma intro!: sigma_sets.Basic)
qed auto

lemma halfspace_span_halfspace_ge:
  "sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i < a}))) \<subseteq> 
   sets (sigma UNIV (range (\<lambda> (a, i). {x. a \<le> x $$ i})))"
  (is "_ \<subseteq> sets ?SIGMA")
proof (rule sigma_algebra.sets_sigma_subset, safe)
  show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
  then interpret sigma_algebra ?SIGMA .
  fix a i have *: "{x::'a. x$$i < a} = space ?SIGMA - {x::'a. a \<le> x$$i}" by auto
  show "{x. x$$i < a} \<in> sets ?SIGMA" unfolding *
    by (safe intro!: Diff)
       (auto simp: sets_sigma intro!: sigma_sets.Basic)
qed auto

lemma halfspace_le_span_halfspace_gt:
  "sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i \<le> a}))) \<subseteq> 
   sets (sigma UNIV (range (\<lambda> (a, i). {x. a < x $$ i})))"
  (is "_ \<subseteq> sets ?SIGMA")
proof (rule sigma_algebra.sets_sigma_subset, safe)
  show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
  then interpret sigma_algebra ?SIGMA .
  fix a i have *: "{x::'a. x$$i \<le> a} = space ?SIGMA - {x::'a. a < x$$i}" by auto
  show "{x. x$$i \<le> a} \<in> sets ?SIGMA" unfolding *
    by (safe intro!: Diff)
       (auto simp: sets_sigma intro!: sigma_sets.Basic)
qed auto

lemma halfspace_le_span_atMost:
  "sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i \<le> a}))) \<subseteq>
   sets (sigma UNIV (range (\<lambda>a. {..a\<Colon>'a\<Colon>ordered_euclidean_space})))"
  (is "_ \<subseteq> sets ?SIGMA")
proof (rule sigma_algebra.sets_sigma_subset, safe)
  show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
  then interpret sigma_algebra ?SIGMA .
  fix a i
  show "{x. x$$i \<le> a} \<in> sets ?SIGMA"
  proof cases
    assume "i < DIM('a)"
    then have *: "{x::'a. x$$i \<le> a} = (\<Union>k::nat. {.. (\<chi>\<chi> n. if n = i then a else real k)})"
    proof (safe, simp_all add: eucl_le[where 'a='a] split: split_if_asm)
      fix x
      from real_arch_simple[of "Max ((\<lambda>i. x$$i)`{..<DIM('a)})"] guess k::nat ..
      then have "\<And>i. i < DIM('a) \<Longrightarrow> x$$i \<le> real k"
        by (subst (asm) Max_le_iff) auto
      then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> x $$ ia \<le> real k"
        by (auto intro!: exI[of _ k])
    qed
    show "{x. x$$i \<le> a} \<in> sets ?SIGMA" unfolding *
      by (safe intro!: countable_UN)
         (auto simp: sets_sigma intro!: sigma_sets.Basic)
  next
    assume "\<not> i < DIM('a)"
    then show "{x. x$$i \<le> a} \<in> sets ?SIGMA"
      using top by auto
  qed
qed auto

lemma halfspace_le_span_greaterThan:
  "sets (sigma UNIV (range (\<lambda> (a, i). {x\<Colon>'a\<Colon>ordered_euclidean_space. x $$ i \<le> a}))) \<subseteq>
   sets (sigma UNIV (range (\<lambda>a. {a<..})))"
  (is "_ \<subseteq> sets ?SIGMA")
proof (rule sigma_algebra.sets_sigma_subset, safe)
  show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
  then interpret sigma_algebra ?SIGMA .
  fix a i
  show "{x. x$$i \<le> a} \<in> sets ?SIGMA"
  proof cases
    assume "i < DIM('a)"
    have "{x::'a. x$$i \<le> a} = space ?SIGMA - {x::'a. a < x$$i}" by auto
    also have *: "{x::'a. a < x$$i} = (\<Union>k::nat. {(\<chi>\<chi> n. if n = i then a else -real k) <..})" using `i <DIM('a)`
    proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm)
      fix x
      from real_arch_lt[of "Max ((\<lambda>i. -x$$i)`{..<DIM('a)})"]
      guess k::nat .. note k = this
      { fix i assume "i < DIM('a)"
        then have "-x$$i < real k"
          using k by (subst (asm) Max_less_iff) auto
        then have "- real k < x$$i" by simp }
      then show "\<exists>k::nat. \<forall>ia. ia \<noteq> i \<longrightarrow> ia < DIM('a) \<longrightarrow> -real k < x $$ ia"
        by (auto intro!: exI[of _ k])
    qed
    finally show "{x. x$$i \<le> a} \<in> sets ?SIGMA"
      apply (simp only:)
      apply (safe intro!: countable_UN Diff)
      by (auto simp: sets_sigma intro!: sigma_sets.Basic)
  next
    assume "\<not> i < DIM('a)"
    then show "{x. x$$i \<le> a} \<in> sets ?SIGMA"
      using top by auto
  qed
qed auto

lemma atMost_span_atLeastAtMost:
  "sets (sigma UNIV (range (\<lambda>a. {..a\<Colon>'a\<Colon>ordered_euclidean_space}))) \<subseteq>
   sets (sigma UNIV (range (\<lambda>(a,b). {a..b})))"
  (is "_ \<subseteq> sets ?SIGMA")
proof (rule sigma_algebra.sets_sigma_subset, safe)
  show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
  then interpret sigma_algebra ?SIGMA .
  fix a::'a
  have *: "{..a} = (\<Union>n::nat. {- real n *\<^sub>R One .. a})"
  proof (safe, simp_all add: eucl_le[where 'a='a])
    fix x
    from real_arch_simple[of "Max ((\<lambda>i. - x$$i)`{..<DIM('a)})"]
    guess k::nat .. note k = this
    { fix i assume "i < DIM('a)"
      with k have "- x$$i \<le> real k"
        by (subst (asm) Max_le_iff) (auto simp: field_simps)
      then have "- real k \<le> x$$i" by simp }
    then show "\<exists>n::nat. \<forall>i<DIM('a). - real n \<le> x $$ i"
      by (auto intro!: exI[of _ k])
  qed
  show "{..a} \<in> sets ?SIGMA" unfolding *
    by (safe intro!: countable_UN)
       (auto simp: sets_sigma intro!: sigma_sets.Basic)
qed auto

lemma borel_space_eq_greaterThanLessThan:
  "sets borel_space = sets (sigma UNIV (range (\<lambda> (a, b). {a <..< (b :: 'a \<Colon> ordered_euclidean_space)})))"
    (is "_ = sets ?SIGMA")
proof (rule antisym)
  show "sets ?SIGMA \<subseteq> sets borel_space"
    by (rule borel_space.sets_sigma_subset) auto
  show "sets borel_space \<subseteq> sets ?SIGMA"
    unfolding borel_space_def
  proof (rule sigma_algebra.sets_sigma_subset, safe)
    show "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
    then interpret sigma_algebra ?SIGMA .
    fix M :: "'a set" assume "M \<in> open"
    then have "open M" by (simp add: mem_def)
    show "M \<in> sets ?SIGMA"
      apply (subst open_UNION[OF `open M`])
      apply (safe intro!: countable_UN)
      by (auto simp add: sigma_def intro!: sigma_sets.Basic)
  qed auto
qed

lemma borel_space_eq_atMost:
  "sets borel_space = sets (sigma UNIV (range (\<lambda> a. {.. a::'a\<Colon>ordered_euclidean_space})))"
    (is "_ = sets ?SIGMA")
proof (rule antisym)
  show "sets borel_space \<subseteq> sets ?SIGMA"
    using halfspace_le_span_atMost halfspace_span_halfspace_le open_span_halfspace
    by auto
  show "sets ?SIGMA \<subseteq> sets borel_space"
    by (rule borel_space.sets_sigma_subset) auto
qed

lemma borel_space_eq_atLeastAtMost:
  "sets borel_space = sets (sigma UNIV (range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space, b). {a .. b})))"
   (is "_ = sets ?SIGMA")
proof (rule antisym)
  show "sets borel_space \<subseteq> sets ?SIGMA"
    using atMost_span_atLeastAtMost halfspace_le_span_atMost
      halfspace_span_halfspace_le open_span_halfspace
    by auto
  show "sets ?SIGMA \<subseteq> sets borel_space"
    by (rule borel_space.sets_sigma_subset) auto
qed

lemma borel_space_eq_greaterThan:
  "sets borel_space = sets (sigma UNIV (range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space). {a <..})))"
   (is "_ = sets ?SIGMA")
proof (rule antisym)
  show "sets borel_space \<subseteq> sets ?SIGMA"
    using halfspace_le_span_greaterThan
      halfspace_span_halfspace_le open_span_halfspace
    by auto
  show "sets ?SIGMA \<subseteq> sets borel_space"
    by (rule borel_space.sets_sigma_subset) auto
qed

lemma borel_space_eq_halfspace_le:
  "sets borel_space = sets (sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i \<le> a})))"
   (is "_ = sets ?SIGMA")
proof (rule antisym)
  show "sets borel_space \<subseteq> sets ?SIGMA"
    using open_span_halfspace halfspace_span_halfspace_le by auto
  show "sets ?SIGMA \<subseteq> sets borel_space"
    by (rule borel_space.sets_sigma_subset) auto
qed

lemma borel_space_eq_halfspace_less:
  "sets borel_space = sets (sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i < a})))"
   (is "_ = sets ?SIGMA")
proof (rule antisym)
  show "sets borel_space \<subseteq> sets ?SIGMA"
    using open_span_halfspace .
  show "sets ?SIGMA \<subseteq> sets borel_space"
    by (rule borel_space.sets_sigma_subset) auto
qed

lemma borel_space_eq_halfspace_gt:
  "sets borel_space = sets (sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. a < x$$i})))"
   (is "_ = sets ?SIGMA")
proof (rule antisym)
  show "sets borel_space \<subseteq> sets ?SIGMA"
    using halfspace_le_span_halfspace_gt open_span_halfspace halfspace_span_halfspace_le by auto
  show "sets ?SIGMA \<subseteq> sets borel_space"
    by (rule borel_space.sets_sigma_subset) auto
qed

lemma borel_space_eq_halfspace_ge:
  "sets borel_space = sets (sigma UNIV (range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. a \<le> x$$i})))"
   (is "_ = sets ?SIGMA")
proof (rule antisym)
  show "sets borel_space \<subseteq> sets ?SIGMA"
    using halfspace_span_halfspace_ge open_span_halfspace by auto
  show "sets ?SIGMA \<subseteq> sets borel_space"
    by (rule borel_space.sets_sigma_subset) auto
qed

lemma (in sigma_algebra) borel_measurable_halfspacesI:
  fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
  assumes "sets borel_space = sets (sigma UNIV (range F))"
  and "\<And>a i. S a i = f -` F (a,i) \<inter> space M"
  and "\<And>a i. \<not> i < DIM('c) \<Longrightarrow> S a i \<in> sets M"
  shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a::real. S a i \<in> sets M)"
proof safe
  fix a :: real and i assume i: "i < DIM('c)" and f: "f \<in> borel_measurable M"
  then show "S a i \<in> sets M" unfolding assms
    by (auto intro!: measurable_sets sigma_sets.Basic simp: assms(1) sigma_def)
next
  assume a: "\<forall>i<DIM('c). \<forall>a. S a i \<in> sets M"
  { fix a i have "S a i \<in> sets M"
    proof cases
      assume "i < DIM('c)"
      with a show ?thesis unfolding assms(2) by simp
    next
      assume "\<not> i < DIM('c)"
      from assms(3)[OF this] show ?thesis .
    qed }
  then have "f \<in> measurable M (sigma UNIV (range F))"
    by (auto intro!: measurable_sigma simp: assms(2))
  then show "f \<in> borel_measurable M" unfolding measurable_def
    unfolding assms(1) by simp
qed

lemma (in sigma_algebra) borel_measurable_iff_halfspace_le:
  fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
  shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. f w $$ i \<le> a} \<in> sets M)"
  by (rule borel_measurable_halfspacesI[OF borel_space_eq_halfspace_le]) auto

lemma (in sigma_algebra) borel_measurable_iff_halfspace_less:
  fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
  shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. f w $$ i < a} \<in> sets M)"
  by (rule borel_measurable_halfspacesI[OF borel_space_eq_halfspace_less]) auto

lemma (in sigma_algebra) borel_measurable_iff_halfspace_ge:
  fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
  shows "f \<in> borel_measurable M = (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. a \<le> f w $$ i} \<in> sets M)"
  by (rule borel_measurable_halfspacesI[OF borel_space_eq_halfspace_ge]) auto

lemma (in sigma_algebra) borel_measurable_iff_halfspace_greater:
  fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
  shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>i<DIM('c). \<forall>a. {w \<in> space M. a < f w $$ i} \<in> sets M)"
  by (rule borel_measurable_halfspacesI[OF borel_space_eq_halfspace_gt]) auto

lemma (in sigma_algebra) borel_measurable_iff_le:
  "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M)"
  using borel_measurable_iff_halfspace_le[where 'c=real] by simp

lemma (in sigma_algebra) borel_measurable_iff_less:
  "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w < a} \<in> sets M)"
  using borel_measurable_iff_halfspace_less[where 'c=real] by simp

lemma (in sigma_algebra) borel_measurable_iff_ge:
  "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)"
  using borel_measurable_iff_halfspace_ge[where 'c=real] by simp

lemma (in sigma_algebra) borel_measurable_iff_greater:
  "(f::'a \<Rightarrow> real) \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)"
  using borel_measurable_iff_halfspace_greater[where 'c=real] by simp

subsection "Borel measurable operators"

lemma (in sigma_algebra) affine_borel_measurable_vector:
  fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
  assumes "f \<in> borel_measurable M"
  shows "(\<lambda>x. a + b *\<^sub>R f x) \<in> borel_measurable M"
proof (rule borel_measurableI)
  fix S :: "'x set" assume "open S"
  show "(\<lambda>x. a + b *\<^sub>R f x) -` S \<inter> space M \<in> sets M"
  proof cases
    assume "b \<noteq> 0"
    with `open S` have "((\<lambda>x. (- a + x) /\<^sub>R b) ` S) \<in> open" (is "?S \<in> open")
      by (auto intro!: open_affinity simp: scaleR.add_right mem_def)
    hence "?S \<in> sets borel_space"
      unfolding borel_space_def by (auto simp: sigma_def intro!: sigma_sets.Basic)
    moreover
    from `b \<noteq> 0` have "(\<lambda>x. a + b *\<^sub>R f x) -` S = f -` ?S"
      apply auto by (rule_tac x="a + b *\<^sub>R f x" in image_eqI, simp_all)
    ultimately show ?thesis using assms unfolding in_borel_measurable_borel_space
      by auto
  qed simp
qed

lemma (in sigma_algebra) affine_borel_measurable:
  fixes g :: "'a \<Rightarrow> real"
  assumes g: "g \<in> borel_measurable M"
  shows "(\<lambda>x. a + (g x) * b) \<in> borel_measurable M"
  using affine_borel_measurable_vector[OF assms] by (simp add: mult_commute)

lemma (in sigma_algebra) borel_measurable_add[simp, intro]:
  fixes f :: "'a \<Rightarrow> real"
  assumes f: "f \<in> borel_measurable M"
  assumes g: "g \<in> borel_measurable M"
  shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
proof -
  have 1: "\<And>a. {w\<in>space M. a \<le> f w + g w} = {w \<in> space M. a + g w * -1 \<le> f w}"
    by auto
  have "\<And>a. (\<lambda>w. a + (g w) * -1) \<in> borel_measurable M"
    by (rule affine_borel_measurable [OF g])
  then have "\<And>a. {w \<in> space M. (\<lambda>w. a + (g w) * -1)(w) \<le> f w} \<in> sets M" using f
    by auto
  then have "\<And>a. {w \<in> space M. a \<le> f w + g w} \<in> sets M"
    by (simp add: 1)
  then show ?thesis
    by (simp add: borel_measurable_iff_ge)
qed

lemma (in sigma_algebra) borel_measurable_square:
  fixes f :: "'a \<Rightarrow> real"
  assumes f: "f \<in> borel_measurable M"
  shows "(\<lambda>x. (f x)^2) \<in> borel_measurable M"
proof -
  {
    fix a
    have "{w \<in> space M. (f w)\<twosuperior> \<le> a} \<in> sets M"
    proof (cases rule: linorder_cases [of a 0])
      case less
      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = {}"
        by auto (metis less order_le_less_trans power2_less_0)
      also have "... \<in> sets M"
        by (rule empty_sets)
      finally show ?thesis .
    next
      case equal
      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} =
             {w \<in> space M. f w \<le> 0} \<inter> {w \<in> space M. 0 \<le> f w}"
        by auto
      also have "... \<in> sets M"
        apply (insert f)
        apply (rule Int)
        apply (simp add: borel_measurable_iff_le)
        apply (simp add: borel_measurable_iff_ge)
        done
      finally show ?thesis .
    next
      case greater
      have "\<forall>x. (f x ^ 2 \<le> sqrt a ^ 2) = (- sqrt a  \<le> f x & f x \<le> sqrt a)"
        by (metis abs_le_interval_iff abs_of_pos greater real_sqrt_abs
                  real_sqrt_le_iff real_sqrt_power)
      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} =
             {w \<in> space M. -(sqrt a) \<le> f w} \<inter> {w \<in> space M. f w \<le> sqrt a}"
        using greater by auto
      also have "... \<in> sets M"
        apply (insert f)
        apply (rule Int)
        apply (simp add: borel_measurable_iff_ge)
        apply (simp add: borel_measurable_iff_le)
        done
      finally show ?thesis .
    qed
  }
  thus ?thesis by (auto simp add: borel_measurable_iff_le)
qed

lemma times_eq_sum_squares:
   fixes x::real
   shows"x*y = ((x+y)^2)/4 - ((x-y)^ 2)/4"
by (simp add: power2_eq_square ring_distribs diff_divide_distrib [symmetric])

lemma (in sigma_algebra) borel_measurable_uminus[simp, intro]:
  fixes g :: "'a \<Rightarrow> real"
  assumes g: "g \<in> borel_measurable M"
  shows "(\<lambda>x. - g x) \<in> borel_measurable M"
proof -
  have "(\<lambda>x. - g x) = (\<lambda>x. 0 + (g x) * -1)"
    by simp
  also have "... \<in> borel_measurable M"
    by (fast intro: affine_borel_measurable g)
  finally show ?thesis .
qed

lemma (in sigma_algebra) borel_measurable_times[simp, intro]:
  fixes f :: "'a \<Rightarrow> real"
  assumes f: "f \<in> borel_measurable M"
  assumes g: "g \<in> borel_measurable M"
  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
proof -
  have 1: "(\<lambda>x. 0 + (f x + g x)\<twosuperior> * inverse 4) \<in> borel_measurable M"
    using assms by (fast intro: affine_borel_measurable borel_measurable_square)
  have "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) =
        (\<lambda>x. 0 + ((f x + -g x) ^ 2 * inverse -4))"
    by (simp add: minus_divide_right)
  also have "... \<in> borel_measurable M"
    using f g by (fast intro: affine_borel_measurable borel_measurable_square f g)
  finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" .
  show ?thesis
    apply (simp add: times_eq_sum_squares diff_minus)
    using 1 2 by simp
qed

lemma (in sigma_algebra) borel_measurable_diff[simp, intro]:
  fixes f :: "'a \<Rightarrow> real"
  assumes f: "f \<in> borel_measurable M"
  assumes g: "g \<in> borel_measurable M"
  shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
  unfolding diff_minus using assms by fast

lemma (in sigma_algebra) borel_measurable_setsum[simp, intro]:
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
proof cases
  assume "finite S"
  thus ?thesis using assms by induct auto
qed simp

lemma (in sigma_algebra) borel_measurable_inverse[simp, intro]:
  fixes f :: "'a \<Rightarrow> real"
  assumes "f \<in> borel_measurable M"
  shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
  unfolding borel_measurable_iff_ge unfolding inverse_eq_divide
proof safe
  fix a :: real
  have *: "{w \<in> space M. a \<le> 1 / f w} =
      ({w \<in> space M. 0 < f w} \<inter> {w \<in> space M. a * f w \<le> 1}) \<union>
      ({w \<in> space M. f w < 0} \<inter> {w \<in> space M. 1 \<le> a * f w}) \<union>
      ({w \<in> space M. f w = 0} \<inter> {w \<in> space M. a \<le> 0})" by (auto simp: le_divide_eq)
  show "{w \<in> space M. a \<le> 1 / f w} \<in> sets M" using assms unfolding *
    by (auto intro!: Int Un)
qed

lemma (in sigma_algebra) borel_measurable_divide[simp, intro]:
  fixes f :: "'a \<Rightarrow> real"
  assumes "f \<in> borel_measurable M"
  and "g \<in> borel_measurable M"
  shows "(\<lambda>x. f x / g x) \<in> borel_measurable M"
  unfolding field_divide_inverse
  by (rule borel_measurable_inverse borel_measurable_times assms)+

lemma (in sigma_algebra) borel_measurable_max[intro, simp]:
  fixes f g :: "'a \<Rightarrow> real"
  assumes "f \<in> borel_measurable M"
  assumes "g \<in> borel_measurable M"
  shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
  unfolding borel_measurable_iff_le
proof safe
  fix a
  have "{x \<in> space M. max (g x) (f x) \<le> a} =
    {x \<in> space M. g x \<le> a} \<inter> {x \<in> space M. f x \<le> a}" by auto
  thus "{x \<in> space M. max (g x) (f x) \<le> a} \<in> sets M"
    using assms unfolding borel_measurable_iff_le
    by (auto intro!: Int)
qed

lemma (in sigma_algebra) borel_measurable_min[intro, simp]:
  fixes f g :: "'a \<Rightarrow> real"
  assumes "f \<in> borel_measurable M"
  assumes "g \<in> borel_measurable M"
  shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
  unfolding borel_measurable_iff_ge
proof safe
  fix a
  have "{x \<in> space M. a \<le> min (g x) (f x)} =
    {x \<in> space M. a \<le> g x} \<inter> {x \<in> space M. a \<le> f x}" by auto
  thus "{x \<in> space M. a \<le> min (g x) (f x)} \<in> sets M"
    using assms unfolding borel_measurable_iff_ge
    by (auto intro!: Int)
qed

lemma (in sigma_algebra) borel_measurable_abs[simp, intro]:
  assumes "f \<in> borel_measurable M"
  shows "(\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
proof -
  have *: "\<And>x. \<bar>f x\<bar> = max 0 (f x) + max 0 (- f x)" by (simp add: max_def)
  show ?thesis unfolding * using assms by auto
qed

section "Borel space over the real line with infinity"

lemma borel_space_Real_measurable:
  "A \<in> sets borel_space \<Longrightarrow> Real -` A \<in> sets borel_space"
proof (rule borel_measurable_translate)
  fix B :: "pinfreal set" assume "open B"
  then obtain T x where T: "open T" "Real ` (T \<inter> {0..}) = B - {\<omega>}" and
    x: "\<omega> \<in> B \<Longrightarrow> 0 \<le> x" "\<omega> \<in> B \<Longrightarrow> {Real x <..} \<subseteq> B"
    unfolding open_pinfreal_def by blast

  have "Real -` B = Real -` (B - {\<omega>})" by auto
  also have "\<dots> = Real -` (Real ` (T \<inter> {0..}))" using T by simp
  also have "\<dots> = (if 0 \<in> T then T \<union> {.. 0} else T \<inter> {0..})"
    apply (auto simp add: Real_eq_Real image_iff)
    apply (rule_tac x="max 0 x" in bexI)
    by (auto simp: max_def)
  finally show "Real -` B \<in> sets borel_space"
    using `open T` by auto
qed simp

lemma borel_space_real_measurable:
  "A \<in> sets borel_space \<Longrightarrow> (real -` A :: pinfreal set) \<in> sets borel_space"
proof (rule borel_measurable_translate)
  fix B :: "real set" assume "open B"
  { fix x have "0 < real x \<longleftrightarrow> (\<exists>r>0. x = Real r)" by (cases x) auto }
  note Ex_less_real = this
  have *: "real -` B = (if 0 \<in> B then real -` (B \<inter> {0 <..}) \<union> {0, \<omega>} else real -` (B \<inter> {0 <..}))"
    by (force simp: Ex_less_real)

  have "open (real -` (B \<inter> {0 <..}) :: pinfreal set)"
    unfolding open_pinfreal_def using `open B`
    by (auto intro!: open_Int exI[of _ "B \<inter> {0 <..}"] simp: image_iff Ex_less_real)
  then show "(real -` B :: pinfreal set) \<in> sets borel_space" unfolding * by auto
qed simp

lemma (in sigma_algebra) borel_measurable_Real[intro, simp]:
  assumes "f \<in> borel_measurable M"
  shows "(\<lambda>x. Real (f x)) \<in> borel_measurable M"
  unfolding in_borel_measurable_borel_space
proof safe
  fix S :: "pinfreal set" assume "S \<in> sets borel_space"
  from borel_space_Real_measurable[OF this]
  have "(Real \<circ> f) -` S \<inter> space M \<in> sets M"
    using assms
    unfolding vimage_compose in_borel_measurable_borel_space
    by auto
  thus "(\<lambda>x. Real (f x)) -` S \<inter> space M \<in> sets M" by (simp add: comp_def)
qed

lemma (in sigma_algebra) borel_measurable_real[intro, simp]:
  fixes f :: "'a \<Rightarrow> pinfreal"
  assumes "f \<in> borel_measurable M"
  shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
  unfolding in_borel_measurable_borel_space
proof safe
  fix S :: "real set" assume "S \<in> sets borel_space"
  from borel_space_real_measurable[OF this]
  have "(real \<circ> f) -` S \<inter> space M \<in> sets M"
    using assms
    unfolding vimage_compose in_borel_measurable_borel_space
    by auto
  thus "(\<lambda>x. real (f x)) -` S \<inter> space M \<in> sets M" by (simp add: comp_def)
qed

lemma (in sigma_algebra) borel_measurable_Real_eq:
  assumes "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
  shows "(\<lambda>x. Real (f x)) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M"
proof
  have [simp]: "(\<lambda>x. Real (f x)) -` {\<omega>} \<inter> space M = {}"
    by auto
  assume "(\<lambda>x. Real (f x)) \<in> borel_measurable M"
  hence "(\<lambda>x. real (Real (f x))) \<in> borel_measurable M"
    by (rule borel_measurable_real)
  moreover have "\<And>x. x \<in> space M \<Longrightarrow> real (Real (f x)) = f x"
    using assms by auto
  ultimately show "f \<in> borel_measurable M"
    by (simp cong: measurable_cong)
qed auto

lemma (in sigma_algebra) borel_measurable_pinfreal_eq_real:
  "f \<in> borel_measurable M \<longleftrightarrow>
    ((\<lambda>x. real (f x)) \<in> borel_measurable M \<and> f -` {\<omega>} \<inter> space M \<in> sets M)"
proof safe
  assume "f \<in> borel_measurable M"
  then show "(\<lambda>x. real (f x)) \<in> borel_measurable M" "f -` {\<omega>} \<inter> space M \<in> sets M"
    by (auto intro: borel_measurable_vimage borel_measurable_real)
next
  assume *: "(\<lambda>x. real (f x)) \<in> borel_measurable M" "f -` {\<omega>} \<inter> space M \<in> sets M"
  have "f -` {\<omega>} \<inter> space M = {x\<in>space M. f x = \<omega>}" by auto
  with * have **: "{x\<in>space M. f x = \<omega>} \<in> sets M" by simp
  have f: "f = (\<lambda>x. if f x = \<omega> then \<omega> else Real (real (f x)))"
    by (simp add: expand_fun_eq Real_real)
  show "f \<in> borel_measurable M"
    apply (subst f)
    apply (rule measurable_If)
    using * ** by auto
qed

lemma (in sigma_algebra) less_eq_ge_measurable:
  fixes f :: "'a \<Rightarrow> 'c::linorder"
  shows "{x\<in>space M. a < f x} \<in> sets M \<longleftrightarrow> {x\<in>space M. f x \<le> a} \<in> sets M"
proof
  assume "{x\<in>space M. f x \<le> a} \<in> sets M"
  moreover have "{x\<in>space M. a < f x} = space M - {x\<in>space M. f x \<le> a}" by auto
  ultimately show "{x\<in>space M. a < f x} \<in> sets M" by auto
next
  assume "{x\<in>space M. a < f x} \<in> sets M"
  moreover have "{x\<in>space M. f x \<le> a} = space M - {x\<in>space M. a < f x}" by auto
  ultimately show "{x\<in>space M. f x \<le> a} \<in> sets M" by auto
qed

lemma (in sigma_algebra) greater_eq_le_measurable:
  fixes f :: "'a \<Rightarrow> 'c::linorder"
  shows "{x\<in>space M. f x < a} \<in> sets M \<longleftrightarrow> {x\<in>space M. a \<le> f x} \<in> sets M"
proof
  assume "{x\<in>space M. a \<le> f x} \<in> sets M"
  moreover have "{x\<in>space M. f x < a} = space M - {x\<in>space M. a \<le> f x}" by auto
  ultimately show "{x\<in>space M. f x < a} \<in> sets M" by auto
next
  assume "{x\<in>space M. f x < a} \<in> sets M"
  moreover have "{x\<in>space M. a \<le> f x} = space M - {x\<in>space M. f x < a}" by auto
  ultimately show "{x\<in>space M. a \<le> f x} \<in> sets M" by auto
qed

lemma (in sigma_algebra) less_eq_le_pinfreal_measurable:
  fixes f :: "'a \<Rightarrow> pinfreal"
  shows "(\<forall>a. {x\<in>space M. a < f x} \<in> sets M) \<longleftrightarrow> (\<forall>a. {x\<in>space M. a \<le> f x} \<in> sets M)"
proof
  assume a: "\<forall>a. {x\<in>space M. a \<le> f x} \<in> sets M"
  show "\<forall>a. {x \<in> space M. a < f x} \<in> sets M"
  proof
    fix a show "{x \<in> space M. a < f x} \<in> sets M"
    proof (cases a)
      case (preal r)
      have "{x\<in>space M. a < f x} = (\<Union>i. {x\<in>space M. a + inverse (of_nat (Suc i)) \<le> f x})"
      proof safe
        fix x assume "a < f x" and [simp]: "x \<in> space M"
        with ex_pinfreal_inverse_of_nat_Suc_less[of "f x - a"]
        obtain n where "a + inverse (of_nat (Suc n)) < f x"
          by (cases "f x", auto simp: pinfreal_minus_order)
        then have "a + inverse (of_nat (Suc n)) \<le> f x" by simp
        then show "x \<in> (\<Union>i. {x \<in> space M. a + inverse (of_nat (Suc i)) \<le> f x})"
          by auto
      next
        fix i x assume [simp]: "x \<in> space M"
        have "a < a + inverse (of_nat (Suc i))" using preal by auto
        also assume "a + inverse (of_nat (Suc i)) \<le> f x"
        finally show "a < f x" .
      qed
      with a show ?thesis by auto
    qed simp
  qed
next
  assume a': "\<forall>a. {x \<in> space M. a < f x} \<in> sets M"
  then have a: "\<forall>a. {x \<in> space M. f x \<le> a} \<in> sets M" unfolding less_eq_ge_measurable .
  show "\<forall>a. {x \<in> space M. a \<le> f x} \<in> sets M" unfolding greater_eq_le_measurable[symmetric]
  proof
    fix a show "{x \<in> space M. f x < a} \<in> sets M"
    proof (cases a)
      case (preal r)
      show ?thesis
      proof cases
        assume "a = 0" then show ?thesis by simp
      next
        assume "a \<noteq> 0"
        have "{x\<in>space M. f x < a} = (\<Union>i. {x\<in>space M. f x \<le> a - inverse (of_nat (Suc i))})"
        proof safe
          fix x assume "f x < a" and [simp]: "x \<in> space M"
          with ex_pinfreal_inverse_of_nat_Suc_less[of "a - f x"]
          obtain n where "inverse (of_nat (Suc n)) < a - f x"
            using preal by (cases "f x") auto
          then have "f x \<le> a - inverse (of_nat (Suc n)) "
            using preal by (cases "f x") (auto split: split_if_asm)
          then show "x \<in> (\<Union>i. {x \<in> space M. f x \<le> a - inverse (of_nat (Suc i))})"
            by auto
        next
          fix i x assume [simp]: "x \<in> space M"
          assume "f x \<le> a - inverse (of_nat (Suc i))"
          also have "\<dots> < a" using `a \<noteq> 0` preal by auto
          finally show "f x < a" .
        qed
        with a show ?thesis by auto
      qed
    next
      case infinite
      have "f -` {\<omega>} \<inter> space M = (\<Inter>n. {x\<in>space M. of_nat n < f x})"
      proof (safe, simp_all, safe)
        fix x assume *: "\<forall>n::nat. Real (real n) < f x"
        show "f x = \<omega>"    proof (rule ccontr)
          assume "f x \<noteq> \<omega>"
          with real_arch_lt[of "real (f x)"] obtain n where "f x < of_nat n"
            by (auto simp: pinfreal_noteq_omega_Ex)
          with *[THEN spec, of n] show False by auto
        qed
      qed
      with a' have \<omega>: "f -` {\<omega>} \<inter> space M \<in> sets M" by auto
      moreover have "{x \<in> space M. f x < a} = space M - f -` {\<omega>} \<inter> space M"
        using infinite by auto
      ultimately show ?thesis by auto
    qed
  qed
qed

lemma (in sigma_algebra) borel_measurable_pinfreal_iff_greater:
  "(f::'a \<Rightarrow> pinfreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. {x\<in>space M. a < f x} \<in> sets M)"
proof safe
  fix a assume f: "f \<in> borel_measurable M"
  have "{x\<in>space M. a < f x} = f -` {a <..} \<inter> space M" by auto
  with f show "{x\<in>space M. a < f x} \<in> sets M"
    by (auto intro!: measurable_sets)
next
  assume *: "\<forall>a. {x\<in>space M. a < f x} \<in> sets M"
  hence **: "\<forall>a. {x\<in>space M. f x < a} \<in> sets M"
    unfolding less_eq_le_pinfreal_measurable
    unfolding greater_eq_le_measurable .

  show "f \<in> borel_measurable M" unfolding borel_measurable_pinfreal_eq_real borel_measurable_iff_greater
  proof safe
    have "f -` {\<omega>} \<inter> space M = space M - {x\<in>space M. f x < \<omega>}" by auto
    then show \<omega>: "f -` {\<omega>} \<inter> space M \<in> sets M" using ** by auto

    fix a
    have "{w \<in> space M. a < real (f w)} =
      (if 0 \<le> a then {w\<in>space M. Real a < f w} - (f -` {\<omega>} \<inter> space M) else space M)"
    proof (split split_if, safe del: notI)
      fix x assume "0 \<le> a"
      { assume "a < real (f x)" then show "Real a < f x" "x \<notin> f -` {\<omega>} \<inter> space M"
          using `0 \<le> a` by (cases "f x", auto) }
      { assume "Real a < f x" "x \<notin> f -` {\<omega>}" then show "a < real (f x)"
          using `0 \<le> a` by (cases "f x", auto) }
    next
      fix x assume "\<not> 0 \<le> a" then show "a < real (f x)" by (cases "f x") auto
    qed
    then show "{w \<in> space M. a < real (f w)} \<in> sets M"
      using \<omega> * by (auto intro!: Diff)
  qed
qed

lemma (in sigma_algebra) borel_measurable_pinfreal_iff_less:
  "(f::'a \<Rightarrow> pinfreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. {x\<in>space M. f x < a} \<in> sets M)"
  using borel_measurable_pinfreal_iff_greater unfolding less_eq_le_pinfreal_measurable greater_eq_le_measurable .

lemma (in sigma_algebra) borel_measurable_pinfreal_iff_le:
  "(f::'a \<Rightarrow> pinfreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. {x\<in>space M. f x \<le> a} \<in> sets M)"
  using borel_measurable_pinfreal_iff_greater unfolding less_eq_ge_measurable .

lemma (in sigma_algebra) borel_measurable_pinfreal_iff_ge:
  "(f::'a \<Rightarrow> pinfreal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. {x\<in>space M. a \<le> f x} \<in> sets M)"
  using borel_measurable_pinfreal_iff_greater unfolding less_eq_le_pinfreal_measurable .

lemma (in sigma_algebra) borel_measurable_pinfreal_eq_const:
  fixes f :: "'a \<Rightarrow> pinfreal" assumes "f \<in> borel_measurable M"
  shows "{x\<in>space M. f x = c} \<in> sets M"
proof -
  have "{x\<in>space M. f x = c} = (f -` {c} \<inter> space M)" by auto
  then show ?thesis using assms by (auto intro!: measurable_sets)
qed

lemma (in sigma_algebra) borel_measurable_pinfreal_neq_const:
  fixes f :: "'a \<Rightarrow> pinfreal"
  assumes "f \<in> borel_measurable M"
  shows "{x\<in>space M. f x \<noteq> c} \<in> sets M"
proof -
  have "{x\<in>space M. f x \<noteq> c} = space M - (f -` {c} \<inter> space M)" by auto
  then show ?thesis using assms by (auto intro!: measurable_sets)
qed

lemma (in sigma_algebra) borel_measurable_pinfreal_less[intro,simp]:
  fixes f g :: "'a \<Rightarrow> pinfreal"
  assumes f: "f \<in> borel_measurable M"
  assumes g: "g \<in> borel_measurable M"
  shows "{x \<in> space M. f x < g x} \<in> sets M"
proof -
  have "(\<lambda>x. real (f x)) \<in> borel_measurable M"
    "(\<lambda>x. real (g x)) \<in> borel_measurable M"
    using assms by (auto intro!: borel_measurable_real)
  from borel_measurable_less[OF this]
  have "{x \<in> space M. real (f x) < real (g x)} \<in> sets M" .
  moreover have "{x \<in> space M. f x \<noteq> \<omega>} \<in> sets M" using f by (rule borel_measurable_pinfreal_neq_const)
  moreover have "{x \<in> space M. g x = \<omega>} \<in> sets M" using g by (rule borel_measurable_pinfreal_eq_const)
  moreover have "{x \<in> space M. g x \<noteq> \<omega>} \<in> sets M" using g by (rule borel_measurable_pinfreal_neq_const)
  moreover have "{x \<in> space M. f x < g x} = ({x \<in> space M. g x = \<omega>} \<inter> {x \<in> space M. f x \<noteq> \<omega>}) \<union>
    ({x \<in> space M. g x \<noteq> \<omega>} \<inter> {x \<in> space M. f x \<noteq> \<omega>} \<inter> {x \<in> space M. real (f x) < real (g x)})"
    by (auto simp: real_of_pinfreal_strict_mono_iff)
  ultimately show ?thesis by auto
qed

lemma (in sigma_algebra) borel_measurable_pinfreal_le[intro,simp]:
  fixes f :: "'a \<Rightarrow> pinfreal"
  assumes f: "f \<in> borel_measurable M"
  assumes g: "g \<in> borel_measurable M"
  shows "{x \<in> space M. f x \<le> g x} \<in> sets M"
proof -
  have "{x \<in> space M. f x \<le> g x} = space M - {x \<in> space M. g x < f x}" by auto
  then show ?thesis using g f by auto
qed

lemma (in sigma_algebra) borel_measurable_pinfreal_eq[intro,simp]:
  fixes f :: "'a \<Rightarrow> pinfreal"
  assumes f: "f \<in> borel_measurable M"
  assumes g: "g \<in> borel_measurable M"
  shows "{w \<in> space M. f w = g w} \<in> sets M"
proof -
  have "{x \<in> space M. f x = g x} = {x \<in> space M. g x \<le> f x} \<inter> {x \<in> space M. f x \<le> g x}" by auto
  then show ?thesis using g f by auto
qed

lemma (in sigma_algebra) borel_measurable_pinfreal_neq[intro,simp]:
  fixes f :: "'a \<Rightarrow> pinfreal"
  assumes f: "f \<in> borel_measurable M"
  assumes g: "g \<in> borel_measurable M"
  shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
proof -
  have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}" by auto
  thus ?thesis using f g by auto
qed

lemma (in sigma_algebra) borel_measurable_pinfreal_add[intro, simp]:
  fixes f :: "'a \<Rightarrow> pinfreal"
  assumes measure: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
proof -
  have *: "(\<lambda>x. f x + g x) =
     (\<lambda>x. if f x = \<omega> then \<omega> else if g x = \<omega> then \<omega> else Real (real (f x) + real (g x)))"
     by (auto simp: expand_fun_eq pinfreal_noteq_omega_Ex)
  show ?thesis using assms unfolding *
    by (auto intro!: measurable_If)
qed

lemma (in sigma_algebra) borel_measurable_pinfreal_times[intro, simp]:
  fixes f :: "'a \<Rightarrow> pinfreal" assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
proof -
  have *: "(\<lambda>x. f x * g x) =
     (\<lambda>x. if f x = 0 then 0 else if g x = 0 then 0 else if f x = \<omega> then \<omega> else if g x = \<omega> then \<omega> else
      Real (real (f x) * real (g x)))"
     by (auto simp: expand_fun_eq pinfreal_noteq_omega_Ex)
  show ?thesis using assms unfolding *
    by (auto intro!: measurable_If)
qed

lemma (in sigma_algebra) borel_measurable_pinfreal_setsum[simp, intro]:
  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> pinfreal"
  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
  shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
proof cases
  assume "finite S"
  thus ?thesis using assms
    by induct auto
qed (simp add: borel_measurable_const)

lemma (in sigma_algebra) borel_measurable_pinfreal_min[intro, simp]:
  fixes f g :: "'a \<Rightarrow> pinfreal"
  assumes "f \<in> borel_measurable M"
  assumes "g \<in> borel_measurable M"
  shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
  using assms unfolding min_def by (auto intro!: measurable_If)

lemma (in sigma_algebra) borel_measurable_pinfreal_max[intro]:
  fixes f g :: "'a \<Rightarrow> pinfreal"
  assumes "f \<in> borel_measurable M"
  and "g \<in> borel_measurable M"
  shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
  using assms unfolding max_def by (auto intro!: measurable_If)

lemma (in sigma_algebra) borel_measurable_SUP[simp, intro]:
  fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> pinfreal"
  assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
  shows "(SUP i : A. f i) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
  unfolding borel_measurable_pinfreal_iff_greater
proof safe
  fix a
  have "{x\<in>space M. a < ?sup x} = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
    by (auto simp: less_Sup_iff SUPR_def[where 'a=pinfreal] SUPR_fun_expand[where 'b=pinfreal])
  then show "{x\<in>space M. a < ?sup x} \<in> sets M"
    using assms by auto
qed

lemma (in sigma_algebra) borel_measurable_INF[simp, intro]:
  fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> pinfreal"
  assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
  shows "(INF i : A. f i) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
  unfolding borel_measurable_pinfreal_iff_less
proof safe
  fix a
  have "{x\<in>space M. ?inf x < a} = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
    by (auto simp: Inf_less_iff INFI_def[where 'a=pinfreal] INFI_fun_expand)
  then show "{x\<in>space M. ?inf x < a} \<in> sets M"
    using assms by auto
qed

lemma (in sigma_algebra) borel_measurable_pinfreal_diff:
  fixes f g :: "'a \<Rightarrow> pinfreal"
  assumes "f \<in> borel_measurable M"
  assumes "g \<in> borel_measurable M"
  shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
  unfolding borel_measurable_pinfreal_iff_greater
proof safe
  fix a
  have "{x \<in> space M. a < f x - g x} = {x \<in> space M. g x + a < f x}"
    by (simp add: pinfreal_less_minus_iff)
  then show "{x \<in> space M. a < f x - g x} \<in> sets M"
    using assms by auto
qed

end