Quelle  Borel_Space.thy

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

section ‹Borel Space›

theory Borel_Space
imports
  Measurable Derivative Ordered_Euclidean_Space Extended_Real_Limits
begin

lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..
  by (auto simp: real_atLeastGreaterThan_eq)

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)

proposition 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

proposition mono_on_imp_deriv_nonneg:
  assumes mono: "mono_on A f" 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 (interior A) f" 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 ((+) (-x) ` interior A)" by (rule open_translation)
    also have "((+) (-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

proposition mono_on_ctble_discont:
  fixes f :: "real ==> real"
  fixes A :: "real set"
  assumes "mono_on A f"
  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 A f› 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)"
        using q2 *[of "a - _"] dist_real_def mono by fastforce
      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)"
        using q2 *[of "_ - a"] dist_real_def mono by fastforce
      thus ?thesis by auto
    qed
  qed
  then obtain g :: "real ==> nat × rat" where "∀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 exE]) blast
  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 A f"
  shows "countable {a∈A. ¬isCont f a}"
  using continuous_within_open [OF _ ‹open A›] ‹mono_on A f›
  by (smt (verit, ccfv_threshold) Collect_cong mono_on_ctble_discont)

lemma mono_ctble_discont:
  fixes f :: "real ==> real"
  assumes "mono f"
  shows "countable {a. ¬ isCont f a}"
  using assms mono_on_ctble_discont [of UNIV f] 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"
  by (meson DERIV_isCont assms continuous_at_imp_continuous_on)

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"
    using c'' d'' calculation by (metis IntE atLeastAtMost_iff mono order_class.order_eq_iff)+
  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🍋‹tag important› (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"
  by (simp add: assms sets_borel)

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"
  by (simp add: set_eq_iff sets.countable)

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 of_bool_def if_distrib[where f="λx. a * x" for a] cong: if_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 of_bool_def if_distrib[where f="λx. a * x" for a] cong: if_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 of_bool_def if_distrib[where f="λx. x *🪙R a" for a] ac_simps
       cong: if_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 (simp add: borel_closed 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}"
    by (metis F image_subset_iff sets_borel sigma_sets_mono)
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 (smt (verit, del_insts) borel_eq_sigmaI1 image_iff prod.collapse split_beta)

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

theorem 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)"
proof -
  have "x ∈ sigma_sets UNIV (Collect closed)" 
     if  "open x" for x :: "'a set"
    by (metis that Compl_eq_Diff_UNIV closed_Compl double_complement mem_Collect_eq 
        sigma_sets.Basic sigma_sets.Compl)
  then show ?thesis
    unfolding borel_def
    by (metis Pow_UNIV borel_closed mem_Collect_eq sets_borel sigma_eqI sigma_sets_eqI top_greatest)
qed

proposition 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 "open" B using assms by (rule countable_basis_openI)
  fix X::"'a set" assume "open X"
  from open_countable_basisE[OF this] obtain B' where B': "B' ⊆ B" "X = ∪ B'" .
  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_onI: "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_onI[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"
  using borel_measurable_continuous_on_restrict borel_measurable_restrict_space_iff inf_top.right_neutral by blast

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<..∈ sets borel"
    and atMost_borel: "{..a} ∈ sets borel"
    and atLeast_borel: "{a..} ∈ sets borel"
    and atLeastAtMost_borel: "{a..b} ∈ sets borel"
    and greaterThanAtMost_borel: "{a<..b} ∈ sets borel"
    and atLeastLessThan_borel: "{a..∈ sets borel"
  unfolding greaterThanAtMost_def atLeastLessThan_def
  by (blast intro: borel_open borel_closed open_lessThan open_greaterThan open_greaterThanLessThan
                   closed_atMost closed_atLeast closed_atLeastAtMost)+

lemma borel_Iio:
  "borel = sigma UNIV (range lessThan :: 'a::{linorder_topology, second_countable_topology} set set)"
  unfolding second_countable_borel_measurable[OF open_generated_order]
proof (intro sigma_eqI sigma_sets_eqI)
  obtain D :: "'a set" where D: "countable D" "∧X. open X ==> X ≠ {} ==> ∃d∈D. d ∈ X"
    by (rule countable_dense_setE) blast

  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)
  obtain D :: "'a set" where D: "countable D" "∧X. open X ==> X ≠ {} ==> ∃d∈D. d ∈ X"
    by (rule countable_dense_setE) blast

  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∃d. x < d ∧ d < y"
      with D(2)[of "{x <..< y}" for x] have "∀x∃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∃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
    by (simp add: borel_measurable_const)
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
    by (simp add: borel_measurable_const)
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 simp add: image_comp)
  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 simp add: image_comp)
  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 ‹🚫› 50)

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

