# Theory Equivalence_Measurable_On_Borel

```(*  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

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, opaque_lifting) 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)"
using fab by (auto simp add: mem_box intro: sum.cong)
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 of_bool_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 of_bool_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 ```