Theory Borel_Space

theory Borel_Space
imports Measurable Ordered_Euclidean_Space
(*  Title:      HOL/Analysis/Borel_Space.thy
    Author:     Johannes Hölzl, TU München
    Author:     Armin Heller, TU München
*)

section ‹Borel spaces›

theory Borel_Space
imports
  Measurable Derivative Ordered_Euclidean_Space Extended_Real_Limits
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 topological_basis_trivial: "topological_basis {A. open A}"
  by (auto simp: topological_basis_def)

lemma open_prod_generated: "open = generate_topology {A × B | A B. open A ∧ open B}"
proof -
  have "{A × B :: ('a × 'b) set | A B. open A ∧ open B} = ((λ(a, b). a × b) ` ({A. open A} × {A. open A}))"
    by auto
  then show ?thesis
    by (auto intro: topological_basis_prod topological_basis_trivial topological_basis_imp_subbasis)
qed

definition "mono_on f A ≡ ∀r s. r ∈ A ∧ s ∈ A ∧ r ≤ s ⟶ f r ≤ f s"

lemma mono_onI:
  "(⋀r s. r ∈ A ⟹ s ∈ A ⟹ r ≤ s ⟹ f r ≤ f s) ⟹ mono_on f A"
  unfolding mono_on_def by simp

lemma mono_onD:
  "⟦mono_on f A; r ∈ A; s ∈ A; r ≤ s⟧ ⟹ f r ≤ f s"
  unfolding mono_on_def by simp

lemma mono_imp_mono_on: "mono f ⟹ mono_on f A"
  unfolding mono_def mono_on_def by auto

lemma mono_on_subset: "mono_on f A ⟹ B ⊆ A ⟹ mono_on f B"
  unfolding mono_on_def by auto

definition "strict_mono_on f A ≡ ∀r s. r ∈ A ∧ s ∈ A ∧ r < s ⟶ f r < f s"

lemma strict_mono_onI:
  "(⋀r s. r ∈ A ⟹ s ∈ A ⟹ r < s ⟹ f r < f s) ⟹ strict_mono_on f A"
  unfolding strict_mono_on_def by simp

lemma strict_mono_onD:
  "⟦strict_mono_on f A; r ∈ A; s ∈ A; r < s⟧ ⟹ f r < f s"
  unfolding strict_mono_on_def by simp

lemma mono_on_greaterD:
  assumes "mono_on g A" "x ∈ A" "y ∈ A" "g x > (g (y::_::linorder) :: _ :: linorder)"
  shows "x > y"
proof (rule ccontr)
  assume "¬x > y"
  hence "x ≤ y" by (simp add: not_less)
  from assms(1-3) and this have "g x ≤ g y" by (rule mono_onD)
  with assms(4) show False by simp
qed

lemma strict_mono_inv:
  fixes f :: "('a::linorder) ⇒ ('b::linorder)"
  assumes "strict_mono f" and "surj f" and inv: "⋀x. g (f x) = x"
  shows "strict_mono g"
proof
  fix x y :: 'b assume "x < y"
  from ‹surj f› obtain x' y' where [simp]: "x = f x'" "y = f y'" by blast
  with ‹x < y› and ‹strict_mono f› have "x' < y'" by (simp add: strict_mono_less)
  with inv show "g x < g y" by simp
qed

lemma strict_mono_on_imp_inj_on:
  assumes "strict_mono_on (f :: (_ :: linorder) ⇒ (_ :: preorder)) A"
  shows "inj_on f A"
proof (rule inj_onI)
  fix x y assume "x ∈ A" "y ∈ 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])
qed

lemma strict_mono_on_leD:
  assumes "strict_mono_on (f :: (_ :: linorder) ⇒ _ :: preorder) A" "x ∈ A" "y ∈ A" "x ≤ y"
  shows "f x ≤ f y"
proof (insert le_less_linear[of y x], elim disjE)
  assume "x < y"
  with assms have "f x < f y" by (rule_tac strict_mono_onD[OF assms(1)]) simp_all
  thus ?thesis by (rule less_imp_le)
qed (insert assms, simp)

lemma strict_mono_on_eqD:
  fixes f :: "(_ :: linorder) ⇒ (_ :: preorder)"
  assumes "strict_mono_on f A" "f x = f y" "x ∈ A" "y ∈ A"
  shows "y = x"
  using assms by (rule_tac linorder_cases[of x y]) (auto dest: strict_mono_onD)

lemma mono_on_imp_deriv_nonneg:
  assumes mono: "mono_on f A" and deriv: "(f has_real_derivative D) (at x)"
  assumes "x ∈ interior A"
  shows "D ≥ 0"
proof (rule tendsto_lowerbound)
  let ?A' = "(λy. y - x) ` interior A"
  from deriv show "((λh. (f (x + h) - f x) / h) ⤏ D) (at 0)"
      by (simp add: field_has_derivative_at has_field_derivative_def)
  from mono have mono': "mono_on f (interior A)" by (rule mono_on_subset) (rule interior_subset)

  show "eventually (λh. (f (x + h) - f x) / h ≥ 0) (at 0)"
  proof (subst eventually_at_topological, intro exI conjI ballI impI)
    have "open (interior A)" by simp
    hence "open (op + (-x) ` interior A)" by (rule open_translation)
    also have "(op + (-x) ` interior A) = ?A'" by auto
    finally show "open ?A'" .
  next
    from ‹x ∈ interior A› show "0 ∈ ?A'" by auto
  next
    fix h assume "h ∈ ?A'"
    hence "x + h ∈ interior A" by auto
    with mono' and ‹x ∈ interior A› show "(f (x + h) - f x) / h ≥ 0"
      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:
  "strict_mono_on (f :: (_ :: linorder) ⇒ _ :: preorder) A ⟹ mono_on f A"
  by (rule mono_onI, rule strict_mono_on_leD)

lemma mono_on_ctble_discont:
  fixes f :: "real ⇒ real"
  fixes A :: "real set"
  assumes "mono_on f A"
  shows "countable {a∈A. ¬ continuous (at a within A) f}"
proof -
  have mono: "⋀x y. x ∈ A ⟹ y ∈ A ⟹ x ≤ y ⟹ f x ≤ f y"
    using ‹mono_on f A› by (simp add: mono_on_def)
  have "∀a ∈ {a∈A. ¬ continuous (at a within A) f}. ∃q :: nat × rat.
      (fst q = 0 ∧ of_rat (snd q) < f a ∧ (∀x ∈ A. x < a ⟶ f x < of_rat (snd q))) ∨
      (fst q = 1 ∧ of_rat (snd q) > f a ∧ (∀x ∈ A. x > a ⟶ f x > of_rat (snd q)))"
  proof (clarsimp simp del: One_nat_def)
    fix a assume "a ∈ A" assume "¬ continuous (at a within A) f"
    thus "∃q1 q2.
            q1 = 0 ∧ real_of_rat q2 < f a ∧ (∀x∈A. x < a ⟶ f x < real_of_rat q2) ∨
            q1 = 1 ∧ f a < real_of_rat q2 ∧ (∀x∈A. a < x ⟶ real_of_rat q2 < f x)"
    proof (auto simp add: continuous_within order_tendsto_iff eventually_at)
      fix l assume "l < f a"
      then obtain q2 where q2: "l < of_rat q2" "of_rat q2 < f a"
        using of_rat_dense by blast
      assume * [rule_format]: "∀d>0. ∃x∈A. x ≠ a ∧ dist x a < d ∧ ¬ l < f x"
      from q2 have "real_of_rat q2 < f a ∧ (∀x∈A. x < a ⟶ f x < real_of_rat q2)"
      proof auto
        fix x assume "x ∈ 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 ≤ f xa")
          by (auto intro: mono)
      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
      assume *[rule_format]: "∀d>0. ∃x∈A. x ≠ a ∧ dist x a < d ∧ ¬ u > f x"
      from q2 have "real_of_rat q2 > f a ∧ (∀x∈A. x > a ⟶ f x > real_of_rat q2)"
      proof auto
        fix x assume "x ∈ 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 ≥ f xa")
          by (auto intro: mono)
      qed
      thus ?thesis by auto
    qed
  qed
  hence "∃g :: real ⇒ nat × rat . ∀a ∈ {a∈A. ¬ continuous (at a within A) f}.
      (fst (g a) = 0 ∧ of_rat (snd (g a)) < f a ∧ (∀x ∈ A. x < a ⟶ f x < of_rat (snd (g a)))) |
      (fst (g a) = 1 ∧ of_rat (snd (g a)) > f a ∧ (∀x ∈ A. x > a ⟶ f x > of_rat (snd (g a))))"
    by (rule bchoice)
  then guess g ..
  hence g: "⋀a x. a ∈ A ⟹ ¬ continuous (at a within A) f ⟹ x ∈ A ⟹
      (fst (g a) = 0 ∧ of_rat (snd (g a)) < f a ∧ (x < a ⟶ f x < of_rat (snd (g a)))) |
      (fst (g a) = 1 ∧ of_rat (snd (g a)) > f a ∧ (x > a ⟶ f x > of_rat (snd (g a))))"
    by auto
  have "inj_on g {a∈A. ¬ continuous (at a within A) f}"
  proof (auto simp add: inj_on_def)
    fix w z
    assume 1: "w ∈ A" and 2: "¬ continuous (at w within A) f" and
           3: "z ∈ A" and 4: "¬ continuous (at z within A) f" and
           5: "g w = g z"
    from g [OF 1 2 3] g [OF 3 4 1] 5
    show "w = z" by auto
  qed
  thus ?thesis
    by (rule countableI')
qed

lemma mono_on_ctble_discont_open:
  fixes f :: "real ⇒ real"
  fixes A :: "real set"
  assumes "open A" "mono_on f A"
  shows "countable {a∈A. ¬isCont f a}"
proof -
  have "{a∈A. ¬isCont f a} = {a∈A. ¬(continuous (at a within A) f)}"
    by (auto simp add: continuous_within_open [OF _ ‹open A›])
  thus ?thesis
    apply (elim ssubst)
    by (rule mono_on_ctble_discont, rule assms)
qed

lemma mono_ctble_discont:
  fixes f :: "real ⇒ real"
  assumes "mono f"
  shows "countable {a. ¬ isCont f a}"
using assms mono_on_ctble_discont [of f UNIV] unfolding mono_on_def mono_def by auto

lemma has_real_derivative_imp_continuous_on:
  assumes "⋀x. x ∈ A ⟹ (f has_real_derivative f' x) (at x)"
  shows "continuous_on A f"
  apply (intro differentiable_imp_continuous_on, unfold differentiable_on_def)
  apply (intro ballI Deriv.differentiableI)
  apply (rule has_field_derivative_subset[OF assms])
  apply simp_all
  done

lemma closure_contains_Sup:
  fixes S :: "real set"
  assumes "S ≠ {}" "bdd_above S"
  shows "Sup S ∈ closure S"
proof-
  have "Inf (uminus ` S) ∈ 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
qed

lemma closed_contains_Sup:
  fixes S :: "real set"
  shows "S ≠ {} ⟹ bdd_above S ⟹ closed S ⟹ Sup S ∈ S"
  by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup)

lemma deriv_nonneg_imp_mono:
  assumes deriv: "⋀x. x ∈ {a..b} ⟹ (g has_real_derivative g' x) (at x)"
  assumes nonneg: "⋀x. x ∈ {a..b} ⟹ g' x ≥ 0"
  assumes ab: "a ≤ b"
  shows "g a ≤ g b"
