imports Improper_Integral Continuous_Extension

(* Title: HOL/Analysis/Equivalence_Measurable_On_Borel Author: LC Paulson (some material ported from HOL Light) *) section‹Equivalence Between Classical Borel Measurability and HOL Light's› theory Equivalence_Measurable_On_Borel imports Equivalence_Lebesgue_Henstock_Integration Improper_Integral Continuous_Extension begin (*Borrowed from Ergodic_Theory/SG_Library_Complement*) abbreviation sym_diff :: "'a set ⇒ 'a set ⇒ 'a set" where "sym_diff A B ≡ ((A - B) ∪ (B-A))" subsection‹Austin's Lemma› lemma Austin_Lemma: fixes 𝒟 :: "'a::euclidean_space set set" assumes "finite 𝒟" and 𝒟: "⋀D. D ∈ 𝒟 ⟹ ∃k a b. D = cbox a b ∧ (∀i ∈ Basis. b∙i - a∙i = k)" obtains 𝒞 where "𝒞 ⊆ 𝒟" "pairwise disjnt 𝒞" "measure lebesgue (⋃𝒞) ≥ measure lebesgue (⋃𝒟) / 3 ^ (DIM('a))" using assms proof (induction "card 𝒟" arbitrary: 𝒟 thesis rule: less_induct) case less show ?case proof (cases "𝒟 = {}") case True then show thesis using less by auto next case False then have "Max (Sigma_Algebra.measure lebesgue ` 𝒟) ∈ Sigma_Algebra.measure lebesgue ` 𝒟" using Max_in finite_imageI ‹finite 𝒟› by blast then obtain D where "D ∈ 𝒟" and "measure lebesgue D = Max (measure lebesgue ` 𝒟)" by auto then have D: "⋀C. C ∈ 𝒟 ⟹ measure lebesgue C ≤ measure lebesgue D" by (simp add: ‹finite 𝒟›) let ?ℰ = "{C. C ∈ 𝒟 - {D} ∧ disjnt C D}" obtain 𝒟' where 𝒟'sub: "𝒟' ⊆ ?ℰ" and 𝒟'dis: "pairwise disjnt 𝒟'" and 𝒟'm: "measure lebesgue (⋃𝒟') ≥ measure lebesgue (⋃?ℰ) / 3 ^ (DIM('a))" proof (rule less.hyps) have *: "?ℰ ⊂ 𝒟" using ‹D ∈ 𝒟› by auto then show "card ?ℰ < card 𝒟" "finite ?ℰ" by (auto simp: ‹finite 𝒟› psubset_card_mono) show "∃k a b. D = cbox a b ∧ (∀i∈Basis. b ∙ i - a ∙ i = k)" if "D ∈ ?ℰ" for D using less.prems(3) that by auto qed then have [simp]: "⋃𝒟' - D = ⋃𝒟'" by (auto simp: disjnt_iff) show ?thesis proof (rule less.prems) show "insert D 𝒟' ⊆ 𝒟" using 𝒟'sub ‹D ∈ 𝒟› by blast show "disjoint (insert D 𝒟')" using 𝒟'dis 𝒟'sub by (fastforce simp add: pairwise_def disjnt_sym) obtain a3 b3 where m3: "content (cbox a3 b3) = 3 ^ DIM('a) * measure lebesgue D" and sub3: "⋀C. ⟦C ∈ 𝒟; ¬ disjnt C D⟧ ⟹ C ⊆ cbox a3 b3" proof - obtain k a b where ab: "D = cbox a b" and k: "⋀i. i ∈ Basis ⟹ b∙i - a∙i = k" using less.prems ‹D ∈ 𝒟› by meson then have eqk: "⋀i. i ∈ Basis ⟹ a ∙ i ≤ b ∙ i ⟷ k ≥ 0" by force show thesis proof let ?a = "(a + b) /⇩_{R}2 - (3/2) *⇩_{R}(b - a)" let ?b = "(a + b) /⇩_{R}2 + (3/2) *⇩_{R}(b - a)" have eq: "(∏i∈Basis. b ∙ i * 3 - a ∙ i * 3) = (∏i∈Basis. b ∙ i - a ∙ i) * 3 ^ DIM('a)" by (simp add: comm_monoid_mult_class.prod.distrib flip: left_diff_distrib inner_diff_left) show "content (cbox ?a ?b) = 3 ^ DIM('a) * measure lebesgue D" by (simp add: content_cbox_if box_eq_empty algebra_simps eq ab k) show "C ⊆ cbox ?a ?b" if "C ∈ 𝒟" and CD: "¬ disjnt C D" for C proof - obtain k' a' b' where ab': "C = cbox a' b'" and k': "⋀i. i ∈ Basis ⟹ b'∙i - a'∙i = k'" using less.prems ‹C ∈ 𝒟› by meson then have eqk': "⋀i. i ∈ Basis ⟹ a' ∙ i ≤ b' ∙ i ⟷ k' ≥ 0" by force show ?thesis proof (clarsimp simp add: disjoint_interval disjnt_def ab ab' not_less subset_box algebra_simps) show "a ∙ i * 2 ≤ a' ∙ i + b ∙ i ∧ a ∙ i + b' ∙ i ≤ b ∙ i * 2" if * [rule_format]: "∀j∈Basis. a' ∙ j ≤ b' ∙ j" and "i ∈ Basis" for i proof - have "a' ∙ i ≤ b' ∙ i ∧ a ∙ i ≤ b ∙ i ∧ a ∙ i ≤ b' ∙ i ∧ a' ∙ i ≤ b ∙ i" using ‹i ∈ Basis› CD by (simp_all add: disjoint_interval disjnt_def ab ab' not_less) then show ?thesis using D [OF ‹C ∈ 𝒟›] ‹i ∈ Basis› apply (simp add: ab ab' k k' eqk eqk' content_cbox_cases) using k k' by fastforce qed qed qed qed qed have 𝒟lm: "⋀D. D ∈ 𝒟 ⟹ D ∈ lmeasurable" using less.prems(3) by blast have "measure lebesgue (⋃𝒟) ≤ measure lebesgue (cbox a3 b3 ∪ (⋃𝒟 - cbox a3 b3))" proof (rule measure_mono_fmeasurable) show "⋃𝒟 ∈ sets lebesgue" using 𝒟lm ‹finite 𝒟› by blast show "cbox a3 b3 ∪ (⋃𝒟 - cbox a3 b3) ∈ lmeasurable" by (simp add: 𝒟lm fmeasurable.Un fmeasurable.finite_Union less.prems(2) subset_eq) qed auto also have "… = content (cbox a3 b3) + measure lebesgue (⋃𝒟 - cbox a3 b3)" by (simp add: 𝒟lm fmeasurable.finite_Union less.prems(2) measure_Un2 subsetI) also have "… ≤ (measure lebesgue D + measure lebesgue (⋃𝒟')) * 3 ^ DIM('a)" proof - have "(⋃𝒟 - cbox a3 b3) ⊆ ⋃?ℰ" using sub3 by fastforce then have "measure lebesgue (⋃𝒟 - cbox a3 b3) ≤ measure lebesgue (⋃?ℰ)" proof (rule measure_mono_fmeasurable) show "⋃ 𝒟 - cbox a3 b3 ∈ sets lebesgue" by (simp add: 𝒟lm fmeasurableD less.prems(2) sets.Diff sets.finite_Union subsetI) show "⋃ {C ∈ 𝒟 - {D}. disjnt C D} ∈ lmeasurable" using 𝒟lm less.prems(2) by auto qed then have "measure lebesgue (⋃𝒟 - cbox a3 b3) / 3 ^ DIM('a) ≤ measure lebesgue (⋃ 𝒟')" using 𝒟'm by (simp add: field_split_simps) then show ?thesis by (simp add: m3 field_simps) qed also have "… ≤ measure lebesgue (⋃(insert D 𝒟')) * 3 ^ DIM('a)" proof (simp add: 𝒟lm ‹D ∈ 𝒟›) show "measure lebesgue D + measure lebesgue (⋃𝒟') ≤ measure lebesgue (D ∪ ⋃ 𝒟')" proof (subst measure_Un2) show "⋃ 𝒟' ∈ lmeasurable" by (meson 𝒟lm ‹insert D 𝒟' ⊆ 𝒟› fmeasurable.finite_Union less.prems(2) finite_subset subset_eq subset_insertI) show "measure lebesgue D + measure lebesgue (⋃ 𝒟') ≤ measure lebesgue D + measure lebesgue (⋃ 𝒟' - D)" using ‹insert D 𝒟' ⊆ 𝒟› infinite_super less.prems(2) by force qed (simp add: 𝒟lm ‹D ∈ 𝒟›) qed finally show "measure lebesgue (⋃𝒟) / 3 ^ DIM('a) ≤ measure lebesgue (⋃(insert D 𝒟'))" by (simp add: field_split_simps) qed qed qed subsection‹A differentiability-like property of the indefinite integral. › proposition integrable_ccontinuous_explicit: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "⋀a b::'a. f integrable_on cbox a b" obtains N where "negligible N" "⋀x e. ⟦x ∉ N; 0 < e⟧ ⟹ ∃d>0. ∀h. 0 < h ∧ h < d ⟶ norm(integral (cbox x (x + h *⇩_{R}One)) f /⇩_{R}h ^ DIM('a) - f x) < e" proof - define BOX where "BOX ≡ λh. λx::'a. cbox x (x + h *⇩_{R}One)" define BOX2 where "BOX2 ≡ λh. λx::'a. cbox (x - h *⇩_{R}One) (x + h *⇩_{R}One)" define i where "i ≡ λh x. integral (BOX h x) f /⇩_{R}h ^ DIM('a)" define Ψ where "Ψ ≡ λx r. ∀d>0. ∃h. 0 < h ∧ h < d ∧ r ≤ norm(i h x - f x)" let ?N = "{x. ∃e>0. Ψ x e}" have "∃N. negligible N ∧ (∀x e. x ∉ N ∧ 0 < e ⟶ ¬ Ψ x e)" proof (rule exI ; intro conjI allI impI) let ?M = "⋃n. {x. Ψ x (inverse(real n + 1))}" have "negligible ({x. Ψ x μ} ∩ cbox a b)" if "μ > 0" for a b μ proof (cases "negligible(cbox a b)") case True then show ?thesis by (simp add: negligible_Int) next case False then have "box a b ≠ {}" by (simp add: negligible_interval) then have ab: "⋀i. i ∈ Basis ⟹ a∙i < b∙i" by (simp add: box_ne_empty) show ?thesis unfolding negligible_outer_le proof (intro allI impI) fix e::real let ?ee = "(e * μ) / 2 / 6 ^ (DIM('a))" assume "e > 0" then have gt0: "?ee > 0" using ‹μ > 0› by auto have f': "f integrable_on cbox (a - One) (b + One)" using assms by blast obtain γ where "gauge γ" and γ: "⋀p. ⟦p tagged_partial_division_of (cbox (a - One) (b + One)); γ fine p⟧ ⟹ (∑(x, k)∈p. norm (content k *⇩_{R}f x - integral k f)) < ?ee" using Henstock_lemma [OF f' gt0] that by auto let ?E = "{x. x ∈ cbox a b ∧ Ψ x μ}" have "∃h>0. BOX h x ⊆ γ x ∧ BOX h x ⊆ cbox (a - One) (b + One) ∧ μ ≤ norm (i h x - f x)" if "x ∈ cbox a b" "Ψ x μ" for x proof - obtain d where "d > 0" and d: "ball x d ⊆ γ x" using gaugeD [OF ‹gauge γ›, of x] openE by blast then obtain h where "0 < h" "h < 1" and hless: "h < d / real DIM('a)" and mule: "μ ≤ norm (i h x - f x)" using ‹Ψ x μ› [unfolded Ψ_def, rule_format, of "min 1 (d / DIM('a))"] by auto show ?thesis proof (intro exI conjI) show "0 < h" "μ ≤ norm (i h x - f x)" by fact+ have "BOX h x ⊆ ball x d" proof (clarsimp simp: BOX_def mem_box dist_norm algebra_simps) fix y assume "∀i∈Basis. x ∙ i ≤ y ∙ i ∧ y ∙ i ≤ h + x ∙ i" then have lt: "¦(x - y) ∙ i¦ < d / real DIM('a)" if "i ∈ Basis" for i using hless that by (force simp: inner_diff_left) have "norm (x - y) ≤ (∑i∈Basis. ¦(x - y) ∙ i¦)" using norm_le_l1 by blast also have "… < d" using sum_bounded_above_strict [of Basis "λi. ¦(x - y) ∙ i¦" "d / DIM('a)", OF lt] by auto finally show "norm (x - y) < d" . qed with d show "BOX h x ⊆ γ x" by blast show "BOX h x ⊆ cbox (a - One) (b + One)" using that ‹h < 1› by (force simp: BOX_def mem_box algebra_simps intro: subset_box_imp) qed qed then obtain η where h0: "⋀x. x ∈ ?E ⟹ η x > 0" and BOX_γ: "⋀x. x ∈ ?E ⟹ BOX (η x) x ⊆ γ x" and "⋀x. x ∈ ?E ⟹ BOX (η x) x ⊆ cbox (a - One) (b + One) ∧ μ ≤ norm (i (η x) x - f x)" by simp metis then have BOX_cbox: "⋀x. x ∈ ?E ⟹ BOX (η x) x ⊆ cbox (a - One) (b + One)" and μ_le: "⋀x. x ∈ ?E ⟹ μ ≤ norm (i (η x) x - f x)" by blast+ define γ' where "γ' ≡ λx. if x ∈ cbox a b ∧ Ψ x μ then ball x (η x) else γ x" have "gauge γ'" using ‹gauge γ› by (auto simp: h0 gauge_def γ'_def) obtain 𝒟 where "countable 𝒟" and 𝒟: "⋃𝒟 ⊆ cbox a b" "⋀K. K ∈ 𝒟 ⟹ interior K ≠ {} ∧ (∃c d. K = cbox c d)" and Dcovered: "⋀K. K ∈ 𝒟 ⟹ ∃x. x ∈ cbox a b ∧ Ψ x μ ∧ x ∈ K ∧ K ⊆ γ' x" and subUD: "?E ⊆ ⋃𝒟" by (rule covering_lemma [of ?E a b γ']) (simp_all add: Bex_def ‹box a b ≠ {}› ‹gauge γ'›) then have "𝒟 ⊆ sets lebesgue" by fastforce show "∃T. {x. Ψ x μ} ∩ cbox a b ⊆ T ∧ T ∈ lmeasurable ∧ measure lebesgue T ≤ e" proof (intro exI conjI) show "{x. Ψ x μ} ∩ cbox a b ⊆ ⋃𝒟" apply auto using subUD by auto have mUE: "measure lebesgue (⋃ ℰ) ≤ measure lebesgue (cbox a b)" if "ℰ ⊆ 𝒟" "finite ℰ" for ℰ proof (rule measure_mono_fmeasurable) show "⋃ ℰ ⊆ cbox a b" using 𝒟(1) that(1) by blast show "⋃ ℰ ∈ sets lebesgue" by (metis 𝒟(2) fmeasurable.finite_Union fmeasurableD lmeasurable_cbox subset_eq that) qed auto then show "⋃𝒟 ∈ lmeasurable" by (metis 𝒟(2) ‹countable 𝒟› fmeasurable_Union_bound lmeasurable_cbox) then have leab: "measure lebesgue (⋃𝒟) ≤ measure lebesgue (cbox a b)" by (meson 𝒟(1) fmeasurableD lmeasurable_cbox measure_mono_fmeasurable) obtain ℱ where "ℱ ⊆ 𝒟" "finite ℱ" and ℱ: "measure lebesgue (⋃𝒟) ≤ 2 * measure lebesgue (⋃ℱ)" proof (cases "measure lebesgue (⋃𝒟) = 0") case True then show ?thesis by (force intro: that [where ℱ = "{}"]) next case False obtain ℱ where "ℱ ⊆ 𝒟" "finite ℱ" and ℱ: "measure lebesgue (⋃𝒟)/2 < measure lebesgue (⋃ℱ)" proof (rule measure_countable_Union_approachable [of 𝒟 "measure lebesgue (⋃𝒟) / 2" "content (cbox a b)"]) show "countable 𝒟" by fact show "0 < measure lebesgue (⋃ 𝒟) / 2" using False by (simp add: zero_less_measure_iff) show Dlm: "D ∈ lmeasurable" if "D ∈ 𝒟" for D using 𝒟(2) that by blast show "measure lebesgue (⋃ ℱ) ≤ content (cbox a b)" if "ℱ ⊆ 𝒟" "finite ℱ" for ℱ proof - have "measure lebesgue (⋃ ℱ) ≤ measure lebesgue (⋃𝒟)" proof (rule measure_mono_fmeasurable) show "⋃ ℱ ⊆ ⋃ 𝒟" by (simp add: Sup_subset_mono ‹ℱ ⊆ 𝒟›) show "⋃ ℱ ∈ sets lebesgue" by (meson Dlm fmeasurableD sets.finite_Union subset_eq that) show "⋃ 𝒟 ∈ lmeasurable" by fact qed also have "… ≤ measure lebesgue (cbox a b)" proof (rule measure_mono_fmeasurable) show "⋃ 𝒟 ∈ sets lebesgue" by (simp add: ‹⋃ 𝒟 ∈ lmeasurable› fmeasurableD) qed (auto simp:𝒟(1)) finally show ?thesis by simp qed qed auto then show ?thesis using that by auto qed obtain tag where tag_in_E: "⋀D. D ∈ 𝒟 ⟹ tag D ∈ ?E" and tag_in_self: "⋀D. D ∈ 𝒟 ⟹ tag D ∈ D" and tag_sub: "⋀D. D ∈ 𝒟 ⟹ D ⊆ γ' (tag D)" using Dcovered by simp metis then have sub_ball_tag: "⋀D. D ∈ 𝒟 ⟹ D ⊆ ball (tag D) (η (tag D))" by (simp add: γ'_def) define Φ where "Φ ≡ λD. BOX (η(tag D)) (tag D)" define Φ2 where "Φ2 ≡ λD. BOX2 (η(tag D)) (tag D)" obtain 𝒞 where "𝒞 ⊆ Φ2 ` ℱ" "pairwise disjnt 𝒞" "measure lebesgue (⋃𝒞) ≥ measure lebesgue (⋃(Φ2`ℱ)) / 3 ^ (DIM('a))" proof (rule Austin_Lemma) show "finite (Φ2`ℱ)" using ‹finite ℱ› by blast have "∃k a b. Φ2 D = cbox a b ∧ (∀i∈Basis. b ∙ i - a ∙ i = k)" if "D ∈ ℱ" for D apply (rule_tac x="2 * η(tag D)" in exI) apply (rule_tac x="tag D - η(tag D) *⇩_{R}One" in exI) apply (rule_tac x="tag D + η(tag D) *⇩_{R}One" in exI) using that apply (auto simp: Φ2_def BOX2_def algebra_simps) done then show "⋀D. D ∈ Φ2 ` ℱ ⟹ ∃k a b. D = cbox a b ∧ (∀i∈Basis. b ∙ i - a ∙ i = k)" by blast qed auto then obtain 𝒢 where "𝒢 ⊆ ℱ" and disj: "pairwise disjnt (Φ2 ` 𝒢)" and "measure lebesgue (⋃(Φ2 ` 𝒢)) ≥ measure lebesgue (⋃(Φ2`ℱ)) / 3 ^ (DIM('a))" unfolding Φ2_def subset_image_iff by (meson empty_subsetI equals0D pairwise_imageI) moreover have "measure lebesgue (⋃(Φ2 ` 𝒢)) * 3 ^ DIM('a) ≤ e/2" proof - have "finite 𝒢" using ‹finite ℱ› ‹𝒢 ⊆ ℱ› infinite_super by blast have BOX2_m: "⋀x. x ∈ tag ` 𝒢 ⟹ BOX2 (η x) x ∈ lmeasurable" by (auto simp: BOX2_def) have BOX_m: "⋀x. x ∈ tag ` 𝒢 ⟹ BOX (η x) x ∈ lmeasurable" by (auto simp: BOX_def) have BOX_sub: "BOX (η x) x ⊆ BOX2 (η x) x" for x by (auto simp: BOX_def BOX2_def subset_box algebra_simps) have DISJ2: "BOX2 (η (tag X)) (tag X) ∩ BOX2 (η (tag Y)) (tag Y) = {}" if "X ∈ 𝒢" "Y ∈ 𝒢" "tag X ≠ tag Y" for X Y proof - obtain i where i: "i ∈ Basis" "tag X ∙ i ≠ tag Y ∙ i" using ‹tag X ≠ tag Y› by (auto simp: euclidean_eq_iff [of "tag X"]) have XY: "X ∈ 𝒟" "Y ∈ 𝒟" using ‹ℱ ⊆ 𝒟› ‹𝒢 ⊆ ℱ› that by auto then have "0 ≤ η (tag X)" "0 ≤ η (tag Y)" by (meson h0 le_cases not_le tag_in_E)+ with XY i have "BOX2 (η (tag X)) (tag X) ≠ BOX2 (η (tag Y)) (tag Y)" unfolding eq_iff by (fastforce simp add: BOX2_def subset_box algebra_simps) then show ?thesis using disj that by (auto simp: pairwise_def disjnt_def Φ2_def) qed then have BOX2_disj: "pairwise (λx y. negligible (BOX2 (η x) x ∩ BOX2 (η y) y)) (tag ` 𝒢)" by (simp add: pairwise_imageI) then have BOX_disj: "pairwise (λx y. negligible (BOX (η x) x ∩ BOX (η y) y)) (tag ` 𝒢)" proof (rule pairwise_mono) show "negligible (BOX (η x) x ∩ BOX (η y) y)" if "negligible (BOX2 (η x) x ∩ BOX2 (η y) y)" for x y by (metis (no_types, hide_lams) that Int_mono negligible_subset BOX_sub) qed auto have eq: "⋀box. (λD. box (η (tag D)) (tag D)) ` 𝒢 = (λt. box (η t) t) ` tag ` 𝒢" by (simp add: image_comp) have "measure lebesgue (BOX2 (η t) t) * 3 ^ DIM('a) = measure lebesgue (BOX (η t) t) * (2*3) ^ DIM('a)" if "t ∈ tag ` 𝒢" for t proof - have "content (cbox (t - η t *⇩_{R}One) (t + η t *⇩_{R}One)) = content (cbox t (t + η t *⇩_{R}One)) * 2 ^ DIM('a)" using that by (simp add: algebra_simps content_cbox_if box_eq_empty) then show ?thesis by (simp add: BOX2_def BOX_def flip: power_mult_distrib) qed then have "measure lebesgue (⋃(Φ2 ` 𝒢)) * 3 ^ DIM('a) = measure lebesgue (⋃(Φ ` 𝒢)) * 6 ^ DIM('a)" unfolding Φ_def Φ2_def eq by (simp add: measure_negligible_finite_Union_image ‹finite 𝒢› BOX2_m BOX_m BOX2_disj BOX_disj sum_distrib_right del: UN_simps) also have "… ≤ e/2" proof - have "μ * measure lebesgue (⋃D∈𝒢. Φ D) ≤ μ * (∑D ∈ Φ`𝒢. measure lebesgue D)" using ‹μ > 0› ‹finite 𝒢› by (force simp: BOX_m Φ_def fmeasurableD intro: measure_Union_le) also have "… = (∑D ∈ Φ`𝒢. measure lebesgue D * μ)" by (metis mult.commute sum_distrib_right) also have "… ≤ (∑(x, K) ∈ (λD. (tag D, Φ D)) ` 𝒢. norm (content K *⇩_{R}f x - integral K f))" proof (rule sum_le_included; clarify?) fix D assume "D ∈ 𝒢" then have "η (tag D) > 0" using ‹ℱ ⊆ 𝒟› ‹𝒢 ⊆ ℱ› h0 tag_in_E by auto then have m_Φ: "measure lebesgue (Φ D) > 0" by (simp add: Φ_def BOX_def algebra_simps) have "μ ≤ norm (i (η(tag D)) (tag D) - f(tag D))" using μ_le ‹D ∈ 𝒢› ‹ℱ ⊆ 𝒟› ‹𝒢 ⊆ ℱ› tag_in_E by auto also have "… = norm ((content (Φ D) *⇩_{R}f(tag D) - integral (Φ D) f) /⇩_{R}measure lebesgue (Φ D))" using m_Φ unfolding i_def Φ_def BOX_def by (simp add: algebra_simps content_cbox_plus norm_minus_commute) finally have "measure lebesgue (Φ D) * μ ≤ norm (content (Φ D) *⇩_{R}f(tag D) - integral (Φ D) f)" using m_Φ by simp (simp add: field_simps) then show "∃y∈(λD. (tag D, Φ D)) ` 𝒢. snd y = Φ D ∧ measure lebesgue (Φ D) * μ ≤ (case y of (x, k) ⇒ norm (content k *⇩_{R}f x - integral k f))" using ‹D ∈ 𝒢› by auto qed (use ‹finite 𝒢› in auto) also have "… < ?ee" proof (rule γ) show "(λD. (tag D, Φ D)) ` 𝒢 tagged_partial_division_of cbox (a - One) (b + One)" unfolding tagged_partial_division_of_def proof (intro conjI allI impI ; clarify ?) show "tag D ∈ Φ D" if "D ∈ 𝒢" for D using that ‹ℱ ⊆ 𝒟› ‹𝒢 ⊆ ℱ› h0 tag_in_E by (auto simp: Φ_def BOX_def mem_box algebra_simps eucl_less_le_not_le in_mono) show "y ∈ cbox (a - One) (b + One)" if "D ∈ 𝒢" "y ∈ Φ D" for D y using that BOX_cbox Φ_def ‹ℱ ⊆ 𝒟› ‹𝒢 ⊆ ℱ› tag_in_E by blast show "tag D = tag E ∧ Φ D = Φ E" if "D ∈ 𝒢" "E ∈ 𝒢" and ne: "interior (Φ D) ∩ interior (Φ E) ≠ {}" for D E proof - have "BOX2 (η (tag D)) (tag D) ∩ BOX2 (η (tag E)) (tag E) = {} ∨ tag E = tag D" using DISJ2 ‹D ∈ 𝒢› ‹E ∈ 𝒢› by force then have "BOX (η (tag D)) (tag D) ∩ BOX (η (tag E)) (tag E) = {} ∨ tag E = tag D" using BOX_sub by blast then show "tag D = tag E ∧ Φ D = Φ E" by (metis Φ_def interior_Int interior_empty ne) qed qed (use ‹finite 𝒢› Φ_def BOX_def in auto) show "γ fine (λD. (tag D, Φ D)) ` 𝒢" unfolding fine_def Φ_def using BOX_γ ‹ℱ ⊆ 𝒟› ‹𝒢 ⊆ ℱ› tag_in_E by blast qed finally show ?thesis using ‹μ > 0› by (auto simp: field_split_simps) qed finally show ?thesis . qed moreover have "measure lebesgue (⋃ℱ) ≤ measure lebesgue (⋃(Φ2`ℱ))" proof (rule measure_mono_fmeasurable) have "D ⊆ ball (tag D) (η(tag D))" if "D ∈ ℱ" for D using ‹ℱ ⊆ 𝒟› sub_ball_tag that by blast moreover have "ball (tag D) (η(tag D)) ⊆ BOX2 (η (tag D)) (tag D)" if "D ∈ ℱ" for D proof (clarsimp simp: Φ2_def BOX2_def mem_box algebra_simps dist_norm) fix x and i::'a assume "norm (tag D - x) < η (tag D)" and "i ∈ Basis" then have "¦tag D ∙ i - x ∙ i¦ ≤ η (tag D)" by (metis eucl_less_le_not_le inner_commute inner_diff_right norm_bound_Basis_le) then show "tag D ∙ i ≤ x ∙ i + η (tag D) ∧ x ∙ i ≤ η (tag D) + tag D ∙ i" by (simp add: abs_diff_le_iff) qed ultimately show "⋃ℱ ⊆ ⋃(Φ2`ℱ)" by (force simp: Φ2_def) show "⋃ℱ ∈ sets lebesgue" using ‹finite ℱ› ‹𝒟 ⊆ sets lebesgue› ‹ℱ ⊆ 𝒟› by blast show "⋃(Φ2`ℱ) ∈ lmeasurable" unfolding Φ2_def BOX2_def using ‹finite ℱ› by blast qed ultimately have "measure lebesgue (⋃ℱ) ≤ e/2" by (auto simp: field_split_simps) then show "measure lebesgue (⋃𝒟) ≤ e" using ℱ by linarith qed qed qed then have "⋀j. negligible {x. Ψ x (inverse(real j + 1))}" using negligible_on_intervals by (metis (full_types) inverse_positive_iff_positive le_add_same_cancel1 linorder_not_le nat_le_real_less not_add_less1 of_nat_0) then have "negligible ?M" by auto moreover have "?N ⊆ ?M" proof (clarsimp simp: dist_norm) fix y e assume "0 < e" and ye [rule_format]: "Ψ y e" then obtain k where k: "0 < k" "inverse (real k + 1) < e" by (metis One_nat_def add.commute less_add_same_cancel2 less_imp_inverse_less less_trans neq0_conv of_nat_1 of_nat_Suc reals_Archimedean zero_less_one) with ye show "∃n. Ψ y (inverse (real n + 1))" apply (rule_tac x=k in exI) unfolding Ψ_def by (force intro: less_le_trans) qed ultimately show "negligible ?N" by (blast intro: negligible_subset) show "¬ Ψ x e" if "x ∉ ?N ∧ 0 < e" for x e using that by blast qed with that show ?thesis unfolding i_def BOX_def Ψ_def by (fastforce simp add: not_le) qed subsection‹HOL Light measurability› definition measurable_on :: "('a::euclidean_space ⇒ 'b::real_normed_vector) ⇒ 'a set ⇒ bool" (infixr "measurable'_on" 46) where "f measurable_on S ≡ ∃N g. negligible N ∧ (∀n. continuous_on UNIV (g n)) ∧ (∀x. x ∉ N ⟶ (λn. g n x) ⇢ (if x ∈ S then f x else 0))" lemma measurable_on_UNIV: "(λx. if x ∈ S then f x else 0) measurable_on UNIV ⟷ f measurable_on S" by (auto simp: measurable_on_def) lemma measurable_on_spike_set: assumes f: "f measurable_on S" and neg: "negligible ((S - T) ∪ (T - S))" shows "f measurable_on T" proof - obtain N and F where N: "negligible N" and conF: "⋀n. continuous_on UNIV (F n)" and tendsF: "⋀x. x ∉ N ⟹ (λn. F n x) ⇢ (if x ∈ S then f x else 0)" using f by (auto simp: measurable_on_def) show ?thesis unfolding measurable_on_def proof (intro exI conjI allI impI) show "continuous_on UNIV (λx. F n x)" for n by (intro conF continuous_intros) show "negligible (N ∪ (S - T) ∪ (T - S))" by (metis (full_types) N neg negligible_Un_eq) show "(λn. F n x) ⇢ (if x ∈ T then f x else 0)" if "x ∉ (N ∪ (S - T) ∪ (T - S))" for x using that tendsF [of x] by auto qed qed text‹ Various common equivalent forms of function measurability. › lemma measurable_on_0 [simp]: "(λx. 0) measurable_on S" unfolding measurable_on_def proof (intro exI conjI allI impI) show "(λn. 0) ⇢ (if x ∈ S then 0::'b else 0)" for x by force qed auto lemma measurable_on_scaleR_const: assumes f: "f measurable_on S" shows "(λx. c *⇩_{R}f x) measurable_on S" proof - obtain NF and F where NF: "negligible NF" and conF: "⋀n. continuous_on UNIV (F n)" and tendsF: "⋀x. x ∉ NF ⟹ (λn. F n x) ⇢ (if x ∈ S then f x else 0)" using f by (auto simp: measurable_on_def) show ?thesis unfolding measurable_on_def proof (intro exI conjI allI impI) show "continuous_on UNIV (λx. c *⇩_{R}F n x)" for n by (intro conF continuous_intros) show "(λn. c *⇩_{R}F n x) ⇢ (if x ∈ S then c *⇩_{R}f x else 0)" if "x ∉ NF" for x using tendsto_scaleR [OF tendsto_const tendsF, of x] that by auto qed (auto simp: NF) qed lemma measurable_on_cmul: fixes c :: real assumes "f measurable_on S" shows "(λx. c * f x) measurable_on S" using measurable_on_scaleR_const [OF assms] by simp lemma measurable_on_cdivide: fixes c :: real assumes "f measurable_on S" shows "(λx. f x / c) measurable_on S" proof (cases "c=0") case False then show ?thesis using measurable_on_cmul [of f S "1/c"] by (simp add: assms) qed auto lemma measurable_on_minus: "f measurable_on S ⟹ (λx. -(f x)) measurable_on S" using measurable_on_scaleR_const [of f S "-1"] by auto lemma continuous_imp_measurable_on: "continuous_on UNIV f ⟹ f measurable_on UNIV" unfolding measurable_on_def apply (rule_tac x="{}" in exI) apply (rule_tac x="λn. f" in exI, auto) done proposition integrable_subintervals_imp_measurable: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "⋀a b. f integrable_on cbox a b" shows "f measurable_on UNIV" proof - define BOX where "BOX ≡ λh. λx::'a. cbox x (x + h *⇩_{R}One)" define i where "i ≡ λh x. integral (BOX h x) f /⇩_{R}h ^ DIM('a)" obtain N where "negligible N" and k: "⋀x e. ⟦x ∉ N; 0 < e⟧ ⟹ ∃d>0. ∀h. 0 < h ∧ h < d ⟶ norm (integral (cbox x (x + h *⇩_{R}One)) f /⇩_{R}h ^ DIM('a) - f x) < e" using integrable_ccontinuous_explicit assms by blast show ?thesis unfolding measurable_on_def proof (intro exI conjI allI impI) show "continuous_on UNIV ((λn x. i (inverse(Suc n)) x) n)" for n proof (clarsimp simp: continuous_on_iff) show "∃d>0. ∀x'. dist x' x < d ⟶ dist (i (inverse (1 + real n)) x') (i (inverse (1 + real n)) x) < e" if "0 < e" for x e proof - let ?e = "e / (1 + real n) ^ DIM('a)" have "?e > 0" using ‹e > 0› by auto moreover have "x ∈ cbox (x - 2 *⇩_{R}One) (x + 2 *⇩_{R}One)" by (simp add: mem_box inner_diff_left inner_left_distrib) moreover have "x + One /⇩_{R}real (Suc n) ∈ cbox (x - 2 *⇩_{R}One) (x + 2 *⇩_{R}One)" by (auto simp: mem_box inner_diff_left inner_left_distrib field_simps) ultimately obtain δ where "δ > 0" and δ: "⋀c' d'. ⟦c' ∈ cbox (x - 2 *⇩_{R}One) (x + 2 *⇩_{R}One); d' ∈ cbox (x - 2 *⇩_{R}One) (x + 2 *⇩_{R}One); norm(c' - x) ≤ δ; norm(d' - (x + One /⇩_{R}Suc n)) ≤ δ⟧ ⟹ norm(integral(cbox c' d') f - integral(cbox x (x + One /⇩_{R}Suc n)) f) < ?e" by (blast intro: indefinite_integral_continuous [of f _ _ x] assms) show ?thesis proof (intro exI impI conjI allI) show "min δ 1 > 0" using ‹δ > 0› by auto show "dist (i (inverse (1 + real n)) y) (i (inverse (1 + real n)) x) < e" if "dist y x < min δ 1" for y proof - have no: "norm (y - x) < 1" using that by (auto simp: dist_norm) have le1: "inverse (1 + real n) ≤ 1" by (auto simp: field_split_simps) have "norm (integral (cbox y (y + One /⇩_{R}real (Suc n))) f - integral (cbox x (x + One /⇩_{R}real (Suc n))) f) < e / (1 + real n) ^ DIM('a)" proof (rule δ) show "y ∈ cbox (x - 2 *⇩_{R}One) (x + 2 *⇩_{R}One)" using no by (auto simp: mem_box algebra_simps dest: Basis_le_norm [of _ "y-x"]) show "y + One /⇩_{R}real (Suc n) ∈ cbox (x - 2 *⇩_{R}One) (x + 2 *⇩_{R}One)" proof (simp add: dist_norm mem_box algebra_simps, intro ballI conjI) fix i::'a assume "i ∈ Basis" then have 1: "¦y ∙ i - x ∙ i¦ < 1" by (metis inner_commute inner_diff_right no norm_bound_Basis_lt) moreover have "… < (2 + inverse (1 + real n))" "1 ≤ 2 - inverse (1 + real n)" by (auto simp: field_simps) ultimately show "x ∙ i ≤ y ∙ i + (2 + inverse (1 + real n))" "y ∙ i + inverse (1 + real n) ≤ x ∙ i + 2" by linarith+ qed show "norm (y - x) ≤ δ" "norm (y + One /⇩_{R}real (Suc n) - (x + One /⇩_{R}real (Suc n))) ≤ δ" using that by (auto simp: dist_norm) qed then show ?thesis using that by (simp add: dist_norm i_def BOX_def flip: scaleR_diff_right) (simp add: field_simps) qed qed qed qed show "negligible N" by (simp add: ‹negligible N›) show "(λn. i (inverse (Suc n)) x) ⇢ (if x ∈ UNIV then f x else 0)" if "x ∉ N" for x unfolding lim_sequentially proof clarsimp show "∃no. ∀n≥no. dist (i (inverse (1 + real n)) x) (f x) < e" if "0 < e" for e proof - obtain d where "d > 0" and d: "⋀h. ⟦0 < h; h < d⟧ ⟹ norm (integral (cbox x (x + h *⇩_{R}One)) f /⇩_{R}h ^ DIM('a) - f x) < e" using k [of x e] ‹x ∉ N› ‹0 < e› by blast then obtain M where M: "M ≠ 0" "0 < inverse (real M)" "inverse (real M) < d" using real_arch_invD by auto show ?thesis proof (intro exI allI impI) show "dist (i (inverse (1 + real n)) x) (f x) < e" if "M ≤ n" for n proof - have *: "0 < inverse (1 + real n)" "inverse (1 + real n) ≤ inverse M" using that ‹M ≠ 0› by auto show ?thesis using that M apply (simp add: i_def BOX_def dist_norm) apply (blast intro: le_less_trans * d) done qed qed qed qed qed qed subsection‹Composing continuous and measurable functions; a few variants› lemma measurable_on_compose_continuous: assumes f: "f measurable_on UNIV" and g: "continuous_on UNIV g" shows "(g ∘ f) measurable_on UNIV" proof - obtain N and F where "negligible N" and conF: "⋀n. continuous_on UNIV (F n)" and tendsF: "⋀x. x ∉ N ⟹ (λn. F n x) ⇢ f x" using f by (auto simp: measurable_on_def) show ?thesis unfolding measurable_on_def proof (intro exI conjI allI impI) show "negligible N" by fact show "continuous_on UNIV (g ∘ (F n))" for n using conF continuous_on_compose continuous_on_subset g by blast show "(λn. (g ∘ F n) x) ⇢ (if x ∈ UNIV then (g ∘ f) x else 0)" if "x ∉ N" for x :: 'a using that g tendsF by (auto simp: continuous_on_def intro: tendsto_compose) qed qed lemma measurable_on_compose_continuous_0: assumes f: "f measurable_on S" and g: "continuous_on UNIV g" and "g 0 = 0" shows "(g ∘ f) measurable_on S" proof - have f': "(λx. if x ∈ S then f x else 0) measurable_on UNIV" using f measurable_on_UNIV by blast show ?thesis using measurable_on_compose_continuous [OF f' g] by (simp add: measurable_on_UNIV o_def if_distrib ‹g 0 = 0› cong: if_cong) qed lemma measurable_on_compose_continuous_box: assumes fm: "f measurable_on UNIV" and fab: "⋀x. f x ∈ box a b" and contg: "continuous_on (box a b) g" shows "(g ∘ f) measurable_on UNIV" proof - have "∃γ. (∀n. continuous_on UNIV (γ n)) ∧ (∀x. x ∉ N ⟶ (λn. γ n x) ⇢ g (f x))" if "negligible N" and conth [rule_format]: "∀n. continuous_on UNIV (λx. h n x)" and tends [rule_format]: "∀x. x ∉ N ⟶ (λn. h n x) ⇢ f x" for N and h :: "nat ⇒ 'a ⇒ 'b" proof - define θ where "θ ≡ λn x. (∑i∈Basis. (max (a∙i + (b∙i - a∙i) / real (n+2)) (min ((h n x)∙i) (b∙i - (b∙i - a∙i) / real (n+2)))) *⇩_{R}i)" have aibi: "⋀i. i ∈ Basis ⟹ a ∙ i < b ∙ i" using box_ne_empty(2) fab by auto then have *: "⋀i n. i ∈ Basis ⟹ a ∙ i + real n * (a ∙ i) < b ∙ i + real n * (b ∙ i)" by (meson add_mono_thms_linordered_field(3) less_eq_real_def mult_left_mono of_nat_0_le_iff) show ?thesis proof (intro exI conjI allI impI) show "continuous_on UNIV (g ∘ (θ n))" for n :: nat unfolding θ_def apply (intro continuous_on_compose2 [OF contg] continuous_intros conth) apply (auto simp: aibi * mem_box less_max_iff_disj min_less_iff_disj algebra_simps field_split_simps) done show "(λn. (g ∘ θ n) x) ⇢ g (f x)" if "x ∉ N" for x unfolding o_def proof (rule isCont_tendsto_compose [where g=g]) show "isCont g (f x)" using contg fab continuous_on_eq_continuous_at by blast have "(λn. θ n x) ⇢ (∑i∈Basis. max (a ∙ i) (min (f x ∙ i) (b ∙ i)) *⇩_{R}i)" unfolding θ_def proof (intro tendsto_intros ‹x ∉ N› tends) fix i::'b assume "i ∈ Basis" have a: "(λn. a ∙ i + (b ∙ i - a ∙ i) / real n) ⇢ a∙i + 0" by (intro tendsto_add lim_const_over_n tendsto_const) show "(λn. a ∙ i + (b ∙ i - a ∙ i) / real (n + 2)) ⇢ a ∙ i" using LIMSEQ_ignore_initial_segment [where k=2, OF a] by simp have b: "(λn. b∙i - (b ∙ i - a ∙ i) / (real n)) ⇢ b∙i - 0" by (intro tendsto_diff lim_const_over_n tendsto_const) show "(λn. b ∙ i - (b ∙ i - a ∙ i) / real (n + 2)) ⇢ b ∙ i" using LIMSEQ_ignore_initial_segment [where k=2, OF b] by simp qed also have "(∑i∈Basis. max (a ∙ i) (min (f x ∙ i) (b ∙ i)) *⇩_{R}i) = (∑i∈Basis. (f x ∙ i) *⇩_{R}i)" apply (rule sum.cong) using fab apply auto apply (intro order_antisym) apply (auto simp: mem_box) using less_imp_le apply blast by (metis (full_types) linear max_less_iff_conj min.bounded_iff not_le) also have "… = f x" using euclidean_representation by blast finally show "(λn. θ n x) ⇢ f x" . qed qed qed then show ?thesis using fm by (auto simp: measurable_on_def) qed lemma measurable_on_Pair: assumes f: "f measurable_on S" and g: "g measurable_on S" shows "(λx. (f x, g x)) measurable_on S" proof - obtain NF and F where NF: "negligible NF" and conF: "⋀n. continuous_on UNIV (F n)" and tendsF: "⋀x. x ∉ NF ⟹ (λn. F n x) ⇢ (if x ∈ S then f x else 0)" using f by (auto simp: measurable_on_def) obtain NG and G where NG: "negligible NG" and conG: "⋀n. continuous_on UNIV (G n)" and tendsG: "⋀x. x ∉ NG ⟹ (λn. G n x) ⇢ (if x ∈ S then g x else 0)" using g by (auto simp: measurable_on_def) show ?thesis unfolding measurable_on_def proof (intro exI conjI allI impI) show "negligible (NF ∪ NG)" by (simp add: NF NG) show "continuous_on UNIV (λx. (F n x, G n x))" for n using conF conG continuous_on_Pair by blast show "(λn. (F n x, G n x)) ⇢ (if x ∈ S then (f x, g x) else 0)" if "x ∉ NF ∪ NG" for x using tendsto_Pair [OF tendsF tendsG, of x x] that unfolding zero_prod_def by (simp add: split: if_split_asm) qed qed lemma measurable_on_combine: assumes f: "f measurable_on S" and g: "g measurable_on S" and h: "continuous_on UNIV (λx. h (fst x) (snd x))" and "h 0 0 = 0" shows "(λx. h (f x) (g x)) measurable_on S" proof - have *: "(λx. h (f x) (g x)) = (λx. h (fst x) (snd x)) ∘ (λx. (f x, g x))" by auto show ?thesis unfolding * by (auto simp: measurable_on_compose_continuous_0 measurable_on_Pair assms) qed lemma measurable_on_add: assumes f: "f measurable_on S" and g: "g measurable_on S" shows "(λx. f x + g x) measurable_on S" by (intro continuous_intros measurable_on_combine [OF assms]) auto lemma measurable_on_diff: assumes f: "f measurable_on S" and g: "g measurable_on S" shows "(λx. f x - g x) measurable_on S" by (intro continuous_intros measurable_on_combine [OF assms]) auto lemma measurable_on_scaleR: assumes f: "f measurable_on S" and g: "g measurable_on S" shows "(λx. f x *⇩_{R}g x) measurable_on S" by (intro continuous_intros measurable_on_combine [OF assms]) auto lemma measurable_on_sum: assumes "finite I" "⋀i. i ∈ I ⟹ f i measurable_on S" shows "(λx. sum (λi. f i x) I) measurable_on S" using assms by (induction I) (auto simp: measurable_on_add) lemma measurable_on_spike: assumes f: "f measurable_on T" and "negligible S" and gf: "⋀x. x ∈ T - S ⟹ g x = f x" shows "g measurable_on T" proof - obtain NF and F where NF: "negligible NF" and conF: "⋀n. continuous_on UNIV (F n)" and tendsF: "⋀x. x ∉ NF ⟹ (λn. F n x) ⇢ (if x ∈ T then f x else 0)" using f by (auto simp: measurable_on_def) show ?thesis unfolding measurable_on_def proof (intro exI conjI allI impI) show "negligible (NF ∪ S)" by (simp add: NF ‹negligible S›) show "⋀x. x ∉ NF ∪ S ⟹ (λn. F n x) ⇢ (if x ∈ T then g x else 0)" by (metis (full_types) Diff_iff Un_iff gf tendsF) qed (auto simp: conF) qed proposition indicator_measurable_on: assumes "S ∈ sets lebesgue" shows "indicat_real S measurable_on UNIV" proof - { fix n::nat let ?ε = "(1::real) / (2 * 2^n)" have ε: "?ε > 0" by auto obtain T where "closed T" "T ⊆ S" "S-T ∈ lmeasurable" and ST: "emeasure lebesgue (S - T) < ?ε" by (meson ε assms sets_lebesgue_inner_closed) obtain U where "open U" "S ⊆ U" "(U - S) ∈ lmeasurable" and US: "emeasure lebesgue (U - S) < ?ε" by (meson ε assms sets_lebesgue_outer_open) have eq: "-T ∩ U = (S-T) ∪ (U - S)" using ‹T ⊆ S› ‹S ⊆ U› by auto have "emeasure lebesgue ((S-T) ∪ (U - S)) ≤ emeasure lebesgue (S - T) + emeasure lebesgue (U - S)" using ‹S - T ∈ lmeasurable› ‹U - S ∈ lmeasurable› emeasure_subadditive by blast also have "… < ?ε + ?ε" using ST US add_mono_ennreal by metis finally have le: "emeasure lebesgue (-T ∩ U) < ennreal (1 / 2^n)" by (simp add: eq) have 1: "continuous_on (T ∪ -U) (indicat_real S)" unfolding indicator_def proof (rule continuous_on_cases [OF ‹closed T›]) show "closed (- U)" using ‹open U› by blast show "continuous_on T (λx. 1::real)" "continuous_on (- U) (λx. 0::real)" by (auto simp: continuous_on) show "∀x. x ∈ T ∧ x ∉ S ∨ x ∈ - U ∧ x ∈ S ⟶ (1::real) = 0" using ‹T ⊆ S› ‹S ⊆ U› by auto qed have 2: "closedin (top_of_set UNIV) (T ∪ -U)" using ‹closed T› ‹open U› by auto obtain g where "continuous_on UNIV g" "⋀x. x ∈ T ∪ -U ⟹ g x = indicat_real S x" "⋀x. norm(g x) ≤ 1" by (rule Tietze [OF 1 2, of 1]) auto with le have "∃g E. continuous_on UNIV g ∧ (∀x ∈ -E. g x = indicat_real S x) ∧ (∀x. norm(g x) ≤ 1) ∧ E ∈ sets lebesgue ∧ emeasure lebesgue E < ennreal (1 / 2^n)" apply (rule_tac x=g in exI) apply (rule_tac x="-T ∩ U" in exI) using ‹S - T ∈ lmeasurable› ‹U - S ∈ lmeasurable› eq by auto } then obtain g E where cont: "⋀n. continuous_on UNIV (g n)" and geq: "⋀n x. x ∈ - E n ⟹ g n x = indicat_real S x" and ng1: "⋀n x. norm(g n x) ≤ 1" and Eset: "⋀n. E n ∈ sets lebesgue" and Em: "⋀n. emeasure lebesgue (E n) < ennreal (1 / 2^n)" by metis have null: "limsup E ∈ null_sets lebesgue" proof (rule borel_cantelli_limsup1 [OF Eset]) show "emeasure lebesgue (E n) < ∞" for n by (metis Em infinity_ennreal_def order.asym top.not_eq_extremum) show "summable (λn. measure lebesgue (E n))" proof (rule summable_comparison_test' [OF summable_geometric, of "1/2" 0]) show "norm (measure lebesgue (E n)) ≤ (1/2) ^ n" for n using Em [of n] by (simp add: measure_def enn2real_leI power_one_over) qed auto qed have tends: "(λn. g n x) ⇢ indicat_real S x" if "x ∉ limsup E" for x proof - have "∀⇩_{F}n in sequentially. x ∈ - E n" using that by (simp add: mem_limsup_iff not_frequently) then show ?thesis unfolding tendsto_iff dist_real_def by (simp add: eventually_mono geq) qed show ?thesis unfolding measurable_on_def proof (intro exI conjI allI impI) show "negligible (limsup E)" using negligible_iff_null_sets null by blast show "continuous_on UNIV (g n)" for n using cont by blast qed (use tends in auto) qed lemma measurable_on_restrict: assumes f: "f measurable_on UNIV" and S: "S ∈ sets lebesgue" shows "(λx. if x ∈ S then f x else 0) measurable_on UNIV" proof - have "indicat_real S measurable_on UNIV" by (simp add: S indicator_measurable_on) then show ?thesis using measurable_on_scaleR [OF _ f, of "indicat_real S"] by (simp add: indicator_scaleR_eq_if) qed lemma measurable_on_const_UNIV: "(λx. k) measurable_on UNIV" by (simp add: continuous_imp_measurable_on) lemma measurable_on_const [simp]: "S ∈ sets lebesgue ⟹ (λx. k) measurable_on S" using measurable_on_UNIV measurable_on_const_UNIV measurable_on_restrict by blast lemma simple_function_indicator_representation_real: fixes f ::"'a ⇒ real" assumes f: "simple_function M f" and x: "x ∈ space M" and nn: "⋀x. f x ≥ 0" shows "f x = (∑y ∈ f ` space M. y * indicator (f -` {y} ∩ space M) x)" proof - have f': "simple_function M (ennreal ∘ f)" by (simp add: f) have *: "f x = enn2real (∑y∈ ennreal ` f ` space M. y * indicator ((ennreal ∘ f) -` {y} ∩ space M) x)" using arg_cong [OF simple_function_indicator_representation [OF f' x], of enn2real, simplified nn o_def] nn unfolding o_def image_comp by (metis enn2real_ennreal) have "enn2real (∑y∈ennreal ` f ` space M. if ennreal (f x) = y ∧ x ∈ space M then y else 0) = sum (enn2real ∘ (λy. if ennreal (f x) = y ∧ x ∈ space M then y else 0)) (ennreal ` f ` space M)" by (rule enn2real_sum) auto also have "… = sum (enn2real ∘ (λy. if ennreal (f x) = y ∧ x ∈ space M then y else 0) ∘ ennreal) (f ` space M)" by (rule sum.reindex) (use nn in ‹auto simp: inj_on_def intro: sum.cong›) also have "… = (∑y∈f ` space M. if f x = y ∧ x ∈ space M then y else 0)" using nn by (auto simp: inj_on_def intro: sum.cong) finally show ?thesis by (subst *) (simp add: enn2real_sum indicator_def if_distrib cong: if_cong) qed lemma✐‹tag important› simple_function_induct_real [consumes 1, case_names cong set mult add, induct set: simple_function]: fixes u :: "'a ⇒ real" assumes u: "simple_function M u" assumes cong: "⋀f g. simple_function M f ⟹ simple_function M g ⟹ (AE x in M. f x = g x) ⟹ P f ⟹ P g" assumes set: "⋀A. A ∈ sets M ⟹ P (indicator A)" assumes mult: "⋀u c. P u ⟹ P (λx. c * u x)" assumes add: "⋀u v. P u ⟹ P v ⟹ P (λx. u x + v x)" and nn: "⋀x. u x ≥ 0" shows "P u" proof (rule cong) from AE_space show "AE x in M. (∑y∈u ` space M. y * indicator (u -` {y} ∩ space M) x) = u x" proof eventually_elim fix x assume x: "x ∈ space M" from simple_function_indicator_representation_real[OF u x] nn show "(∑y∈u ` space M. y * indicator (u -` {y} ∩ space M) x) = u x" by metis qed next from u have "finite (u ` space M)" unfolding simple_function_def by auto then show "P (λx. ∑y∈u ` space M. y * indicator (u -` {y} ∩ space M) x)" proof induct case empty then show ?case using set[of "{}"] by (simp add: indicator_def[abs_def]) next case (insert a F) have eq: "∑ {y. u x = y ∧ (y = a ∨ y ∈ F) ∧ x ∈ space M} = (if u x = a ∧ x ∈ space M then a else 0) + ∑ {y. u x = y ∧ y ∈ F ∧ x ∈ space M}" for x proof (cases "x ∈ space M") case True have *: "{y. u x = y ∧ (y = a ∨ y ∈ F)} = {y. u x = a ∧ y = a} ∪ {y. u x = y ∧ y ∈ F}" by auto show ?thesis using insert by (simp add: * True) qed auto have a: "P (λx. a * indicator (u -` {a} ∩ space M) x)" proof (intro mult set) show "u -` {a} ∩ space M ∈ sets M" using u by auto qed show ?case using nn insert a by (simp add: eq indicator_times_eq_if [where f = "λx. a"] add) qed next show "simple_function M (λx. (∑y∈u ` space M. y * indicator (u -` {y} ∩ space M) x))" apply (subst simple_function_cong) apply (rule simple_function_indicator_representation_real[symmetric]) apply (auto intro: u nn) done qed fact proposition simple_function_measurable_on_UNIV: fixes f :: "'a::euclidean_space ⇒ real" assumes f: "simple_function lebesgue f" and nn: "⋀x. f x ≥ 0" shows "f measurable_on UNIV" using f proof (induction f) case (cong f g) then obtain N where "negligible N" "{x. g x ≠ f x} ⊆ N" by (auto simp: eventually_ae_filter_negligible eq_commute) then show ?case by (blast intro: measurable_on_spike cong) next case (set S) then show ?case by (simp add: indicator_measurable_on) next case (mult u c) then show ?case by (simp add: measurable_on_cmul) case (add u v) then show ?case by (simp add: measurable_on_add) qed (auto simp: nn) lemma simple_function_lebesgue_if: fixes f :: "'a::euclidean_space ⇒ real" assumes f: "simple_function lebesgue f" and S: "S ∈ sets lebesgue" shows "simple_function lebesgue (λx. if x ∈ S then f x else 0)" proof - have ffin: "finite (range f)" and fsets: "∀x. f -` {f x} ∈ sets lebesgue" using f by (auto simp: simple_function_def) have "finite (f ` S)" by (meson finite_subset subset_image_iff ffin top_greatest) moreover have "finite ((λx. 0::real) ` T)" for T :: "'a set" by (auto simp: image_def) moreover have if_sets: "(λx. if x ∈ S then f x else 0) -` {f a} ∈ sets lebesgue" for a proof - have *: "(λx. if x ∈ S then f x else 0) -` {f a} = (if f a = 0 then -S ∪ f -` {f a} else (f -` {f a}) ∩ S)" by (auto simp: split: if_split_asm) show ?thesis unfolding * by (metis Compl_in_sets_lebesgue S sets.Int sets.Un fsets) qed moreover have "(λx. if x ∈ S then f x else 0) -` {0} ∈ sets lebesgue" proof (cases "0 ∈ range f") case True then show ?thesis by (metis (no_types, lifting) if_sets rangeE) next case False then have "(λx. if x ∈ S then f x else 0) -` {0} = -S" by auto then show ?thesis by (simp add: Compl_in_sets_lebesgue S) qed ultimately show ?thesis by (auto simp: simple_function_def) qed corollary simple_function_measurable_on: fixes f :: "'a::euclidean_space ⇒ real" assumes f: "simple_function lebesgue f" and nn: "⋀x. f x ≥ 0" and S: "S ∈ sets lebesgue" shows "f measurable_on S" by (simp add: measurable_on_UNIV [symmetric, of f] S f simple_function_lebesgue_if nn simple_function_measurable_on_UNIV) lemma fixes f :: "'a::euclidean_space ⇒ 'b::ordered_euclidean_space" assumes f: "f measurable_on S" and g: "g measurable_on S" shows measurable_on_sup: "(λx. sup (f x) (g x)) measurable_on S" and measurable_on_inf: "(λx. inf (f x) (g x)) measurable_on S" proof - obtain NF and F where NF: "negligible NF" and conF: "⋀n. continuous_on UNIV (F n)" and tendsF: "⋀x. x ∉ NF ⟹ (λn. F n x) ⇢ (if x ∈ S then f x else 0)" using f by (auto simp: measurable_on_def) obtain NG and G where NG: "negligible NG" and conG: "⋀n. continuous_on UNIV (G n)" and tendsG: "⋀x. x ∉ NG ⟹ (λn. G n x) ⇢ (if x ∈ S then g x else 0)" using g by (auto simp: measurable_on_def) show "(λx. sup (f x) (g x)) measurable_on S" unfolding measurable_on_def proof (intro exI conjI allI impI) show "continuous_on UNIV (λx. sup (F n x) (G n x))" for n unfolding sup_max eucl_sup by (intro conF conG continuous_intros) show "(λn. sup (F n x) (G n x)) ⇢ (if x ∈ S then sup (f x) (g x) else 0)" if "x ∉ NF ∪ NG" for x using tendsto_sup [OF tendsF tendsG, of x x] that by auto qed (simp add: NF NG) show "(λx. inf (f x) (g x)) measurable_on S" unfolding measurable_on_def proof (intro exI conjI allI impI) show "continuous_on UNIV (λx. inf (F n x) (G n x))" for n unfolding inf_min eucl_inf by (intro conF conG continuous_intros) show "(λn. inf (F n x) (G n x)) ⇢ (if x ∈ S then inf (f x) (g x) else 0)" if "x ∉ NF ∪ NG" for x using tendsto_inf [OF tendsF tendsG, of x x] that by auto qed (simp add: NF NG) qed proposition measurable_on_componentwise_UNIV: "f measurable_on UNIV ⟷ (∀i∈Basis. (λx. (f x ∙ i) *⇩_{R}i) measurable_on UNIV)" (is "?lhs = ?rhs") proof assume L: ?lhs show ?rhs proof fix i::'b assume "i ∈ Basis" have cont: "continuous_on UNIV (λx. (x ∙ i) *⇩_{R}i)" by (intro continuous_intros) show "(λx. (f x ∙ i) *⇩_{R}i) measurable_on UNIV" using measurable_on_compose_continuous [OF L cont] by (simp add: o_def) qed next assume ?rhs then have "∃N g. negligible N ∧ (∀n. continuous_on UNIV (g n)) ∧ (∀x. x ∉ N ⟶ (λn. g n x) ⇢ (f x ∙ i) *⇩_{R}i)" if "i ∈ Basis" for i by (simp add: measurable_on_def that) then obtain N g where N: "⋀i. i ∈ Basis ⟹ negligible (N i)" and cont: "⋀i n. i ∈ Basis ⟹ continuous_on UNIV (g i n)" and tends: "⋀i x. ⟦i ∈ Basis; x ∉ N i⟧ ⟹ (λn. g i n x) ⇢ (f x ∙ i) *⇩_{R}i" by metis show ?lhs unfolding measurable_on_def proof (intro exI conjI allI impI) show "negligible (⋃i ∈ Basis. N i)" using N eucl.finite_Basis by blast show "continuous_on UNIV (λx. (∑i∈Basis. g i n x))" for n by (intro continuous_intros cont) next fix x assume "x ∉ (⋃i ∈ Basis. N i)" then have "⋀i. i ∈ Basis ⟹ x ∉ N i" by auto then have "(λn. (∑i∈Basis. g i n x)) ⇢ (∑i∈Basis. (f x ∙ i) *⇩_{R}i)" by (intro tends tendsto_intros) then show "(λn. (∑i∈Basis. g i n x)) ⇢ (if x ∈ UNIV then f x else 0)" by (simp add: euclidean_representation) qed qed corollary measurable_on_componentwise: "f measurable_on S ⟷ (∀i∈Basis. (λx. (f x ∙ i) *⇩_{R}i) measurable_on S)" apply (subst measurable_on_UNIV [symmetric]) apply (subst measurable_on_componentwise_UNIV) apply (simp add: measurable_on_UNIV if_distrib [of "λx. inner x _"] if_distrib [of "λx. scaleR x _"] cong: if_cong) done (*FIXME: avoid duplication of proofs WRT borel_measurable_implies_simple_function_sequence*) lemma✐‹tag important› borel_measurable_implies_simple_function_sequence_real: fixes u :: "'a ⇒ real" assumes u[measurable]: "u ∈ borel_measurable M" and nn: "⋀x. u x ≥ 0" shows "∃f. incseq f ∧ (∀i. simple_function M (f i)) ∧ (∀x. bdd_above (range (λi. f i x))) ∧ (∀i x. 0 ≤ f i x) ∧ u = (SUP i. f i)" proof - define f where [abs_def]: "f i x = real_of_int (floor ((min i (u x)) * 2^i)) / 2^i" for i x have [simp]: "0 ≤ f i x" for i x by (auto simp: f_def intro!: divide_nonneg_nonneg mult_nonneg_nonneg nn) have *: "2^n * real_of_int x = real_of_int (2^n * x)" for n x by simp have "real_of_int ⌊real i * 2 ^ i⌋ = real_of_int ⌊i * 2 ^ i⌋" for i by (intro arg_cong[where f=real_of_int]) simp then have [simp]: "real_of_int ⌊real i * 2 ^ i⌋ = i * 2 ^ i" for i unfolding floor_of_nat by simp have bdd: "bdd_above (range (λi. f i x))" for x by (rule bdd_aboveI [where M = "u x"]) (auto simp: f_def field_simps min_def) have "incseq f" proof (intro monoI le_funI) fix m n :: nat and x assume "m ≤ n" moreover { fix d :: nat have "⌊2^d::real⌋ * ⌊2^m * (min (of_nat m) (u x))⌋ ≤ ⌊2^d * (2^m * (min (of_nat m) (u x)))⌋" by (rule le_mult_floor) (auto simp: nn) also have "… ≤ ⌊2^d * (2^m * (min (of_nat d + of_nat m) (u x)))⌋" by (intro floor_mono mult_mono min.mono) (auto simp: nn min_less_iff_disj of_nat_less_top) finally have "f m x ≤ f(m + d) x" unfolding f_def by (auto simp: field_simps power_add * simp del: of_int_mult) } ultimately show "f m x ≤ f n x" by (auto simp: le_iff_add) qed then have inc_f: "incseq (λi. f i x)" for x by (auto simp: incseq_def le_fun_def) moreover have "simple_function M (f i)" for i proof (rule simple_function_borel_measurable) have "⌊(min (of_nat i) (u x)) * 2 ^ i⌋ ≤ ⌊int i * 2 ^ i⌋" for x by (auto split: split_min intro!: floor_mono) then have "f i ` space M ⊆ (λn. real_of_int n / 2^i) ` {0 .. of_nat i * 2^i}" unfolding floor_of_int by (auto simp: f_def nn intro!: imageI) then show "finite (f i ` space M)" by (rule finite_subset) auto show "f i ∈ borel_measurable M" unfolding f_def enn2real_def by measurable qed moreover { fix x have "(SUP i. (f i x)) = u x" proof - obtain n where "u x ≤ of_nat n" using real_arch_simple by auto then have min_eq_r: "∀⇩_{F}i in sequentially. min (real i) (u x) = u x" by (auto simp: eventually_sequentially intro!: exI[of _ n] split: split_min) have "(λi. real_of_int ⌊min (real i) (u x) * 2^i⌋ / 2^i) ⇢ u x" proof (rule tendsto_sandwich) show "(λn. u x - (1/2)^n) ⇢ u x" by (auto intro!: tendsto_eq_intros LIMSEQ_power_zero) show "∀⇩_{F}n in sequentially. real_of_int ⌊min (real n) (u x) * 2 ^ n⌋ / 2 ^ n ≤ u x" using min_eq_r by eventually_elim (auto simp: field_simps) have *: "u x * (2 ^ n * 2 ^ n) ≤ 2^n + 2^n * real_of_int ⌊u x * 2 ^ n⌋" for n using real_of_int_floor_ge_diff_one[of "u x * 2^n", THEN mult_left_mono, of "2^n"] by (auto simp: field_simps) show "∀⇩_{F}n in sequentially. u x - (1/2)^n ≤ real_of_int ⌊min (real n) (u x) * 2 ^ n⌋ / 2 ^ n" using min_eq_r by eventually_elim (insert *, auto simp: field_simps) qed auto then have "(λi. (f i x)) ⇢ u x" by (simp add: f_def) from LIMSEQ_unique LIMSEQ_incseq_SUP [OF bdd inc_f] this show ?thesis by blast qed } ultimately show ?thesis by (intro exI [of _ "λi x. f i x"]) (auto simp: ‹incseq f› bdd image_comp) qed lemma homeomorphic_open_interval_UNIV: fixes a b:: real assumes "a < b" shows "{a<..<b} homeomorphic (UNIV::real set)" proof - have "{a<..<b} = ball ((b+a) / 2) ((b-a) / 2)" using assms by (auto simp: dist_real_def abs_if field_split_simps split: if_split_asm) then show ?thesis by (simp add: homeomorphic_ball_UNIV assms) qed proposition homeomorphic_box_UNIV: fixes a b:: "'a::euclidean_space" assumes "box a b ≠ {}" shows "box a b homeomorphic (UNIV::'a set)" proof - have "{a ∙ i <..<b ∙ i} homeomorphic (UNIV::real set)" if "i ∈ Basis" for i using assms box_ne_empty that by (blast intro: homeomorphic_open_interval_UNIV) then have "∃f g. (∀x. a ∙ i < x ∧ x < b ∙ i ⟶ g (f x) = x) ∧ (∀y. a ∙ i < g y ∧ g y < b ∙ i ∧ f(g y) = y) ∧ continuous_on {a ∙ i<..<b ∙ i} f ∧ continuous_on (UNIV::real set) g" if "i ∈ Basis" for i using that by (auto simp: homeomorphic_minimal mem_box Ball_def) then obtain f g where gf: "⋀i x. ⟦i ∈ Basis; a ∙ i < x; x < b ∙ i⟧ ⟹ g i (f i x) = x" and fg: "⋀i y. i ∈ Basis ⟹ a ∙ i < g i y ∧ g i y < b ∙ i ∧ f i (g i y) = y" and contf: "⋀i. i ∈ Basis ⟹ continuous_on {a ∙ i<..<b ∙ i} (f i)" and contg: "⋀i. i ∈ Basis ⟹ continuous_on (UNIV::real set) (g i)" by metis define F where "F ≡ λx. ∑i∈Basis. (f i (x ∙ i)) *⇩_{R}i" define G where "G ≡ λx. ∑i∈Basis. (g i (x ∙ i)) *⇩_{R}i" show ?thesis unfolding homeomorphic_minimal proof (intro exI conjI ballI) show "G y ∈ box a b" for y using fg by (simp add: G_def mem_box) show "G (F x) = x" if "x ∈ box a b" for x using that by (simp add: F_def G_def gf mem_box euclidean_representation) show "F (G y) = y" for y by (simp add: F_def G_def fg mem_box euclidean_representation) show "continuous_on (box a b) F" unfolding F_def proof (intro continuous_intros continuous_on_compose2 [OF contf continuous_on_inner]) show "(λx. x ∙ i) ` box a b ⊆ {a ∙ i<..<b ∙ i}" if "i ∈ Basis" for i using that by (auto simp: mem_box) qed show "continuous_on UNIV G" unfolding G_def by (intro continuous_intros continuous_on_compose2 [OF contg continuous_on_inner]) auto qed auto qed lemma diff_null_sets_lebesgue: "⟦N ∈ null_sets (lebesgue_on S); X-N ∈ sets (lebesgue_on S); N ⊆ X⟧ ⟹ X ∈ sets (lebesgue_on S)" by (metis Int_Diff_Un inf.commute inf.orderE null_setsD2 sets.Un) lemma borel_measurable_diff_null: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes N: "N ∈ null_sets (lebesgue_on S)" and S: "S ∈ sets lebesgue" shows "f ∈ borel_measurable (lebesgue_on (S-N)) ⟷ f ∈ borel_measurable (lebesgue_on S)" unfolding in_borel_measurable space_lebesgue_on sets_restrict_UNIV proof (intro ball_cong iffI) show "f -` T ∩ S ∈ sets (lebesgue_on S)" if "f -` T ∩ (S-N) ∈ sets (lebesgue_on (S-N))" for T proof - have "N ∩ S = N" by (metis N S inf.orderE null_sets_restrict_space) moreover have "N ∩ S ∈ sets lebesgue" by (metis N S inf.orderE null_setsD2 null_sets_restrict_space) moreover have "f -` T ∩ S ∩ (f -` T ∩ N) ∈ sets lebesgue" by (metis N S completion.complete inf.absorb2 inf_le2 inf_mono null_sets_restrict_space) ultimately show ?thesis by (metis Diff_Int_distrib Int_Diff_Un S inf_le2 sets.Diff sets.Un sets_restrict_space_iff space_lebesgue_on space_restrict_space that) qed show "f -` T ∩ (S-N) ∈ sets (lebesgue_on (S-N))" if "f -` T ∩ S ∈ sets (lebesgue_on S)" for T proof - have "(S - N) ∩ f -` T = (S - N) ∩ (f -` T ∩ S)" by blast then have "(S - N) ∩ f -` T ∈ sets.restricted_space lebesgue (S - N)" by (metis S image_iff sets.Int_space_eq2 sets_restrict_space_iff that) then show ?thesis by (simp add: inf.commute sets_restrict_space) qed qed auto lemma lebesgue_measurable_diff_null: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "N ∈ null_sets lebesgue" shows "f ∈ borel_measurable (lebesgue_on (-N)) ⟷ f ∈ borel_measurable lebesgue" by (simp add: Compl_eq_Diff_UNIV assms borel_measurable_diff_null lebesgue_on_UNIV_eq) proposition measurable_on_imp_borel_measurable_lebesgue_UNIV: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "f measurable_on UNIV" shows "f ∈ borel_measurable lebesgue" proof - obtain N and F where NF: "negligible N" and conF: "⋀n. continuous_on UNIV (F n)" and tendsF: "⋀x. x ∉ N ⟹ (λn. F n x) ⇢ f x" using assms by (auto simp: measurable_on_def) obtain N where "N ∈ null_sets lebesgue" "f ∈ borel_measurable (lebesgue_on (-N))" proof show "f ∈ borel_measurable (lebesgue_on (- N))" proof (rule borel_measurable_LIMSEQ_metric) show "F i ∈ borel_measurable (lebesgue_on (- N))" for i by (meson Compl_in_sets_lebesgue NF conF continuous_imp_measurable_on_sets_lebesgue continuous_on_subset negligible_imp_sets subset_UNIV) show "(λi. F i x) ⇢ f x" if "x ∈ space (lebesgue_on (- N))" for x using that by (simp add: tendsF) qed show "N ∈ null_sets lebesgue" using NF negligible_iff_null_sets by blast qed then show ?thesis using lebesgue_measurable_diff_null by blast qed corollary measurable_on_imp_borel_measurable_lebesgue: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "f measurable_on S" and S: "S ∈ sets lebesgue" shows "f ∈ borel_measurable (lebesgue_on S)" proof - have "(λx. if x ∈ S then f x else 0) measurable_on UNIV" using assms(1) measurable_on_UNIV by blast then show ?thesis by (simp add: borel_measurable_if_D measurable_on_imp_borel_measurable_lebesgue_UNIV) qed proposition measurable_on_limit: fixes f :: "nat ⇒ 'a::euclidean_space ⇒ 'b::euclidean_space" assumes f: "⋀n. f n measurable_on S" and N: "negligible N" and lim: "⋀x. x ∈ S - N ⟹ (λn. f n x) ⇢ g x" shows "g measurable_on S" proof - have "box (0::'b) One homeomorphic (UNIV::'b set)" by (simp add: homeomorphic_box_UNIV) then obtain h h':: "'b⇒'b" where hh': "⋀x. x ∈ box 0 One ⟹ h (h' x) = x" and h'im: "h' ` box 0 One = UNIV" and conth: "continuous_on UNIV h" and conth': "continuous_on (box 0 One) h'" and h'h: "⋀y. h' (h y) = y" and rangeh: "range h = box 0 One" by (auto simp: homeomorphic_def homeomorphism_def) have "norm y ≤ DIM('b)" if y: "y ∈ box 0 One" for y::'b proof - have y01: "0 < y ∙ i" "y ∙ i < 1" if "i ∈ Basis" for i using that y by (auto simp: mem_box) have "norm y ≤ (∑i∈Basis. ¦y ∙ i¦)" using norm_le_l1 by blast also have "… ≤ (∑i::'b∈Basis. 1)" proof (rule sum_mono) show "¦y ∙ i¦ ≤ 1" if "i ∈ Basis" for i using y01 that by fastforce qed also have "… ≤ DIM('b)" by auto finally show ?thesis . qed then have norm_le: "norm(h y) ≤ DIM('b)" for y by (metis UNIV_I image_eqI rangeh) have "(h' ∘ (h ∘ (λx. if x ∈ S then g x else 0))) measurable_on UNIV" proof (rule measurable_on_compose_continuous_box) let ?χ = "h ∘ (λx. if x ∈ S then g x else 0)" let ?f = "λn. h ∘ (λx. if x ∈ S then f n x else 0)" show "?χ measurable_on UNIV" proof (rule integrable_subintervals_imp_measurable) show "?χ integrable_on cbox a b" for a b proof (rule integrable_spike_set) show "?χ integrable_on (cbox a b - N)" proof (rule dominated_convergence_integrable) show const: "(λx. DIM('b)) integrable_on cbox a b - N" by (simp add: N has_integral_iff integrable_const integrable_negligible integrable_setdiff negligible_diff) show "norm ((h ∘ (λx. if x ∈ S then g x else 0)) x) ≤ DIM('b)" if "x ∈ cbox a b - N" for x using that norm_le by (simp add: o_def) show "(λk. ?f k x) ⇢ ?χ x" if "x ∈ cbox a b - N" for x using that lim [of x] conth by (auto simp: continuous_on_def intro: tendsto_compose) show "(?f n) absolutely_integrable_on cbox a b - N" for n proof (rule measurable_bounded_by_integrable_imp_absolutely_integrable) show "?f n ∈ borel_measurable (lebesgue_on (cbox a b - N))" proof (rule measurable_on_imp_borel_measurable_lebesgue [OF measurable_on_spike_set]) show "?f n measurable_on cbox a b" unfolding measurable_on_UNIV [symmetric, of _ "cbox a b"] proof (rule measurable_on_restrict) have f': "(λx. if x ∈ S then f n x else 0) measurable_on UNIV" by (simp add: f measurable_on_UNIV) show "?f n measurable_on UNIV" using measurable_on_compose_continuous [OF f' conth] by auto qed auto show "negligible (sym_diff (cbox a b) (cbox a b - N))" by (auto intro: negligible_subset [OF N]) show "cbox a b - N ∈ sets lebesgue" by (simp add: N negligible_imp_sets sets.Diff) qed show "cbox a b - N ∈ sets lebesgue" by (simp add: N negligible_imp_sets sets.Diff) show "norm (?f n x) ≤ DIM('b)" if "x ∈ cbox a b - N" for x using that local.norm_le by simp qed (auto simp: const) qed show "negligible {x ∈ cbox a b - N - cbox a b. ?χ x ≠ 0}" by (auto simp: empty_imp_negligible) have "{x ∈ cbox a b - (cbox a b - N). ?χ x ≠ 0} ⊆ N" by auto then show "negligible {x ∈ cbox a b - (cbox a b - N). ?χ x ≠ 0}" using N negligible_subset by blast qed qed show "?χ x ∈ box 0 One" for x using rangeh by auto show "continuous_on (box 0 One) h'" by (rule conth') qed then show ?thesis by (simp add: o_def h'h measurable_on_UNIV) qed lemma measurable_on_if_simple_function_limit: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" shows "⟦⋀n. g n measurable_on UNIV; ⋀n. finite (range (g n)); ⋀x. (λn. g n x) ⇢ f x⟧ ⟹ f measurable_on UNIV" by (force intro: measurable_on_limit [where N="{}"]) lemma lebesgue_measurable_imp_measurable_on_nnreal_UNIV: fixes u :: "'a::euclidean_space ⇒ real" assumes u: "u ∈ borel_measurable lebesgue" and nn: "⋀x. u x ≥ 0" shows "u measurable_on UNIV" proof - obtain f where "incseq f" and f: "∀i. simple_function lebesgue (f i)" and bdd: "⋀x. bdd_above (range (λi. f i x))" and nnf: "⋀i x. 0 ≤ f i x" and *: "u = (SUP i. f i)" using borel_measurable_implies_simple_function_sequence_real nn u by metis show ?thesis unfolding * proof (rule measurable_on_if_simple_function_limit [of concl: "Sup (range f)"]) show "(f i) measurable_on UNIV" for i by (simp add: f nnf simple_function_measurable_on_UNIV) show "finite (range (f i))" for i by (metis f simple_function_def space_borel space_completion space_lborel) show "(λi. f i x) ⇢ Sup (range f) x" for x proof - have "incseq (λi. f i x)" using ‹incseq f› apply (auto simp: incseq_def) by (simp add: le_funD) then show ?thesis by (metis SUP_apply bdd LIMSEQ_incseq_SUP) qed qed qed lemma lebesgue_measurable_imp_measurable_on_nnreal: fixes u :: "'a::euclidean_space ⇒ real" assumes "u ∈ borel_measurable lebesgue" "⋀x. u x ≥ 0""S ∈ sets lebesgue" shows "u measurable_on S" unfolding measurable_on_UNIV [symmetric, of u] using assms by (auto intro: lebesgue_measurable_imp_measurable_on_nnreal_UNIV) lemma lebesgue_measurable_imp_measurable_on_real: fixes u :: "'a::euclidean_space ⇒ real" assumes u: "u ∈ borel_measurable lebesgue" and S: "S ∈ sets lebesgue" shows "u measurable_on S" proof - let ?f = "λx. ¦u x¦ + u x" let ?g = "λx. ¦u x¦ - u x" have "?f measurable_on S" "?g measurable_on S" using S u by (auto intro: lebesgue_measurable_imp_measurable_on_nnreal) then have "(λx. (?f x - ?g x) / 2) measurable_on S" using measurable_on_cdivide measurable_on_diff by blast then show ?thesis by auto qed proposition lebesgue_measurable_imp_measurable_on: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes f: "f ∈ borel_measurable lebesgue" and S: "S ∈ sets lebesgue" shows "f measurable_on S" unfolding measurable_on_componentwise [of f] proof fix i::'b assume "i ∈ Basis" have "(λx. (f x ∙ i)) ∈ borel_measurable lebesgue" using ‹i ∈ Basis› borel_measurable_euclidean_space f by blast then have "(λx. (f x ∙ i)) measurable_on S" using S lebesgue_measurable_imp_measurable_on_real by blast then show "(λx. (f x ∙ i) *⇩_{R}i) measurable_on S" by (intro measurable_on_scaleR measurable_on_const S) qed proposition measurable_on_iff_borel_measurable: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "S ∈ sets lebesgue" shows "f measurable_on S ⟷ f ∈ borel_measurable (lebesgue_on S)" (is "?lhs = ?rhs") proof show "f ∈ borel_measurable (lebesgue_on S)" if "f measurable_on S" using that by (simp add: assms measurable_on_imp_borel_measurable_lebesgue) next assume "f ∈ borel_measurable (lebesgue_on S)" then have "(λa. if a ∈ S then f a else 0) measurable_on UNIV" by (simp add: assms borel_measurable_if lebesgue_measurable_imp_measurable_on) then show "f measurable_on S" using measurable_on_UNIV by blast qed subsection ‹Measurability on generalisations of the binary product› lemma measurable_on_bilinear: fixes h :: "'a::euclidean_space ⇒ 'b::euclidean_space ⇒ 'c::euclidean_space" assumes h: "bilinear h" and f: "f measurable_on S" and g: "g measurable_on S" shows "(λx. h (f x) (g x)) measurable_on S" proof (rule measurable_on_combine [where h = h]) show "continuous_on UNIV (λx. h (fst x) (snd x))" by (simp add: bilinear_continuous_on_compose [OF continuous_on_fst continuous_on_snd h]) show "h 0 0 = 0" by (simp add: bilinear_lzero h) qed (auto intro: assms) lemma borel_measurable_bilinear: fixes h :: "'a::euclidean_space ⇒ 'b::euclidean_space ⇒ 'c::euclidean_space" assumes "bilinear h" "f ∈ borel_measurable (lebesgue_on S)" "g ∈ borel_measurable (lebesgue_on S)" and S: "S ∈ sets lebesgue" shows "(λx. h (f x) (g x)) ∈ borel_measurable (lebesgue_on S)" using assms measurable_on_bilinear [of h f S g] by (simp flip: measurable_on_iff_borel_measurable) lemma absolutely_integrable_bounded_measurable_product: fixes h :: "'a::euclidean_space ⇒ 'b::euclidean_space ⇒ 'c::euclidean_space" assumes "bilinear h" and f: "f ∈ borel_measurable (lebesgue_on S)" "S ∈ sets lebesgue" and bou: "bounded (f ` S)" and g: "g absolutely_integrable_on S" shows "(λx. h (f x) (g x)) absolutely_integrable_on S" proof - obtain B where "B > 0" and B: "⋀x y. norm (h x y) ≤ B * norm x * norm y" using bilinear_bounded_pos ‹bilinear h› by blast obtain C where "C > 0" and C: "⋀x. x ∈ S ⟹ norm (f x) ≤ C" using bounded_pos by (metis bou imageI) show ?thesis proof (rule measurable_bounded_by_integrable_imp_absolutely_integrable [OF _ ‹S ∈ sets lebesgue›]) show "norm (h (f x) (g x)) ≤ B * C * norm(g x)" if "x ∈ S" for x by (meson less_le mult_left_mono mult_right_mono norm_ge_zero order_trans that ‹B > 0› B C) show "(λx. h (f x) (g x)) ∈ borel_measurable (lebesgue_on S)" using ‹bilinear h› f g by (blast intro: borel_measurable_bilinear dest: absolutely_integrable_measurable) show "(λx. B * C * norm(g x)) integrable_on S" using ‹0 < B› ‹0 < C› absolutely_integrable_on_def g by auto qed qed lemma absolutely_integrable_bounded_measurable_product_real: fixes f :: "real ⇒ real" assumes "f ∈ borel_measurable (lebesgue_on S)" "S ∈ sets lebesgue" and "bounded (f ` S)" and "g absolutely_integrable_on S" shows "(λx. f x * g x) absolutely_integrable_on S" using absolutely_integrable_bounded_measurable_product bilinear_times assms by blast lemma borel_measurable_AE: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "f ∈ borel_measurable lebesgue" and ae: "AE x in lebesgue. f x = g x" shows "g ∈ borel_measurable lebesgue" proof - obtain N where N: "N ∈ null_sets lebesgue" "⋀x. x ∉ N ⟹ f x = g x" using ae unfolding completion.AE_iff_null_sets by auto have "f measurable_on UNIV" by (simp add: assms lebesgue_measurable_imp_measurable_on) then have "g measurable_on UNIV" by (metis Diff_iff N measurable_on_spike negligible_iff_null_sets) then show ?thesis using measurable_on_imp_borel_measurable_lebesgue_UNIV by blast qed lemma has_bochner_integral_combine: fixes f :: "real ⇒ 'a::euclidean_space" assumes "a ≤ c" "c ≤ b" and ac: "has_bochner_integral (lebesgue_on {a..c}) f i" and cb: "has_bochner_integral (lebesgue_on {c..b}) f j" shows "has_bochner_integral (lebesgue_on {a..b}) f(i + j)" proof - have i: "has_bochner_integral lebesgue (λx. indicator {a..c} x *⇩_{R}f x) i" and j: "has_bochner_integral lebesgue (λx. indicator {c..b} x *⇩_{R}f x) j" using assms by (auto simp: has_bochner_integral_restrict_space) have AE: "AE x in lebesgue. indicat_real {a..c} x *⇩_{R}f x + indicat_real {c..b} x *⇩_{R}f x = indicat_real {a..b} x *⇩_{R}f x" proof (rule AE_I') have eq: "indicat_real {a..c} x *⇩_{R}f x + indicat_real {c..b} x *⇩_{R}f x = indicat_real {a..b} x *⇩_{R}f x" if "x ≠ c" for x using assms that by (auto simp: indicator_def) then show "{x ∈ space lebesgue. indicat_real {a..c} x *⇩_{R}f x + indicat_real {c..b} x *⇩_{R}f x ≠ indicat_real {a..b} x *⇩_{R}f x} ⊆ {c}" by auto qed auto have "has_bochner_integral lebesgue (λx. indicator {a..b} x *⇩_{R}f x) (i + j)" proof (rule has_bochner_integralI_AE [OF has_bochner_integral_add [OF i j] _ AE]) have eq: "indicat_real {a..c} x *⇩_{R}f x + indicat_real {c..b} x *⇩_{R}f x = indicat_real {a..b} x *⇩_{R}f x" if "x ≠ c" for x using assms that by (auto simp: indicator_def) show "(λx. indicat_real {a..b} x *⇩_{R}f x) ∈ borel_measurable lebesgue" proof (rule borel_measurable_AE [OF borel_measurable_add AE]) show "(λx. indicator {a..c} x *⇩_{R}f x) ∈ borel_measurable lebesgue" "(λx. indicator {c..b} x *⇩_{R}f x) ∈ borel_measurable lebesgue" using i j by auto qed qed then show ?thesis by (simp add: has_bochner_integral_restrict_space) qed lemma integrable_combine: fixes f :: "real ⇒ 'a::euclidean_space" assumes "integrable (lebesgue_on {a..c}) f" "integrable (lebesgue_on {c..b}) f" and "a ≤ c" "c ≤ b" shows "integrable (lebesgue_on {a..b}) f" using assms has_bochner_integral_combine has_bochner_integral_iff by blast lemma integral_combine: fixes f :: "real ⇒ 'a::euclidean_space" assumes f: "integrable (lebesgue_on {a..b}) f" and "a ≤ c" "c ≤ b" shows "integral⇧^{L}(lebesgue_on {a..b}) f = integral⇧^{L}(lebesgue_on {a..c}) f + integral⇧^{L}(lebesgue_on {c..b}) f" proof - have i: "has_bochner_integral (lebesgue_on {a..c}) f(integral⇧^{L}(lebesgue_on {a..c}) f)" using integrable_subinterval ‹c ≤ b› f has_bochner_integral_iff by fastforce have j: "has_bochner_integral (lebesgue_on {c..b}) f(integral⇧^{L}(lebesgue_on {c..b}) f)" using integrable_subinterval ‹a ≤ c› f has_bochner_integral_iff by fastforce show ?thesis by (meson ‹a ≤ c› ‹c ≤ b› has_bochner_integral_combine has_bochner_integral_iff i j) qed lemma has_bochner_integral_null [intro]: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "N ∈ null_sets lebesgue" shows "has_bochner_integral (lebesgue_on N) f 0" unfolding has_bochner_integral_iff ―‹strange that the proof's so long› proof show "integrable (lebesgue_on N) f" proof (subst integrable_restrict_space) show "N ∩ space lebesgue ∈ sets lebesgue" using assms by force show "integrable lebesgue (λx. indicat_real N x *⇩_{R}f x)" proof (rule integrable_cong_AE_imp) show "integrable lebesgue (λx. 0)" by simp show *: "AE x in lebesgue. 0 = indicat_real N x *⇩_{R}f x" using assms by (simp add: indicator_def completion.null_sets_iff_AE eventually_mono) show "(λx. indicat_real N x *⇩_{R}f x) ∈ borel_measurable lebesgue" by (auto intro: borel_measurable_AE [OF _ *]) qed qed show "integral⇧^{L}(lebesgue_on N) f = 0" proof (rule integral_eq_zero_AE) show "AE x in lebesgue_on N. f x = 0" by (rule AE_I' [where N=N]) (auto simp: assms null_setsD2 null_sets_restrict_space) qed qed lemma has_bochner_integral_null_eq[simp]: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "N ∈ null_sets lebesgue" shows "has_bochner_integral (lebesgue_on N) f i ⟷ i = 0" using assms has_bochner_integral_eq by blast end