lemma eucl_ivals[measurable]:
  fixes a b :: "'a::ordered_euclidean_space"
  shows "{x. x ∈ sets borel"
    and "{x. a ∈ sets borel"
    and "{..a} ∈ sets borel"
    and "{a..} ∈ sets borel"
    and "{a..b} ∈ sets borel"
    and  "{x. a ∧ x ≤ b} ∈ sets borel"
    and "{x. a ≤ x ∧ x ∈ 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
    obtain k where "Max ((∙) x ` Basis) ≤ real k"
      using real_arch_simple by blast
    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
  (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 **: "∃y. ∀j∈Basis. j ≠ i ⟶ - real y < x ∙ j" if "a < x ∙ i" for x
  proof -
    obtain k where k: "Max ((∙) (- x) ` Basis) < real k"
      using reals_Archimedean2 by blast
    { 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 ?thesis
      by (auto intro!: exI[of _ k])
  qed
  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 -k) *??R n)  
    using i ** by (force simp add: eucl_less_def split: if_split_asm)
  finally have eq: "{x. x ∙ i ≤ a} = UNIV - (∪x. {xa. (∑n∈Basis. (if n = i then a else - real x) *🪙R n)  .
  show "{x. x∙i ≤ a} ∈ ?SIGMA"
    unfolding eq by (fastforce intro!: sigma_sets_top sets.Diff)
qed auto

lemma borel_eq_lessThan:
  "borel = sigma UNIV (range (λa::'a::ordered_euclidean_space. {x. x
  (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 **: "∃y. ∀j∈Basis. j ≠ i ⟶ real y > x ∙ j" if "a > x ∙ i" for x
  proof -
    obtain k where k: "Max ((∙) x ` Basis) < real k"
      using reals_Archimedean2 by blast
    { 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 ?thesis
      by (auto intro!: exI[of _ k])
  qed
  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 ∑n∈Basis. (if n = i then a else real k) *??R n)})" using ‹i∈ Basis›
    using i ** by (force simp add: eucl_less_def split: if_split_asm)
  finally
  have eq: "{x. a ≤ x ∙ i} =
            UNIV - (∪k. {x. x ∑n∈Basis. (if n = i then a else real k) *🪙R n)})" .

  show "{x. a ≤ x∙i} ∈ ?SIGMA"
    unfolding eq by (fastforce intro!: sigma_sets_top sets.Diff)
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
    obtain k where k: "Max ((∙) (- x) ` Basis) ≤ real k"
      using real_arch_simple by blast
    { 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
  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 "{..∪i::nat. {-real i ..< x})"
    by (auto simp: move_uminus real_arch_simple)
  then show "{y. y ∈ ?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_onI 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")
  by (smt (verit, ccfv_SIG) borel_measurable_uminus equation_minus_iff measurable_cong)

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
    have "∧x. [a + b *🪙R f x ∈ S] ==> f x ∈ (λx. (x - a) /🪙R b) ` S"
      using ‹b ≠ 0› image_iff by fastforce
    with ‹b ≠ 0› have "(λx. a + b *🪙R f x) -` S = f -` ?S"
      by auto
    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"
proof -
  have "countable {0::'b}" "continuous_on (- {0::'b}) inverse"
    by (auto intro!: continuous_on_inverse continuous_on_id)
  then show ?thesis
    by (metis borel_measurable_continuous_countable_exceptions f measurable_compose)
qed

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"
  using borel_measurable_continuous_countable_exceptions[of "{0}"] measurable_compose[OF f]
  by (auto intro!: continuous_on_ln continuous_on_id)

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_onI 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_onI continuous_intros)

lemma borel_measurable_sqrt [measurable]: "sqrt ∈ borel_measurable borel"
  by (intro borel_measurable_continuous_onI 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_onI continuous_intros)

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

lemma borel_measurable_of_real [measurable]: "(of_real :: _ ==> (_::real_normed_algebra)) ∈ borel_measurable borel"
  by (intro borel_measurable_continuous_onI continuous_intros)

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

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

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