proof (cases "a < b")
  assume "a < b"
  from deriv have "∀x. x ≥ a ∧ x ≤ b ⟶ (g has_real_derivative g' x) (at x)" by simp
  from MVT2[OF ‹a < b› this] and deriv
    obtain ξ where ξ_ab: "ξ > a" "ξ < b" and g_ab: "g b - g a = (b - a) * g' ξ" by blast
  from ξ_ab ab nonneg have "(b - a) * g' ξ ≥ 0" by simp
  with g_ab show ?thesis by simp
qed (insert ab, simp)

lemma continuous_interval_vimage_Int:
  assumes "continuous_on {a::real..b} g" and mono: "⋀x y. a ≤ x ⟹ x ≤ y ⟹ y ≤ b ⟹ g x ≤ g y"
  assumes "a ≤ b" "(c::real) ≤ d" "{c..d} ⊆ {g a..g b}"
  obtains c' d' where "{a..b} ∩ g -` {c..d} = {c'..d'}" "c' ≤ d'" "g c' = c" "g d' = d"
proof-
  let ?A = "{a..b} ∩ g -` {c..d}"
  from IVT'[of g a c b, OF _ _ ‹a ≤ b› assms(1)] assms(4,5)
  obtain c'' where c'': "c'' ∈ ?A" "g c'' = c" by auto
  from IVT'[of g a d b, OF _ _ ‹a ≤ b› assms(1)] assms(4,5)
  obtain d'' where d'': "d'' ∈ ?A" "g d'' = d" by auto
  hence [simp]: "?A ≠ {}" by blast

  define c' where "c' = Inf ?A"
  define d' where "d' = Sup ?A"
  have "?A ⊆ {c'..d'}" unfolding c'_def d'_def
    by (intro subsetI) (auto intro: cInf_lower cSup_upper)
  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' ∈ ?A" "d' ∈ ?A" unfolding c'_def d'_def
    by ((intro closed_contains_Inf closed_contains_Sup, simp_all)[])+
  hence "{c'..d'} ⊆ ?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]
             intro!: mono)
  moreover have "c' ≤ d'" using c'd'_in_set(2) unfolding c'_def by (intro cInf_lower) auto
  moreover have "g c' ≤ c" "g d' ≥ d"
    apply (insert c'' d'' c'd'_in_set)
    apply (subst c''(2)[symmetric])
    apply (auto simp: c'_def intro!: mono cInf_lower c'') []
    apply (subst d''(2)[symmetric])
    apply (auto simp: d'_def intro!: mono cSup_upper d'') []
    done
  with c'd'_in_set have "g c' = c" "g d' = d" by auto
  ultimately show ?thesis using that by blast
qed

subsection ‹Generic Borel spaces›

definition (in topological_space) borel :: "'a measure" where
  "borel = sigma UNIV {S. open S}"

abbreviation "borel_measurable M ≡ measurable M borel"

lemma in_borel_measurable:
   "f ∈ borel_measurable M ⟷
    (∀S ∈ sigma_sets UNIV {S. open S}. f -` S ∩ space M ∈ sets M)"
  by (auto simp add: measurable_def borel_def)

lemma in_borel_measurable_borel:
   "f ∈ borel_measurable M ⟷
    (∀S ∈ sets borel.
      f -` S ∩ space M ∈ sets M)"
  by (auto simp add: measurable_def borel_def)

lemma space_borel[simp]: "space borel = UNIV"
  unfolding borel_def by auto

lemma space_in_borel[measurable]: "UNIV ∈ sets borel"
  unfolding borel_def by auto

lemma sets_borel: "sets borel = sigma_sets UNIV {S. open S}"
  unfolding borel_def by (rule sets_measure_of) simp

lemma measurable_sets_borel:
    "⟦f ∈ measurable borel M; A ∈ sets M⟧ ⟹ f -` A ∈ sets borel"
  by (drule (1) measurable_sets) simp

lemma pred_Collect_borel[measurable (raw)]: "Measurable.pred borel P ⟹ {x. P x} ∈ sets borel"
  unfolding borel_def pred_def by auto

lemma borel_open[measurable (raw generic)]:
  assumes "open A" shows "A ∈ sets borel"
proof -
  have "A ∈ {S. open S}" unfolding mem_Collect_eq using assms .
  thus ?thesis unfolding borel_def by auto
qed

lemma borel_closed[measurable (raw generic)]:
  assumes "closed A" shows "A ∈ sets borel"
proof -
  have "space borel - (- A) ∈ sets borel"
    using assms unfolding closed_def by (blast intro: borel_open)
  thus ?thesis by simp
qed

lemma borel_singleton[measurable]:
  "A ∈ sets borel ⟹ insert x A ∈ sets (borel :: 'a::t1_space measure)"
  unfolding insert_def by (rule sets.Un) auto

lemma sets_borel_eq_count_space: "sets (borel :: 'a::{countable, t2_space} measure) = count_space UNIV"
proof -
  have "(⋃a∈A. {a}) ∈ sets borel" for A :: "'a set"
    by (intro sets.countable_UN') auto
  then show ?thesis
    by auto
qed

lemma borel_comp[measurable]: "A ∈ sets borel ⟹ - A ∈ sets borel"
  unfolding Compl_eq_Diff_UNIV by simp

lemma borel_measurable_vimage:
  fixes f :: "'a ⇒ 'x::t2_space"
  assumes borel[measurable]: "f ∈ borel_measurable M"
  shows "f -` {x} ∩ space M ∈ sets M"
  by simp

lemma borel_measurableI:
  fixes f :: "'a ⇒ 'x::topological_space"
  assumes "⋀S. open S ⟹ f -` S ∩ space M ∈ sets M"
  shows "f ∈ borel_measurable M"
  unfolding borel_def
proof (rule measurable_measure_of, simp_all)
  fix S :: "'x set" assume "open S" thus "f -` S ∩ space M ∈ sets M"
    using assms[of S] by simp
qed

lemma borel_measurable_const:
  "(λx. c) ∈ borel_measurable M"
  by auto

lemma borel_measurable_indicator:
  assumes A: "A ∈ sets M"
  shows "indicator A ∈ borel_measurable M"
  unfolding indicator_def [abs_def] using A
  by (auto intro!: measurable_If_set)

lemma borel_measurable_count_space[measurable (raw)]:
  "f ∈ borel_measurable (count_space S)"
  unfolding measurable_def by auto

lemma borel_measurable_indicator'[measurable (raw)]:
  assumes [measurable]: "{x∈space M. f x ∈ A x} ∈ sets M"
  shows "(λx. indicator (A x) (f x)) ∈ borel_measurable M"
  unfolding indicator_def[abs_def]
  by (auto intro!: measurable_If)

lemma borel_measurable_indicator_iff:
  "(indicator A :: 'a ⇒ 'x::{t1_space, zero_neq_one}) ∈ borel_measurable M ⟷ A ∩ space M ∈ sets M"
    (is "?I ∈ borel_measurable M ⟷ _")
proof
  assume "?I ∈ borel_measurable M"
  then have "?I -` {1} ∩ space M ∈ sets M"
    unfolding measurable_def by auto
  also have "?I -` {1} ∩ space M = A ∩ space M"
    unfolding indicator_def [abs_def] by auto
  finally show "A ∩ space M ∈ sets M" .
next
  assume "A ∩ space M ∈ sets M"
  moreover have "?I ∈ borel_measurable M ⟷
    (indicator (A ∩ space M) :: 'a ⇒ 'x) ∈ borel_measurable M"
    by (intro measurable_cong) (auto simp: indicator_def)
  ultimately show "?I ∈ borel_measurable M" by auto
qed

lemma borel_measurable_subalgebra:
  assumes "sets N ⊆ sets M" "space N = space M" "f ∈ borel_measurable N"
  shows "f ∈ borel_measurable M"
  using assms unfolding measurable_def by auto

lemma borel_measurable_restrict_space_iff_ereal:
  fixes f :: "'a ⇒ ereal"
  assumes Ω[measurable, simp]: "Ω ∩ space M ∈ sets M"
  shows "f ∈ borel_measurable (restrict_space M Ω) ⟷
    (λx. f x * indicator Ω x) ∈ borel_measurable M"
  by (subst measurable_restrict_space_iff)
     (auto simp: indicator_def if_distrib[where f="λx. a * x" for a] cong del: if_weak_cong)

lemma borel_measurable_restrict_space_iff_ennreal:
  fixes f :: "'a ⇒ ennreal"
  assumes Ω[measurable, simp]: "Ω ∩ space M ∈ sets M"
  shows "f ∈ borel_measurable (restrict_space M Ω) ⟷
    (λx. f x * indicator Ω x) ∈ borel_measurable M"
  by (subst measurable_restrict_space_iff)
     (auto simp: indicator_def if_distrib[where f="λx. a * x" for a] cong del: if_weak_cong)

lemma borel_measurable_restrict_space_iff:
  fixes f :: "'a ⇒ 'b::real_normed_vector"
  assumes Ω[measurable, simp]: "Ω ∩ space M ∈ sets M"
  shows "f ∈ borel_measurable (restrict_space M Ω) ⟷
    (λx. indicator Ω x *R f x) ∈ borel_measurable M"
  by (subst measurable_restrict_space_iff)
     (auto simp: indicator_def if_distrib[where f="λx. x *R a" for a] ac_simps
       cong del: if_weak_cong)

lemma cbox_borel[measurable]: "cbox a b ∈ sets borel"
  by (auto intro: borel_closed)

lemma box_borel[measurable]: "box a b ∈ sets borel"
  by (auto intro: borel_open)

lemma borel_compact: "compact (A::'a::t2_space set) ⟹ A ∈ sets borel"
  by (auto intro: borel_closed dest!: compact_imp_closed)

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"
  shows "borel = sigma UNIV X"
  unfolding borel_def
proof (intro sigma_eqI sigma_sets_eqI)
  interpret X: sigma_algebra UNIV "sigma_sets UNIV X"
    by (rule sigma_algebra_sigma_sets) simp

  fix S :: "'a set" assume "S ∈ Collect open"
  then have "generate_topology X S"
    by (auto simp: eq)
  then show "S ∈ sigma_sets UNIV X"
  proof induction
    case (UN K)
    then have K: "⋀k. k ∈ K ⟹ open k"
      unfolding eq by auto
    from ex_countable_basis obtain B :: "'a set set" where
      B:  "⋀b. b ∈ B ⟹ open b" "⋀X. open X ⟹ ∃b⊆B. (⋃b) = X" and "countable B"
      by (auto simp: topological_basis_def)
    from B(2)[OF K] obtain m where m: "⋀k. k ∈ K ⟹ m k ⊆ B" "⋀k. k ∈ K ⟹ (⋃m k) = k"
      by metis
    define U where "U = (⋃k∈K. m k)"
    with m have "countable U"
      by (intro countable_subset[OF _ ‹countable B›]) auto
    have "⋃U = (⋃A∈U. A)" by simp
    also have "… = ⋃K"
      unfolding U_def UN_simps by (simp add: m)
    finally have "⋃U = ⋃K" .

    have "∀b∈U. ∃k∈K. b ⊆ k"
      using m by (auto simp: U_def)
    then obtain u where u: "⋀b. b ∈ U ⟹ u b ∈ K" and "⋀b. b ∈ U ⟹ b ⊆ u b"
      by metis
    then have "(⋃b∈U. u b) ⊆ ⋃K" "⋃U ⊆ (⋃b∈U. u b)"
      by auto
    then have "⋃K = (⋃b∈U. u b)"
      unfolding ‹⋃U = ⋃K› by auto
    also have "… ∈ sigma_sets UNIV X"
      using u UN by (intro X.countable_UN' ‹countable U›) auto
    finally show "⋃K ∈ sigma_sets UNIV X" .
  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"
  shows "f ∈ borel_measurable (restrict_space borel A)"
proof (rule borel_measurableI)
  fix S :: "'b set" assume "open S"
  with f obtain T where "f -` S ∩ A = T ∩ A" "open T"
    by (metis continuous_on_open_invariant)
  then show "f -` S ∩ space (restrict_space borel A) ∈ sets (restrict_space borel A)"
    by (force simp add: sets_restrict_space space_restrict_space)
qed

lemma borel_measurable_continuous_on1: "continuous_on UNIV f ⟹ f ∈ borel_measurable borel"
  by (drule borel_measurable_continuous_on_restrict) simp

lemma borel_measurable_continuous_on_if:
  "A ∈ sets borel ⟹ continuous_on A f ⟹ continuous_on (- A) g ⟹
    (λx. if x ∈ A then f x else g x) ∈ borel_measurable borel"
  by (auto simp add: measurable_If_restrict_space_iff Collect_neg_eq
           intro!: borel_measurable_continuous_on_restrict)

lemma borel_measurable_continuous_countable_exceptions:
  fixes f :: "'a::t1_space ⇒ 'b::topological_space"
  assumes X: "countable X"
  assumes "continuous_on (- X) f"
  shows "f ∈ borel_measurable borel"
proof (rule measurable_discrete_difference[OF _ X])
  have "X ∈ sets borel"
    by (rule sets.countable[OF _ X]) auto
  then show "(λx. if x ∈ X then undefined else f x) ∈ borel_measurable borel"
    by (intro borel_measurable_continuous_on_if assms continuous_intros)
qed auto

lemma borel_measurable_continuous_on:
  assumes f: "continuous_on UNIV f" and g: "g ∈ borel_measurable M"
  shows "(λx. f (g x)) ∈ borel_measurable M"
  using measurable_comp[OF g borel_measurable_continuous_on1[OF f]] by (simp add: comp_def)

lemma borel_measurable_continuous_on_indicator:
  fixes f g :: "'a::topological_space ⇒ 'b::real_normed_vector"
  shows "A ∈ sets borel ⟹ continuous_on A f ⟹ (λx. indicator A x *R f x) ∈ borel_measurable borel"
  by (subst borel_measurable_restrict_space_iff[symmetric])
     (auto intro: borel_measurable_continuous_on_restrict)

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"
  assumes g[measurable]: "g ∈ borel_measurable M"
  shows "(λx. (f x, g x)) ∈ borel_measurable M"
proof (subst borel_eq_countable_basis)
  let ?B = "SOME B::'b set set. countable B ∧ topological_basis B"
  let ?C = "SOME B::'c set set. countable B ∧ topological_basis B"
  let ?P = "(λ(b, c). b × c) ` (?B × ?C)"
  show "countable ?P" "topological_basis ?P"
    by (auto intro!: countable_basis topological_basis_prod is_basis)

  show "(λx. (f x, g x)) ∈ measurable M (sigma UNIV ?P)"
  proof (rule measurable_measure_of)
    fix S assume "S ∈ ?P"
    then obtain b c where "b ∈ ?B" "c ∈ ?C" and S: "S = b × c" by auto
    then have borel: "open b" "open c"
      by (auto intro: is_basis topological_basis_open)
    have "(λx. (f x, g x)) -` S ∩ space M = (f -` b ∩ space M) ∩ (g -` c ∩ space M)"
      unfolding S by auto
    also have "… ∈ sets M"
      using borel by simp
    finally show "(λx. (f x, g x)) -` S ∩ space M ∈ sets M" .
  qed auto
qed

lemma borel_measurable_continuous_Pair:
  fixes f :: "'a ⇒ 'b::second_countable_topology" and g :: "'a ⇒ 'c::second_countable_topology"
  assumes [measurable]: "f ∈ borel_measurable M"
  assumes [measurable]: "g ∈ borel_measurable M"
  assumes H: "continuous_on UNIV (λx. H (fst x) (snd x))"
  shows "(λx. H (f x) (g x)) ∈ borel_measurable M"
proof -
  have eq: "(λx. H (f x) (g x)) = (λx. (λx. H (fst x) (snd x)) (f x, g x))" by auto
  show ?thesis
    unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
qed

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<..<b} ∈ 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..<b} ∈ 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)"
  unfolding second_countable_borel_measurable[OF open_generated_order]
proof (intro sigma_eqI sigma_sets_eqI)
  from countable_dense_setE guess D :: "'a set" . note D = this

  interpret L: sigma_algebra UNIV "sigma_sets UNIV (range lessThan)"
    by (rule sigma_algebra_sigma_sets) simp

  fix A :: "'a set" assume "A ∈ range lessThan ∪ range greaterThan"
  then obtain y where "A = {y <..} ∨ A = {..< y}"
    by blast
  then show "A ∈ sigma_sets UNIV (range lessThan)"
  proof
    assume A: "A = {y <..}"
    show ?thesis
    proof cases
      assume "∀x>y. ∃d. y < d ∧ d < x"
      with D(2)[of "{y <..< x}" for x] have "∀x>y. ∃d∈D. y < d ∧ d < x"
        by (auto simp: set_eq_iff)
      then have "A = UNIV - (⋂d∈{d∈D. y < d}. {..< d})"
        by (auto simp: A) (metis less_asym)
      also have "… ∈ sigma_sets UNIV (range lessThan)"
        using D(1) by (intro L.Diff L.top L.countable_INT'') auto
      finally show ?thesis .
    next
      assume "¬ (∀x>y. ∃d. y < d ∧ d < x)"
      then obtain x where "y < x"  "⋀d. y < d ⟹ ¬ d < x"
        by auto
      then have "A = UNIV - {..< x}"
        unfolding A by (auto simp: not_less[symmetric])
      also have "… ∈ sigma_sets UNIV (range lessThan)"
        by auto
      finally show ?thesis .
    qed
  qed auto
qed auto

lemma borel_Ioi:
  "borel = sigma UNIV (range greaterThan :: 'a::{linorder_topology, second_countable_topology} set set)"
  unfolding second_countable_borel_measurable[OF open_generated_order]
proof (intro sigma_eqI sigma_sets_eqI)
  from countable_dense_setE guess D :: "'a set" . note D = this

  interpret L: sigma_algebra UNIV "sigma_sets UNIV (range greaterThan)"
    by (rule sigma_algebra_sigma_sets) simp

  fix A :: "'a set" assume "A ∈ range lessThan ∪ range greaterThan"
  then obtain y where "A = {y <..} ∨ A = {..< y}"
    by blast
  then show "A ∈ sigma_sets UNIV (range greaterThan)"
  proof
    assume A: "A = {..< y}"
    show ?thesis
    proof cases
      assume "∀x<y. ∃d. x < d ∧ d < y"
      with D(2)[of "{x <..< y}" for x] have "∀x<y. ∃d∈D. x < d ∧ d < y"
        by (auto simp: set_eq_iff)
      then have "A = UNIV - (⋂d∈{d∈D. d < y}. {d <..})"
        by (auto simp: A) (metis less_asym)
      also have "… ∈ sigma_sets UNIV (range greaterThan)"
        using D(1) by (intro L.Diff L.top L.countable_INT'') auto
      finally show ?thesis .
    next
      assume "¬ (∀x<y. ∃d. x < d ∧ d < y)"
      then obtain x where "x < y"  "⋀d. y > d ⟹ x ≥ d"
        by (auto simp: not_less[symmetric])
      then have "A = UNIV - {x <..}"
        unfolding A Compl_eq_Diff_UNIV[symmetric] by auto
      also have "… ∈ sigma_sets UNIV (range greaterThan)"
        by auto
      finally show ?thesis .
    qed
  qed auto
qed auto

lemma borel_measurableI_less:
  fixes f :: "'a ⇒ 'b::{linorder_topology, second_countable_topology}"
  shows "(⋀y. {x∈space M. f x < y} ∈ sets M) ⟹ f ∈ borel_measurable M"
  unfolding borel_Iio
  by (rule measurable_measure_of) (auto simp: Int_def conj_commute)

lemma borel_measurableI_greater:
  fixes f :: "'a ⇒ 'b::{linorder_topology, second_countable_topology}"
  shows "(⋀y. {x∈space M. y < f x} ∈ sets M) ⟹ f ∈ borel_measurable M"
  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, 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, 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"
  assumes [measurable]: "⋀i. i ∈ I ⟹ F i ∈ borel_measurable M"
  shows "(λx. SUP i:I. F i x) ∈ borel_measurable M"
  by (rule borel_measurableI_greater) (simp add: less_SUP_iff)

lemma borel_measurable_INF[measurable (raw)]:
  fixes F :: "_ ⇒ _ ⇒ _::{complete_linorder, linorder_topology, second_countable_topology}"
  assumes [simp]: "countable I"
  assumes [measurable]: "⋀i. i ∈ I ⟹ F i ∈ borel_measurable M"
  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"
  assumes *: "⋀f. f ∈ borel_measurable M ⟹ F f ∈ borel_measurable M"
  shows "lfp F ∈ borel_measurable M"
proof -
  { fix i have "((F ^^ i) bot) ∈ borel_measurable M"
      by (induct i) (auto intro!: *) }
  then have "(λx. SUP i. (F ^^ i) bot x) ∈ borel_measurable M"
    by measurable
  also have "(λx. SUP i. (F ^^ i) bot x) = (SUP i. (F ^^ i) bot)"
    by auto
  also have "(SUP i. (F ^^ i) bot) = lfp F"
    by (rule sup_continuous_lfp[symmetric]) fact
  finally show ?thesis .
qed

lemma borel_measurable_gfp[consumes 1, case_names continuity step]:
  fixes F :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b::{complete_linorder, linorder_topology, second_countable_topology})"
  assumes "inf_continuous F"
  assumes *: "⋀f. f ∈ borel_measurable M ⟹ F f ∈ borel_measurable M"
  shows "gfp F ∈ borel_measurable M"
