(* 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<..<M::ereal})" 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)" proof auto fix x assume "x ∈ A" "x < a" with q2 *[of "a - x"] show "f x < real_of_rat q2" apply (auto simp add: dist_real_def not_less) apply (subgoal_tac "f x ≤ f xa") by (auto intro: mono) qed thus ?thesis by auto next fix u assume "u > f a" then obtain q2 where q2: "f a < of_rat q2" "of_rat q2 < u" using of_rat_dense by blast assume *[rule_format]: "∀d>0. ∃x∈A. x ≠ a ∧ dist x a < d ∧ ¬ u > f x" from q2 have "real_of_rat q2 > f a ∧ (∀x∈A. x > a ⟶ f x > real_of_rat q2)" proof auto fix x assume "x ∈ A" "x > a" with q2 *[of "x - a"] show "f x > real_of_rat q2" apply (auto simp add: dist_real_def) apply (subgoal_tac "f x ≥ f xa") by (auto intro: mono) qed thus ?thesis by auto qed qed 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}" proof - have "{a∈A. ¬isCont f a} = {a∈A. ¬(continuous (at a within A) f)}" by (auto simp add: continuous_within_open [OF _ ‹open A›]) thus ?thesis apply (elim ssubst) by (rule mono_on_ctble_discont, rule assms) qed lemma mono_ctble_discont: fixes f :: "real ⇒ real" assumes "mono f" shows "countable {a. ¬ isCont f a}" using assms mono_on_ctble_discont [of 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" apply (intro differentiable_imp_continuous_on, unfold differentiable_on_def) using assms differentiable_at_withinI real_differentiable_def by blast lemma continuous_interval_vimage_Int: assumes "continuous_on {a::real..b} g" and mono: "⋀x y. a ≤ x ⟹ x ≤ y ⟹ y ≤ b ⟹ g x ≤ g y" assumes "a ≤ b" "(c::real) ≤ d" "{c..d} ⊆ {g a..g b}" obtains c' d' where "{a..b} ∩ g -` {c..d} = {c'..d'}" "c' ≤ d'" "g c' = c" "g d' = d" proof- let ?A = "{a..b} ∩ g -` {c..d}" from IVT'[of g a c b, OF _ _ ‹a ≤ b› assms(1)] assms(4,5) obtain c'' where c'': "c'' ∈ ?A" "g c'' = c" by auto from IVT'[of g a d b, OF _ _ ‹a ≤ b› assms(1)] assms(4,5) obtain d'' where d'': "d'' ∈ ?A" "g d'' = d" by auto hence [simp]: "?A ≠ {}" by blast define c' where "c' = Inf ?A" define d' where "d' = Sup ?A" have "?A ⊆ {c'..d'}" unfolding c'_def d'_def by (intro subsetI) (auto intro: cInf_lower cSup_upper) moreover from assms have "closed ?A" using continuous_on_closed_vimage[of "{a..b}" g] by (subst Int_commute) simp hence c'd'_in_set: "c' ∈ ?A" "d' ∈ ?A" unfolding c'_def d'_def by ((intro closed_contains_Inf closed_contains_Sup, simp_all)[])+ hence "{c'..d'} ⊆ ?A" using assms by (intro subsetI) (auto intro!: order_trans[of c "g c'" "g x" for x] order_trans[of "g x" "g d'" d for x] intro!: mono) moreover have "c' ≤ d'" using c'd'_in_set(2) unfolding c'_def by (intro cInf_lower) auto moreover have "g c' ≤ c" "g d' ≥ d" apply (insert c'' d'' c'd'_in_set) apply (subst c''(2)[symmetric]) apply (auto simp: c'_def intro!: mono cInf_lower c'') [] apply (subst d''(2)[symmetric]) apply (auto simp: d'_def intro!: mono cSup_upper d'') [] done with c'd'_in_set have "g c' = c" "g d' = d" by auto ultimately show ?thesis using that by blast qed subsection ‹Generic Borel spaces› definition✐‹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" proof - have "A ∈ {S. open S}" unfolding mem_Collect_eq using assms . thus ?thesis unfolding borel_def by auto qed lemma borel_closed[measurable (raw generic)]: assumes "closed A" shows "A ∈ sets borel" proof - have "space borel - (- A) ∈ sets borel" using assms unfolding closed_def by (blast intro: borel_open) thus ?thesis by simp qed lemma borel_singleton[measurable]: "A ∈ sets borel ⟹ insert x A ∈ sets (borel :: 'a::t1_space measure)" unfolding insert_def by (rule sets.Un) auto lemma sets_borel_eq_count_space: "sets (borel :: 'a::{countable, t2_space} measure) = count_space UNIV" proof - have "(⋃a∈A. {a}) ∈ sets borel" for A :: "'a set" by (intro sets.countable_UN') auto then show ?thesis by auto qed lemma borel_comp[measurable]: "A ∈ sets borel ⟹ - A ∈ sets borel" unfolding Compl_eq_Diff_UNIV by simp lemma borel_measurable_vimage: fixes f :: "'a ⇒ 'x::t2_space" assumes borel[measurable]: "f ∈ borel_measurable M" shows "f -` {x} ∩ space M ∈ sets M" by simp lemma borel_measurableI: fixes f :: "'a ⇒ 'x::topological_space" assumes "⋀S. open S ⟹ f -` S ∩ space M ∈ sets M" shows "f ∈ borel_measurable M" unfolding borel_def proof (rule measurable_measure_of, simp_all) fix S :: "'x set" assume "open S" thus "f -` S ∩ space M ∈ sets M" using assms[of S] by simp qed lemma borel_measurable_const: "(λx. c) ∈ borel_measurable M" by auto lemma borel_measurable_indicator: assumes A: "A ∈ sets M" shows "indicator A ∈ borel_measurable M" unfolding indicator_def [abs_def] using A by (auto intro!: measurable_If_set) lemma borel_measurable_count_space[measurable (raw)]: "f ∈ borel_measurable (count_space S)" unfolding measurable_def by auto lemma borel_measurable_indicator'[measurable (raw)]: assumes [measurable]: "{x∈space M. f x ∈ A x} ∈ sets M" shows "(λx. indicator (A x) (f x)) ∈ borel_measurable M" unfolding indicator_def[abs_def] by (auto intro!: measurable_If) lemma borel_measurable_indicator_iff: "(indicator A :: 'a ⇒ 'x::{t1_space, zero_neq_one}) ∈ borel_measurable M ⟷ A ∩ space M ∈ sets M" (is "?I ∈ borel_measurable M ⟷ _") proof assume "?I ∈ borel_measurable M" then have "?I -` {1} ∩ space M ∈ sets M" unfolding measurable_def by auto also have "?I -` {1} ∩ space M = A ∩ space M" unfolding indicator_def [abs_def] by auto finally show "A ∩ space M ∈ sets M" . next assume "A ∩ space M ∈ sets M" moreover have "?I ∈ borel_measurable M ⟷ (indicator (A ∩ space M) :: 'a ⇒ 'x) ∈ borel_measurable M" by (intro measurable_cong) (auto simp: indicator_def) ultimately show "?I ∈ borel_measurable M" by auto qed lemma borel_measurable_subalgebra: assumes "sets N ⊆ sets M" "space N = space M" "f ∈ borel_measurable N" shows "f ∈ borel_measurable M" using assms unfolding measurable_def by auto lemma borel_measurable_restrict_space_iff_ereal: fixes f :: "'a ⇒ ereal" assumes Ω[measurable, simp]: "Ω ∩ space M ∈ sets M" shows "f ∈ borel_measurable (restrict_space M Ω) ⟷ (λx. f x * indicator Ω x) ∈ borel_measurable M" by (subst measurable_restrict_space_iff) (auto simp: indicator_def of_bool_def if_distrib[where f="λx. a * x" for a] cong del: if_weak_cong) lemma borel_measurable_restrict_space_iff_ennreal: fixes f :: "'a ⇒ ennreal" assumes Ω[measurable, simp]: "Ω ∩ space M ∈ sets M" shows "f ∈ borel_measurable (restrict_space M Ω) ⟷ (λx. f x * indicator Ω x) ∈ borel_measurable M" by (subst measurable_restrict_space_iff) (auto simp: indicator_def of_bool_def if_distrib[where f="λx. a * x" for a] cong del: if_weak_cong) lemma borel_measurable_restrict_space_iff: fixes f :: "'a ⇒ 'b::real_normed_vector" assumes Ω[measurable, simp]: "Ω ∩ space M ∈ sets M" shows "f ∈ borel_measurable (restrict_space M Ω) ⟷ (λx. indicator Ω x *⇩_{R}f x) ∈ borel_measurable M" by (subst measurable_restrict_space_iff) (auto simp: indicator_def of_bool_def if_distrib[where f="λx. x *⇩_{R}a" for a] ac_simps cong del: if_weak_cong) lemma cbox_borel[measurable]: "cbox a b ∈ sets borel" by (auto intro: borel_closed) lemma box_borel[measurable]: "box a b ∈ sets borel" by (auto intro: borel_open) lemma borel_compact: "compact (A::'a::t2_space set) ⟹ A ∈ sets borel" by (auto intro: borel_closed dest!: compact_imp_closed) lemma borel_sigma_sets_subset: "A ⊆ sets borel ⟹ sigma_sets UNIV A ⊆ sets borel" using sets.sigma_sets_subset[of A borel] by simp lemma borel_eq_sigmaI1: fixes F :: "'i ⇒ 'a::topological_space set" and X :: "'a::topological_space set set" assumes borel_eq: "borel = sigma UNIV X" assumes X: "⋀x. x ∈ X ⟹ x ∈ sets (sigma UNIV (F ` A))" assumes F: "⋀i. i ∈ A ⟹ F i ∈ sets borel" shows "borel = sigma UNIV (F ` A)" unfolding borel_def proof (intro sigma_eqI antisym) have borel_rev_eq: "sigma_sets UNIV {S::'a set. open S} = sets borel" unfolding borel_def by simp also have "… = sigma_sets UNIV X" unfolding borel_eq by simp also have "… ⊆ sigma_sets UNIV (F`A)" using X by (intro sigma_algebra.sigma_sets_subset[OF sigma_algebra_sigma_sets]) auto finally show "sigma_sets UNIV {S. open S} ⊆ sigma_sets UNIV (F`A)" . show "sigma_sets UNIV (F`A) ⊆ sigma_sets UNIV {S. open S}" unfolding borel_rev_eq using F by (intro borel_sigma_sets_subset) auto qed auto lemma borel_eq_sigmaI2: fixes F :: "'i ⇒ 'j ⇒ 'a::topological_space set" and G :: "'l ⇒ 'k ⇒ 'a::topological_space set" assumes borel_eq: "borel = sigma UNIV ((λ(i, j). G i j)`B)" assumes X: "⋀i j. (i, j) ∈ B ⟹ G i j ∈ sets (sigma UNIV ((λ(i, j). F i j) ` A))" assumes F: "⋀i j. (i, j) ∈ A ⟹ F i j ∈ sets borel" shows "borel = sigma UNIV ((λ(i, j). F i j) ` A)" using assms by (intro borel_eq_sigmaI1[where X="(λ(i, j). G i j) ` B" and F="(λ(i, j). F i j)"]) auto lemma borel_eq_sigmaI3: fixes F :: "'i ⇒ 'j ⇒ 'a::topological_space set" and X :: "'a::topological_space set set" assumes borel_eq: "borel = sigma UNIV X" assumes X: "⋀x. x ∈ X ⟹ x ∈ sets (sigma UNIV ((λ(i, j). F i j) ` A))" assumes F: "⋀i j. (i, j) ∈ A ⟹ F i j ∈ sets borel" shows "borel = sigma UNIV ((λ(i, j). F i j) ` A)" using assms by (intro borel_eq_sigmaI1[where X=X and F="(λ(i, j). F i j)"]) auto lemma borel_eq_sigmaI4: fixes F :: "'i ⇒ 'a::topological_space set" and G :: "'l ⇒ 'k ⇒ 'a::topological_space set" assumes borel_eq: "borel = sigma UNIV ((λ(i, j). G i j)`A)" assumes X: "⋀i j. (i, j) ∈ A ⟹ G i j ∈ sets (sigma UNIV (range F))" assumes F: "⋀i. F i ∈ sets borel" shows "borel = sigma UNIV (range F)" using assms by (intro borel_eq_sigmaI1[where X="(λ(i, j). G i j) ` A" and F=F]) auto lemma borel_eq_sigmaI5: fixes F :: "'i ⇒ 'j ⇒ 'a::topological_space set" and G :: "'l ⇒ 'a::topological_space set" assumes borel_eq: "borel = sigma UNIV (range G)" assumes X: "⋀i. G i ∈ sets (sigma UNIV (range (λ(i, j). F i j)))" assumes F: "⋀i j. F i j ∈ sets borel" shows "borel = sigma UNIV (range (λ(i, j). F i j))" using assms by (intro borel_eq_sigmaI1[where X="range G" and F="(λ(i, j). F i j)"]) auto 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)" unfolding borel_def proof (intro sigma_eqI sigma_sets_eqI, safe) fix x :: "'a set" assume "open x" hence "x = UNIV - (UNIV - x)" by auto also have "… ∈ sigma_sets UNIV (Collect closed)" by (force intro: sigma_sets.Compl simp: ‹open x›) finally show "x ∈ sigma_sets UNIV (Collect closed)" by simp next fix x :: "'a set" assume "closed x" hence "x = UNIV - (UNIV - x)" by auto also have "… ∈ sigma_sets UNIV (Collect open)" by (force intro: sigma_sets.Compl simp: ‹closed x›) finally show "x ∈ sigma_sets UNIV (Collect open)" by simp qed simp_all 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" by (subst borel_measurable_restrict_space_iff[symmetric]) (auto intro: borel_measurable_continuous_on_restrict) lemma borel_measurable_Pair[measurable (raw)]: fixes f :: "'a ⇒ 'b::second_countable_topology" and g :: "'a ⇒ 'c::second_countable_topology" assumes f[measurable]: "f ∈ borel_measurable M" assumes g[measurable]: "g ∈ borel_measurable M" shows "(λx. (f x, g x)) ∈ borel_measurable M" proof (subst borel_eq_countable_basis) let ?B = "SOME B::'b set set. countable B ∧ topological_basis B" let ?C = "SOME B::'c set set. countable B ∧ topological_basis B" let ?P = "(λ(b, c). b × c) ` (?B × ?C)" show "countable ?P" "topological_basis ?P" by (auto intro!: countable_basis topological_basis_prod is_basis) show "(λx. (f x, g x)) ∈ measurable M (sigma UNIV ?P)" proof (rule measurable_measure_of) fix S assume "S ∈ ?P" then obtain b c where "b ∈ ?B" "c ∈ ?C" and S: "S = b × c" by auto then have borel: "open b" "open c" by (auto intro: is_basis topological_basis_open) have "(λx. (f x, g x)) -` S ∩ space M = (f -` b ∩ space M) ∩ (g -` c ∩ space M)" unfolding S by auto also have "… ∈ sets M" using borel by simp finally show "(λx. (f x, g x)) -` S ∩ space M ∈ sets M" . qed auto qed lemma borel_measurable_continuous_Pair: fixes f :: "'a ⇒ 'b::second_countable_topology" and g :: "'a ⇒ 'c::second_countable_topology" assumes [measurable]: "f ∈ borel_measurable M" assumes [measurable]: "g ∈ borel_measurable M" assumes H: "continuous_on UNIV (λx. H (fst x) (snd x))" shows "(λx. H (f x) (g x)) ∈ borel_measurable M" proof - have eq: "(λx. H (f x) (g x)) = (λx. (λx. H (fst x) (snd x)) (f x, g x))" by auto show ?thesis unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto qed subsection ‹Borel spaces on order topologies› lemma [measurable]: fixes a b :: "'a::linorder_topology" shows lessThan_borel: "{..< a} ∈ sets borel" and greaterThan_borel: "{a <..} ∈ sets borel" and greaterThanLessThan_borel: "{a<..<b} ∈ sets borel" and atMost_borel: "{..a} ∈ sets borel" and atLeast_borel: "{a..} ∈ sets borel" and atLeastAtMost_borel: "{a..b} ∈ sets borel" and greaterThanAtMost_borel: "{a<..b} ∈ sets borel" and atLeastLessThan_borel: "{a..<b} ∈ sets borel" unfolding greaterThanAtMost_def atLeastLessThan_def by (blast intro: borel_open borel_closed open_lessThan open_greaterThan open_greaterThanLessThan closed_atMost closed_atLeast closed_atLeastAtMost)+ lemma borel_Iio: "borel = sigma UNIV (range lessThan :: 'a::{linorder_topology, second_countable_topology} set set)" unfolding second_countable_borel_measurable[OF open_generated_order] proof (intro sigma_eqI sigma_sets_eqI) 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<y. ∃d. x < d ∧ d < y" with D(2)[of "{x <..< y}" for x] have "∀x<y. ∃d∈D. x < d ∧ d < y" by (auto simp: set_eq_iff) then have "A = UNIV - (⋂d∈{d∈D. d < y}. {d <..})" by (auto simp: A) (metis less_asym) also have "… ∈ sigma_sets UNIV (range greaterThan)" using D(1) by (intro L.Diff L.top L.countable_INT'') auto finally show ?thesis . next assume "¬ (∀x<y. ∃d. x < d ∧ d < y)" then obtain x where "x < y" "⋀d. y > d ⟹ x ≥ d" by (auto simp: not_less[symmetric]) then have "A = UNIV - {x <..}" unfolding A Compl_eq_Diff_UNIV[symmetric] by auto also have "… ∈ sigma_sets UNIV (range greaterThan)" by auto finally show ?thesis . qed qed auto qed auto lemma borel_measurableI_less: fixes f :: "'a ⇒ 'b::{linorder_topology, second_countable_topology}" shows "(⋀y. {x∈space M. f x < y} ∈ sets M) ⟹ f ∈ borel_measurable M" unfolding borel_Iio by (rule measurable_measure_of) (auto simp: Int_def conj_commute) lemma borel_measurableI_greater: fixes f :: "'a ⇒ 'b::{linorder_topology, second_countable_topology}" shows "(⋀y. {x∈space M. y < f x} ∈ sets M) ⟹ f ∈ borel_measurable M" unfolding borel_Ioi by (rule measurable_measure_of) (auto simp: Int_def conj_commute) lemma borel_measurableI_le: fixes f :: "'a ⇒ 'b::{linorder_topology, second_countable_topology}" shows "(⋀y. {x∈space M. f x ≤ y} ∈ sets M) ⟹ f ∈ borel_measurable M" by (rule borel_measurableI_greater) (auto simp: not_le[symmetric]) lemma borel_measurableI_ge: fixes f :: "'a ⇒ 'b::{linorder_topology, second_countable_topology}" shows "(⋀y. {x∈space M. y ≤ f x} ∈ sets M) ⟹ f ∈ borel_measurable M" by (rule borel_measurableI_less) (auto simp: not_le[symmetric]) lemma borel_measurable_less[measurable]: fixes f :: "'a ⇒ 'b::{second_countable_topology, linorder_topology}" assumes "f ∈ borel_measurable M" assumes "g ∈ borel_measurable M" shows "{w ∈ space M. f w < g w} ∈ sets M" proof - have "{w ∈ space M. f w < g w} = (λx. (f x, g x)) -` {x. fst x < snd x} ∩ space M" by auto also have "… ∈ sets M" by (intro measurable_sets[OF borel_measurable_Pair borel_open, OF assms open_Collect_less] continuous_intros) finally show ?thesis . qed lemma fixes f :: "'a ⇒ 'b::{second_countable_topology, linorder_topology}" assumes f[measurable]: "f ∈ borel_measurable M" assumes g[measurable]: "g ∈ borel_measurable M" shows borel_measurable_le[measurable]: "{w ∈ space M. f w ≤ g w} ∈ sets M" and borel_measurable_eq[measurable]: "{w ∈ space M. f w = g w} ∈ sets M" and borel_measurable_neq: "{w ∈ space M. f w ≠ g w} ∈ sets M" unfolding eq_iff not_less[symmetric] by measurable lemma borel_measurable_SUP[measurable (raw)]: fixes F :: "_ ⇒ _ ⇒ _::{complete_linorder, linorder_topology, second_countable_topology}" assumes [simp]: "countable I" assumes [measurable]: "⋀i. i ∈ I ⟹ F i ∈ borel_measurable M" shows "(λx. SUP i∈I. F i x) ∈ borel_measurable M" by (rule borel_measurableI_greater) (simp add: less_SUP_iff) lemma borel_measurable_INF[measurable (raw)]: fixes F :: "_ ⇒ _ ⇒ _::{complete_linorder, linorder_topology, second_countable_topology}" assumes [simp]: "countable I" assumes [measurable]: "⋀i. i ∈ I ⟹ F i ∈ borel_measurable M" shows "(λx. INF i∈I. F i x) ∈ borel_measurable M" by (rule borel_measurableI_less) (simp add: INF_less_iff) lemma borel_measurable_cSUP[measurable (raw)]: fixes F :: "_ ⇒ _ ⇒ 'a::{conditionally_complete_linorder, linorder_topology, second_countable_topology}" assumes [simp]: "countable I" assumes [measurable]: "⋀i. i ∈ I ⟹ F i ∈ borel_measurable M" assumes bdd: "⋀x. x ∈ space M ⟹ bdd_above ((λi. F i x) ` I)" shows "(λx. SUP i∈I. F i x) ∈ borel_measurable M" proof cases assume "I = {}" then show ?thesis unfolding ‹I = {}› image_empty by simp next assume "I ≠ {}" show ?thesis proof (rule borel_measurableI_le) fix y have "{x ∈ space M. ∀i∈I. F i x ≤ y} ∈ sets M" by measurable also have "{x ∈ space M. ∀i∈I. F i x ≤ y} = {x ∈ space M. (SUP i∈I. F i x) ≤ y}" by (simp add: cSUP_le_iff ‹I ≠ {}› bdd cong: conj_cong) finally show "{x ∈ space M. (SUP i∈I. F i x) ≤ y} ∈ sets M" . qed qed lemma borel_measurable_cINF[measurable (raw)]: fixes F :: "_ ⇒ _ ⇒ 'a::{conditionally_complete_linorder, linorder_topology, second_countable_topology}" assumes [simp]: "countable I" assumes [measurable]: "⋀i. i ∈ I ⟹ F i ∈ borel_measurable M" assumes bdd: "⋀x. x ∈ space M ⟹ bdd_below ((λi. F i x) ` I)" shows "(λx. INF i∈I. F i x) ∈ borel_measurable M" proof cases assume "I = {}" then show ?thesis unfolding ‹I = {}› image_empty by simp next assume "I ≠ {}" show ?thesis proof (rule borel_measurableI_ge) fix y have "{x ∈ space M. ∀i∈I. y ≤ F i x} ∈ sets M" by measurable also have "{x ∈ space M. ∀i∈I. y ≤ F i x} = {x ∈ space M. y ≤ (INF i∈I. F i x)}" by (simp add: le_cINF_iff ‹I ≠ {}› bdd cong: conj_cong) finally show "{x ∈ space M. y ≤ (INF i∈I. F i x)} ∈ sets M" . qed qed lemma borel_measurable_lfp[consumes 1, case_names continuity step]: fixes F :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b::{complete_linorder, linorder_topology, second_countable_topology})" assumes "sup_continuous F" assumes *: "⋀f. f ∈ borel_measurable M ⟹ F f ∈ borel_measurable M" shows "lfp F ∈ borel_measurable M" proof - { fix i have "((F ^^ i) bot) ∈ borel_measurable M" by (induct i) (auto intro!: *) } then have "(λx. SUP i. (F ^^ i) bot x) ∈ borel_measurable M" by measurable also have "(λx. SUP i. (F ^^ i) bot x) = (SUP i. (F ^^ i) bot)" by (auto 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 "<e" 50) lemma box_oc: "{x. a <e x ∧ x ≤ b} = {x. a <e x} ∩ {..b}" and box_co: "{x. a ≤ x ∧ x <e b} = {a..} ∩ {x. x <e b}" by auto lemma eucl_ivals[measurable]: fixes a b :: "'a::ordered_euclidean_space" shows "{x. x <e a} ∈ sets borel" and "{x. a <e x} ∈ sets borel" and "{..a} ∈ sets borel" and "{a..} ∈ sets borel" and "{a..b} ∈ sets borel" and "{x. a <e x ∧ x ≤ b} ∈ sets borel" and "{x. a ≤ x ∧ x <e b} ∈ sets borel" unfolding box_oc box_co by (auto intro: borel_open borel_closed) lemma fixes i :: "'a::{second_countable_topology, real_inner}" shows hafspace_less_borel: "{x. a < x ∙ i} ∈ sets borel" and hafspace_greater_borel: "{x. x ∙ i < a} ∈ sets borel" and hafspace_less_eq_borel: "{x. a ≤ x ∙ i} ∈ sets borel" and hafspace_greater_eq_borel: "{x. x ∙ i ≤ a} ∈ sets borel" by simp_all lemma borel_eq_box: "borel = sigma UNIV (range (λ (a, b). box a b :: 'a :: euclidean_space set))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI1[OF borel_def]) fix M :: "'a set" assume "M ∈ {S. open S}" then have "open M" by simp show "M ∈ ?SIGMA" apply (subst open_UNION_box[OF ‹open M›]) apply (safe intro!: sets.countable_UN' countable_PiE countable_Collect) apply (auto intro: countable_rat) done qed (auto simp: box_def) lemma halfspace_gt_in_halfspace: assumes i: "i ∈ A" shows "{x::'a. a < x ∙ i} ∈ sigma_sets UNIV ((λ (a, i). {x::'a::euclidean_space. x ∙ i < a}) ` (UNIV × A))" (is "?set ∈ ?SIGMA") proof - interpret sigma_algebra UNIV ?SIGMA by (intro sigma_algebra_sigma_sets) simp_all have *: "?set = (⋃n. UNIV - {x::'a. x ∙ i < a + 1 / real (Suc n)})" proof (safe, simp_all add: not_less del: of_nat_Suc) fix x :: 'a assume "a < x ∙ i" with reals_Archimedean[of "x ∙ i - a"] obtain n where "a + 1 / real (Suc n) < x ∙ i" by (auto simp: field_simps) then show "∃n. a + 1 / real (Suc n) ≤ x ∙ i" by (blast intro: less_imp_le) next fix x n have "a < a + 1 / real (Suc n)" by auto also assume "… ≤ x" finally show "a < x" . qed show "?set ∈ ?SIGMA" unfolding * by (auto intro!: Diff sigma_sets_Inter i) qed lemma borel_eq_halfspace_less: "borel = sigma UNIV ((λ(a, i). {x::'a::euclidean_space. x ∙ i < a}) ` (UNIV × Basis))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI2[OF borel_eq_box]) fix a b :: 'a have "box a b = {x∈space ?SIGMA. ∀i∈Basis. a ∙ i < x ∙ i ∧ x ∙ i < b ∙ i}" by (auto simp: box_def) also have "… ∈ sets ?SIGMA" by (intro sets.sets_Collect_conj sets.sets_Collect_finite_All sets.sets_Collect_const) (auto intro!: halfspace_gt_in_halfspace countable_PiE countable_rat) finally show "box a b ∈ sets ?SIGMA" . qed auto lemma borel_eq_halfspace_le: "borel = sigma UNIV ((λ (a, i). {x::'a::euclidean_space. x ∙ i ≤ a}) ` (UNIV × Basis))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less]) fix a :: real and i :: 'a assume "(a, i) ∈ UNIV × Basis" then have i: "i ∈ Basis" by auto have *: "{x::'a. x∙i < a} = (⋃n. {x. x∙i ≤ a - 1/real (Suc n)})" proof (safe, simp_all del: of_nat_Suc) fix x::'a assume *: "x∙i < a" with reals_Archimedean[of "a - x∙i"] obtain n where "x ∙ i < a - 1 / (real (Suc n))" by (auto simp: field_simps) then show "∃n. x ∙ i ≤ a - 1 / (real (Suc n))" by (blast intro: less_imp_le) next fix x::'a and n assume "x∙i ≤ a - 1 / real (Suc n)" also have "… < a" by auto finally show "x∙i < a" . qed show "{x. x∙i < a} ∈ ?SIGMA" unfolding * by (intro sets.countable_UN) (auto intro: i) qed auto lemma borel_eq_halfspace_ge: "borel = sigma UNIV ((λ (a, i). {x::'a::euclidean_space. a ≤ x ∙ i}) ` (UNIV × Basis))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less]) fix a :: real and i :: 'a assume i: "(a, i) ∈ UNIV × Basis" have *: "{x::'a. x∙i < a} = space ?SIGMA - {x::'a. a ≤ x∙i}" by auto show "{x. x∙i < a} ∈ ?SIGMA" unfolding * using i by (intro sets.compl_sets) auto qed auto lemma borel_eq_halfspace_greater: "borel = sigma UNIV ((λ (a, i). {x::'a::euclidean_space. a < x ∙ i}) ` (UNIV × Basis))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_le]) fix a :: real and i :: 'a assume "(a, i) ∈ (UNIV × Basis)" then have i: "i ∈ Basis" by auto have *: "{x::'a. x∙i ≤ a} = space ?SIGMA - {x::'a. a < x∙i}" by auto show "{x. x∙i ≤ a} ∈ ?SIGMA" unfolding * by (intro sets.compl_sets) (auto intro: i) qed auto lemma borel_eq_atMost: "borel = sigma UNIV (range (λa. {..a::'a::ordered_euclidean_space}))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le]) fix a :: real and i :: 'a assume "(a, i) ∈ UNIV × Basis" then have "i ∈ Basis" by auto then have *: "{x::'a. x∙i ≤ a} = (⋃k::nat. {.. (∑n∈Basis. (if n = i then a else real k)*⇩_{R}n)})" proof (safe, simp_all add: eucl_le[where 'a='a] split: if_split_asm) fix x :: 'a 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 <e x}))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le]) fix a :: real and i :: 'a assume "(a, i) ∈ UNIV × Basis" then have i: "i ∈ Basis" by auto have "{x::'a. x∙i ≤ a} = UNIV - {x::'a. a < x∙i}" by auto also have *: "{x::'a. a < x∙i} = (⋃k::nat. {x. (∑n∈Basis. (if n = i then a else -real k) *⇩_{R}n) <e x})" using i proof (safe, simp_all add: eucl_less_def split: if_split_asm) fix x :: 'a 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 "∃k::nat. ∀ia∈Basis. ia ≠ i ⟶ -real k < x ∙ ia" by (auto intro!: exI[of _ k]) qed finally show "{x. x∙i ≤ a} ∈ ?SIGMA" apply (simp only:) apply (intro sets.countable_UN sets.Diff) apply (auto intro: sigma_sets_top) done qed auto lemma borel_eq_lessThan: "borel = sigma UNIV (range (λa::'a::ordered_euclidean_space. {x. x <e a}))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_ge]) fix a :: real and i :: 'a assume "(a, i) ∈ UNIV × Basis" then have i: "i ∈ Basis" by auto have "{x::'a. a ≤ x∙i} = UNIV - {x::'a. x∙i < a}" by auto also have *: "{x::'a. x∙i < a} = (⋃k::nat. {x. x <e (∑n∈Basis. (if n = i then a else real k) *⇩_{R}n)})" using ‹i∈ Basis› proof (safe, simp_all add: eucl_less_def split: if_split_asm) fix x :: 'a 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 "∃k::nat. ∀ia∈Basis. ia ≠ i ⟶ x ∙ ia < real k" by (auto intro!: exI[of _ k]) qed finally show "{x. a ≤ x∙i} ∈ ?SIGMA" apply (simp only:) apply (intro sets.countable_UN sets.Diff) apply (auto intro: sigma_sets_top ) done qed auto lemma borel_eq_atLeastAtMost: "borel = sigma UNIV (range (λ(a,b). {a..b} ::'a::ordered_euclidean_space set))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI5[OF borel_eq_atMost]) fix a::'a have *: "{..a} = (⋃n::nat. {- real n *⇩_{R}One .. a})" proof (safe, simp_all add: eucl_le[where 'a='a]) fix x :: 'a 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 <e a} = lessThan a" by (simp add: eucl_less_def lessThan_def) lemma borel_eq_atLeastLessThan: "borel = sigma UNIV (range (λ(a, b). {a ..< b :: real}))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI5[OF borel_eq_lessThan]) have move_uminus: "⋀x y::real. -x ≤ y ⟷ -y ≤ x" by auto fix x :: real have "{..<x} = (⋃i::nat. {-real i ..< x})" by (auto simp: move_uminus real_arch_simple) then show "{y. y <e x} ∈ ?SIGMA" by (auto intro: sigma_sets.intros(2-) simp: eucl_lessThan) qed auto lemma borel_measurable_halfspacesI: fixes f :: "'a ⇒ 'c::euclidean_space" assumes F: "borel = sigma UNIV (F ` (UNIV × Basis))" and S_eq: "⋀a i. S a i = f -` F (a,i) ∩ space M" shows "f ∈ borel_measurable M = (∀i∈Basis. ∀a::real. S a i ∈ sets M)" proof safe fix a :: real and i :: 'b assume i: "i ∈ Basis" and f: "f ∈ borel_measurable M" then show "S a i ∈ sets M" unfolding assms by (auto intro!: measurable_sets simp: assms(1)) next assume a: "∀i∈Basis. ∀a. S a i ∈ sets M" then show "f ∈ borel_measurable M" by (auto intro!: measurable_measure_of simp: S_eq F) qed lemma borel_measurable_iff_halfspace_le: fixes f :: "'a ⇒ 'c::euclidean_space" shows "f ∈ borel_measurable M = (∀i∈Basis. ∀a. {w ∈ space M. f w ∙ i ≤ a} ∈ sets M)" by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto lemma borel_measurable_iff_halfspace_less: fixes f :: "'a ⇒ 'c::euclidean_space" shows "f ∈ borel_measurable M ⟷ (∀i∈Basis. ∀a. {w ∈ space M. f w ∙ i < a} ∈ sets M)" by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto lemma borel_measurable_iff_halfspace_ge: fixes f :: "'a ⇒ 'c::euclidean_space" shows "f ∈ borel_measurable M = (∀i∈Basis. ∀a. {w ∈ space M. a ≤ f w ∙ i} ∈ sets M)" by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto lemma borel_measurable_iff_halfspace_greater: fixes f :: "'a ⇒ 'c::euclidean_space" shows "f ∈ borel_measurable M ⟷ (∀i∈Basis. ∀a. {w ∈ space M. a < f w ∙ i} ∈ sets M)" by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_greater]) auto lemma borel_measurable_iff_le: "(f::'a ⇒ real) ∈ borel_measurable M = (∀a. {w ∈ space M. f w ≤ a} ∈ sets M)" using borel_measurable_iff_halfspace_le[where 'c=real] by simp lemma borel_measurable_iff_less: "(f::'a ⇒ real) ∈ borel_measurable M = (∀a. {w ∈ space M. f w < a} ∈ sets M)" using borel_measurable_iff_halfspace_less[where 'c=real] by simp lemma borel_measurable_iff_ge: "(f::'a ⇒ real) ∈ borel_measurable M = (∀a. {w ∈ space M. a ≤ f w} ∈ sets M)" using borel_measurable_iff_halfspace_ge[where 'c=real] by simp lemma borel_measurable_iff_greater: "(f::'a ⇒ real) ∈ borel_measurable M = (∀a. {w ∈ space M. a < f w} ∈ sets M)" using borel_measurable_iff_halfspace_greater[where 'c=real] by simp lemma borel_measurable_euclidean_space: fixes f :: "'a ⇒ 'c::euclidean_space" shows "f ∈ borel_measurable M ⟷ (∀i∈Basis. (λx. f x ∙ i) ∈ borel_measurable M)" proof safe assume f: "∀i∈Basis. (λx. f x ∙ i) ∈ borel_measurable M" then show "f ∈ borel_measurable M" by (subst borel_measurable_iff_halfspace_le) auto qed auto subsection "Borel measurable operators" lemma borel_measurable_norm[measurable]: "norm ∈ borel_measurable borel" by (intro borel_measurable_continuous_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") proof assume ?l from borel_measurable_uminus[OF this] show ?r by simp qed auto lemma affine_borel_measurable_vector: fixes f :: "'a ⇒ 'x::real_normed_vector" assumes "f ∈ borel_measurable M" shows "(λx. a + b *⇩_{R}f x) ∈