(* Title: HOL/Analysis/Borel_Space.thy Author: Johannes Hölzl, TU München Author: Armin Heller, TU München *) section ‹Borel spaces› theory Borel_Space imports Measurable Derivative Ordered_Euclidean_Space Extended_Real_Limits begin lemma sets_Collect_eventually_sequentially[measurable]: "(⋀i. {x∈space M. P x i} ∈ sets M) ⟹ {x∈space M. eventually (P x) sequentially} ∈ sets M" unfolding eventually_sequentially by simp lemma topological_basis_trivial: "topological_basis {A. open A}" by (auto simp: topological_basis_def) lemma open_prod_generated: "open = generate_topology {A × B | A B. open A ∧ open B}" proof - have "{A × B :: ('a × 'b) set | A B. open A ∧ open B} = ((λ(a, b). a × b) ` ({A. open A} × {A. open A}))" by auto then show ?thesis by (auto intro: topological_basis_prod topological_basis_trivial topological_basis_imp_subbasis) qed definition "mono_on f A ≡ ∀r s. r ∈ A ∧ s ∈ A ∧ r ≤ s ⟶ f r ≤ f s" lemma mono_onI: "(⋀r s. r ∈ A ⟹ s ∈ A ⟹ r ≤ s ⟹ f r ≤ f s) ⟹ mono_on f A" unfolding mono_on_def by simp lemma mono_onD: "⟦mono_on f A; r ∈ A; s ∈ A; r ≤ s⟧ ⟹ f r ≤ f s" unfolding mono_on_def by simp lemma mono_imp_mono_on: "mono f ⟹ mono_on f A" unfolding mono_def mono_on_def by auto lemma mono_on_subset: "mono_on f A ⟹ B ⊆ A ⟹ mono_on f B" unfolding mono_on_def by auto definition "strict_mono_on f A ≡ ∀r s. r ∈ A ∧ s ∈ A ∧ r < s ⟶ f r < f s" lemma strict_mono_onI: "(⋀r s. r ∈ A ⟹ s ∈ A ⟹ r < s ⟹ f r < f s) ⟹ strict_mono_on f A" unfolding strict_mono_on_def by simp lemma strict_mono_onD: "⟦strict_mono_on f A; r ∈ A; s ∈ A; r < s⟧ ⟹ f r < f s" unfolding strict_mono_on_def by simp lemma mono_on_greaterD: assumes "mono_on g A" "x ∈ A" "y ∈ A" "g x > (g (y::_::linorder) :: _ :: linorder)" shows "x > y" proof (rule ccontr) assume "¬x > y" hence "x ≤ y" by (simp add: not_less) from assms(1-3) and this have "g x ≤ g y" by (rule mono_onD) with assms(4) show False by simp qed lemma strict_mono_inv: fixes f :: "('a::linorder) ⇒ ('b::linorder)" assumes "strict_mono f" and "surj f" and inv: "⋀x. g (f x) = x" shows "strict_mono g" proof fix x y :: 'b assume "x < y" from ‹surj f› obtain x' y' where [simp]: "x = f x'" "y = f y'" by blast with ‹x < y› and ‹strict_mono f› have "x' < y'" by (simp add: strict_mono_less) with inv show "g x < g y" by simp qed lemma strict_mono_on_imp_inj_on: assumes "strict_mono_on (f :: (_ :: linorder) ⇒ (_ :: preorder)) A" shows "inj_on f A" proof (rule inj_onI) fix x y assume "x ∈ A" "y ∈ A" "f x = f y" thus "x = y" by (cases x y rule: linorder_cases) (auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x]) qed lemma strict_mono_on_leD: assumes "strict_mono_on (f :: (_ :: linorder) ⇒ _ :: preorder) A" "x ∈ A" "y ∈ A" "x ≤ y" shows "f x ≤ f y" proof (insert le_less_linear[of y x], elim disjE) assume "x < y" with assms have "f x < f y" by (rule_tac strict_mono_onD[OF assms(1)]) simp_all thus ?thesis by (rule less_imp_le) qed (insert assms, simp) lemma strict_mono_on_eqD: fixes f :: "(_ :: linorder) ⇒ (_ :: preorder)" assumes "strict_mono_on f A" "f x = f y" "x ∈ A" "y ∈ A" shows "y = x" using assms by (rule_tac linorder_cases[of x y]) (auto dest: strict_mono_onD) lemma mono_on_imp_deriv_nonneg: assumes mono: "mono_on f A" and deriv: "(f has_real_derivative D) (at x)" assumes "x ∈ interior A" shows "D ≥ 0" proof (rule tendsto_lowerbound) let ?A' = "(λy. y - x) ` interior A" from deriv show "((λh. (f (x + h) - f x) / h) ⤏ D) (at 0)" by (simp add: field_has_derivative_at has_field_derivative_def) from mono have mono': "mono_on f (interior A)" by (rule mono_on_subset) (rule interior_subset) show "eventually (λh. (f (x + h) - f x) / h ≥ 0) (at 0)" proof (subst eventually_at_topological, intro exI conjI ballI impI) have "open (interior A)" by simp hence "open ((+) (-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 lemma strict_mono_on_imp_mono_on: "strict_mono_on (f :: (_ :: linorder) ⇒ _ :: preorder) A ⟹ mono_on f A" by (rule mono_onI, rule strict_mono_on_leD) lemma mono_on_ctble_discont: fixes f :: "real ⇒ real" fixes A :: "real set" assumes "mono_on f A" shows "countable {a∈A. ¬ continuous (at a within A) f}" proof - have mono: "⋀x y. x ∈ A ⟹ y ∈ A ⟹ x ≤ y ⟹ f x ≤ f y" using ‹mono_on f A› by (simp add: mono_on_def) have "∀a ∈ {a∈A. ¬ continuous (at a within A) f}. ∃q :: nat × rat. (fst q = 0 ∧ of_rat (snd q) < f a ∧ (∀x ∈ A. x < a ⟶ f x < of_rat (snd q))) ∨ (fst q = 1 ∧ of_rat (snd q) > f a ∧ (∀x ∈ A. x > a ⟶ f x > of_rat (snd q)))" proof (clarsimp simp del: One_nat_def) fix a assume "a ∈ A" assume "¬ continuous (at a within A) f" thus "∃q1 q2. q1 = 0 ∧ real_of_rat q2 < f a ∧ (∀x∈A. x < a ⟶ f x < real_of_rat q2) ∨ q1 = 1 ∧ f a < real_of_rat q2 ∧ (∀x∈A. a < x ⟶ real_of_rat q2 < f x)" proof (auto simp add: continuous_within order_tendsto_iff eventually_at) fix l assume "l < f a" then obtain q2 where q2: "l < of_rat q2" "of_rat q2 < f a" using of_rat_dense by blast assume * [rule_format]: "∀d>0. ∃x∈A. x ≠ a ∧ dist x a < d ∧ ¬ l < f x" from q2 have "real_of_rat q2 < f a ∧ (∀x∈A. x < a ⟶ f x < real_of_rat q2)" proof auto fix x assume "x ∈ A" "x < a" with q2 *[of "a - x"] show "f x < real_of_rat q2" apply (auto simp add: dist_real_def not_less) apply (subgoal_tac "f x ≤ f xa") by (auto intro: mono) qed thus ?thesis by auto next fix u assume "u > f a" then obtain q2 where q2: "f a < of_rat q2" "of_rat q2 < u" using of_rat_dense by blast assume *[rule_format]: "∀d>0. ∃x∈A. x ≠ a ∧ dist x a < d ∧ ¬ u > f x" from q2 have "real_of_rat q2 > f a ∧ (∀x∈A. x > a ⟶ f x > real_of_rat q2)" proof auto fix x assume "x ∈ A" "x > a" with q2 *[of "x - a"] show "f x > real_of_rat q2" apply (auto simp add: dist_real_def) apply (subgoal_tac "f x ≥ f xa") by (auto intro: mono) qed thus ?thesis by auto qed qed hence "∃g :: real ⇒ nat × rat . ∀a ∈ {a∈A. ¬ continuous (at a within A) f}. (fst (g a) = 0 ∧ of_rat (snd (g a)) < f a ∧ (∀x ∈ A. x < a ⟶ f x < of_rat (snd (g a)))) | (fst (g a) = 1 ∧ of_rat (snd (g a)) > f a ∧ (∀x ∈ A. x > a ⟶ f x > of_rat (snd (g a))))" by (rule bchoice) then guess g .. hence g: "⋀a x. a ∈ A ⟹ ¬ continuous (at a within A) f ⟹ x ∈ A ⟹ (fst (g a) = 0 ∧ of_rat (snd (g a)) < f a ∧ (x < a ⟶ f x < of_rat (snd (g a)))) | (fst (g a) = 1 ∧ of_rat (snd (g a)) > f a ∧ (x > a ⟶ f x > of_rat (snd (g a))))" by auto have "inj_on g {a∈A. ¬ continuous (at a within A) f}" proof (auto simp add: inj_on_def) fix w z assume 1: "w ∈ A" and 2: "¬ continuous (at w within A) f" and 3: "z ∈ A" and 4: "¬ continuous (at z within A) f" and 5: "g w = g z" from g [OF 1 2 3] g [OF 3 4 1] 5 show "w = z" by auto qed thus ?thesis by (rule countableI') qed lemma mono_on_ctble_discont_open: fixes f :: "real ⇒ real" fixes A :: "real set" assumes "open A" "mono_on f A" shows "countable {a∈A. ¬isCont f a}" proof - have "{a∈A. ¬isCont f a} = {a∈A. ¬(continuous (at a within A) f)}" by (auto simp add: continuous_within_open [OF _ ‹open A›]) thus ?thesis apply (elim ssubst) by (rule mono_on_ctble_discont, rule assms) qed lemma mono_ctble_discont: fixes f :: "real ⇒ real" assumes "mono f" shows "countable {a. ¬ isCont f a}" using assms mono_on_ctble_discont [of f UNIV] unfolding mono_on_def mono_def by auto lemma has_real_derivative_imp_continuous_on: assumes "⋀x. x ∈ A ⟹ (f has_real_derivative f' x) (at x)" shows "continuous_on A f" apply (intro differentiable_imp_continuous_on, unfold differentiable_on_def) apply (intro ballI Deriv.differentiableI) apply (rule has_field_derivative_subset[OF assms]) apply simp_all done lemma closure_contains_Sup: fixes S :: "real set" assumes "S ≠ {}" "bdd_above S" shows "Sup S ∈ closure S" proof- have "Inf (uminus ` S) ∈ closure (uminus ` S)" using assms by (intro closure_contains_Inf) auto also have "Inf (uminus ` S) = -Sup S" by (simp add: Inf_real_def) also have "closure (uminus ` S) = uminus ` closure S" by (rule sym, intro closure_injective_linear_image) (auto intro: linearI) finally show ?thesis by auto qed lemma closed_contains_Sup: fixes S :: "real set" shows "S ≠ {} ⟹ bdd_above S ⟹ closed S ⟹ Sup S ∈ S" by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup) lemma closed_subset_contains_Sup: fixes A C :: "real set" shows "closed C ⟹ A ⊆ C ⟹ A ≠ {} ⟹ bdd_above A ⟹ Sup A ∈ C" by (metis closure_contains_Sup closure_minimal subset_eq) lemma deriv_nonneg_imp_mono: assumes deriv: "⋀x. x ∈ {a..b} ⟹ (g has_real_derivative g' x) (at x)" assumes nonneg: "⋀x. x ∈ {a..b} ⟹ g' x ≥ 0" assumes ab: "a ≤ b" shows "g a ≤ g b" proof (cases "a < b") assume "a < b" from deriv have "⋀x. ⟦x ≥ a; x ≤ b⟧ ⟹ (g has_real_derivative g' x) (at x)" by simp with MVT2[OF ‹a < b›] and deriv obtain ξ where ξ_ab: "ξ > a" "ξ < b" and g_ab: "g b - g a = (b - a) * g' ξ" by blast from ξ_ab ab nonneg have "(b - a) * g' ξ ≥ 0" by simp with g_ab show ?thesis by simp qed (insert ab, simp) lemma continuous_interval_vimage_Int: assumes "continuous_on {a::real..b} g" and mono: "⋀x y. a ≤ x ⟹ x ≤ y ⟹ y ≤ b ⟹ g x ≤ g y" assumes "a ≤ b" "(c::real) ≤ d" "{c..d} ⊆ {g a..g b}" obtains c' d' where "{a..b} ∩ g -` {c..d} = {c'..d'}" "c' ≤ d'" "g c' = c" "g d' = d" proof- let ?A = "{a..b} ∩ g -` {c..d}" from IVT'[of g a c b, OF _ _ ‹a ≤ b› assms(1)] assms(4,5) obtain c'' where c'': "c'' ∈ ?A" "g c'' = c" by auto from IVT'[of g a d b, OF _ _ ‹a ≤ b› assms(1)] assms(4,5) obtain d'' where d'': "d'' ∈ ?A" "g d'' = d" by auto hence [simp]: "?A ≠ {}" by blast define c' where "c' = Inf ?A" define d' where "d' = Sup ?A" have "?A ⊆ {c'..d'}" unfolding c'_def d'_def by (intro subsetI) (auto intro: cInf_lower cSup_upper) moreover from assms have "closed ?A" using continuous_on_closed_vimage[of "{a..b}" g] by (subst Int_commute) simp hence c'd'_in_set: "c' ∈ ?A" "d' ∈ ?A" unfolding c'_def d'_def by ((intro closed_contains_Inf closed_contains_Sup, simp_all)[])+ hence "{c'..d'} ⊆ ?A" using assms by (intro subsetI) (auto intro!: order_trans[of c "g c'" "g x" for x] order_trans[of "g x" "g d'" d for x] intro!: mono) moreover have "c' ≤ d'" using c'd'_in_set(2) unfolding c'_def by (intro cInf_lower) auto moreover have "g c' ≤ c" "g d' ≥ d" apply (insert c'' d'' c'd'_in_set) apply (subst c''(2)[symmetric]) apply (auto simp: c'_def intro!: mono cInf_lower c'') [] apply (subst d''(2)[symmetric]) apply (auto simp: d'_def intro!: mono cSup_upper d'') [] done with c'd'_in_set have "g c' = c" "g d' = d" by auto ultimately show ?thesis using that by blast qed subsection ‹Generic Borel spaces› definition (in topological_space) borel :: "'a measure" where "borel = sigma UNIV {S. open S}" abbreviation "borel_measurable M ≡ measurable M borel" lemma in_borel_measurable: "f ∈ borel_measurable M ⟷ (∀S ∈ sigma_sets UNIV {S. open S}. f -` S ∩ space M ∈ sets M)" by (auto simp add: measurable_def borel_def) lemma in_borel_measurable_borel: "f ∈ borel_measurable M ⟷ (∀S ∈ sets borel. f -` S ∩ space M ∈ sets M)" by (auto simp add: measurable_def borel_def) lemma space_borel[simp]: "space borel = UNIV" unfolding borel_def by auto lemma space_in_borel[measurable]: "UNIV ∈ sets borel" unfolding borel_def by auto lemma sets_borel: "sets borel = sigma_sets UNIV {S. open S}" unfolding borel_def by (rule sets_measure_of) simp lemma measurable_sets_borel: "⟦f ∈ measurable borel M; A ∈ sets M⟧ ⟹ f -` A ∈ sets borel" by (drule (1) measurable_sets) simp lemma pred_Collect_borel[measurable (raw)]: "Measurable.pred borel P ⟹ {x. P x} ∈ sets borel" unfolding borel_def pred_def by auto lemma borel_open[measurable (raw generic)]: assumes "open A" shows "A ∈ sets borel" proof - have "A ∈ {S. open S}" unfolding mem_Collect_eq using assms . thus ?thesis unfolding borel_def by auto qed lemma borel_closed[measurable (raw generic)]: assumes "closed A" shows "A ∈ sets borel" proof - have "space borel - (- A) ∈ sets borel" using assms unfolding closed_def by (blast intro: borel_open) thus ?thesis by simp qed lemma borel_singleton[measurable]: "A ∈ sets borel ⟹ insert x A ∈ sets (borel :: 'a::t1_space measure)" unfolding insert_def by (rule sets.Un) auto lemma sets_borel_eq_count_space: "sets (borel :: 'a::{countable, t2_space} measure) = count_space UNIV" proof - have "(⋃a∈A. {a}) ∈ sets borel" for A :: "'a set" by (intro sets.countable_UN') auto then show ?thesis by auto qed lemma borel_comp[measurable]: "A ∈ sets borel ⟹ - A ∈ sets borel" unfolding Compl_eq_Diff_UNIV by simp lemma borel_measurable_vimage: fixes f :: "'a ⇒ 'x::t2_space" assumes borel[measurable]: "f ∈ borel_measurable M" shows "f -` {x} ∩ space M ∈ sets M" by simp lemma borel_measurableI: fixes f :: "'a ⇒ 'x::topological_space" assumes "⋀S. open S ⟹ f -` S ∩ space M ∈ sets M" shows "f ∈ borel_measurable M" unfolding borel_def proof (rule measurable_measure_of, simp_all) fix S :: "'x set" assume "open S" thus "f -` S ∩ space M ∈ sets M" using assms[of S] by simp qed lemma borel_measurable_const: "(λx. c) ∈ borel_measurable M" by auto lemma borel_measurable_indicator: assumes A: "A ∈ sets M" shows "indicator A ∈ borel_measurable M" unfolding indicator_def [abs_def] using A by (auto intro!: measurable_If_set) lemma borel_measurable_count_space[measurable (raw)]: "f ∈ borel_measurable (count_space S)" unfolding measurable_def by auto lemma borel_measurable_indicator'[measurable (raw)]: assumes [measurable]: "{x∈space M. f x ∈ A x} ∈ sets M" shows "(λx. indicator (A x) (f x)) ∈ borel_measurable M" unfolding indicator_def[abs_def] by (auto intro!: measurable_If) lemma borel_measurable_indicator_iff: "(indicator A :: 'a ⇒ 'x::{t1_space, zero_neq_one}) ∈ borel_measurable M ⟷ A ∩ space M ∈ sets M" (is "?I ∈ borel_measurable M ⟷ _") proof assume "?I ∈ borel_measurable M" then have "?I -` {1} ∩ space M ∈ sets M" unfolding measurable_def by auto also have "?I -` {1} ∩ space M = A ∩ space M" unfolding indicator_def [abs_def] by auto finally show "A ∩ space M ∈ sets M" . next assume "A ∩ space M ∈ sets M" moreover have "?I ∈ borel_measurable M ⟷ (indicator (A ∩ space M) :: 'a ⇒ 'x) ∈ borel_measurable M" by (intro measurable_cong) (auto simp: indicator_def) ultimately show "?I ∈ borel_measurable M" by auto qed lemma borel_measurable_subalgebra: assumes "sets N ⊆ sets M" "space N = space M" "f ∈ borel_measurable N" shows "f ∈ borel_measurable M" using assms unfolding measurable_def by auto lemma borel_measurable_restrict_space_iff_ereal: fixes f :: "'a ⇒ ereal" assumes Ω[measurable, simp]: "Ω ∩ space M ∈ sets M" shows "f ∈ borel_measurable (restrict_space M Ω) ⟷ (λx. f x * indicator Ω x) ∈ borel_measurable M" by (subst measurable_restrict_space_iff) (auto simp: indicator_def if_distrib[where f="λx. a * x" for a] cong del: if_weak_cong) lemma borel_measurable_restrict_space_iff_ennreal: fixes f :: "'a ⇒ ennreal" assumes Ω[measurable, simp]: "Ω ∩ space M ∈ sets M" shows "f ∈ borel_measurable (restrict_space M Ω) ⟷ (λx. f x * indicator Ω x) ∈ borel_measurable M" by (subst measurable_restrict_space_iff) (auto simp: indicator_def if_distrib[where f="λx. a * x" for a] cong del: if_weak_cong) lemma borel_measurable_restrict_space_iff: fixes f :: "'a ⇒ 'b::real_normed_vector" assumes Ω[measurable, simp]: "Ω ∩ space M ∈ sets M" shows "f ∈ borel_measurable (restrict_space M Ω) ⟷ (λx. indicator Ω x *⇩_{R}f x) ∈ borel_measurable M" by (subst measurable_restrict_space_iff) (auto simp: indicator_def if_distrib[where f="λx. x *⇩_{R}a" for a] ac_simps cong del: if_weak_cong) lemma cbox_borel[measurable]: "cbox a b ∈ sets borel" by (auto intro: borel_closed) lemma box_borel[measurable]: "box a b ∈ sets borel" by (auto intro: borel_open) lemma borel_compact: "compact (A::'a::t2_space set) ⟹ A ∈ sets borel" by (auto intro: borel_closed dest!: compact_imp_closed) lemma borel_sigma_sets_subset: "A ⊆ sets borel ⟹ sigma_sets UNIV A ⊆ sets borel" using sets.sigma_sets_subset[of A borel] by simp lemma borel_eq_sigmaI1: fixes F :: "'i ⇒ 'a::topological_space set" and X :: "'a::topological_space set set" assumes borel_eq: "borel = sigma UNIV X" assumes X: "⋀x. x ∈ X ⟹ x ∈ sets (sigma UNIV (F ` A))" assumes F: "⋀i. i ∈ A ⟹ F i ∈ sets borel" shows "borel = sigma UNIV (F ` A)" unfolding borel_def proof (intro sigma_eqI antisym) have borel_rev_eq: "sigma_sets UNIV {S::'a set. open S} = sets borel" unfolding borel_def by simp also have "… = sigma_sets UNIV X" unfolding borel_eq by simp also have "… ⊆ sigma_sets UNIV (F`A)" using X by (intro sigma_algebra.sigma_sets_subset[OF sigma_algebra_sigma_sets]) auto finally show "sigma_sets UNIV {S. open S} ⊆ sigma_sets UNIV (F`A)" . show "sigma_sets UNIV (F`A) ⊆ sigma_sets UNIV {S. open S}" unfolding borel_rev_eq using F by (intro borel_sigma_sets_subset) auto qed auto lemma borel_eq_sigmaI2: fixes F :: "'i ⇒ 'j ⇒ 'a::topological_space set" and G :: "'l ⇒ 'k ⇒ 'a::topological_space set" assumes borel_eq: "borel = sigma UNIV ((λ(i, j). G i j)`B)" assumes X: "⋀i j. (i, j) ∈ B ⟹ G i j ∈ sets (sigma UNIV ((λ(i, j). F i j) ` A))" assumes F: "⋀i j. (i, j) ∈ A ⟹ F i j ∈ sets borel" shows "borel = sigma UNIV ((λ(i, j). F i j) ` A)" using assms by (intro borel_eq_sigmaI1[where X="(λ(i, j). G i j) ` B" and F="(λ(i, j). F i j)"]) auto lemma borel_eq_sigmaI3: fixes F :: "'i ⇒ 'j ⇒ 'a::topological_space set" and X :: "'a::topological_space set set" assumes borel_eq: "borel = sigma UNIV X" assumes X: "⋀x. x ∈ X ⟹ x ∈ sets (sigma UNIV ((λ(i, j). F i j) ` A))" assumes F: "⋀i j. (i, j) ∈ A ⟹ F i j ∈ sets borel" shows "borel = sigma UNIV ((λ(i, j). F i j) ` A)" using assms by (intro borel_eq_sigmaI1[where X=X and F="(λ(i, j). F i j)"]) auto lemma borel_eq_sigmaI4: fixes F :: "'i ⇒ 'a::topological_space set" and G :: "'l ⇒ 'k ⇒ 'a::topological_space set" assumes borel_eq: "borel = sigma UNIV ((λ(i, j). G i j)`A)" assumes X: "⋀i j. (i, j) ∈ A ⟹ G i j ∈ sets (sigma UNIV (range F))" assumes F: "⋀i. F i ∈ sets borel" shows "borel = sigma UNIV (range F)" using assms by (intro borel_eq_sigmaI1[where X="(λ(i, j). G i j) ` A" and F=F]) auto lemma borel_eq_sigmaI5: fixes F :: "'i ⇒ 'j ⇒ 'a::topological_space set" and G :: "'l ⇒ 'a::topological_space set" assumes borel_eq: "borel = sigma UNIV (range G)" assumes X: "⋀i. G i ∈ sets (sigma UNIV (range (λ(i, j). F i j)))" assumes F: "⋀i j. F i j ∈ sets borel" shows "borel = sigma UNIV (range (λ(i, j). F i j))" using assms by (intro borel_eq_sigmaI1[where X="range G" and F="(λ(i, j). F i j)"]) auto lemma second_countable_borel_measurable: fixes X :: "'a::second_countable_topology set set" assumes eq: "open = generate_topology X" shows "borel = sigma UNIV X" unfolding borel_def proof (intro sigma_eqI sigma_sets_eqI) interpret X: sigma_algebra UNIV "sigma_sets UNIV X" by (rule sigma_algebra_sigma_sets) simp fix S :: "'a set" assume "S ∈ Collect open" then have "generate_topology X S" by (auto simp: eq) then show "S ∈ sigma_sets UNIV X" proof induction case (UN K) then have K: "⋀k. k ∈ K ⟹ open k" unfolding eq by auto from ex_countable_basis obtain B :: "'a set set" where B: "⋀b. b ∈ B ⟹ open b" "⋀X. open X ⟹ ∃b⊆B. (⋃b) = X" and "countable B" by (auto simp: topological_basis_def) from B(2)[OF K] obtain m where m: "⋀k. k ∈ K ⟹ m k ⊆ B" "⋀k. k ∈ K ⟹ (⋃m k) = k" by metis define U where "U = (⋃k∈K. m k)" with m have "countable U" by (intro countable_subset[OF _ ‹countable B›]) auto have "⋃U = (⋃A∈U. A)" by simp also have "… = ⋃K" unfolding U_def UN_simps by (simp add: m) finally have "⋃U = ⋃K" . have "∀b∈U. ∃k∈K. b ⊆ k" using m by (auto simp: U_def) then obtain u where u: "⋀b. b ∈ U ⟹ u b ∈ K" and "⋀b. b ∈ U ⟹ b ⊆ u b" by metis then have "(⋃b∈U. u b) ⊆ ⋃K" "⋃U ⊆ (⋃b∈U. u b)" by auto then have "⋃K = (⋃b∈U. u b)" unfolding ‹⋃U = ⋃K› by auto also have "… ∈ sigma_sets UNIV X" using u UN by (intro X.countable_UN' ‹countable U›) auto finally show "⋃K ∈ sigma_sets UNIV X" . qed auto qed (auto simp: eq intro: generate_topology.Basis) lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)" unfolding borel_def proof (intro sigma_eqI sigma_sets_eqI, safe) fix x :: "'a set" assume "open x" hence "x = UNIV - (UNIV - x)" by auto also have "… ∈ sigma_sets UNIV (Collect closed)" by (force intro: sigma_sets.Compl simp: ‹open x›) finally show "x ∈ sigma_sets UNIV (Collect closed)" by simp next fix x :: "'a set" assume "closed x" hence "x = UNIV - (UNIV - x)" by auto also have "… ∈ sigma_sets UNIV (Collect open)" by (force intro: sigma_sets.Compl simp: ‹closed x›) finally show "x ∈ sigma_sets UNIV (Collect open)" by simp qed simp_all lemma borel_eq_countable_basis: fixes B::"'a::topological_space set set" assumes "countable B" assumes "topological_basis B" shows "borel = sigma UNIV B" unfolding borel_def proof (intro sigma_eqI sigma_sets_eqI, safe) interpret countable_basis using assms by unfold_locales fix X::"'a set" assume "open X" from open_countable_basisE[OF this] guess B' . note B' = this then show "X ∈ sigma_sets UNIV B" by (blast intro: sigma_sets_UNION ‹countable B› countable_subset) next fix b assume "b ∈ B" hence "open b" by (rule topological_basis_open[OF assms(2)]) thus "b ∈ sigma_sets UNIV (Collect open)" by auto qed simp_all lemma borel_measurable_continuous_on_restrict: fixes f :: "'a::topological_space ⇒ 'b::topological_space" assumes f: "continuous_on A f" shows "f ∈ borel_measurable (restrict_space borel A)" proof (rule borel_measurableI) fix S :: "'b set" assume "open S" with f obtain T where "f -` S ∩ A = T ∩ A" "open T" by (metis continuous_on_open_invariant) then show "f -` S ∩ space (restrict_space borel A) ∈ sets (restrict_space borel A)" by (force simp add: sets_restrict_space space_restrict_space) qed lemma borel_measurable_continuous_on1: "continuous_on UNIV f ⟹ f ∈ borel_measurable borel" by (drule borel_measurable_continuous_on_restrict) simp lemma borel_measurable_continuous_on_if: "A ∈ sets borel ⟹ continuous_on A f ⟹ continuous_on (- A) g ⟹ (λx. if x ∈ A then f x else g x) ∈ borel_measurable borel" by (auto simp add: measurable_If_restrict_space_iff Collect_neg_eq intro!: borel_measurable_continuous_on_restrict) lemma borel_measurable_continuous_countable_exceptions: fixes f :: "'a::t1_space ⇒ 'b::topological_space" assumes X: "countable X" assumes "continuous_on (- X) f" shows "f ∈ borel_measurable borel" proof (rule measurable_discrete_difference[OF _ X]) have "X ∈ sets borel" by (rule sets.countable[OF _ X]) auto then show "(λx. if x ∈ X then undefined else f x) ∈ borel_measurable borel" by (intro borel_measurable_continuous_on_if assms continuous_intros) qed auto lemma borel_measurable_continuous_on: assumes f: "continuous_on UNIV f" and g: "g ∈ borel_measurable M" shows "(λx. f (g x)) ∈ borel_measurable M" using measurable_comp[OF g borel_measurable_continuous_on1[OF f]] by (simp add: comp_def) lemma borel_measurable_continuous_on_indicator: fixes f g :: "'a::topological_space ⇒ 'b::real_normed_vector" shows "A ∈ sets borel ⟹ continuous_on A f ⟹ (λx. indicator A x *⇩_{R}f x) ∈ borel_measurable borel" by (subst borel_measurable_restrict_space_iff[symmetric]) (auto intro: borel_measurable_continuous_on_restrict) lemma borel_measurable_Pair[measurable (raw)]: fixes f :: "'a ⇒ 'b::second_countable_topology" and g :: "'a ⇒ 'c::second_countable_topology" assumes f[measurable]: "f ∈ borel_measurable M" assumes g[measurable]: "g ∈ borel_measurable M" shows "(λx. (f x, g x)) ∈ borel_measurable M" proof (subst borel_eq_countable_basis) let ?B = "SOME B::'b set set. countable B ∧ topological_basis B" let ?C = "SOME B::'c set set. countable B ∧ topological_basis B" let ?P = "(λ(b, c). b × c) ` (?B × ?C)" show "countable ?P" "topological_basis ?P" by (auto intro!: countable_basis topological_basis_prod is_basis) show "(λx. (f x, g x)) ∈ measurable M (sigma UNIV ?P)" proof (rule measurable_measure_of) fix S assume "S ∈ ?P" then obtain b c where "b ∈ ?B" "c ∈ ?C" and S: "S = b × c" by auto then have borel: "open b" "open c" by (auto intro: is_basis topological_basis_open) have "(λx. (f x, g x)) -` S ∩ space M = (f -` b ∩ space M) ∩ (g -` c ∩ space M)" unfolding S by auto also have "… ∈ sets M" using borel by simp finally show "(λx. (f x, g x)) -` S ∩ space M ∈ sets M" . qed auto qed lemma borel_measurable_continuous_Pair: fixes f :: "'a ⇒ 'b::second_countable_topology" and g :: "'a ⇒ 'c::second_countable_topology" assumes [measurable]: "f ∈ borel_measurable M" assumes [measurable]: "g ∈ borel_measurable M" assumes H: "continuous_on UNIV (λx. H (fst x) (snd x))" shows "(λx. H (f x) (g x)) ∈ borel_measurable M" proof - have eq: "(λx. H (f x) (g x)) = (λx. (λx. H (fst x) (snd x)) (f x, g x))" by auto show ?thesis unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto qed subsection ‹Borel spaces on order topologies› lemma [measurable]: fixes a b :: "'a::linorder_topology" shows lessThan_borel: "{..< a} ∈ sets borel" and greaterThan_borel: "{a <..} ∈ sets borel" and greaterThanLessThan_borel: "{a<..<b} ∈ sets borel" and atMost_borel: "{..a} ∈ sets borel" and atLeast_borel: "{a..} ∈ sets borel" and atLeastAtMost_borel: "{a..b} ∈ sets borel" and greaterThanAtMost_borel: "{a<..b} ∈ sets borel" and atLeastLessThan_borel: "{a..<b} ∈ sets borel" unfolding greaterThanAtMost_def atLeastLessThan_def by (blast intro: borel_open borel_closed open_lessThan open_greaterThan open_greaterThanLessThan closed_atMost closed_atLeast closed_atLeastAtMost)+ lemma borel_Iio: "borel = sigma UNIV (range lessThan :: 'a::{linorder_topology, second_countable_topology} set set)" unfolding second_countable_borel_measurable[OF open_generated_order] proof (intro sigma_eqI sigma_sets_eqI) from countable_dense_setE guess D :: "'a set" . note D = this interpret L: sigma_algebra UNIV "sigma_sets UNIV (range lessThan)" by (rule sigma_algebra_sigma_sets) simp fix A :: "'a set" assume "A ∈ range lessThan ∪ range greaterThan" then obtain y where "A = {y <..} ∨ A = {..< y}" by blast then show "A ∈ sigma_sets UNIV (range lessThan)" proof assume A: "A = {y <..}" show ?thesis proof cases assume "∀x>y. ∃d. y < d ∧ d < x" with D(2)[of "{y <..< x}" for x] have "∀x>y. ∃d∈D. y < d ∧ d < x" by (auto simp: set_eq_iff) then have "A = UNIV - (⋂d∈{d∈D. y < d}. {..< d})" by (auto simp: A) (metis less_asym) also have "… ∈ sigma_sets UNIV (range lessThan)" using D(1) by (intro L.Diff L.top L.countable_INT'') auto finally show ?thesis . next assume "¬ (∀x>y. ∃d. y < d ∧ d < x)" then obtain x where "y < x" "⋀d. y < d ⟹ ¬ d < x" by auto then have "A = UNIV - {..< x}" unfolding A by (auto simp: not_less[symmetric]) also have "… ∈ sigma_sets UNIV (range lessThan)" by auto finally show ?thesis . qed qed auto qed auto lemma borel_Ioi: "borel = sigma UNIV (range greaterThan :: 'a::{linorder_topology, second_countable_topology} set set)" unfolding second_countable_borel_measurable[OF open_generated_order] proof (intro sigma_eqI sigma_sets_eqI) from countable_dense_setE guess D :: "'a set" . note D = this interpret L: sigma_algebra UNIV "sigma_sets UNIV (range greaterThan)" by (rule sigma_algebra_sigma_sets) simp fix A :: "'a set" assume "A ∈ range lessThan ∪ range greaterThan" then obtain y where "A = {y <..} ∨ A = {..< y}" by blast then show "A ∈ sigma_sets UNIV (range greaterThan)" proof assume A: "A = {..< y}" show ?thesis proof cases assume "∀x<y. ∃d. x < d ∧ d < y" with D(2)[of "{x <..< y}" for x] have "∀x<y. ∃d∈D. x < d ∧ d < y" by (auto simp: set_eq_iff) then have "A = UNIV - (⋂d∈{d∈D. d < y}. {d <..})" by (auto simp: A) (metis less_asym) also have "… ∈ sigma_sets UNIV (range greaterThan)" using D(1) by (intro L.Diff L.top L.countable_INT'') auto finally show ?thesis . next assume "¬ (∀x<y. ∃d. x < d ∧ d < y)" then obtain x where "x < y" "⋀d. y > d ⟹ x ≥ d" by (auto simp: not_less[symmetric]) then have "A = UNIV - {x <..}" unfolding A Compl_eq_Diff_UNIV[symmetric] by auto also have "… ∈ sigma_sets UNIV (range greaterThan)" by auto finally show ?thesis . qed qed auto qed auto lemma borel_measurableI_less: fixes f :: "'a ⇒ 'b::{linorder_topology, second_countable_topology}" shows "(⋀y. {x∈space M. f x < y} ∈ sets M) ⟹ f ∈ borel_measurable M" unfolding borel_Iio by (rule measurable_measure_of) (auto simp: Int_def conj_commute) lemma borel_measurableI_greater: fixes f :: "'a ⇒ 'b::{linorder_topology, second_countable_topology}" shows "(⋀y. {x∈space M. y < f x} ∈ sets M) ⟹ f ∈ borel_measurable M" unfolding borel_Ioi by (rule measurable_measure_of) (auto simp: Int_def conj_commute) lemma borel_measurableI_le: fixes f :: "'a ⇒ 'b::{linorder_topology, second_countable_topology}" shows "(⋀y. {x∈space M. f x ≤ y} ∈ sets M) ⟹ f ∈ borel_measurable M" by (rule borel_measurableI_greater) (auto simp: not_le[symmetric]) lemma borel_measurableI_ge: fixes f :: "'a ⇒ 'b::{linorder_topology, second_countable_topology}" shows "(⋀y. {x∈space M. y ≤ f x} ∈ sets M) ⟹ f ∈ borel_measurable M" by (rule borel_measurableI_less) (auto simp: not_le[symmetric]) lemma borel_measurable_less[measurable]: fixes f :: "'a ⇒ 'b::{second_countable_topology, linorder_topology}" assumes "f ∈ borel_measurable M" assumes "g ∈ borel_measurable M" shows "{w ∈ space M. f w < g w} ∈ sets M" proof - have "{w ∈ space M. f w < g w} = (λx. (f x, g x)) -` {x. fst x < snd x} ∩ space M" by auto also have "… ∈ sets M" by (intro measurable_sets[OF borel_measurable_Pair borel_open, OF assms open_Collect_less] continuous_intros) finally show ?thesis . qed lemma fixes f :: "'a ⇒ 'b::{second_countable_topology, linorder_topology}" assumes f[measurable]: "f ∈ borel_measurable M" assumes g[measurable]: "g ∈ borel_measurable M" shows borel_measurable_le[measurable]: "{w ∈ space M. f w ≤ g w} ∈ sets M" and borel_measurable_eq[measurable]: "{w ∈ space M. f w = g w} ∈ sets M" and borel_measurable_neq: "{w ∈ space M. f w ≠ g w} ∈ sets M" unfolding eq_iff not_less[symmetric] by measurable lemma borel_measurable_SUP[measurable (raw)]: fixes F :: "_ ⇒ _ ⇒ _::{complete_linorder, linorder_topology, second_countable_topology}" assumes [simp]: "countable I" assumes [measurable]: "⋀i. i ∈ I ⟹ F i ∈ borel_measurable M" shows "(λx. SUP i:I. F i x) ∈ borel_measurable M" by (rule borel_measurableI_greater) (simp add: less_SUP_iff) lemma borel_measurable_INF[measurable (raw)]: fixes F :: "_ ⇒ _ ⇒ _::{complete_linorder, linorder_topology, second_countable_topology}" assumes [simp]: "countable I" assumes [measurable]: "⋀i. i ∈ I ⟹ F i ∈ borel_measurable M" shows "(λx. INF i:I. F i x) ∈ borel_measurable M" by (rule borel_measurableI_less) (simp add: INF_less_iff) lemma borel_measurable_cSUP[measurable (raw)]: fixes F :: "_ ⇒ _ ⇒ 'a::{conditionally_complete_linorder, linorder_topology, second_countable_topology}" assumes [simp]: "countable I" assumes [measurable]: "⋀i. i ∈ I ⟹ F i ∈ borel_measurable M" assumes bdd: "⋀x. x ∈ space M ⟹ bdd_above ((λi. F i x) ` I)" shows "(λx. SUP i:I. F i x) ∈ borel_measurable M" proof cases assume "I = {}" then show ?thesis unfolding ‹I = {}› image_empty by simp next assume "I ≠ {}" show ?thesis proof (rule borel_measurableI_le) fix y have "{x ∈ space M. ∀i∈I. F i x ≤ y} ∈ sets M" by measurable also have "{x ∈ space M. ∀i∈I. F i x ≤ y} = {x ∈ space M. (SUP i:I. F i x) ≤ y}" by (simp add: cSUP_le_iff ‹I ≠ {}› bdd cong: conj_cong) finally show "{x ∈ space M. (SUP i:I. F i x) ≤ y} ∈ sets M" . qed qed lemma borel_measurable_cINF[measurable (raw)]: fixes F :: "_ ⇒ _ ⇒ 'a::{conditionally_complete_linorder, linorder_topology, second_countable_topology}" assumes [simp]: "countable I" assumes [measurable]: "⋀i. i ∈ I ⟹ F i ∈ borel_measurable M" assumes bdd: "⋀x. x ∈ space M ⟹ bdd_below ((λi. F i x) ` I)" shows "(λx. INF i:I. F i x) ∈ borel_measurable M" proof cases assume "I = {}" then show ?thesis unfolding ‹I = {}› image_empty by simp next assume "I ≠ {}" show ?thesis proof (rule borel_measurableI_ge) fix y have "{x ∈ space M. ∀i∈I. y ≤ F i x} ∈ sets M" by measurable also have "{x ∈ space M. ∀i∈I. y ≤ F i x} = {x ∈ space M. y ≤ (INF i:I. F i x)}" by (simp add: le_cINF_iff ‹I ≠ {}› bdd cong: conj_cong) finally show "{x ∈ space M. y ≤ (INF i:I. F i x)} ∈ sets M" . qed qed lemma borel_measurable_lfp[consumes 1, case_names continuity step]: fixes F :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b::{complete_linorder, linorder_topology, second_countable_topology})" assumes "sup_continuous F" assumes *: "⋀f. f ∈ borel_measurable M ⟹ F f ∈ borel_measurable M" shows "lfp F ∈ borel_measurable M" proof - { fix i have "((F ^^ i) bot) ∈ borel_measurable M" by (induct i) (auto intro!: *) } then have "(λx. SUP i. (F ^^ i) bot x) ∈ borel_measurable M" by measurable also have "(λx. SUP i. (F ^^ i) bot x) = (SUP i. (F ^^ i) bot)" by auto also have "(SUP i. (F ^^ i) bot) = lfp F" by (rule sup_continuous_lfp[symmetric]) fact finally show ?thesis . qed lemma borel_measurable_gfp[consumes 1, case_names continuity step]: fixes F :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b::{complete_linorder, linorder_topology, second_countable_topology})" assumes "inf_continuous F" assumes *: "⋀f. f ∈ borel_measurable M ⟹ F f ∈ borel_measurable M" shows "gfp F ∈ borel_measurable M" proof - { fix i have "((F ^^ i) top) ∈ borel_measurable M" by (induct i) (auto intro!: * simp: bot_fun_def) } then have "(λx. INF i. (F ^^ i) top x) ∈ borel_measurable M" by measurable also have "(λx. INF i. (F ^^ i) top x) = (INF i. (F ^^ i) top)" by auto also have "… = gfp F" by (rule inf_continuous_gfp[symmetric]) fact finally show ?thesis . qed lemma borel_measurable_max[measurable (raw)]: "f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ (λx. max (g x) (f x) :: 'b::{second_countable_topology, linorder_topology}) ∈ borel_measurable M" by (rule borel_measurableI_less) simp lemma borel_measurable_min[measurable (raw)]: "f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ (λx. min (g x) (f x) :: 'b::{second_countable_topology, linorder_topology}) ∈ borel_measurable M" by (rule borel_measurableI_greater) simp lemma borel_measurable_Min[measurable (raw)]: "finite I ⟹ (⋀i. i ∈ I ⟹ f i ∈ borel_measurable M) ⟹ (λx. Min ((λi. f i x)`I) :: 'b::{second_countable_topology, linorder_topology}) ∈ borel_measurable M" proof (induct I rule: finite_induct) case (insert i I) then show ?case by (cases "I = {}") auto qed auto lemma borel_measurable_Max[measurable (raw)]: "finite I ⟹ (⋀i. i ∈ I ⟹ f i ∈ borel_measurable M) ⟹ (λx. Max ((λi. f i x)`I) :: 'b::{second_countable_topology, linorder_topology}) ∈ borel_measurable M" proof (induct I rule: finite_induct) case (insert i I) then show ?case by (cases "I = {}") auto qed auto lemma borel_measurable_sup[measurable (raw)]: "f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ (λx. sup (g x) (f x) :: 'b::{lattice, second_countable_topology, linorder_topology}) ∈ borel_measurable M" unfolding sup_max by measurable lemma borel_measurable_inf[measurable (raw)]: "f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ (λx. inf (g x) (f x) :: 'b::{lattice, second_countable_topology, linorder_topology}) ∈ borel_measurable M" unfolding inf_min by measurable lemma [measurable (raw)]: fixes f :: "nat ⇒ 'a ⇒ 'b::{complete_linorder, second_countable_topology, linorder_topology}" assumes "⋀i. f i ∈ borel_measurable M" shows borel_measurable_liminf: "(λx. liminf (λi. f i x)) ∈ borel_measurable M" and borel_measurable_limsup: "(λx. limsup (λi. f i x)) ∈ borel_measurable M" unfolding liminf_SUP_INF limsup_INF_SUP using assms by auto lemma measurable_convergent[measurable (raw)]: fixes f :: "nat ⇒ 'a ⇒ 'b::{complete_linorder, second_countable_topology, linorder_topology}" assumes [measurable]: "⋀i. f i ∈ borel_measurable M" shows "Measurable.pred M (λx. convergent (λi. f i x))" unfolding convergent_ereal by measurable lemma sets_Collect_convergent[measurable]: fixes f :: "nat ⇒ 'a ⇒ 'b::{complete_linorder, second_countable_topology, linorder_topology}" assumes f[measurable]: "⋀i. f i ∈ borel_measurable M" shows "{x∈space M. convergent (λi. f i x)} ∈ sets M" by measurable lemma borel_measurable_lim[measurable (raw)]: fixes f :: "nat ⇒ 'a ⇒ 'b::{complete_linorder, second_countable_topology, linorder_topology}" assumes [measurable]: "⋀i. f i ∈ borel_measurable M" shows "(λx. lim (λi. f i x)) ∈ borel_measurable M" proof - have "⋀x. lim (λi. f i x) = (if convergent (λi. f i x) then limsup (λi. f i x) else (THE i. False))" by (simp add: lim_def convergent_def convergent_limsup_cl) then show ?thesis by simp qed lemma borel_measurable_LIMSEQ_order: fixes u :: "nat ⇒ 'a ⇒ 'b::{complete_linorder, second_countable_topology, linorder_topology}" assumes u': "⋀x. x ∈ space M ⟹ (λi. u i x) ⇢ u' x" and u: "⋀i. u i ∈ borel_measurable M" shows "u' ∈ borel_measurable M" proof - have "⋀x. x ∈ space M ⟹ u' x = liminf (λn. u n x)" using u' by (simp add: lim_imp_Liminf[symmetric]) with u show ?thesis by (simp cong: measurable_cong) qed subsection ‹Borel spaces on topological monoids› lemma borel_measurable_add[measurable (raw)]: fixes f g :: "'a ⇒ 'b::{second_countable_topology, topological_monoid_add}" assumes f: "f ∈ borel_measurable M" assumes g: "g ∈ borel_measurable M" shows "(λx. f x + g x) ∈ borel_measurable M" using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) lemma borel_measurable_sum[measurable (raw)]: fixes f :: "'c ⇒ 'a ⇒ 'b::{second_countable_topology, topological_comm_monoid_add}" assumes "⋀i. i ∈ S ⟹ f i ∈ borel_measurable M" shows "(λx. ∑i∈S. f i x) ∈ borel_measurable M" proof cases assume "finite S" thus ?thesis using assms by induct auto qed simp lemma borel_measurable_suminf_order[measurable (raw)]: fixes f :: "nat ⇒ 'a ⇒ 'b::{complete_linorder, second_countable_topology, linorder_topology, topological_comm_monoid_add}" assumes f[measurable]: "⋀i. f i ∈ borel_measurable M" shows "(λx. suminf (λi. f i x)) ∈ borel_measurable M" unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp subsection ‹Borel spaces on Euclidean spaces› lemma borel_measurable_inner[measurable (raw)]: fixes f g :: "'a ⇒ 'b::{second_countable_topology, real_inner}" assumes "f ∈ borel_measurable M" assumes "g ∈ borel_measurable M" shows "(λx. f x ∙ g x) ∈ borel_measurable M" using assms by (rule borel_measurable_continuous_Pair) (intro continuous_intros) notation eucl_less (infix "<e" 50) lemma box_oc: "{x. a <e x ∧ x ≤ b} = {x. a <e x} ∩ {..b}" and box_co: "{x. a ≤ x ∧ x <e b} = {a..} ∩ {x. x <e b}" by auto lemma eucl_ivals[measurable]: fixes a b :: "'a::ordered_euclidean_space" shows "{x. x <e a} ∈ sets borel" and "{x. a <e x} ∈ sets borel" and "{..a} ∈ sets borel" and "{a..} ∈ sets borel" and "{a..b} ∈ sets borel" and "{x. a <e x ∧ x ≤ b} ∈ sets borel" and "{x. a ≤ x ∧ x <e b} ∈ sets borel" unfolding box_oc box_co by (auto intro: borel_open borel_closed) lemma fixes i :: "'a::{second_countable_topology, real_inner}" shows hafspace_less_borel: "{x. a < x ∙ i} ∈ sets borel" and hafspace_greater_borel: "{x. x ∙ i < a} ∈ sets borel" and hafspace_less_eq_borel: "{x. a ≤ x ∙ i} ∈ sets borel" and hafspace_greater_eq_borel: "{x. x ∙ i ≤ a} ∈ sets borel" by simp_all lemma borel_eq_box: "borel = sigma UNIV (range (λ (a, b). box a b :: 'a :: euclidean_space set))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI1[OF borel_def]) fix M :: "'a set" assume "M ∈ {S. open S}" then have "open M" by simp show "M ∈ ?SIGMA" apply (subst open_UNION_box[OF ‹open M›]) apply (safe intro!: sets.countable_UN' countable_PiE countable_Collect) apply (auto intro: countable_rat) done qed (auto simp: box_def) lemma halfspace_gt_in_halfspace: assumes i: "i ∈ A" shows "{x::'a. a < x ∙ i} ∈ sigma_sets UNIV ((λ (a, i). {x::'a::euclidean_space. x ∙ i < a}) ` (UNIV × A))" (is "?set ∈ ?SIGMA") proof - interpret sigma_algebra UNIV ?SIGMA by (intro sigma_algebra_sigma_sets) simp_all have *: "?set = (⋃n. UNIV - {x::'a. x ∙ i < a + 1 / real (Suc n)})" proof (safe, simp_all add: not_less del: of_nat_Suc) fix x :: 'a assume "a < x ∙ i" with reals_Archimedean[of "x ∙ i - a"] obtain n where "a + 1 / real (Suc n) < x ∙ i" by (auto simp: field_simps) then show "∃n. a + 1 / real (Suc n) ≤ x ∙ i" by (blast intro: less_imp_le) next fix x n have "a < a + 1 / real (Suc n)" by auto also assume "… ≤ x" finally show "a < x" . qed show "?set ∈ ?SIGMA" unfolding * by (auto intro!: Diff sigma_sets_Inter i) qed lemma borel_eq_halfspace_less: "borel = sigma UNIV ((λ(a, i). {x::'a::euclidean_space. x ∙ i < a}) ` (UNIV × Basis))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI2[OF borel_eq_box]) fix a b :: 'a have "box a b = {x∈space ?SIGMA. ∀i∈Basis. a ∙ i < x ∙ i ∧ x ∙ i < b ∙ i}" by (auto simp: box_def) also have "… ∈ sets ?SIGMA" by (intro sets.sets_Collect_conj sets.sets_Collect_finite_All sets.sets_Collect_const) (auto intro!: halfspace_gt_in_halfspace countable_PiE countable_rat) finally show "box a b ∈ sets ?SIGMA" . qed auto lemma borel_eq_halfspace_le: "borel = sigma UNIV ((λ (a, i). {x::'a::euclidean_space. x ∙ i ≤ a}) ` (UNIV × Basis))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less]) fix a :: real and i :: 'a assume "(a, i) ∈ UNIV × Basis" then have i: "i ∈ Basis" by auto have *: "{x::'a. x∙i < a} = (⋃n. {x. x∙i ≤ a - 1/real (Suc n)})" proof (safe, simp_all del: of_nat_Suc) fix x::'a assume *: "x∙i < a" with reals_Archimedean[of "a - x∙i"] obtain n where "x ∙ i < a - 1 / (real (Suc n))" by (auto simp: field_simps) then show "∃n. x ∙ i ≤ a - 1 / (real (Suc n))" by (blast intro: less_imp_le) next fix x::'a and n assume "x∙i ≤ a - 1 / real (Suc n)" also have "… < a" by auto finally show "x∙i < a" . qed show "{x. x∙i < a} ∈ ?SIGMA" unfolding * by (intro sets.countable_UN) (auto intro: i) qed auto lemma borel_eq_halfspace_ge: "borel = sigma UNIV ((λ (a, i). {x::'a::euclidean_space. a ≤ x ∙ i}) ` (UNIV × Basis))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less]) fix a :: real and i :: 'a assume i: "(a, i) ∈ UNIV × Basis" have *: "{x::'a. x∙i < a} = space ?SIGMA - {x::'a. a ≤ x∙i}" by auto show "{x. x∙i < a} ∈ ?SIGMA" unfolding * using i by (intro sets.compl_sets) auto qed auto lemma borel_eq_halfspace_greater: "borel = sigma UNIV ((λ (a, i). {x::'a::euclidean_space. a < x ∙ i}) ` (UNIV × Basis))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_le]) fix a :: real and i :: 'a assume "(a, i) ∈ (UNIV × Basis)" then have i: "i ∈ Basis" by auto have *: "{x::'a. x∙i ≤ a} = space ?SIGMA - {x::'a. a < x∙i}" by auto show "{x. x∙i ≤ a} ∈ ?SIGMA" unfolding * by (intro sets.compl_sets) (auto intro: i) qed auto lemma borel_eq_atMost: "borel = sigma UNIV (range (λa. {..a::'a::ordered_euclidean_space}))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le]) fix a :: real and i :: 'a assume "(a, i) ∈ UNIV × Basis" then have "i ∈ Basis" by auto then have *: "{x::'a. x∙i ≤ a} = (⋃k::nat. {.. (∑n∈Basis. (if n = i then a else real k)*⇩_{R}n)})" proof (safe, simp_all add: eucl_le[where 'a='a] split: if_split_asm) fix x :: 'a from real_arch_simple[of "Max ((λi. x∙i)`Basis)"] guess k::nat .. then have "⋀i. i ∈ Basis ⟹ x∙i ≤ real k" by (subst (asm) Max_le_iff) auto then show "∃k::nat. ∀ia∈Basis. ia ≠ i ⟶ x ∙ ia ≤ real k" by (auto intro!: exI[of _ k]) qed show "{x. x∙i ≤ a} ∈ ?SIGMA" unfolding * by (intro sets.countable_UN) auto qed auto lemma borel_eq_greaterThan: "borel = sigma UNIV (range (λa::'a::ordered_euclidean_space. {x. a <e x}))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le]) fix a :: real and i :: 'a assume "(a, i) ∈ UNIV × Basis" then have i: "i ∈ Basis" by auto have "{x::'a. x∙i ≤ a} = UNIV - {x::'a. a < x∙i}" by auto also have *: "{x::'a. a < x∙i} = (⋃k::nat. {x. (∑n∈Basis. (if n = i then a else -real k) *⇩_{R}n) <e x})" using i proof (safe, simp_all add: eucl_less_def split: if_split_asm) fix x :: 'a from reals_Archimedean2[of "Max ((λi. -x∙i)`Basis)"] guess k::nat .. note k = this { fix i :: 'a assume "i ∈ Basis" then have "-x∙i < real k" using k by (subst (asm) Max_less_iff) auto then have "- real k < x∙i" by simp } then show "∃k::nat. ∀ia∈Basis. ia ≠ i ⟶ -real k < x ∙ ia" by (auto intro!: exI[of _ k]) qed finally show "{x. x∙i ≤ a} ∈ ?SIGMA" apply (simp only:) apply (intro sets.countable_UN sets.Diff) apply (auto intro: sigma_sets_top) done qed auto lemma borel_eq_lessThan: "borel = sigma UNIV (range (λa::'a::ordered_euclidean_space. {x. x <e a}))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_ge]) fix a :: real and i :: 'a assume "(a, i) ∈ UNIV × Basis" then have i: "i ∈ Basis" by auto have "{x::'a. a ≤ x∙i} = UNIV - {x::'a. x∙i < a}" by auto also have *: "{x::'a. x∙i < a} = (⋃k::nat. {x. x <e (∑n∈Basis. (if n = i then a else real k) *⇩_{R}n)})" using ‹i∈ Basis› proof (safe, simp_all add: eucl_less_def split: if_split_asm) fix x :: 'a from reals_Archimedean2[of "Max ((λi. x∙i)`Basis)"] guess k::nat .. note k = this { fix i :: 'a assume "i ∈ Basis" then have "x∙i < real k" using k by (subst (asm) Max_less_iff) auto then have "x∙i < real k" by simp } then show "∃k::nat. ∀ia∈Basis. ia ≠ i ⟶ x ∙ ia < real k" by (auto intro!: exI[of _ k]) qed finally show "{x. a ≤ x∙i} ∈ ?SIGMA" apply (simp only:) apply (intro sets.countable_UN sets.Diff) apply (auto intro: sigma_sets_top ) done qed auto lemma borel_eq_atLeastAtMost: "borel = sigma UNIV (range (λ(a,b). {a..b} ::'a::ordered_euclidean_space set))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI5[OF borel_eq_atMost]) fix a::'a have *: "{..a} = (⋃n::nat. {- real n *⇩_{R}One .. a})" proof (safe, simp_all add: eucl_le[where 'a='a]) fix x :: 'a from real_arch_simple[of "Max ((λi. - x∙i)`Basis)"] guess k::nat .. note k = this { fix i :: 'a assume "i ∈ Basis" with k have "- x∙i ≤ real k" by (subst (asm) Max_le_iff) (auto simp: field_simps) then have "- real k ≤ x∙i" by simp } then show "∃n::nat. ∀i∈Basis. - real n ≤ x ∙ i" by (auto intro!: exI[of _ k]) qed show "{..a} ∈ ?SIGMA" unfolding * by (intro sets.countable_UN) (auto intro!: sigma_sets_top) qed auto lemma borel_set_induct[consumes 1, case_names empty interval compl union]: assumes "A ∈ sets borel" assumes empty: "P {}" and int: "⋀a b. a ≤ b ⟹ P {a..b}" and compl: "⋀A. A ∈ sets borel ⟹ P A ⟹ P (-A)" and un: "⋀f. disjoint_family f ⟹ (⋀i. f i ∈ sets borel) ⟹ (⋀i. P (f i)) ⟹ P (⋃i::nat. f i)" shows "P (A::real set)" proof- let ?G = "range (λ(a,b). {a..b::real})" have "Int_stable ?G" "?G ⊆ Pow UNIV" "A ∈ sigma_sets UNIV ?G" using assms(1) by (auto simp add: borel_eq_atLeastAtMost Int_stable_def) thus ?thesis proof (induction rule: sigma_sets_induct_disjoint) case (union f) from union.hyps(2) have "⋀i. f i ∈ sets borel" by (auto simp: borel_eq_atLeastAtMost) with union show ?case by (auto intro: un) next case (basic A) then obtain a b where "A = {a .. b}" by auto then show ?case by (cases "a ≤ b") (auto intro: int empty) qed (auto intro: empty compl simp: Compl_eq_Diff_UNIV[symmetric] borel_eq_atLeastAtMost) qed lemma borel_sigma_sets_Ioc: "borel = sigma UNIV (range (λ(a, b). {a <.. b::real}))" proof (rule borel_eq_sigmaI5[OF borel_eq_atMost]) fix i :: real have "{..i} = (⋃j::nat. {-j <.. i})" by (auto simp: minus_less_iff reals_Archimedean2) also have "… ∈ sets (sigma UNIV (range (λ(i, j). {i<..j})))" by (intro sets.countable_nat_UN) auto finally show "{..i} ∈ sets (sigma UNIV (range (λ(i, j). {i<..j})))" . qed simp lemma eucl_lessThan: "{x::real. x <e a} = lessThan a" by (simp add: eucl_less_def lessThan_def) lemma borel_eq_atLeastLessThan: "borel = sigma UNIV (range (λ(a, b). {a ..< b :: real}))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI5[OF borel_eq_lessThan]) have move_uminus: "⋀x y::real. -x ≤ y ⟷ -y ≤ x" by auto fix x :: real have "{..<x} = (⋃i::nat. {-real i ..< x})" by (auto simp: move_uminus real_arch_simple) then show "{y. y <e x} ∈ ?SIGMA" by (auto intro: sigma_sets.intros(2-) simp: eucl_lessThan) qed auto lemma borel_measurable_halfspacesI: fixes f :: "'a ⇒ 'c::euclidean_space" assumes F: "borel = sigma UNIV (F ` (UNIV × Basis))" and S_eq: "⋀a i. S a i = f -` F (a,i) ∩ space M" shows "f ∈ borel_measurable M = (∀i∈Basis. ∀a::real. S a i ∈ sets M)" proof safe fix a :: real and i :: 'b assume i: "i ∈ Basis" and f: "f ∈ borel_measurable M" then show "S a i ∈ sets M" unfolding assms by (auto intro!: measurable_sets simp: assms(1)) next assume a: "∀i∈Basis. ∀a. S a i ∈ sets M" then show "f ∈ borel_measurable M" by (auto intro!: measurable_measure_of simp: S_eq F) qed lemma borel_measurable_iff_halfspace_le: fixes f :: "'a ⇒ 'c::euclidean_space" shows "f ∈ borel_measurable M = (∀i∈Basis. ∀a. {w ∈ space M. f w ∙ i ≤ a} ∈ sets M)" by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_le]) auto lemma borel_measurable_iff_halfspace_less: fixes f :: "'a ⇒ 'c::euclidean_space" shows "f ∈ borel_measurable M ⟷ (∀i∈Basis. ∀a. {w ∈ space M. f w ∙ i < a} ∈ sets M)" by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_less]) auto lemma borel_measurable_iff_halfspace_ge: fixes f :: "'a ⇒ 'c::euclidean_space" shows "f ∈ borel_measurable M = (∀i∈Basis. ∀a. {w ∈ space M. a ≤ f w ∙ i} ∈ sets M)" by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_ge]) auto lemma borel_measurable_iff_halfspace_greater: fixes f :: "'a ⇒ 'c::euclidean_space" shows "f ∈ borel_measurable M ⟷ (∀i∈Basis. ∀a. {w ∈ space M. a < f w ∙ i} ∈ sets M)" by (rule borel_measurable_halfspacesI[OF borel_eq_halfspace_greater]) auto lemma borel_measurable_iff_le: "(f::'a ⇒ real) ∈ borel_measurable M = (∀a. {w ∈ space M. f w ≤ a} ∈ sets M)" using borel_measurable_iff_halfspace_le[where 'c=real] by simp lemma borel_measurable_iff_less: "(f::'a ⇒ real) ∈ borel_measurable M = (∀a. {w ∈ space M. f w < a} ∈ sets M)" using borel_measurable_iff_halfspace_less[where 'c=real] by simp lemma borel_measurable_iff_ge: "(f::'a ⇒ real) ∈ borel_measurable M = (∀a. {w ∈ space M. a ≤ f w} ∈ sets M)" using borel_measurable_iff_halfspace_ge[where 'c=real] by simp lemma borel_measurable_iff_greater: "(f::'a ⇒ real) ∈ borel_measurable M = (∀a. {w ∈ space M. a < f w} ∈ sets M)" using borel_measurable_iff_halfspace_greater[where 'c=real] by simp lemma borel_measurable_euclidean_space: fixes f :: "'a ⇒ 'c::euclidean_space" shows "f ∈ borel_measurable M ⟷ (∀i∈Basis. (λx. f x ∙ i) ∈ borel_measurable M)" proof safe assume f: "∀i∈Basis. (λx. f x ∙ i) ∈ borel_measurable M" then show "f ∈ borel_measurable M" by (subst borel_measurable_iff_halfspace_le) auto qed auto subsection "Borel measurable operators" lemma borel_measurable_norm[measurable]: "norm ∈ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_intros) lemma borel_measurable_sgn [measurable]: "(sgn::'a::real_normed_vector ⇒ 'a) ∈ borel_measurable borel" by (rule borel_measurable_continuous_countable_exceptions[where X="{0}"]) (auto intro!: continuous_on_sgn continuous_on_id) lemma borel_measurable_uminus[measurable (raw)]: fixes g :: "'a ⇒ 'b::{second_countable_topology, real_normed_vector}" assumes g: "g ∈ borel_measurable M" shows "(λx. - g x) ∈ borel_measurable M" by (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_intros) lemma borel_measurable_diff[measurable (raw)]: fixes f :: "'a ⇒ 'b::{second_countable_topology, real_normed_vector}" assumes f: "f ∈ borel_measurable M" assumes g: "g ∈ borel_measurable M" shows "(λx. f x - g x) ∈ borel_measurable M" using borel_measurable_add [of f M "- g"] assms by (simp add: fun_Compl_def) lemma borel_measurable_times[measurable (raw)]: fixes f :: "'a ⇒ 'b::{second_countable_topology, real_normed_algebra}" assumes f: "f ∈ borel_measurable M" assumes g: "g ∈ borel_measurable M" shows "(λx. f x * g x) ∈ borel_measurable M" using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) lemma borel_measurable_prod[measurable (raw)]: fixes f :: "'c ⇒ 'a ⇒ 'b::{second_countable_topology, real_normed_field}" assumes "⋀i. i ∈ S ⟹ f i ∈ borel_measurable M" shows "(λx. ∏i∈S. f i x) ∈ borel_measurable M" proof cases assume "finite S" thus ?thesis using assms by induct auto qed simp lemma borel_measurable_dist[measurable (raw)]: fixes g f :: "'a ⇒ 'b::{second_countable_topology, metric_space}" assumes f: "f ∈ borel_measurable M" assumes g: "g ∈ borel_measurable M" shows "(λx. dist (f x) (g x)) ∈ borel_measurable M" using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) lemma borel_measurable_scaleR[measurable (raw)]: fixes g :: "'a ⇒ 'b::{second_countable_topology, real_normed_vector}" assumes f: "f ∈ borel_measurable M" assumes g: "g ∈ borel_measurable M" shows "(λx. f x *⇩_{R}g x) ∈ borel_measurable M" using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros) lemma borel_measurable_uminus_eq [simp]: fixes f :: "'a ⇒ 'b::{second_countable_topology, real_normed_vector}" shows "(λx. - f x) ∈ borel_measurable M ⟷ f ∈ borel_measurable M" (is "?l = ?r") proof assume ?l from borel_measurable_uminus[OF this] show ?r by simp qed auto lemma affine_borel_measurable_vector: fixes f :: "'a ⇒ 'x::real_normed_vector" assumes "f ∈ borel_measurable M" shows "(λx. a + b *⇩_{R}f x) ∈ borel_measurable M" proof (rule borel_measurableI) fix S :: "'x set" assume "open S" show "(λx. a + b *⇩_{R}f x) -` S ∩ space M ∈ sets M" proof cases assume "b ≠ 0" with ‹open S› have "open ((λx. (- a + x) /⇩_{R}b) ` S)" (is "open ?S") using open_affinity [of S "inverse b" "- a /⇩_{R}b"] by (auto simp: algebra_simps) hence "?S ∈ sets borel" by auto moreover from ‹b ≠ 0› have "(λx. a + b *⇩_{R}f x) -` S = f -` ?S" apply auto by (rule_tac x="a + b *⇩_{R}f x" in image_eqI, simp_all) ultimately show ?thesis using assms unfolding in_borel_measurable_borel by auto qed simp qed lemma borel_measurable_const_scaleR[measurable (raw)]: "f ∈ borel_measurable M ⟹ (λx. b *⇩_{R}f x ::'a::real_normed_vector) ∈ borel_measurable M" using affine_borel_measurable_vector[of f M 0 b] by simp lemma borel_measurable_const_add[measurable (raw)]: "f ∈ borel_measurable M ⟹ (λx. a + f x ::'a::real_normed_vector) ∈ borel_measurable M" using affine_borel_measurable_vector[of f M a 1] by simp lemma borel_measurable_inverse[measurable (raw)]: fixes f :: "'a ⇒ 'b::real_normed_div_algebra" assumes f: "f ∈ borel_measurable M" shows "(λx. inverse (f x)) ∈ borel_measurable M" apply (rule measurable_compose[OF f]) apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"]) apply (auto intro!: continuous_on_inverse continuous_on_id) done lemma borel_measurable_divide[measurable (raw)]: "f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ (λx. f x / g x::'b::{second_countable_topology, real_normed_div_algebra}) ∈ borel_measurable M" by (simp add: divide_inverse) lemma borel_measurable_abs[measurable (raw)]: "f ∈ borel_measurable M ⟹ (λx. ¦f x :: real¦) ∈ borel_measurable M" unfolding abs_real_def by simp lemma borel_measurable_nth[measurable (raw)]: "(λx::real^'n. x $ i) ∈ borel_measurable borel" by (simp add: cart_eq_inner_axis) lemma convex_measurable: fixes A :: "'a :: euclidean_space set" shows "X ∈ borel_measurable M ⟹ X ` space M ⊆ A ⟹ open A ⟹ convex_on A q ⟹ (λx. q (X x)) ∈ borel_measurable M" by (rule measurable_compose[where f=X and N="restrict_space borel A"]) (auto intro!: borel_measurable_continuous_on_restrict convex_on_continuous measurable_restrict_space2) lemma borel_measurable_ln[measurable (raw)]: assumes f: "f ∈ borel_measurable M" shows "(λx. ln (f x :: real)) ∈ borel_measurable M" apply (rule measurable_compose[OF f]) apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"]) apply (auto intro!: continuous_on_ln continuous_on_id) done lemma borel_measurable_log[measurable (raw)]: "f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ (λx. log (g x) (f x)) ∈ borel_measurable M" unfolding log_def by auto lemma borel_measurable_exp[measurable]: "(exp::'a::{real_normed_field,banach}⇒'a) ∈ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_exp) lemma measurable_real_floor[measurable]: "(floor :: real ⇒ int) ∈ measurable borel (count_space UNIV)" proof - have "⋀a x. ⌊x⌋ = a ⟷ (real_of_int a ≤ x ∧ x < real_of_int (a + 1))" by (auto intro: floor_eq2) then show ?thesis by (auto simp: vimage_def measurable_count_space_eq2_countable) qed lemma measurable_real_ceiling[measurable]: "(ceiling :: real ⇒ int) ∈ measurable borel (count_space UNIV)" unfolding ceiling_def[abs_def] by simp lemma borel_measurable_real_floor: "(λx::real. real_of_int ⌊x⌋) ∈ borel_measurable borel" by simp lemma borel_measurable_root [measurable]: "root n ∈ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_intros) lemma borel_measurable_sqrt [measurable]: "sqrt ∈ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_intros) lemma borel_measurable_power [measurable (raw)]: fixes f :: "_ ⇒ 'b::{power,real_normed_algebra}" assumes f: "f ∈ borel_measurable M" shows "(λx. (f x) ^ n) ∈ borel_measurable M" by (intro borel_measurable_continuous_on [OF _ f] continuous_intros) lemma borel_measurable_Re [measurable]: "Re ∈ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_intros) lemma borel_measurable_Im [measurable]: "Im ∈ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_intros) lemma borel_measurable_of_real [measurable]: "(of_real :: _ ⇒ (_::real_normed_algebra)) ∈ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_intros) lemma borel_measurable_sin [measurable]: "(sin :: _ ⇒ (_::{real_normed_field,banach})) ∈ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_intros) lemma borel_measurable_cos [measurable]: "(cos :: _ ⇒ (_::{real_normed_field,banach})) ∈ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_intros) lemma borel_measurable_arctan [measurable]: "arctan ∈ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_intros) lemma borel_measurable_complex_iff: "f ∈ borel_measurable M ⟷ (λx. Re (f x)) ∈ borel_measurable M ∧ (λx. Im (f x)) ∈ borel_measurable M" apply auto apply (subst fun_complex_eq) apply (intro borel_measurable_add) apply auto done lemma powr_real_measurable [measurable]: assumes "f ∈ measurable M borel" "g ∈ measurable M borel" shows "(λx. f x powr g x :: real) ∈ measurable M borel" using assms by (simp_all add: powr_def) lemma measurable_of_bool[measurable]: "of_bool ∈ count_space UNIV →⇩_{M}borel" by simp subsection "Borel space on the extended reals" lemma borel_measurable_ereal[measurable (raw)]: assumes f: "f ∈ borel_measurable M" shows "(λx. ereal (f x)) ∈ borel_measurable M" using continuous_on_ereal f by (rule borel_measurable_continuous_on) (rule continuous_on_id) lemma borel_measurable_real_of_ereal[measurable (raw)]: fixes f :: "'a ⇒ ereal" assumes f: "f ∈ borel_measurable M" shows "(λx. real_of_ereal (f x)) ∈ borel_measurable M" apply (rule measurable_compose[OF f]) apply (rule borel_measurable_continuous_countable_exceptions[of "{∞, -∞ }"]) apply (auto intro: continuous_on_real simp: Compl_eq_Diff_UNIV) done lemma borel_measurable_ereal_cases: fixes f :: "'a ⇒ ereal" assumes f: "f ∈ borel_measurable M" assumes H: "(λx. H (ereal (real_of_ereal (f x)))) ∈ borel_measurable M" shows "(λx. H (f x)) ∈ borel_measurable M" proof - let ?F = "λx. if f x = ∞ then H ∞ else if f x = - ∞ then H (-∞) else H (ereal (real_of_ereal (f x)))" { fix x have "H (f x) = ?F x" by (cases "f x") auto } with f H show ?thesis by simp qed lemma fixes f :: "'a ⇒ ereal" assumes f[measurable]: "f ∈ borel_measurable M" shows borel_measurable_ereal_abs[measurable(raw)]: "(λx. ¦f x¦) ∈ borel_measurable M" and borel_measurable_ereal_inverse[measurable(raw)]: "(λx. inverse (f x) :: ereal) ∈ borel_measurable M" and borel_measurable_uminus_ereal[measurable(raw)]: "(λx. - f x :: ereal) ∈ borel_measurable M" by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If) lemma borel_measurable_uminus_eq_ereal[simp]: "(λx. - f x :: ereal) ∈ borel_measurable M ⟷ f ∈ borel_measurable M" (is "?l = ?r") proof assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp qed auto lemma set_Collect_ereal2: fixes f g :: "'a ⇒ ereal" assumes f: "f ∈ borel_measurable M" assumes g: "g ∈ borel_measurable M" assumes H: "{x ∈ space M. H (ereal (real_of_ereal (f x))) (ereal (real_of_ereal (g x)))} ∈ sets M" "{x ∈ space borel. H (-∞) (ereal x)} ∈ sets borel" "{x ∈ space borel. H (∞) (ereal x)} ∈ sets borel" "{x ∈ space borel. H (ereal x) (-∞)} ∈ sets borel" "{x ∈ space borel. H (ereal x) (∞)} ∈ sets borel" shows "{x ∈ space M. H (f x) (g x)} ∈ sets M" proof - let ?G = "λy x. if g x = ∞ then H y ∞ else if g x = -∞ then H y (-∞) else H y (ereal (real_of_ereal (g x)))" let ?F = "λx. if f x = ∞ then ?G ∞ x else if f x = -∞ then ?G (-∞) x else ?G (ereal (real_of_ereal (f x))) x" { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto } note * = this from assms show ?thesis by (subst *) (simp del: space_borel split del: if_split) qed lemma borel_measurable_ereal_iff: shows "(λx. ereal (f x)) ∈ borel_measurable M ⟷ f ∈ borel_measurable M" proof assume "(λx. ereal (f x)) ∈ borel_measurable M" from borel_measurable_real_of_ereal[OF this] show "f ∈ borel_measurable M" by auto qed auto lemma borel_measurable_erealD[measurable_dest]: "(λx. ereal (f x)) ∈ borel_measurable M ⟹ g ∈ measurable N M ⟹ (λx. f (g x)) ∈ borel_measurable N" unfolding borel_measurable_ereal_iff by simp lemma borel_measurable_ereal_iff_real: fixes f :: "'a ⇒ ereal" shows "f ∈ borel_measurable M ⟷ ((λx. real_of_ereal (f x)) ∈ borel_measurable M ∧ f -` {∞} ∩ space M ∈ sets M ∧ f -` {-∞} ∩ space M ∈ sets M)" proof safe assume *: "(λx. real_of_ereal (f x)) ∈ borel_measurable M" "f -` {∞} ∩ space M ∈ sets M" "f -` {-∞} ∩ space M ∈ sets M" have "f -` {∞} ∩ space M = {x∈space M. f x = ∞}" "f -` {-∞} ∩ space M = {x∈space M. f x = -∞}" by auto with * have **: "{x∈space M. f x = ∞} ∈ sets M" "{x∈space M. f x = -∞} ∈ sets M" by simp_all let ?f = "λx. if f x = ∞ then ∞ else if f x = -∞ then -∞ else ereal (real_of_ereal (f x))" have "?f ∈ borel_measurable M" using * ** by (intro measurable_If) auto also have "?f = f" by (auto simp: fun_eq_iff ereal_real) finally show "f ∈ borel_measurable M" . qed simp_all lemma borel_measurable_ereal_iff_Iio: "(f::'a ⇒ ereal) ∈ borel_measurable M ⟷ (∀a. f -` {..< a} ∩ space M ∈ sets M)" by (auto simp: borel_Iio measurable_iff_measure_of) lemma borel_measurable_ereal_iff_Ioi: "(f::'a ⇒ ereal) ∈ borel_measurable M ⟷ (∀a. f -` {a <..} ∩ space M ∈ sets M)" by (auto simp: borel_Ioi measurable_iff_measure_of) lemma vimage_sets_compl_iff: "f -` A ∩ space M ∈ sets M ⟷ f -` (- A) ∩ space M ∈ sets M" proof - { fix A assume "f -` A ∩ space M ∈ sets M" moreover have "f -` (- A) ∩ space M = space M - f -` A ∩ space M" by auto ultimately have "f -` (- A) ∩ space M ∈ sets M" by auto } from this[of A] this[of "-A"] show ?thesis by (metis double_complement) qed lemma borel_measurable_iff_Iic_ereal: "(f::'a⇒ereal) ∈ borel_measurable M ⟷ (∀a. f -` {..a} ∩ space M ∈ sets M)" unfolding borel_measurable_ereal_iff_Ioi vimage_sets_compl_iff[where A="{a <..}" for a] by simp lemma borel_measurable_iff_Ici_ereal: "(f::'a ⇒ ereal) ∈ borel_measurable M ⟷ (∀a. f -` {a..} ∩ space M ∈ sets M)" unfolding borel_measurable_ereal_iff_Iio vimage_sets_compl_iff[where A="{..< a}" for a] by simp lemma borel_measurable_ereal2: fixes f g :: "'a ⇒ ereal" assumes f: "f ∈ borel_measurable M" assumes g: "g ∈ borel_measurable M" assumes H: "(λx. H (ereal (real_of_ereal (f x))) (ereal (real_of_ereal (g x)))) ∈ borel_measurable M" "(λx. H (-∞) (ereal (real_of_ereal (g x)))) ∈ borel_measurable M" "(λx. H (∞) (ereal (real_of_ereal (g x)))) ∈ borel_measurable M" "(λx. H (ereal (real_of_ereal (f x))) (-∞)) ∈ borel_measurable M" "(λx. H (ereal (real_of_ereal (f x))) (∞)) ∈ borel_measurable M" shows "(λx. H (f x) (g x)) ∈ borel_measurable M" proof - let ?G = "λy x. if g x = ∞ then H y ∞ else if g x = - ∞ then H y (-∞) else H y (ereal (real_of_ereal (g x)))" let ?F = "λx. if f x = ∞ then ?G ∞ x else if f x = - ∞ then ?G (-∞) x else ?G (ereal (real_of_ereal (f x))) x" { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto } note * = this from assms show ?thesis unfolding * by simp qed lemma [measurable(raw)]: fixes f :: "'a ⇒ ereal" assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M" shows borel_measurable_ereal_add: "(λx. f x + g x) ∈ borel_measurable M" and borel_measurable_ereal_times: "(λx. f x * g x) ∈ borel_measurable M" by (simp_all add: borel_measurable_ereal2) lemma [measurable(raw)]: fixes f g :: "'a ⇒ ereal" assumes "f ∈ borel_measurable M" assumes "g ∈ borel_measurable M" shows borel_measurable_ereal_diff: "(λx. f x - g x) ∈ borel_measurable M" and borel_measurable_ereal_divide: "(λx. f x / g x) ∈ borel_measurable M" using assms by (simp_all add: minus_ereal_def divide_ereal_def) lemma borel_measurable_ereal_sum[measurable (raw)]: fixes f :: "'c ⇒ 'a ⇒ ereal" assumes "⋀i. i ∈ S ⟹ f i ∈ borel_measurable M" shows "(λx. ∑i∈S. f i x) ∈ borel_measurable M" using assms by (induction S rule: infinite_finite_induct) auto lemma borel_measurable_ereal_prod[measurable (raw)]: fixes f :: "'c ⇒ 'a ⇒ ereal" assumes "⋀i. i ∈ S ⟹ f i ∈ borel_measurable M" shows "(λx. ∏i∈S. f i x) ∈ borel_measurable M" using assms by (induction S rule: infinite_finite_induct) auto lemma borel_measurable_extreal_suminf[measurable (raw)]: fixes f :: "nat ⇒ 'a ⇒ ereal" assumes [measurable]: "⋀i. f i ∈ borel_measurable M" shows "(λx. (∑i. f i x)) ∈ borel_measurable M" unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp subsection "Borel space on the extended non-negative reals" text ‹ @{type ennreal} is a topological monoid, so no rules for plus are required, also all order statements are usually done on type classes. › lemma measurable_enn2ereal[measurable]: "enn2ereal ∈ borel →⇩_{M}borel" by (intro borel_measurable_continuous_on1 continuous_on_enn2ereal) lemma measurable_e2ennreal[measurable]: "e2ennreal ∈ borel →⇩_{M}borel" by (intro borel_measurable_continuous_on1 continuous_on_e2ennreal) lemma borel_measurable_enn2real[measurable (raw)]: "f ∈ M →⇩_{M}borel ⟹ (λx. enn2real (f x)) ∈ M →⇩_{M}borel" unfolding enn2real_def[abs_def] by measurable definition [simp]: "is_borel f M ⟷ f ∈ borel_measurable M" lemma is_borel_transfer[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) (=) is_borel is_borel" unfolding is_borel_def[abs_def] proof (safe intro!: rel_funI ext dest!: rel_fun_eq_pcr_ennreal[THEN iffD1]) fix f and M :: "'a measure" show "f ∈ borel_measurable M" if f: "enn2ereal ∘ f ∈ borel_measurable M" using measurable_compose[OF f measurable_e2ennreal] by simp qed simp context includes ennreal.lifting begin lemma measurable_ennreal[measurable]: "ennreal ∈ borel →⇩_{M}borel" unfolding is_borel_def[symmetric] by transfer simp lemma borel_measurable_ennreal_iff[simp]: assumes [simp]: "⋀x. x ∈ space M ⟹ 0 ≤ f x" shows "(λx. ennreal (f x)) ∈ M →⇩_{M}borel ⟷ f ∈ M →⇩_{M}borel" proof safe assume "(λx. ennreal (f x)) ∈ M →⇩_{M}borel" then have "(λx. enn2real (ennreal (f x))) ∈ M →⇩_{M}borel" by measurable then show "f ∈ M →⇩_{M}borel" by (rule measurable_cong[THEN iffD1, rotated]) auto qed measurable lemma borel_measurable_times_ennreal[measurable (raw)]: fixes f g :: "'a ⇒ ennreal" shows "f ∈ M →⇩_{M}borel ⟹ g ∈ M →⇩_{M}borel ⟹ (λx. f x * g x) ∈ M →⇩_{M}borel" unfolding is_borel_def[symmetric] by transfer simp lemma borel_measurable_inverse_ennreal[measurable (raw)]: fixes f :: "'a ⇒ ennreal" shows "f ∈ M →⇩_{M}borel ⟹ (λx. inverse (f x)) ∈ M →⇩_{M}borel" unfolding is_borel_def[symmetric] by transfer simp lemma borel_measurable_divide_ennreal[measurable (raw)]: fixes f :: "'a ⇒ ennreal" shows "f ∈ M →⇩_{M}borel ⟹ g ∈ M →⇩_{M}borel ⟹ (λx. f x / g x) ∈ M →⇩_{M}borel" unfolding divide_ennreal_def by simp lemma borel_measurable_minus_ennreal[measurable (raw)]: fixes f :: "'a ⇒ ennreal" shows "f ∈ M →⇩_{M}borel ⟹ g ∈ M →⇩_{M}borel ⟹ (λx. f x - g x) ∈ M →⇩_{M}borel" unfolding is_borel_def[symmetric] by transfer simp lemma borel_measurable_prod_ennreal[measurable (raw)]: fixes f :: "'c ⇒ 'a ⇒ ennreal" assumes "⋀i. i ∈ S ⟹ f i ∈ borel_measurable M" shows "(λx. ∏i∈S. f i x) ∈ borel_measurable M" using assms by (induction S rule: infinite_finite_induct) auto end hide_const (open) is_borel subsection ‹LIMSEQ is borel measurable› lemma borel_measurable_LIMSEQ_real: fixes u :: "nat ⇒ 'a ⇒ real" assumes u': "⋀x. x ∈ space M ⟹ (λi. u i x) ⇢ u' x" and u: "⋀i. u i ∈ borel_measurable M" shows "u' ∈ borel_measurable M" proof - have "⋀x. x ∈ space M ⟹ liminf (λn. ereal (u n x)) = ereal (u' x)" using u' by (simp add: lim_imp_Liminf) moreover from u have "(λx. liminf (λn. ereal (u n x))) ∈ borel_measurable M" by auto ultimately show ?thesis by (simp cong: measurable_cong add: borel_measurable_ereal_iff) qed lemma borel_measurable_LIMSEQ_metric: fixes f :: "nat ⇒ 'a ⇒ 'b :: metric_space" assumes [measurable]: "⋀i. f i ∈ borel_measurable M" assumes lim: "⋀x. x ∈ space M ⟹ (λi. f i x) ⇢ g x" shows "g ∈ borel_measurable M" unfolding borel_eq_closed proof (safe intro!: measurable_measure_of) fix A :: "'b set" assume "closed A" have [measurable]: "(λx. infdist (g x) A) ∈ borel_measurable M" proof (rule borel_measurable_LIMSEQ_real) show "⋀x. x ∈ space M ⟹ (λi. infdist (f i x) A) ⇢ infdist (g x) A" by (intro tendsto_infdist lim) show "⋀i. (λx. infdist (f i x) A) ∈ borel_measurable M" by (intro borel_measurable_continuous_on[where f="λx. infdist x A"] continuous_at_imp_continuous_on ballI continuous_infdist continuous_ident) auto qed show "g -` A ∩ space M ∈ sets M" proof cases assume "A ≠ {}" then have "⋀x. infdist x A = 0 ⟷ x ∈ A" using ‹closed A› by (simp add: in_closed_iff_infdist_zero) then have "g -` A ∩ space M = {x∈space M. infdist (g x) A = 0}" by auto also have "… ∈ sets M" by measurable finally show ?thesis . qed simp qed auto lemma sets_Collect_Cauchy[measurable]: fixes f :: "nat ⇒ 'a => 'b::{metric_space, second_countable_topology}" assumes f[measurable]: "⋀i. f i ∈ borel_measurable M" shows "{x∈space M. Cauchy (λi. f i x)} ∈ sets M" unfolding metric_Cauchy_iff2 using f by auto lemma borel_measurable_lim_metric[measurable (raw)]: fixes f :: "nat ⇒ 'a ⇒ 'b::{banach, second_countable_topology}" assumes f[measurable]: "⋀i. f i ∈ borel_measurable M" shows "(λx. lim (λi. f i x)) ∈ borel_measurable M" proof - define u' where "u' x = lim (λi. if Cauchy (λi. f i x) then f i x else 0)" for x then have *: "⋀x. lim (λi. f i x) = (if Cauchy (λi. f i x) then u' x else (THE x. False))" by (auto simp: lim_def convergent_eq_Cauchy[symmetric]) have "u' ∈ borel_measurable M" proof (rule borel_measurable_LIMSEQ_metric) fix x have "convergent (λi. if Cauchy (λi. f i x) then f i x else 0)" by (cases "Cauchy (λi. f i x)") (auto simp add: convergent_eq_Cauchy[symmetric] convergent_def) then show "(λi. if Cauchy (λi. f i x) then f i x else 0) ⇢ u' x" unfolding u'_def by (rule convergent_LIMSEQ_iff[THEN iffD1]) qed measurable then show ?thesis unfolding * by measurable qed lemma borel_measurable_suminf[measurable (raw)]: fixes f :: "nat ⇒ 'a ⇒ 'b::{banach, second_countable_topology}" assumes f[measurable]: "⋀i. f i ∈ borel_measurable M" shows "(λx. suminf (λi. f i x)) ∈ borel_measurable M" unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp lemma Collect_closed_imp_pred_borel: "closed {x. P x} ⟹ Measurable.pred borel P" by (simp add: pred_def) (* Proof by Jeremy Avigad and Luke Serafin *) lemma isCont_borel_pred[measurable]: fixes f :: "'b::metric_space ⇒ 'a::metric_space" shows "Measurable.pred borel (isCont f)" proof (subst measurable_cong) let ?I = "λj. inverse(real (Suc j))" show "isCont f x = (∀i. ∃j. ∀y z. dist x y < ?I j ∧ dist x z < ?I j ⟶ dist (f y) (f z) ≤ ?I i)" for x unfolding continuous_at_eps_delta proof safe fix i assume "∀e>0. ∃d>0. ∀y. dist y x < d ⟶ dist (f y) (f x) < e" moreover have "0 < ?I i / 2" by simp ultimately obtain d where d: "0 < d" "⋀y. dist x y < d ⟹ dist (f y) (f x) < ?I i / 2" by (metis dist_commute) then obtain j where j: "?I j < d" by (metis reals_Archimedean) show "∃j. ∀y z. dist x y < ?I j ∧ dist x z < ?I j ⟶ dist (f y) (f z) ≤ ?I i" proof (safe intro!: exI[where x=j]) fix y z assume *: "dist x y < ?I j" "dist x z < ?I j" have "dist (f y) (f z) ≤ dist (f y) (f x) + dist (f z) (f x)" by (rule dist_triangle2) also have "… < ?I i / 2 + ?I i / 2" by (intro add_strict_mono d less_trans[OF _ j] *) also have "… ≤ ?I i" by (simp add: field_simps of_nat_Suc) finally show "dist (f y) (f z) ≤ ?I i" by simp qed next fix e::real assume "0 < e" then obtain n where n: "?I n < e" by (metis reals_Archimedean) assume "∀i. ∃j. ∀y z. dist x y < ?I j ∧ dist x z < ?I j ⟶ dist (f y) (f z) ≤ ?I i" from this[THEN spec, of "Suc n"] obtain j where j: "⋀y z. dist x y < ?I j ⟹ dist x z < ?I j ⟹ dist (f y) (f z) ≤ ?I (Suc n)" by auto show "∃d>0. ∀y. dist y x < d ⟶ dist (f y) (f x) < e" proof (safe intro!: exI[of _ "?I j"]) fix y assume "dist y x < ?I j" then have "dist (f y) (f x) ≤ ?I (Suc n)" by (intro j) (auto simp: dist_commute) also have "?I (Suc n) < ?I n" by simp also note n finally show "dist (f y) (f x) < e" . qed simp qed qed (intro pred_intros_countable closed_Collect_all closed_Collect_le open_Collect_less Collect_closed_imp_pred_borel closed_Collect_imp open_Collect_conj continuous_intros) lemma isCont_borel: fixes f :: "'b::metric_space ⇒ 'a::metric_space" shows "{x. isCont f x} ∈ sets borel" by simp lemma is_real_interval: assumes S: "is_interval S" shows "∃a b::real. S = {} ∨ S = UNIV ∨ S = {..<b} ∨ S = {..b} ∨ S = {a<..} ∨ S = {a..} ∨ S = {a<..<b} ∨ S = {a<..b} ∨ S = {a..<b} ∨ S = {a..b}" using S unfolding is_interval_1 by (blast intro: interval_cases) lemma real_interval_borel_measurable: assumes "is_interval (S::real set)" shows "S ∈ sets borel" proof - from assms is_real_interval have "∃a b::real. S = {} ∨ S = UNIV ∨ S = {..<b} ∨ S = {..b} ∨ S = {a<..} ∨ S = {a..} ∨ S = {a<..<b} ∨ S = {a<..b} ∨ S = {a..<b} ∨ S = {a..b}" by auto then guess a .. then guess b .. thus ?thesis by auto qed text ‹The next lemmas hold in any second countable linorder (including ennreal or ereal for instance), but in the current state they are restricted to reals.› lemma borel_measurable_mono_on_fnc: fixes f :: "real ⇒ real" and A :: "real set" assumes "mono_on f A" shows "f ∈ borel_measurable (restrict_space borel A)" apply (rule measurable_restrict_countable[OF mono_on_ctble_discont[OF assms]]) apply (auto intro!: image_eqI[where x="{x}" for x] simp: sets_restrict_space) apply (auto simp add: sets_restrict_restrict_space continuous_on_eq_continuous_within cong: measurable_cong_sets intro!: borel_measurable_continuous_on_restrict intro: continuous_within_subset) done lemma borel_measurable_piecewise_mono: fixes f::"real ⇒ real" and C::"real set set" assumes "countable C" "⋀c. c ∈ C ⟹ c ∈ sets borel" "⋀c. c ∈ C ⟹ mono_on f c" "(⋃C) = UNIV" shows "f ∈ borel_measurable borel" by (rule measurable_piecewise_restrict[of C], auto intro: borel_measurable_mono_on_fnc simp: assms) lemma borel_measurable_mono: fixes f :: "real ⇒ real" shows "mono f ⟹ f ∈ borel_measurable borel" using borel_measurable_mono_on_fnc[of f UNIV] by (simp add: mono_def mono_on_def) lemma measurable_bdd_below_real[measurable (raw)]: fixes F :: "'a ⇒ 'i ⇒ real" assumes [simp]: "countable I" and [measurable]: "⋀i. i ∈ I ⟹ F i ∈ M →⇩_{M}borel" shows "Measurable.pred M (λx. bdd_below ((λi. F i x)`I))" proof (subst measurable_cong) show "bdd_below ((λi. F i x)`I) ⟷ (∃q∈ℤ. ∀i∈I. q ≤ F i x)" for x by (auto simp: bdd_below_def intro!: bexI[of _ "of_int (floor _)"] intro: order_trans of_int_floor_le) show "Measurable.pred M (λw. ∃q∈ℤ. ∀i∈I. q ≤ F i w)" using countable_int by measurable qed lemma borel_measurable_cINF_real[measurable (raw)]: fixes F :: "_ ⇒ _ ⇒ real" assumes [simp]: "countable I" assumes F[measurable]: "⋀i. i ∈ I ⟹ F i ∈ borel_measurable M" shows "(λx. INF i:I. F i x) ∈ borel_measurable M" proof (rule measurable_piecewise_restrict) let ?Ω = "{x∈space M. bdd_below ((λi. F i x)`I)}" show "countable {?Ω, - ?Ω}" "space M ⊆ ⋃{?Ω, - ?Ω}" "⋀X. X ∈ {?Ω, - ?Ω} ⟹ X ∩ space M ∈ sets M" by auto fix X assume "X ∈ {?Ω, - ?Ω}" then show "(λx. INF i:I. F i x) ∈ borel_measurable (restrict_space M X)" proof safe show "(λx. INF i:I. F i x) ∈ borel_measurable (restrict_space M ?Ω)" by (intro borel_measurable_cINF measurable_restrict_space1 F) (auto simp: space_restrict_space) show "(λx. INF i:I. F i x) ∈ borel_measurable (restrict_space M (-?Ω))" proof (subst measurable_cong) fix x assume "x ∈ space (restrict_space M (-?Ω))" then have "¬ (∀i∈I. - F i x ≤ y)" for y by (auto simp: space_restrict_space bdd_above_def bdd_above_uminus[symmetric]) then show "(INF i:I. F i x) = - (THE x. False)" by (auto simp: space_restrict_space Inf_real_def Sup_real_def Least_def simp del: Set.ball_simps(10)) qed simp qed qed lemma borel_Ici: "borel = sigma UNIV (range (λx::real. {x ..}))" proof (safe intro!: borel_eq_sigmaI1[OF borel_Iio]) fix x :: real have eq: "{..<x} = space (sigma UNIV (range atLeast)) - {x ..}" by auto show "{..<x} ∈ sets (sigma UNIV (range atLeast))" unfolding eq by (intro sets.compl_sets) auto qed auto lemma borel_measurable_pred_less[measurable (raw)]: fixes f :: "'a ⇒ 'b::{second_countable_topology, linorder_topology}" shows "f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ Measurable.pred M (λw. f w < g w)" unfolding Measurable.pred_def by (rule borel_measurable_less) no_notation eucl_less (infix "<e" 50) lemma borel_measurable_Max2[measurable (raw)]: fixes f::"_ ⇒ _ ⇒ 'a::{second_countable_topology, dense_linorder, linorder_topology}" assumes "finite I" and [measurable]: "⋀i. f i ∈ borel_measurable M" shows "(λx. Max{f i x |i. i ∈ I}) ∈ borel_measurable M" by (simp add: borel_measurable_Max[OF assms(1), where ?f=f and ?M=M] Setcompr_eq_image) lemma measurable_compose_n [measurable (raw)]: assumes "T ∈ measurable M M" shows "(T^^n) ∈ measurable M M" by (induction n, auto simp add: measurable_compose[OF _ assms]) lemma measurable_real_imp_nat: fixes f::"'a ⇒ nat" assumes [measurable]: "(λx. real(f x)) ∈ borel_measurable M" shows "f ∈ measurable M (count_space UNIV)" proof - let ?g = "(λx. real(f x))" have "⋀(n::nat). ?g-`({real n}) ∩ space M = f-`{n} ∩ space M" by auto moreover have "⋀(n::nat). ?g-`({real n}) ∩ space M ∈ sets M" using assms by measurable ultimately have "⋀(n::nat). f-`{n} ∩ space M ∈ sets M" by simp then show ?thesis using measurable_count_space_eq2_countable by blast qed lemma measurable_equality_set [measurable]: fixes f g::"_⇒ 'a::{second_countable_topology, t2_space}" assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M" shows "{x ∈ space M. f x = g x} ∈ sets M" proof - define A where "A = {x ∈ space M. f x = g x}" define B where "B = {y. ∃x::'a. y = (x,x)}" have "A = (λx. (f x, g x))-`B ∩ space M" unfolding A_def B_def by auto moreover have "(λx. (f x, g x)) ∈ borel_measurable M" by simp moreover have "B ∈ sets borel" unfolding B_def by (simp add: closed_diagonal) ultimately have "A ∈ sets M" by simp then show ?thesis unfolding A_def by simp qed lemma measurable_inequality_set [measurable]: fixes f g::"_ ⇒ 'a::{second_countable_topology, linorder_topology}" assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M" shows "{x ∈ space M. f x ≤ g x} ∈ sets M" "{x ∈ space M. f x < g x} ∈ sets M" "{x ∈ space M. f x ≥ g x} ∈ sets M" "{x ∈ space M. f x > g x} ∈ sets M" proof - define F where "F = (λx. (f x, g x))" have * [measurable]: "F ∈ borel_measurable M" unfolding F_def by simp have "{x ∈ space M. f x ≤ g x} = F-`{(x, y) | x y. x ≤ y} ∩ space M" unfolding F_def by auto moreover have "{(x, y) | x y. x ≤ (y::'a)} ∈ sets borel" using closed_subdiagonal borel_closed by blast ultimately show "{x ∈ space M. f x ≤ g x} ∈ sets M" using * by (metis (mono_tags, lifting) measurable_sets) have "{x ∈ space M. f x < g x} = F-`{(x, y) | x y. x < y} ∩ space M" unfolding F_def by auto moreover have "{(x, y) | x y. x < (y::'a)} ∈ sets borel" using open_subdiagonal borel_open by blast ultimately show "{x ∈ space M. f x < g x} ∈ sets M" using * by (metis (mono_tags, lifting) measurable_sets) have "{x ∈ space M. f x ≥ g x} = F-`{(x, y) | x y. x ≥ y} ∩ space M" unfolding F_def by auto moreover have "{(x, y) | x y. x ≥ (y::'a)} ∈ sets borel" using closed_superdiagonal borel_closed by blast ultimately show "{x ∈ space M. f x ≥ g x} ∈ sets M" using * by (metis (mono_tags, lifting) measurable_sets) have "{x ∈ space M. f x > g x} = F-`{(x, y) | x y. x > y} ∩ space M" unfolding F_def by auto moreover have "{(x, y) | x y. x > (y::'a)} ∈ sets borel" using open_superdiagonal borel_open by blast ultimately show "{x ∈ space M. f x > g x} ∈ sets M" using * by (metis (mono_tags, lifting) measurable_sets) qed lemma measurable_limit [measurable]: fixes f::"nat ⇒ 'a ⇒ 'b::first_countable_topology" assumes [measurable]: "⋀n::nat. f n ∈ borel_measurable M" shows "Measurable.pred M (λx. (λn. f n x) ⇢ c)" proof - obtain A :: "nat ⇒ 'b set" where A: "⋀i. open (A i)" "⋀i. c ∈ A i" "⋀S. open S ⟹ c ∈ S ⟹ eventually (λi. A i ⊆ S) sequentially" by (rule countable_basis_at_decseq) blast have [measurable]: "⋀N i. (f N)-`(A i) ∩ space M ∈ sets M" using A(1) by auto then have mes: "(⋂i. ⋃n. ⋂N∈{n..}. (f N)-`(A i) ∩ space M) ∈ sets M" by blast have "(u ⇢ c) ⟷ (∀i. eventually (λn. u n ∈ A i) sequentially)" for u::"nat ⇒ 'b" proof assume "u ⇢ c" then have "eventually (λn. u n ∈ A i) sequentially" for i using A(1)[of i] A(2)[of i] by (simp add: topological_tendstoD) then show "(∀i. eventually (λn. u n ∈ A i) sequentially)" by auto next assume H: "(∀i. eventually (λn. u n ∈ A i) sequentially)" show "(u ⇢ c)" proof (rule topological_tendstoI) fix S assume "open S" "c ∈ S" with A(3)[OF this] obtain i where "A i ⊆ S" using eventually_False_sequentially eventually_mono by blast moreover have "eventually (λn. u n ∈ A i) sequentially" using H by simp ultimately show "∀⇩_{F}n in sequentially. u n ∈ S" by (simp add: eventually_mono subset_eq) qed qed then have "{x. (λn. f n x) ⇢ c} = (⋂i. ⋃n. ⋂N∈{n..}. (f N)-`(A i))" by (auto simp add: atLeast_def eventually_at_top_linorder) then have "{x ∈ space M. (λn. f n x) ⇢ c} = (⋂i. ⋃n. ⋂N∈{n..}. (f N)-`(A i) ∩ space M)" by auto then have "{x ∈ space M. (λn. f n x) ⇢ c} ∈ sets M" using mes by simp then show ?thesis by auto qed lemma measurable_limit2 [measurable]: fixes u::"nat ⇒ 'a ⇒ real" assumes [measurable]: "⋀n. u n ∈ borel_measurable M" "v ∈ borel_measurable M" shows "Measurable.pred M (λx. (λn. u n x) ⇢ v x)" proof - define w where "w = (λn x. u n x - v x)" have [measurable]: "w n ∈ borel_measurable M" for n unfolding w_def by auto have "((λn. u n x) ⇢ v x) ⟷ ((λn. w n x) ⇢ 0)" for x unfolding w_def using Lim_null by auto then show ?thesis using measurable_limit by auto qed lemma measurable_P_restriction [measurable (raw)]: assumes [measurable]: "Measurable.pred M P" "A ∈ sets M" shows "{x ∈ A. P x} ∈ sets M" proof - have "A ⊆ space M" using sets.sets_into_space[OF assms(2)]. then have "{x ∈ A. P x} = A ∩ {x ∈ space M. P x}" by blast then show ?thesis by auto qed lemma measurable_sum_nat [measurable (raw)]: fixes f :: "'c ⇒ 'a ⇒ nat" assumes "⋀i. i ∈ S ⟹ f i ∈ measurable M (count_space UNIV)" shows "(λx. ∑i∈S. f i x) ∈ measurable M (count_space UNIV)" proof cases assume "finite S" then show ?thesis using assms by induct auto qed simp lemma measurable_abs_powr [measurable]: fixes p::real assumes [measurable]: "f ∈ borel_measurable M" shows "(λx. ¦f x¦ powr p) ∈ borel_measurable M" unfolding powr_def by auto text ‹The next one is a variation around \verb+measurable_restrict_space+.› lemma measurable_restrict_space3: assumes "f ∈ measurable M N" and "f ∈ A → B" shows "f ∈ measurable (restrict_space M A) (restrict_space N B)" proof - have "f ∈ measurable (restrict_space M A) N" using assms(1) measurable_restrict_space1 by auto then show ?thesis by (metis Int_iff funcsetI funcset_mem measurable_restrict_space2[of f, of "restrict_space M A", of B, of N] assms(2) space_restrict_space) qed text ‹The next one is a variation around \verb+measurable_piecewise_restrict+.› lemma measurable_piecewise_restrict2: assumes [measurable]: "⋀n. A n ∈ sets M" and "space M = (⋃(n::nat). A n)" "⋀n. ∃h ∈ measurable M N. (∀x ∈ A n. f x = h x)" shows "f ∈ measurable M N" proof (rule measurableI) fix B assume [measurable]: "B ∈ sets N" { fix n::nat obtain h where [measurable]: "h ∈ measurable M N" and "∀x ∈ A n. f x = h x" using assms(3) by blast then have *: "f-`B ∩ A n = h-`B ∩ A n" by auto have "h-`B ∩ A n = h-`B ∩ space M ∩ A n" using assms(2) sets.sets_into_space by auto then have "h-`B ∩ A n ∈ sets M" by simp then have "f-`B ∩ A n ∈ sets M" using * by simp } then have "(⋃n. f-`B ∩ A n) ∈ sets M" by measurable moreover have "f-`B ∩ space M = (⋃n. f-`B ∩ A n)" using assms(2) by blast ultimately show "f-`B ∩ space M ∈ sets M" by simp next fix x assume "x ∈ space M" then obtain n where "x ∈ A n" using assms(2) by blast obtain h where [measurable]: "h ∈ measurable M N" and "∀x ∈ A n. f x = h x" using assms(3) by blast then have "f x = h x" using ‹x ∈ A n› by blast moreover have "h x ∈ space N" by (metis measurable_space ‹x ∈ space M› ‹h ∈ measurable M N›) ultimately show "f x ∈ space N" by simp qed end