proof -
  { fix i have "((F ^^ i) top) ∈ borel_measurable M"
      by (induct i) (auto intro!: * simp: bot_fun_def) }
  then have "(λx. INF i. (F ^^ i) top x) ∈ borel_measurable M"
    by measurable
  also have "(λx. INF i. (F ^^ i) top x) = (INF i. (F ^^ i) top)"
    by auto
  also have "… = gfp F"
    by (rule inf_continuous_gfp[symmetric]) fact
  finally show ?thesis .
qed

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, 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, 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, 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, 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_sum[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, 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}"
  assumes "f ∈ borel_measurable M"
  assumes "g ∈ borel_measurable M"
  shows "(λx. f x ∙ g x) ∈ borel_measurable M"
  using assms
  by (rule borel_measurable_continuous_Pair) (intro continuous_intros)

notation
  eucl_less (infix "<e" 50)

lemma box_oc: "{x. a <e x ∧ x ≤ b} = {x. a <e x} ∩ {..b}"
  and box_co: "{x. a ≤ x ∧ x <e b} = {a..} ∩ {x. x <e b}"
  by auto

lemma eucl_ivals[measurable]:
  fixes a b :: "'a::ordered_euclidean_space"
  shows "{x. x <e a} ∈ sets borel"
    and "{x. a <e x} ∈ sets borel"
    and "{..a} ∈ sets borel"
    and "{a..} ∈ sets borel"
    and "{a..b} ∈ sets borel"
    and  "{x. a <e x ∧ x ≤ b} ∈ sets borel"
    and "{x. a ≤ x ∧  x <e b} ∈ sets borel"
  unfolding box_oc box_co
  by (auto intro: borel_open borel_closed)

