Quelle Borel_Space.thy Sprache: Isabelle

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

section \<open>Borel Space\<close>

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 \<open>x \<in> interior A\<close> show "0 \<in> ?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 \<open>mono_on A f\<close> by (simp add: mono_on_def)
  have "\a \ {a\A. \ continuous (at a within A) f}. \q :: nat \ rat.
      (fst q = 0 \<and> of_rat (snd q) < f a \<and> (\<forall>x \<in> A. x < a \<longrightarrow> f x < of_rat (snd q))) \<or>
      (fst q = 1 \<and> of_rat (snd q) > f a \<and> (\<forall>x \<in> A. x > a \<longrightarrow> 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 \<and> real_of_rat q2 < f a \<and> (\<forall>x\<in>A. x < a \<longrightarrow> f x < real_of_rat q2) \<or>
            q1 = 1 \<and> f a < real_of_rat q2 \<and> (\<forall>x\<in>A. a < x \<longrightarrow> 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 \<and> of_rat (snd (g a)) < f a \<and> (\<forall>x \<in> A. x < a \<longrightarrow> f x < of_rat (snd (g a)))) |
      (fst (g a) = 1 \<and> of_rat (snd (g a)) > f a \<and> (\<forall>x \<in> A. x > a \<longrightarrow> f x > of_rat (snd (g a))))"
    by (rule bchoice [THEN exE]) blast
  hence g: "\a x. a \ A \ \ continuous (at a within A) f \ x \ A \
      (fst (g a) = 0 \<and> of_rat (snd (g a)) < f a \<and> (x < a \<longrightarrow> f x < of_rat (snd (g a)))) |
      (fst (g a) = 1 \<and> of_rat (snd (g a)) > f a \<and> (x > a \<longrightarrow> 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>open A\<close>] \<open>mono_on A f\<close>
  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 \<open>Generic Borel spaces\<close>

definition\<^marker>\<open>tag important\<close> (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 \
    (\<forall>S \<in> sigma_sets UNIV {S. open S}. f -` S \<inter> space M \<in> 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 \<inter> space M) :: 'a \<Rightarrow> 'x) \<in> 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 \<Omega>[measurable, simp]: "\<Omega> \<inter> space M \<in> sets M"
  shows "f \ borel_measurable (restrict_space M \) \
    (\<lambda>x. f x * indicator \<Omega> x) \<in> 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 \<Omega>[measurable, simp]: "\<Omega> \<inter> space M \<in> sets M"
  shows "f \ borel_measurable (restrict_space M \) \
    (\<lambda>x. f x * indicator \<Omega> x) \<in> 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 \<Omega>[measurable, simp]: "\<Omega> \<inter> space M \<in> sets M"
  shows "f \ borel_measurable (restrict_space M \) \
    (\<lambda>x. indicator \<Omega> x *\<^sub>R f x) \<in> borel_measurable M"
  by (subst measurable_restrict_space_iff)
     (auto simp: indicator_def of_bool_def if_distrib[where f="\x. x *\<^sub>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 _ \<open>countable B\<close>]) 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 \<open>\<Union>U = \<Union>K\<close> 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 \<open>countable B\<close> 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 \
    (\<lambda>x. if x \<in> A then f x else g x) \<in> 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 *\<^sub>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 \<open>Borel spaces on order topologies\<close>

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 "\xd. x < d \ d < y"
      with D(2)[of "{x <..< y}" for x] have "\xd\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 "\ (\xd. 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 \<open>I \<noteq> {}\<close> 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 \<open>I \<noteq> {}\<close> 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 \<open>Borel spaces on topological monoids\<close>

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 \<open>Borel spaces on Euclidean spaces\<close>

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 \<open><e\<close> 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>open M\<close>])
    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 ((\<lambda> (a, i). {x::'a::euclidean_space. x \<bullet> i < a}) ` (UNIV \<times> 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)*\<^sub>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) *\<^sub>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) *\<^sub>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) *\<^sub>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 - (\<Union>k. {x. x <e (\<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>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 *\<^sub>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 *\<^sub>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 *\<^sub>R f x) \ borel_measurable M"
proof (rule borel_measurableI)
  fix S :: "'x set" assume "open S"
  show "(\x. a + b *\<^sub>R f x) -` S \ space M \ sets M"
  proof cases
    assume "b \ 0"
    with \<open>open S\<close> have "open ((\x. (- a + x) /\<^sub>R b) ` S)" (is "open ?S")
      using open_affinity [of S "inverse b" "- a /\<^sub>R b"]
      by (auto simp: algebra_simps)
    hence "?S \ sets borel" by auto
    moreover
    have "\x. \a + b *\<^sub>R f x \ S\ \ f x \ (\x. (x - a) /\<^sub>R b) ` S"
      using \<open>b \<noteq> 0\<close> image_iff by fastforce
    with \<open>b \<noteq> 0\<close> have "(\x. a + b *\<^sub>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 *\<^sub>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 \
    (\<lambda>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 \
    (\<lambda>x. q (X x)) \<in> borel_measurable M"
  by (rule measurable_compose[where f=X and N="restrict_space borel A"])
     (auto intro!: borel_measurable_continuous_on_restrict convex_on_continuous measurable_restrict_space2)

lemma borel_measurable_ln[measurable (raw)]:
  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"
--> --------------------

--> maximum size reached

--> --------------------

quality93%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.31Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.