# Theory Equivalence_Measurable_On_Borel

theory Equivalence_Measurable_On_Borel
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"
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
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 𝒟'))"
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
next
case False
then have "box a b ≠ {}"
then have ab: "⋀i. i ∈ Basis ⟹ a∙i < b∙i"
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))"
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 ` 𝒢)"
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 ` 𝒢"
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
‹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"
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
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"]
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"
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 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"
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)"
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
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

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)"
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
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"
then show ?thesis
using measurable_on_scaleR [OF _ f, of "indicat_real S"]
qed

lemma measurable_on_const_UNIV: "(λx. k) measurable_on UNIV"

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)"
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
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
next
case (mult u c)
then show ?case
then show ?case
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
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
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

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]
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
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)"
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"
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"
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
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
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
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
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)"
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"
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)
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"
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"
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
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
```