lemma
  fixes i :: "'a::{second_countable_topology, real_inner}"
  shows hafspace_less_borel: "{x. a < x ∙ i} ∈ sets borel"
    and hafspace_greater_borel: "{x. x ∙ i < a} ∈ sets borel"
    and hafspace_less_eq_borel: "{x. a ≤ x ∙ i} ∈ sets borel"
    and hafspace_greater_eq_borel: "{x. x ∙ i ≤ a} ∈ sets borel"
  by simp_all

lemma borel_eq_box:
  "borel = sigma UNIV (range (λ (a, b). box a b :: 'a :: euclidean_space set))"
    (is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI1[OF borel_def])
  fix M :: "'a set" assume "M ∈ {S. open S}"
  then have "open M" by simp
  show "M ∈ ?SIGMA"
    apply (subst open_UNION_box[OF ‹open M›])
    apply (safe intro!: sets.countable_UN' countable_PiE countable_Collect)
    apply (auto intro: countable_rat)
    done
qed (auto simp: box_def)

lemma halfspace_gt_in_halfspace:
  assumes i: "i ∈ A"
  shows "{x::'a. a < x ∙ i} ∈
    sigma_sets UNIV ((λ (a, i). {x::'a::euclidean_space. x ∙ i < a}) ` (UNIV × A))"
  (is "?set ∈ ?SIGMA")
proof -
  interpret sigma_algebra UNIV ?SIGMA
    by (intro sigma_algebra_sigma_sets) simp_all
  have *: "?set = (⋃n. UNIV - {x::'a. x ∙ i < a + 1 / real (Suc n)})"
  proof (safe, simp_all add: not_less del: of_nat_Suc)
    fix x :: 'a assume "a < x ∙ i"
    with reals_Archimedean[of "x ∙ i - a"]
    obtain n where "a + 1 / real (Suc n) < x ∙ i"
      by (auto simp: field_simps)
    then show "∃n. a + 1 / real (Suc n) ≤ x ∙ i"
      by (blast intro: less_imp_le)
  next
    fix x n
    have "a < a + 1 / real (Suc n)" by auto
    also assume "… ≤ x"
    finally show "a < x" .
  qed
  show "?set ∈ ?SIGMA" unfolding *
    by (auto intro!: Diff sigma_sets_Inter i)
qed

lemma borel_eq_halfspace_less:
  "borel = sigma UNIV ((λ(a, i). {x::'a::euclidean_space. x ∙ i < a}) ` (UNIV × Basis))"
  (is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI2[OF borel_eq_box])
  fix a b :: 'a
  have "box a b = {x∈space ?SIGMA. ∀i∈Basis. a ∙ i < x ∙ i ∧ x ∙ i < b ∙ i}"
    by (auto simp: box_def)
  also have "… ∈ sets ?SIGMA"
    by (intro sets.sets_Collect_conj sets.sets_Collect_finite_All sets.sets_Collect_const)
       (auto intro!: halfspace_gt_in_halfspace countable_PiE countable_rat)
  finally show "box a b ∈ sets ?SIGMA" .
qed auto

lemma borel_eq_halfspace_le:
  "borel = sigma UNIV ((λ (a, i). {x::'a::euclidean_space. x ∙ i ≤ a}) ` (UNIV × Basis))"
  (is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less])
  fix a :: real and i :: 'a assume "(a, i) ∈ UNIV × Basis"
  then have i: "i ∈ Basis" by auto
  have *: "{x::'a. x∙i < a} = (⋃n. {x. x∙i ≤ a - 1/real (Suc n)})"
  proof (safe, simp_all del: of_nat_Suc)
    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)
    then show "∃n. x ∙ i ≤ a - 1 / (real (Suc n))"
      by (blast intro: less_imp_le)
  next
    fix x::'a and n
    assume "x∙i ≤ a - 1 / real (Suc n)"
    also have "… < a" by auto
    finally show "x∙i < a" .
  qed
  show "{x. x∙i < a} ∈ ?SIGMA" unfolding *
    by (intro sets.countable_UN) (auto intro: i)
qed auto

lemma borel_eq_halfspace_ge:
  "borel = sigma UNIV ((λ (a, i). {x::'a::euclidean_space. a ≤ x ∙ i}) ` (UNIV × Basis))"
  (is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less])
  fix a :: real and i :: 'a assume i: "(a, i) ∈ UNIV × Basis"
  have *: "{x::'a. x∙i < a} = space ?SIGMA - {x::'a. a ≤ x∙i}" by auto
  show "{x. x∙i < a} ∈ ?SIGMA" unfolding *
    using i by (intro sets.compl_sets) auto
qed auto

lemma borel_eq_halfspace_greater:
  "borel = sigma UNIV ((λ (a, i). {x::'a::euclidean_space. a < x ∙ i}) ` (UNIV × Basis))"
  (is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_le])
  fix a :: real and i :: 'a assume "(a, i) ∈ (UNIV × Basis)"
  then have i: "i ∈ Basis" by auto
  have *: "{x::'a. x∙i ≤ a} = space ?SIGMA - {x::'a. a < x∙i}" by auto
  show "{x. x∙i ≤ a} ∈ ?SIGMA" unfolding *
    by (intro sets.compl_sets) (auto intro: i)
qed auto

lemma borel_eq_atMost:
  "borel = sigma UNIV (range (λa. {..a::'a::ordered_euclidean_space}))"
  (is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le])
  fix a :: real and i :: 'a assume "(a, i) ∈ UNIV × Basis"
  then have "i ∈ Basis" by auto
  then have *: "{x::'a. x∙i ≤ a} = (⋃k::nat. {.. (∑n∈Basis. (if n = i then a else real k)*R n)})"
  proof (safe, simp_all add: eucl_le[where 'a='a] split: if_split_asm)
    fix x :: 'a
    from real_arch_simple[of "Max ((λi. x∙i)`Basis)"] guess k::nat ..
    then have "⋀i. i ∈ Basis ⟹ x∙i ≤ real k"
      by (subst (asm) Max_le_iff) auto
    then show "∃k::nat. ∀ia∈Basis. ia ≠ i ⟶ x ∙ ia ≤ real k"
      by (auto intro!: exI[of _ k])
  qed
  show "{x. x∙i ≤ a} ∈ ?SIGMA" unfolding *
    by (intro sets.countable_UN) auto
qed auto

lemma borel_eq_greaterThan:
  "borel = sigma UNIV (range (λa::'a::ordered_euclidean_space. {x. a <e x}))"
  (is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le])
  fix a :: real and i :: 'a assume "(a, i) ∈ UNIV × Basis"
  then have i: "i ∈ Basis" by auto
  have "{x::'a. x∙i ≤ a} = UNIV - {x::'a. a < x∙i}" by auto
  also have *: "{x::'a. a < x∙i} =
      (⋃k::nat. {x. (∑n∈Basis. (if n = i then a else -real k) *R n) <e x})" using i
  proof (safe, simp_all add: eucl_less_def split: if_split_asm)
    fix x :: 'a
    from reals_Archimedean2[of "Max ((λi. -x∙i)`Basis)"]
    guess k::nat .. note k = this
    { fix i :: 'a assume "i ∈ Basis"
      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 "∃k::nat. ∀ia∈Basis. ia ≠ i ⟶ -real k < x ∙ ia"
      by (auto intro!: exI[of _ k])
  qed
  finally show "{x. x∙i ≤ a} ∈ ?SIGMA"
    apply (simp only:)
    apply (intro sets.countable_UN sets.Diff)
    apply (auto intro: sigma_sets_top)
    done
qed auto

lemma borel_eq_lessThan:
  "borel = sigma UNIV (range (λa::'a::ordered_euclidean_space. {x. x <e a}))"
  (is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_ge])
  fix a :: real and i :: 'a assume "(a, i) ∈ UNIV × Basis"
  then have i: "i ∈ Basis" by auto
  have "{x::'a. a ≤ x∙i} = UNIV - {x::'a. x∙i < a}" by auto
  also have *: "{x::'a. x∙i < a} = (⋃k::nat. {x. x <e (∑n∈Basis. (if n = i then a else real k) *R n)})" using ‹i∈ Basis›
  proof (safe, simp_all add: eucl_less_def split: if_split_asm)
    fix x :: 'a
    from reals_Archimedean2[of "Max ((λi. x∙i)`Basis)"]
    guess k::nat .. note k = this
    { fix i :: 'a assume "i ∈ Basis"
      then have "x∙i < real k"
        using k by (subst (asm) Max_less_iff) auto
      then have "x∙i < real k" by simp }
    then show "∃k::nat. ∀ia∈Basis. ia ≠ i ⟶ x ∙ ia < real k"
      by (auto intro!: exI[of _ k])
  qed
  finally show "{x. a ≤ x∙i} ∈ ?SIGMA"
    apply (simp only:)
    apply (intro sets.countable_UN sets.Diff)
    apply (auto intro: sigma_sets_top )
    done
qed auto