lemma🍋‹tag important› borel_measurable_complex_iff:
  "f ∈ borel_measurable M ⟷
    (λx. Re (f x)) ∈ borel_measurable M ∧ (λx. Im (f x)) ∈ borel_measurable M" (is "?lhs ⟷ ?rhs")
proof
  show "?lhs ==> ?rhs"
    using borel_measurable_Im borel_measurable_Re measurable_compose by blast
  assume R: ?rhs
  then have "(λx. complex_of_real (Re (f x)) + i * complex_of_real (Im (f x))) ∈ borel_measurable M"
    by (intro borel_measurable_add) auto
  then show ?lhs
    using complex_eq by force
qed

lemma powr_real_measurable [measurable]:
  assumes "f ∈ measurable M borel" "g ∈ measurable M borel"
  shows   "(λx. f x powr g x :: real) ∈ measurable M borel"
  using assms by (simp_all add: powr_def)

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"
  using measurable_compose[OF f] borel_measurable_continuous_countable_exceptions[of "{∞, -∞ }"]
  by (auto intro: continuous_on_real simp: Compl_eq_Diff_UNIV)

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"
  by (smt (verit, ccfv_SIG) borel_measurable_uminus_ereal ereal_uminus_uminus measurable_cong)

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

theorem 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"
  by (metis Diff_Compl Diff_Diff_Int diff_eq inf_aci(1) sets.Diff sets.top vimage_Compl)

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 ‹ 🪙‹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_onI continuous_on_enn2ereal)

lemma measurable_e2ennreal[measurable]: "e2ennreal ∈ borel →🪙M borel"
  by (intro borel_measurable_continuous_onI 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🍋‹tag important› [simp]: "is_borel f M ⟷ f ∈ borel_measurable M"

lemma is_borel_transfer[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) (=) 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_power_ennreal [measurable (raw)]:
  fixes f :: "_ ==> ennreal"
  assumes f: "f ∈ borel_measurable M"
  shows "(λx. (f x) ^ n) ∈ borel_measurable M"
  by (induction n) (use f in auto)

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)

text ‹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)
      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 = {..∨ S = {..b} ∨ S = {a<..} ∨ S = {a..} ∨
    S = {a<..∨ S = {a<..b} ∨ S = {a..∨ 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 = {..∨ S = {..b} ∨
    S = {a<..} ∨ S = {a..} ∨ S = {a<..∨ S = {a<..b} ∨ S = {a..∨ S = {a..b}" by auto
  then show ?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 A f"
  shows "f ∈ borel_measurable (restrict_space borel A)"
proof -
  have "∧x. x ∈ A ==> {x} ∈ sets (restrict_space borel A)"
    using sets_restrict_space by fastforce
  moreover
  have "continuous_on (A ∩ - {a ∈ A. ¬ continuous (at a within A) f}) f"
    by (force simp: continuous_on_eq_continuous_within intro: continuous_within_subset)
  then have "f ∈ borel_measurable (restrict_space (restrict_space borel A)
              (- {a ∈ A. ¬ continuous (at a within A) f}))"
    by (smt (verit, best) borel_measurable_continuous_on_restrict measurable_cong_sets sets_restrict_restrict_space)
  ultimately show ?thesis
    using measurable_restrict_countable[OF mono_on_ctble_discont[OF assms]]
    by (smt (verit, del_insts) UNIV_I mem_Collect_eq space_borel)
qed

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 c f" "(∪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 UNIV f] 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: "{..
    by auto
  show "{..∈ 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 ‹🚫› 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

text ‹Logically equivalent to those with the opposite orientation, still these are needed›
lemma measurable_inequality_set_flipped:
  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"
  by auto

lemmas measurable_inequality_set [measurable] =
  borel_measurable_le borel_measurable_less measurable_inequality_set_flipped

proposition 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"
  by simp

text ‹The next one is a variation around ‹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

lemma measurable_restrict_mono:
  assumes f: "f ∈ restrict_space M A →🪙M N" and "B ⊆ A"
  shows "f ∈ restrict_space M B →🪙M N"
  by (rule measurable_compose[OF measurable_restrict_space3 f]) (use ‹B ⊆ A› in auto)


text ‹The next one is a variation around ‹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 "f-`B ∩ A n ∈ sets M"
      by (simp add: "*")
  }
  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 show "f x ∈ space N"
    by (metis ‹x ∈ A n› ‹x ∈ space M› measurable_space)
qed

end