lemma borel_eq_atLeastAtMost:
  "borel = sigma UNIV (range (λ(a,b). {a..b} ::'a::ordered_euclidean_space set))"
  (is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI5[OF borel_eq_atMost])
  fix a::'a
  have *: "{..a} = (⋃n::nat. {- real n *R One .. a})"
  proof (safe, simp_all add: eucl_le[where 'a='a])
    fix x :: 'a
    from real_arch_simple[of "Max ((λi. - x∙i)`Basis)"]
    guess k::nat .. note k = this
    { fix i :: 'a assume "i ∈ Basis"
      with k have "- x∙i ≤ real k"
        by (subst (asm) Max_le_iff) (auto simp: field_simps)
      then have "- real k ≤ x∙i" by simp }
    then show "∃n::nat. ∀i∈Basis. - real n ≤ x ∙ i"
      by (auto intro!: exI[of _ k])
  qed
  show "{..a} ∈ ?SIGMA" unfolding *
    by (intro sets.countable_UN)
       (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
  have "{..i} = (⋃j::nat. {-j <.. i})"
    by (auto simp: minus_less_iff reals_Archimedean2)
  also have "… ∈ sets (sigma UNIV (range (λ(i, j). {i<..j})))"
    by (intro sets.countable_nat_UN) auto
  finally show "{..i} ∈ sets (sigma UNIV (range (λ(i, j). {i<..j})))" .
qed simp

lemma eucl_lessThan: "{x::real. x <e a} = lessThan a"
  by (simp add: eucl_less_def lessThan_def)

lemma borel_eq_atLeastLessThan:
  "borel = sigma UNIV (range (λ(a, b). {a ..< b :: real}))" (is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI5[OF borel_eq_lessThan])
  have move_uminus: "⋀x y::real. -x ≤ y ⟷ -y ≤ x" by auto
  fix x :: real
  have "{..<x} = (⋃i::nat. {-real i ..< x})"
    by (auto simp: move_uminus real_arch_simple)
  then show "{y. y <e x} ∈ ?SIGMA"
    by (auto intro: sigma_sets.intros(2-) simp: eucl_lessThan)
qed auto

lemma borel_measurable_halfspacesI:
  fixes f :: "'a ⇒ 'c::euclidean_space"
  assumes F: "borel = sigma UNIV (F ` (UNIV × Basis))"
  and S_eq: "⋀a i. S a i = f -` F (a,i) ∩ space M"
  shows "f ∈ borel_measurable M = (∀i∈Basis. ∀a::real. S a i ∈ sets M)"
proof safe
  fix a :: real and i :: 'b assume i: "i ∈ Basis" and f: "f ∈ borel_measurable M"
  then show "S a i ∈ sets M" unfolding assms
    by (auto intro!: measurable_sets simp: assms(1))
next
  assume a: "∀i∈Basis. ∀a. S a i ∈ sets M"
  then show "f ∈ borel_measurable M"
    by (auto intro!: measurable_measure_of simp: S_eq F)
qed

lemma borel_measurable_iff_halfspace_le:
  fixes f :: "'a ⇒ 'c::euclidean_space"
  shows "f ∈ borel_measurable M = (∀i∈Basis. ∀a. {w ∈ space M. f w ∙ i ≤ a} ∈ sets M)"
  by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto

lemma borel_measurable_iff_halfspace_less:
  fixes f :: "'a ⇒ 'c::euclidean_space"
  shows "f ∈ borel_measurable M ⟷ (∀i∈Basis. ∀a. {w ∈ space M. f w ∙ i < a} ∈ sets M)"
  by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto

lemma borel_measurable_iff_halfspace_ge:
  fixes f :: "'a ⇒ 'c::euclidean_space"
  shows "f ∈ borel_measurable M = (∀i∈Basis. ∀a. {w ∈ space M. a ≤ f w ∙ i} ∈ sets M)"
  by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto

lemma borel_measurable_iff_halfspace_greater:
  fixes f :: "'a ⇒ 'c::euclidean_space"
  shows "f ∈ borel_measurable M ⟷ (∀i∈Basis. ∀a. {w ∈ space M. a < f w ∙ i} ∈ sets M)"
  by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_greater]) auto

lemma borel_measurable_iff_le:
  "(f::'a ⇒ real) ∈ borel_measurable M = (∀a. {w ∈ space M. f w ≤ a} ∈ sets M)"
  using borel_measurable_iff_halfspace_le[where 'c=real] by simp

lemma borel_measurable_iff_less:
  "(f::'a ⇒ real) ∈ borel_measurable M = (∀a. {w ∈ space M. f w < a} ∈ sets M)"
  using borel_measurable_iff_halfspace_less[where 'c=real] by simp

lemma borel_measurable_iff_ge:
  "(f::'a ⇒ real) ∈ borel_measurable M = (∀a. {w ∈ space M. a ≤ f w} ∈ sets M)"
  using borel_measurable_iff_halfspace_ge[where 'c=real]
  by simp

lemma borel_measurable_iff_greater:
  "(f::'a ⇒ real) ∈ borel_measurable M = (∀a. {w ∈ space M. a < f w} ∈ sets M)"
  using borel_measurable_iff_halfspace_greater[where 'c=real] by simp

lemma borel_measurable_euclidean_space:
  fixes f :: "'a ⇒ 'c::euclidean_space"
  shows "f ∈ borel_measurable M ⟷ (∀i∈Basis. (λx. f x ∙ i) ∈ borel_measurable M)"
proof safe
  assume f: "∀i∈Basis. (λx. f x ∙ i) ∈ borel_measurable M"
  then show "f ∈ borel_measurable M"
    by (subst borel_measurable_iff_halfspace_le) auto
qed auto

subsection "Borel measurable operators"

lemma borel_measurable_norm[measurable]: "norm ∈ borel_measurable borel"
  by (intro borel_measurable_continuous_on1 continuous_intros)

lemma borel_measurable_sgn [measurable]: "(sgn::'a::real_normed_vector ⇒ 'a) ∈ borel_measurable borel"
  by (rule borel_measurable_continuous_countable_exceptions[where X="{0}"])
     (auto intro!: continuous_on_sgn continuous_on_id)

lemma borel_measurable_uminus[measurable (raw)]:
  fixes g :: "'a ⇒ 'b::{second_countable_topology, real_normed_vector}"
  assumes g: "g ∈ borel_measurable M"
  shows "(λx. - g x) ∈ borel_measurable M"
  by (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_intros)

lemma borel_measurable_diff[measurable (raw)]:
  fixes f :: "'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 borel_measurable_add [of f M "- g"] assms by (simp add: fun_Compl_def)

lemma borel_measurable_times[measurable (raw)]:
  fixes f :: "'a ⇒ 'b::{second_countable_topology, real_normed_algebra}"
  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_prod[measurable (raw)]:
  fixes f :: "'c ⇒ 'a ⇒ 'b::{second_countable_topology, real_normed_field}"
  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_dist[measurable (raw)]:
  fixes g f :: "'a ⇒ 'b::{second_countable_topology, metric_space}"
  assumes f: "f ∈ borel_measurable M"
  assumes g: "g ∈ borel_measurable M"
  shows "(λx. dist (f x) (g x)) ∈ borel_measurable M"
  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)

lemma borel_measurable_scaleR[measurable (raw)]:
  fixes 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 *R g x) ∈ borel_measurable M"
  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)

lemma borel_measurable_uminus_eq [simp]:
  fixes f :: "'a ⇒ 'b::{second_countable_topology, real_normed_vector}"
  shows "(λx. - f x) ∈ borel_measurable M ⟷ f ∈ borel_measurable M" (is "?l = ?r")
proof
  assume ?l from borel_measurable_uminus[OF this] show ?r by simp
qed auto

lemma affine_borel_measurable_vector:
  fixes f :: "'a ⇒ 'x::real_normed_vector"
  assumes "f ∈ borel_measurable M"
  shows "(λx. a + b *R f x) ∈ borel_measurable M"
proof (rule borel_measurableI)
  fix S :: "'x set" assume "open S"
  show "(λx. a + b *R f x) -` S ∩ space M ∈ sets M"
  proof cases
    assume "b ≠ 0"
    with ‹open S› have "open ((λx. (- a + x) /R b) ` S)" (is "open ?S")
      using open_affinity [of S "inverse b" "- a /R b"]
      by (auto simp: algebra_simps)
    hence "?S ∈ sets borel" by auto
    moreover
    from ‹b ≠ 0› have "(λx. a + b *R f x) -` S = f -` ?S"
      apply auto by (rule_tac x="a + b *R f x" in image_eqI, simp_all)
    ultimately show ?thesis using assms unfolding in_borel_measurable_borel
      by auto
  qed simp
qed

lemma borel_measurable_const_scaleR[measurable (raw)]:
  "f ∈ borel_measurable M ⟹ (λx. b *R f x ::'a::real_normed_vector) ∈ borel_measurable M"
  using affine_borel_measurable_vector[of f M 0 b] by simp

lemma borel_measurable_const_add[measurable (raw)]:
  "f ∈ borel_measurable M ⟹ (λx. a + f x ::'a::real_normed_vector) ∈ borel_measurable M"
  using affine_borel_measurable_vector[of f M a 1] by simp

lemma borel_measurable_inverse[measurable (raw)]:
  fixes f :: "'a ⇒ 'b::real_normed_div_algebra"
  assumes f: "f ∈ borel_measurable M"
  shows "(λx. inverse (f x)) ∈ borel_measurable M"
  apply (rule measurable_compose[OF f])
  apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"])
  apply (auto intro!: continuous_on_inverse continuous_on_id)
  done

lemma borel_measurable_divide[measurable (raw)]:
  "f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹
    (λx. f x / g x::'b::{second_countable_topology, real_normed_div_algebra}) ∈ borel_measurable M"
  by (simp add: divide_inverse)

lemma borel_measurable_abs[measurable (raw)]:
  "f ∈ borel_measurable M ⟹ (λx. ¦f x :: real¦) ∈ borel_measurable M"
  unfolding abs_real_def by simp

lemma borel_measurable_nth[measurable (raw)]:
  "(λx::real^'n. x $ i) ∈ borel_measurable borel"
  by (simp add: cart_eq_inner_axis)

lemma convex_measurable:
  fixes A :: "'a :: euclidean_space set"
  shows "X ∈ borel_measurable M ⟹ X ` space M ⊆ A ⟹ open A ⟹ convex_on A q ⟹
    (λx. q (X x)) ∈ 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)]:
  assumes f: "f ∈ borel_measurable M"
  shows "(λx. ln (f x :: real)) ∈ borel_measurable M"
  apply (rule measurable_compose[OF f])
  apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"])
  apply (auto intro!: continuous_on_ln continuous_on_id)
  done

lemma borel_measurable_log[measurable (raw)]:
  "f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ (λx. log (g x) (f x)) ∈ borel_measurable M"
  unfolding log_def by auto

lemma borel_measurable_exp[measurable]:
  "(exp::'a::{real_normed_field,banach}⇒'a) ∈ borel_measurable borel"
  by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_exp)

lemma measurable_real_floor[measurable]:
  "(floor :: real ⇒ int) ∈ measurable borel (count_space UNIV)"
proof -
  have "⋀a x. ⌊x⌋ = a ⟷ (real_of_int a ≤ x ∧ x < real_of_int (a + 1))"
    by (auto intro: floor_eq2)
  then show ?thesis
    by (auto simp: vimage_def measurable_count_space_eq2_countable)
qed

lemma measurable_real_ceiling[measurable]:
  "(ceiling :: real ⇒ int) ∈ measurable borel (count_space UNIV)"
  unfolding ceiling_def[abs_def] by simp

lemma borel_measurable_real_floor: "(λx::real. real_of_int ⌊x⌋) ∈ borel_measurable borel"
  by simp

lemma borel_measurable_root [measurable]: "root n ∈ borel_measurable borel"
  by (intro borel_measurable_continuous_on1 continuous_intros)

lemma borel_measurable_sqrt [measurable]: "sqrt ∈ borel_measurable borel"
  by (intro borel_measurable_continuous_on1 continuous_intros)

lemma borel_measurable_power [measurable (raw)]:
  fixes f :: "_ ⇒ 'b::{power,real_normed_algebra}"
  assumes f: "f ∈ borel_measurable M"
  shows "(λx. (f x) ^ n) ∈ borel_measurable M"
  by (intro borel_measurable_continuous_on [OF _ f] continuous_intros)

lemma borel_measurable_Re [measurable]: "Re ∈ borel_measurable borel"
  by (intro borel_measurable_continuous_on1 continuous_intros)

lemma borel_measurable_Im [measurable]: "Im ∈ borel_measurable borel"
  by (intro borel_measurable_continuous_on1 continuous_intros)

lemma borel_measurable_of_real [measurable]: "(of_real :: _ ⇒ (_::real_normed_algebra)) ∈ borel_measurable borel"
  by (intro borel_measurable_continuous_on1 continuous_intros)

lemma borel_measurable_sin [measurable]: "(sin :: _ ⇒ (_::{real_normed_field,banach})) ∈ borel_measurable borel"
  by (intro borel_measurable_continuous_on1 continuous_intros)

lemma borel_measurable_cos [measurable]: "(cos :: _ ⇒ (_::{real_normed_field,banach})) ∈ borel_measurable borel"
  by (intro borel_measurable_continuous_on1 continuous_intros)

lemma borel_measurable_arctan [measurable]: "arctan ∈ borel_measurable borel"
  by (intro borel_measurable_continuous_on1 continuous_intros)

lemma borel_measurable_complex_iff:
  "f ∈ borel_measurable M ⟷
    (λx. Re (f x)) ∈ borel_measurable M ∧ (λx. Im (f x)) ∈ borel_measurable M"
  apply auto
  apply (subst fun_complex_eq)
  apply (intro borel_measurable_add)
  apply auto
  done

lemma measurable_of_bool[measurable]: "of_bool ∈ count_space UNIV →M borel"
  by simp

subsection "Borel space on the extended reals"

lemma borel_measurable_ereal[measurable (raw)]:
  assumes f: "f ∈ borel_measurable M" shows "(λx. ereal (f x)) ∈ 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 ⇒ ereal"
  assumes f: "f ∈ borel_measurable M"
  shows "(λx. real_of_ereal (f x)) ∈ borel_measurable M"
  apply (rule measurable_compose[OF f])
  apply (rule borel_measurable_continuous_countable_exceptions[of "{∞, -∞ }"])
  apply (auto intro: continuous_on_real simp: Compl_eq_Diff_UNIV)
  done

lemma borel_measurable_ereal_cases:
  fixes f :: "'a ⇒ ereal"
  assumes f: "f ∈ borel_measurable M"
  assumes H: "(λx. H (ereal (real_of_ereal (f x)))) ∈ borel_measurable M"
  shows "(λx. H (f x)) ∈ borel_measurable M"
proof -
  let ?F = "λx. if f x = ∞ then H ∞ else if f x = - ∞ then H (-∞) else H (ereal (real_of_ereal (f x)))"
  { fix x have "H (f x) = ?F x" by (cases "f x") auto }
  with f H show ?thesis by simp
qed

lemma
  fixes f :: "'a ⇒ ereal" assumes f[measurable]: "f ∈ borel_measurable M"
  shows borel_measurable_ereal_abs[measurable(raw)]: "(λx. ¦f x¦) ∈ borel_measurable M"
    and borel_measurable_ereal_inverse[measurable(raw)]: "(λx. inverse (f x) :: ereal) ∈ borel_measurable M"
    and borel_measurable_uminus_ereal[measurable(raw)]: "(λx. - f x :: ereal) ∈ borel_measurable M"
  by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If)

lemma borel_measurable_uminus_eq_ereal[simp]:
  "(λx. - f x :: ereal) ∈ borel_measurable M ⟷ f ∈ borel_measurable M" (is "?l = ?r")
proof
  assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp
qed auto

lemma set_Collect_ereal2:
  fixes f g :: "'a ⇒ ereal"
  assumes f: "f ∈ borel_measurable M"
  assumes g: "g ∈ borel_measurable M"
  assumes H: "{x ∈ space M. H (ereal (real_of_ereal (f x))) (ereal (real_of_ereal (g x)))} ∈ sets M"
    "{x ∈ space borel. H (-∞) (ereal x)} ∈ sets borel"
    "{x ∈ space borel. H (∞) (ereal x)} ∈ sets borel"
    "{x ∈ space borel. H (ereal x) (-∞)} ∈ sets borel"
    "{x ∈ space borel. H (ereal x) (∞)} ∈ sets borel"
  shows "{x ∈ space M. H (f x) (g x)} ∈ sets M"
proof -
  let ?G = "λy x. if g x = ∞ then H y ∞ else if g x = -∞ then H y (-∞) else H y (ereal (real_of_ereal (g x)))"
  let ?F = "λx. if f x = ∞ then ?G ∞ x else if f x = -∞ then ?G (-∞) x else ?G (ereal (real_of_ereal (f x))) x"
  { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
  note * = this
  from assms show ?thesis
    by (subst *) (simp del: space_borel split del: if_split)
qed

lemma borel_measurable_ereal_iff:
  shows "(λx. ereal (f x)) ∈ borel_measurable M ⟷ f ∈ borel_measurable M"
proof
  assume "(λx. ereal (f x)) ∈ borel_measurable M"
  from borel_measurable_real_of_ereal[OF this]
  show "f ∈ borel_measurable M" by auto
qed auto

lemma borel_measurable_erealD[measurable_dest]:
  "(λx. ereal (f x)) ∈ borel_measurable M ⟹ g ∈ measurable N M ⟹ (λx. f (g x)) ∈ borel_measurable N"
  unfolding borel_measurable_ereal_iff by simp

lemma borel_measurable_ereal_iff_real:
  fixes f :: "'a ⇒ ereal"
  shows "f ∈ borel_measurable M ⟷
    ((λx. real_of_ereal (f x)) ∈ borel_measurable M ∧ f -` {∞} ∩ space M ∈ sets M ∧ f -` {-∞} ∩ space M ∈ sets M)"
proof safe
  assume *: "(λx. real_of_ereal (f x)) ∈ borel_measurable M" "f -` {∞} ∩ space M ∈ sets M" "f -` {-∞} ∩ space M ∈ sets M"
  have "f -` {∞} ∩ space M = {x∈space M. f x = ∞}" "f -` {-∞} ∩ space M = {x∈space M. f x = -∞}" by auto
  with * have **: "{x∈space M. f x = ∞} ∈ sets M" "{x∈space M. f x = -∞} ∈ sets M" by simp_all
  let ?f = "λx. if f x = ∞ then ∞ else if f x = -∞ then -∞ else ereal (real_of_ereal (f x))"
  have "?f ∈ borel_measurable M" using * ** by (intro measurable_If) auto
  also have "?f = f" by (auto simp: fun_eq_iff ereal_real)
  finally show "f ∈ borel_measurable M" .
qed simp_all

lemma borel_measurable_ereal_iff_Iio:
  "(f::'a ⇒ ereal) ∈ borel_measurable M ⟷ (∀a. f -` {..< a} ∩ space M ∈ sets M)"
  by (auto simp: borel_Iio measurable_iff_measure_of)

lemma borel_measurable_ereal_iff_Ioi:
  "(f::'a ⇒ ereal) ∈ borel_measurable M ⟷ (∀a. f -` {a <..} ∩ space M ∈ sets M)"
  by (auto simp: borel_Ioi measurable_iff_measure_of)

lemma vimage_sets_compl_iff:
  "f -` A ∩ space M ∈ sets M ⟷ f -` (- A) ∩ space M ∈ sets M"
proof -
  { fix A assume "f -` A ∩ space M ∈ sets M"
    moreover have "f -` (- A) ∩ space M = space M - f -` A ∩ space M" by auto
    ultimately have "f -` (- A) ∩ space M ∈ sets M" by auto }
  from this[of A] this[of "-A"] show ?thesis
    by (metis double_complement)
qed

lemma borel_measurable_iff_Iic_ereal:
  "(f::'a⇒ereal) ∈ borel_measurable M ⟷ (∀a. f -` {..a} ∩ space M ∈ sets M)"
  unfolding borel_measurable_ereal_iff_Ioi vimage_sets_compl_iff[where A="{a <..}" for a] by simp

lemma borel_measurable_iff_Ici_ereal:
  "(f::'a ⇒ ereal) ∈ borel_measurable M ⟷ (∀a. f -` {a..} ∩ space M ∈ 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 ⇒ ereal"
  assumes f: "f ∈ borel_measurable M"
  assumes g: "g ∈ borel_measurable M"
  assumes H: "(λx. H (ereal (real_of_ereal (f x))) (ereal (real_of_ereal (g x)))) ∈ borel_measurable M"
    "(λx. H (-∞) (ereal (real_of_ereal (g x)))) ∈ borel_measurable M"
    "(λx. H (∞) (ereal (real_of_ereal (g x)))) ∈ borel_measurable M"
    "(λx. H (ereal (real_of_ereal (f x))) (-∞)) ∈ borel_measurable M"
    "(λx. H (ereal (real_of_ereal (f x))) (∞)) ∈ borel_measurable M"
  shows "(λx. H (f x) (g x)) ∈ borel_measurable M"
proof -
  let ?G = "λy x. if g x = ∞ then H y ∞ else if g x = - ∞ then H y (-∞) else H y (ereal (real_of_ereal (g x)))"
  let ?F = "λx. if f x = ∞ then ?G ∞ x else if f x = - ∞ then ?G (-∞) x else ?G (ereal (real_of_ereal (f x))) x"
  { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
  note * = this
  from assms show ?thesis unfolding * by simp
qed

lemma [measurable(raw)]:
  fixes f :: "'a ⇒ ereal"
  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"
  by (simp_all add: borel_measurable_ereal2)

lemma [measurable(raw)]:
  fixes f g :: "'a ⇒ ereal"
  assumes "f ∈ borel_measurable M"
  assumes "g ∈ borel_measurable M"
  shows borel_measurable_ereal_diff: "(λx. f x - g x) ∈ borel_measurable M"
    and borel_measurable_ereal_divide: "(λx. f x / g x) ∈ borel_measurable M"
  using assms by (simp_all add: minus_ereal_def divide_ereal_def)

lemma borel_measurable_ereal_sum[measurable (raw)]:
  fixes f :: "'c ⇒ 'a ⇒ ereal"
  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

lemma borel_measurable_ereal_prod[measurable (raw)]:
  fixes f :: "'c ⇒ 'a ⇒ ereal"
  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

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 →M borel"
  by (intro borel_measurable_continuous_on1 continuous_on_enn2ereal)

lemma measurable_e2ennreal[measurable]: "e2ennreal ∈ borel →M borel"
  by (intro borel_measurable_continuous_on1 continuous_on_e2ennreal)

lemma borel_measurable_enn2real[measurable (raw)]:
  "f ∈ M →M borel ⟹ (λx. enn2real (f x)) ∈ M →M borel"
  unfolding enn2real_def[abs_def] by measurable

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

context
  includes ennreal.lifting
begin

lemma measurable_ennreal[measurable]: "ennreal ∈ borel →M borel"
  unfolding is_borel_def[symmetric]
  by transfer simp

lemma borel_measurable_ennreal_iff[simp]:
  assumes [simp]: "⋀x. x ∈ space M ⟹ 0 ≤ f x"
  shows "(λx. ennreal (f x)) ∈ M →M borel ⟷ f ∈ M →M borel"
proof safe
  assume "(λx. ennreal (f x)) ∈ M →M borel"
  then have "(λx. enn2real (ennreal (f x))) ∈ M →M borel"
    by measurable
  then show "f ∈ M →M borel"
    by (rule measurable_cong[THEN iffD1, rotated]) auto
qed measurable

lemma borel_measurable_times_ennreal[measurable (raw)]:
  fixes f g :: "'a ⇒ ennreal"
  shows "f ∈ M →M borel ⟹ g ∈ M →M borel ⟹ (λx. f x * g x) ∈ M →M borel"
  unfolding is_borel_def[symmetric] by transfer simp

lemma borel_measurable_inverse_ennreal[measurable (raw)]:
  fixes f :: "'a ⇒ ennreal"
  shows "f ∈ M →M borel ⟹ (λx. inverse (f x)) ∈ M →M borel"
  unfolding is_borel_def[symmetric] by transfer simp

lemma borel_measurable_divide_ennreal[measurable (raw)]:
  fixes f :: "'a ⇒ ennreal"
  shows "f ∈ M →M borel ⟹ g ∈ M →M borel ⟹ (λx. f x / g x) ∈ M →M borel"
  unfolding divide_ennreal_def by simp

lemma borel_measurable_minus_ennreal[measurable (raw)]:
  fixes f :: "'a ⇒ ennreal"
  shows "f ∈ M →M borel ⟹ g ∈ M →M borel ⟹ (λx. f x - g x) ∈ M →M borel"
  unfolding is_borel_def[symmetric] by transfer simp

lemma borel_measurable_prod_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

end

hide_const (open) is_borel

subsection ‹LIMSEQ is borel measurable›

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"
  shows "u' ∈ borel_measurable M"
proof -
  have "⋀x. x ∈ space M ⟹ liminf (λn. ereal (u n x)) = ereal (u' x)"
    using u' by (simp add: lim_imp_Liminf)
  moreover from u have "(λx. liminf (λn. ereal (u n x))) ∈ borel_measurable M"
    by auto
  ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff)
qed

lemma borel_measurable_LIMSEQ_metric:
  fixes f :: "nat ⇒ 'a ⇒ 'b :: metric_space"
  assumes [measurable]: "⋀i. f i ∈ borel_measurable M"
  assumes lim: "⋀x. x ∈ space M ⟹ (λi. f i x) ⇢ g x"
  shows "g ∈ borel_measurable M"
  unfolding borel_eq_closed
proof (safe intro!: measurable_measure_of)
  fix A :: "'b set" assume "closed A"

  have [measurable]: "(λx. infdist (g x) A) ∈ borel_measurable M"
  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"
      by (intro borel_measurable_continuous_on[where f="λx. infdist x A"]
        continuous_at_imp_continuous_on ballI continuous_infdist continuous_ident) auto
  qed

  show "g -` A ∩ space M ∈ sets M"
  proof cases
    assume "A ≠ {}"
    then have "⋀x. infdist x A = 0 ⟷ x ∈ A"
      using ‹closed A› by (simp add: in_closed_iff_infdist_zero)
    then have "g -` A ∩ space M = {x∈space M. infdist (g x) A = 0}"
      by auto
    also have "… ∈ sets M"
      by measurable
    finally show ?thesis .
  qed simp
qed auto

lemma sets_Collect_Cauchy[measurable]:
  fixes f :: "nat ⇒ 'a => 'b::{metric_space, second_countable_topology}"
  assumes f[measurable]: "⋀i. f i ∈ borel_measurable M"
  shows "{x∈space M. Cauchy (λi. f i x)} ∈ sets M"
  unfolding metric_Cauchy_iff2 using f by auto

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"
proof -
  define u' where "u' x = lim (λi. if Cauchy (λi. f i x) then f i x else 0)" for x
  then have *: "⋀x. lim (λi. f i x) = (if Cauchy (λi. f i x) then u' x else (THE x. False))"
    by (auto simp: lim_def convergent_eq_Cauchy[symmetric])
  have "u' ∈ borel_measurable M"
  proof (rule borel_measurable_LIMSEQ_metric)
    fix x
    have "convergent (λi. if Cauchy (λi. f i x) then f i x else 0)"
      by (cases "Cauchy (λi. f i x)")
         (auto simp add: convergent_eq_Cauchy[symmetric] convergent_def)
    then show "(λi. if Cauchy (λi. f i x) then f i x else 0) ⇢ u' x"
      unfolding u'_def
      by (rule convergent_LIMSEQ_iff[THEN iffD1])
  qed measurable
  then show ?thesis
    unfolding * by measurable
qed

lemma borel_measurable_suminf[measurable (raw)]:
  fixes f :: "nat ⇒ 'a ⇒ 'b::{banach, second_countable_topology}"
  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

lemma Collect_closed_imp_pred_borel: "closed {x. P x} ⟹ Measurable.pred borel P"
  by (simp add: pred_def)

(* Proof by Jeremy Avigad and Luke Serafin *)
lemma isCont_borel_pred[measurable]:
  fixes f :: "'b::metric_space ⇒ 'a::metric_space"
  shows "Measurable.pred borel (isCont f)"
proof (subst measurable_cong)
  let ?I = "λj. inverse(real (Suc j))"
  show "isCont f x = (∀i. ∃j. ∀y z. dist x y < ?I j ∧ dist x z < ?I j ⟶ dist (f y) (f z) ≤ ?I i)" for x
    unfolding continuous_at_eps_delta
  proof safe
    fix i assume "∀e>0. ∃d>0. ∀y. dist y x < d ⟶ dist (f y) (f x) < e"
    moreover have "0 < ?I i / 2"
      by simp
    ultimately obtain d where d: "0 < d" "⋀y. dist x y < d ⟹ dist (f y) (f x) < ?I i / 2"
      by (metis dist_commute)
    then obtain j where j: "?I j < d"
      by (metis reals_Archimedean)

    show "∃j. ∀y z. dist x y < ?I j ∧ dist x z < ?I j ⟶ dist (f y) (f z) ≤ ?I i"
    proof (safe intro!: exI[where x=j])
      fix y z assume *: "dist x y < ?I j" "dist x z < ?I j"
      have "dist (f y) (f z) ≤ dist (f y) (f x) + dist (f z) (f x)"
        by (rule dist_triangle2)
      also have "… < ?I i / 2 + ?I i / 2"
        by (intro add_strict_mono d less_trans[OF _ j] *)
      also have "… ≤ ?I i"
        by (simp add: field_simps of_nat_Suc)
      finally show "dist (f y) (f z) ≤ ?I i"
        by simp
    qed
  next
    fix e::real assume "0 < e"
    then obtain n where n: "?I n < e"
      by (metis reals_Archimedean)
    assume "∀i. ∃j. ∀y z. dist x y < ?I j ∧ dist x z < ?I j ⟶ dist (f y) (f z) ≤ ?I i"
    from this[THEN spec, of "Suc n"]
    obtain j where j: "⋀y z. dist x y < ?I j ⟹ dist x z < ?I j ⟹ dist (f y) (f z) ≤ ?I (Suc n)"
      by auto

    show "∃d>0. ∀y. dist y x < d ⟶ dist (f y) (f x) < e"
    proof (safe intro!: exI[of _ "?I j"])
      fix y assume "dist y x < ?I j"
      then have "dist (f y) (f x) ≤ ?I (Suc n)"
        by (intro j) (auto simp: dist_commute)
      also have "?I (Suc n) < ?I n"
        by simp
      also note n
      finally show "dist (f y) (f x) < e" .
    qed simp
  qed
qed (intro pred_intros_countable closed_Collect_all closed_Collect_le open_Collect_less
           Collect_closed_imp_pred_borel closed_Collect_imp open_Collect_conj continuous_intros)

lemma isCont_borel:
  fixes f :: "'b::metric_space ⇒ 'a::metric_space"
  shows "{x. isCont f x} ∈ sets borel"
  by simp

lemma is_real_interval:
  assumes S: "is_interval S"
  shows "∃a b::real. S = {} ∨ S = UNIV ∨ S = {..<b} ∨ S = {..b} ∨ S = {a<..} ∨ S = {a..} ∨
    S = {a<..<b} ∨ S = {a<..b} ∨ S = {a..<b} ∨ S = {a..b}"
  using S unfolding is_interval_1 by (blast intro: interval_cases)

lemma real_interval_borel_measurable:
  assumes "is_interval (S::real set)"
  shows "S ∈ sets borel"
proof -
  from assms is_real_interval have "∃a b::real. S = {} ∨ S = UNIV ∨ S = {..<b} ∨ S = {..b} ∨
    S = {a<..} ∨ S = {a..} ∨ S = {a<..<b} ∨ S = {a<..b} ∨ S = {a..<b} ∨ S = {a..b}" by auto
  then guess a ..
  then guess b ..
  thus ?thesis
    by auto
qed

text ‹The next lemmas hold in any second countable linorder (including ennreal or ereal for instance),
but in the current state they are restricted to reals.›

lemma borel_measurable_mono_on_fnc:
  fixes f :: "real ⇒ real" and A :: "real set"
  assumes "mono_on f A"
  shows "f ∈ 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
              intro!: borel_measurable_continuous_on_restrict intro: continuous_within_subset)
  done

lemma borel_measurable_piecewise_mono:
  fixes f::"real ⇒ real" and C::"real set set"
  assumes "countable C" "⋀c. c ∈ C ⟹ c ∈ sets borel" "⋀c. c ∈ C ⟹ mono_on f c" "(⋃C) = UNIV"
  shows "f ∈ borel_measurable borel"
by (rule measurable_piecewise_restrict[of C], auto intro: borel_measurable_mono_on_fnc simp: assms)

lemma borel_measurable_mono:
  fixes f :: "real ⇒ real"
  shows "mono f ⟹ f ∈ borel_measurable borel"
  using borel_measurable_mono_on_fnc[of f UNIV] by (simp add: mono_def mono_on_def)

lemma measurable_bdd_below_real[measurable (raw)]:
  fixes F :: "'a ⇒ 'i ⇒ real"
  assumes [simp]: "countable I" and [measurable]: "⋀i. i ∈ I ⟹ F i ∈ M →M borel"
  shows "Measurable.pred M (λx. bdd_below ((λi. F i x)`I))"
proof (subst measurable_cong)
  show "bdd_below ((λi. F i x)`I) ⟷ (∃q∈ℤ. ∀i∈I. q ≤ F i x)" for x
    by (auto simp: bdd_below_def intro!: bexI[of _ "of_int (floor _)"] intro: order_trans of_int_floor_le)
  show "Measurable.pred M (λw. ∃q∈ℤ. ∀i∈I. q ≤ F i w)"
    using countable_int by measurable
qed

lemma borel_measurable_cINF_real[measurable (raw)]:
  fixes F :: "_ ⇒ _ ⇒ real"
  assumes [simp]: "countable I"
  assumes F[measurable]: "⋀i. i ∈ I ⟹ F i ∈ borel_measurable M"
  shows "(λx. INF i:I. F i x) ∈ borel_measurable M"
proof (rule measurable_piecewise_restrict)
  let  = "{x∈space M. bdd_below ((λi. F i x)`I)}"
  show "countable {?Ω, - ?Ω}" "space M ⊆ ⋃{?Ω, - ?Ω}" "⋀X. X ∈ {?Ω, - ?Ω} ⟹ X ∩ space M ∈ sets M"
    by auto
  fix X assume "X ∈ {?Ω, - ?Ω}" then show "(λx. INF i:I. F i x) ∈ borel_measurable (restrict_space M X)"
  proof safe
    show "(λx. INF i:I. F i x) ∈ borel_measurable (restrict_space M ?Ω)"
      by (intro borel_measurable_cINF measurable_restrict_space1 F)
         (auto simp: space_restrict_space)
    show "(λx. INF i:I. F i x) ∈ borel_measurable (restrict_space M (-?Ω))"
    proof (subst measurable_cong)
      fix x assume "x ∈ space (restrict_space M (-?Ω))"
      then have "¬ (∀i∈I. - F i x ≤ y)" for y
        by (auto simp: space_restrict_space bdd_above_def bdd_above_uminus[symmetric])
      then show "(INF i:I. F i x) = - (THE x. False)"
        by (auto simp: space_restrict_space Inf_real_def Sup_real_def Least_def simp del: Set.ball_simps(10))
    qed simp
  qed
qed

lemma borel_Ici: "borel = sigma UNIV (range (λx::real. {x ..}))"
proof (safe intro!: borel_eq_sigmaI1[OF borel_Iio])
  fix x :: real
  have eq: "{..<x} = space (sigma UNIV (range atLeast)) - {x ..}"
    by auto
  show "{..<x} ∈ sets (sigma UNIV (range atLeast))"
    unfolding eq by (intro sets.compl_sets) auto
qed auto

lemma borel_measurable_pred_less[measurable (raw)]:
  fixes f :: "'a ⇒ 'b::{second_countable_topology, linorder_topology}"
  shows "f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ Measurable.pred M (λw. f w < g w)"
  unfolding Measurable.pred_def by (rule borel_measurable_less)

no_notation
  eucl_less (infix "<e" 50)

lemma borel_measurable_Max2[measurable (raw)]:
  fixes f::"_ ⇒ _ ⇒ 'a::{second_countable_topology, dense_linorder, linorder_topology}"
  assumes "finite I"
    and [measurable]: "⋀i. f i ∈ borel_measurable M"
  shows "(λx. Max{f i x |i. i ∈ I}) ∈ borel_measurable M"
by (simp add: borel_measurable_Max[OF assms(1), where ?f=f and ?M=M] Setcompr_eq_image)

lemma measurable_compose_n [measurable (raw)]:
  assumes "T ∈ measurable M M"
  shows "(T^^n) ∈ measurable M M"
by (induction n, auto simp add: measurable_compose[OF _ assms])

lemma measurable_real_imp_nat:
  fixes f::"'a ⇒ nat"
  assumes [measurable]: "(λx. real(f x)) ∈ borel_measurable M"
  shows "f ∈ measurable M (count_space UNIV)"
proof -
  let ?g = "(λx. real(f x))"
  have "⋀(n::nat). ?g-`({real n}) ∩ space M = f-`{n} ∩ space M" by auto
  moreover have "⋀(n::nat). ?g-`({real n}) ∩ space M ∈ sets M" using assms by measurable
  ultimately have "⋀(n::nat). f-`{n} ∩ space M ∈ sets M" by simp
  then show ?thesis using measurable_count_space_eq2_countable by blast
qed

lemma measurable_equality_set [measurable]:
  fixes f g::"_⇒ 'a::{second_countable_topology, t2_space}"
  assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
  shows "{x ∈ space M. f x = g x} ∈ sets M"

proof -
  define A where "A = {x ∈ space M. f x = g x}"
  define B where "B = {y. ∃x::'a. y = (x,x)}"
  have "A = (λx. (f x, g x))-`B ∩ space M" unfolding A_def B_def by auto
  moreover have "(λx. (f x, g x)) ∈ borel_measurable M" by simp
  moreover have "B ∈ sets borel" unfolding B_def by (simp add: closed_diagonal)
  ultimately have "A ∈ sets M" by simp
  then show ?thesis unfolding A_def by simp
qed

lemma measurable_inequality_set [measurable]:
  fixes f g::"_ ⇒ 'a::{second_countable_topology, linorder_topology}"
  assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
  shows "{x ∈ space M. f x ≤ g x} ∈ sets M"
        "{x ∈ space M. f x < g x} ∈ sets M"
        "{x ∈ space M. f x ≥ g x} ∈ sets M"
        "{x ∈ space M. f x > g x} ∈ sets M"
proof -
  define F where "F = (λx. (f x, g x))"
  have * [measurable]: "F ∈ borel_measurable M" unfolding F_def by simp

  have "{x ∈ space M. f x ≤ g x} = F-`{(x, y) | x y. x ≤ y} ∩ space M" unfolding F_def by auto
  moreover have "{(x, y) | x y. x ≤ (y::'a)} ∈ sets borel" using closed_subdiagonal borel_closed by blast
  ultimately show "{x ∈ space M. f x ≤ g x} ∈ sets M" using * by (metis (mono_tags, lifting) measurable_sets)

  have "{x ∈ space M. f x < g x} = F-`{(x, y) | x y. x < y} ∩ space M" unfolding F_def by auto
  moreover have "{(x, y) | x y. x < (y::'a)} ∈ sets borel" using open_subdiagonal borel_open by blast
  ultimately show "{x ∈ space M. f x < g x} ∈ sets M" using * by (metis (mono_tags, lifting) measurable_sets)

  have "{x ∈ space M. f x ≥ g x} = F-`{(x, y) | x y. x ≥ y} ∩ space M" unfolding F_def by auto
  moreover have "{(x, y) | x y. x ≥ (y::'a)} ∈ sets borel" using closed_superdiagonal borel_closed by blast
  ultimately show "{x ∈ space M. f x ≥ g x} ∈ sets M" using * by (metis (mono_tags, lifting) measurable_sets)

  have "{x ∈ space M. f x > g x} = F-`{(x, y) | x y. x > y} ∩ space M" unfolding F_def by auto
  moreover have "{(x, y) | x y. x > (y::'a)} ∈ sets borel" using open_superdiagonal borel_open by blast
  ultimately show "{x ∈ space M. f x > g x} ∈ sets M" using * by (metis (mono_tags, lifting) measurable_sets)
qed

lemma measurable_limit [measurable]:
  fixes f::"nat ⇒ 'a ⇒ 'b::first_countable_topology"
  assumes [measurable]: "⋀n::nat. f n ∈ borel_measurable M"
  shows "Measurable.pred M (λx. (λn. f n x) ⇢ c)"
proof -
  obtain A :: "nat ⇒ 'b set" where A:
    "⋀i. open (A i)"
    "⋀i. c ∈ A i"
    "⋀S. open S ⟹ c ∈ S ⟹ eventually (λi. A i ⊆ S) sequentially"
  by (rule countable_basis_at_decseq) blast

  have [measurable]: "⋀N i. (f N)-`(A i) ∩ space M ∈ sets M" using A(1) by auto
  then have mes: "(⋂i. ⋃n. ⋂N∈{n..}. (f N)-`(A i) ∩ space M) ∈ sets M" by blast

  have "(u ⇢ c) ⟷ (∀i. eventually (λn. u n ∈ A i) sequentially)" for u::"nat ⇒ 'b"
  proof
    assume "u ⇢ c"
    then have "eventually (λn. u n ∈ A i) sequentially" for i using A(1)[of i] A(2)[of i]
      by (simp add: topological_tendstoD)
    then show "(∀i. eventually (λn. u n ∈ A i) sequentially)" by auto
  next
    assume H: "(∀i. eventually (λn. u n ∈ A i) sequentially)"
    show "(u ⇢ c)"
    proof (rule topological_tendstoI)
      fix S assume "open S" "c ∈ S"
      with A(3)[OF this] obtain i where "A i ⊆ S"
        using eventually_False_sequentially eventually_mono by blast
      moreover have "eventually (λn. u n ∈ A i) sequentially" using H by simp
      ultimately show "∀F n in sequentially. u n ∈ S"
        by (simp add: eventually_mono subset_eq)
    qed
  qed
  then have "{x. (λn. f n x) ⇢ c} = (⋂i. ⋃n. ⋂N∈{n..}. (f N)-`(A i))"
    by (auto simp add: atLeast_def eventually_at_top_linorder)
  then have "{x ∈ space M. (λn. f n x) ⇢ c} = (⋂i. ⋃n. ⋂N∈{n..}. (f N)-`(A i) ∩ space M)"
    by auto
  then have "{x ∈ space M. (λn. f n x) ⇢ c} ∈ sets M" using mes by simp
  then show ?thesis by auto
qed

lemma measurable_limit2 [measurable]:
  fixes u::"nat ⇒ 'a ⇒ real"
  assumes [measurable]: "⋀n. u n ∈ borel_measurable M" "v ∈ borel_measurable M"
  shows "Measurable.pred M (λx. (λn. u n x) ⇢ v x)"
proof -
  define w where "w = (λn x. u n x - v x)"
  have [measurable]: "w n ∈ borel_measurable M" for n unfolding w_def by auto
  have "((λn. u n x) ⇢ v x) ⟷ ((λn. w n x) ⇢ 0)" for x
    unfolding w_def using Lim_null by auto
  then show ?thesis using measurable_limit by auto
qed

lemma measurable_P_restriction [measurable (raw)]:
  assumes [measurable]: "Measurable.pred M P" "A ∈ sets M"
  shows "{x ∈ A. P x} ∈ sets M"
proof -
  have "A ⊆ space M" using sets.sets_into_space[OF assms(2)].
  then have "{x ∈ A. P x} = A ∩ {x ∈ space M. P x}" by blast
  then show ?thesis by auto
qed

lemma measurable_sum_nat [measurable (raw)]:
  fixes f :: "'c ⇒ 'a ⇒ nat"
  assumes "⋀i. i ∈ S ⟹ f i ∈ measurable M (count_space UNIV)"
  shows "(λx. ∑i∈S. f i x) ∈ measurable M (count_space UNIV)"
proof cases
  assume "finite S"
  then show ?thesis using assms by induct auto
qed simp


lemma measurable_abs_powr [measurable]:
  fixes p::real
  assumes [measurable]: "f ∈ borel_measurable M"
  shows "(λx. ¦f x¦ powr p) ∈ borel_measurable M"
unfolding powr_def by auto

text ‹The next one is a variation around \verb+measurable_restrict_space+.›

lemma measurable_restrict_space3:
  assumes "f ∈ measurable M N" and
          "f ∈ A → B"
  shows "f ∈ measurable (restrict_space M A) (restrict_space N B)"
proof -
  have "f ∈ measurable (restrict_space M A) N" using assms(1) measurable_restrict_space1 by auto
  then show ?thesis by (metis Int_iff funcsetI funcset_mem
      measurable_restrict_space2[of f, of "restrict_space M A", of B, of N] assms(2) space_restrict_space)
qed

text ‹The next one is a variation around \verb+measurable_piecewise_restrict+.›

lemma measurable_piecewise_restrict2:
  assumes [measurable]: "⋀n. A n ∈ sets M"
      and "space M = (⋃(n::nat). A n)"
          "⋀n. ∃h ∈ measurable M N. (∀x ∈ A n. f x = h x)"
  shows "f ∈ measurable M N"
proof (rule measurableI)
  fix B assume [measurable]: "B ∈ sets N"
  {
    fix n::nat
    obtain h where [measurable]: "h ∈ measurable M N" and "∀x ∈ A n. f x = h x" using assms(3) by blast
    then have *: "f-`B ∩ A n = h-`B ∩ A n" by auto
    have "h-`B ∩ A n = h-`B ∩ space M ∩ A n" using assms(2) sets.sets_into_space by auto
    then have "h-`B ∩ A n ∈ sets M" by simp
    then have "f-`B ∩ A n ∈ sets M" using * by simp
  }
  then have "(⋃n. f-`B ∩ A n) ∈ sets M" by measurable
  moreover have "f-`B ∩ space M = (⋃n. f-`B ∩ A n)" using assms(2) by blast
  ultimately show "f-`B ∩ space M ∈ sets M" by simp
next
  fix x assume "x ∈ space M"
  then obtain n where "x ∈ A n" using assms(2) by blast
  obtain h where [measurable]: "h ∈ measurable M N" and "∀x ∈ A n. f x = h x" using assms(3) by blast
  then have "f x = h x" using ‹x ∈ A n› by blast
  moreover have "h x ∈ space N" by (metis measurable_space ‹x ∈ space M› ‹h ∈ measurable M N›)
  ultimately show "f x ∈ space N" by simp
qed

end