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"
      by (simp add: ‹finite 𝒟›)
    let ?ℰ = "{C. C ∈ 𝒟 - {D} ∧ disjnt C D}"
    obtain 𝒟' where 𝒟'sub: "𝒟' ⊆ ?ℰ" and 𝒟'dis: "pairwise disjnt 𝒟'"
      and 𝒟'm: "measure lebesgue (⋃𝒟') ≥ measure lebesgue (⋃?ℰ) / 3 ^ (DIM('a))"
    proof (rule less.hyps)
      have *: "?ℰ ⊂ 𝒟"
        using ‹D ∈ 𝒟› by auto
      then show "card ?ℰ < card 𝒟" "finite ?ℰ"
        by (auto simp: ‹finite 𝒟› psubset_card_mono)
      show "∃k a b. D = cbox a b ∧ (∀i∈Basis. b ∙ i - a ∙ i = k)" if "D ∈ ?ℰ" for D
        using less.prems(3) that by auto
    qed
    then have [simp]: "⋃𝒟' - D = ⋃𝒟'"
      by (auto simp: disjnt_iff)
    show ?thesis
    proof (rule less.prems)
      show "insert D 𝒟' ⊆ 𝒟"
        using 𝒟'sub ‹D ∈ 𝒟› by blast
      show "disjoint (insert D 𝒟')"
        using 𝒟'dis 𝒟'sub by (fastforce simp add: pairwise_def disjnt_sym)
      obtain a3 b3 where  m3: "content (cbox a3 b3) = 3 ^ DIM('a) * measure lebesgue D"
        and sub3: "⋀C. ⟦C ∈ 𝒟; ¬ disjnt C D⟧ ⟹ C ⊆ cbox a3 b3"
      proof -
        obtain k a b where ab: "D = cbox a b" and k: "⋀i. i ∈ Basis ⟹ b∙i - a∙i = k"
          using less.prems ‹D ∈ 𝒟› by meson
        then have eqk: "⋀i. i ∈ Basis ⟹ a ∙ i ≤ b ∙ i ⟷ k ≥ 0"
          by force
        show thesis
        proof
          let ?a = "(a + b) /⇩R 2 - (3/2) *⇩R (b - a)"
          let ?b = "(a + b) /⇩R 2 + (3/2) *⇩R (b - a)"
          have eq: "(∏i∈Basis. b ∙ i * 3 - a ∙ i * 3) = (∏i∈Basis. b ∙ i - a ∙ i) * 3 ^ DIM('a)"
            by (simp add: comm_monoid_mult_class.prod.distrib flip: left_diff_distrib inner_diff_left)
          show "content (cbox ?a ?b) = 3 ^ DIM('a) * measure lebesgue D"
            by (simp add: content_cbox_if box_eq_empty algebra_simps eq ab k)
          show "C ⊆ cbox ?a ?b" if "C ∈ 𝒟" and CD: "¬ disjnt C D" for C
          proof -
            obtain k' a' b' where ab': "C = cbox a' b'" and k': "⋀i. i ∈ Basis ⟹ b'∙i - a'∙i = k'"
              using less.prems ‹C ∈ 𝒟› by meson
            then have eqk': "⋀i. i ∈ Basis ⟹ a' ∙ i ≤ b' ∙ i ⟷ k' ≥ 0"
              by force
            show ?thesis
            proof (clarsimp simp add: disjoint_interval disjnt_def ab ab' not_less subset_box algebra_simps)
              show "a ∙ i * 2 ≤ a' ∙ i + b ∙ i ∧ a ∙ i + b' ∙ i ≤ b ∙ i * 2"
                if * [rule_format]: "∀j∈Basis. a' ∙ j ≤ b' ∙ j" and "i ∈ Basis" for i
              proof -
                have "a' ∙ i ≤ b' ∙ i ∧ a ∙ i ≤ b ∙ i ∧ a ∙ i ≤ b' ∙ i ∧ a' ∙ i ≤ b ∙ i"
                  using ‹i ∈ Basis› CD by (simp_all add: disjoint_interval disjnt_def ab ab' not_less)
                then show ?thesis
                  using D [OF ‹C ∈ 𝒟›] ‹i ∈ Basis›
                  apply (simp add: ab ab' k k' eqk eqk' content_cbox_cases)
                  using k k' by fastforce
              qed
            qed
          qed
        qed
      qed
      have 𝒟lm: "⋀D. D ∈ 𝒟 ⟹ D ∈ lmeasurable"
        using less.prems(3) by blast
      have "measure lebesgue (⋃𝒟)  ≤ measure lebesgue (cbox a3 b3 ∪ (⋃𝒟 - cbox a3 b3))"
      proof (rule measure_mono_fmeasurable)
        show "⋃𝒟 ∈ sets lebesgue"
          using 𝒟lm ‹finite 𝒟› by blast
        show "cbox a3 b3 ∪ (⋃𝒟 - cbox a3 b3) ∈ lmeasurable"
          by (simp add: 𝒟lm fmeasurable.Un fmeasurable.finite_Union less.prems(2) subset_eq)
      qed auto
      also have "… = content (cbox a3 b3) + measure lebesgue (⋃𝒟 - cbox a3 b3)"
        by (simp add: 𝒟lm fmeasurable.finite_Union less.prems(2) measure_Un2 subsetI)
      also have "… ≤ (measure lebesgue D + measure lebesgue (⋃𝒟')) * 3 ^ DIM('a)"
      proof -
        have "(⋃𝒟 - cbox a3 b3) ⊆ ⋃?ℰ"
          using sub3 by fastforce
        then have "measure lebesgue (⋃𝒟 - cbox a3 b3) ≤ measure lebesgue (⋃?ℰ)"
        proof (rule measure_mono_fmeasurable)
          show "⋃ 𝒟 - cbox a3 b3 ∈ sets lebesgue"
            by (simp add: 𝒟lm fmeasurableD less.prems(2) sets.Diff sets.finite_Union subsetI)
          show "⋃ {C ∈ 𝒟 - {D}. disjnt C D} ∈ lmeasurable"
            using 𝒟lm less.prems(2) by auto
        qed
        then have "measure lebesgue (⋃𝒟 - cbox a3 b3) / 3 ^ DIM('a) ≤ measure lebesgue (⋃ 𝒟')"
          using 𝒟'm by (simp add: field_split_simps)
        then show ?thesis
          by (simp add: m3 field_simps)
      qed
      also have "… ≤ measure lebesgue (⋃(insert D 𝒟')) * 3 ^ DIM('a)"
      proof (simp add: 𝒟lm ‹D ∈ 𝒟›)
        show "measure lebesgue D + measure lebesgue (⋃𝒟') ≤ measure lebesgue (D ∪ ⋃ 𝒟')"
        proof (subst measure_Un2)
          show "⋃ 𝒟' ∈ lmeasurable"
            by (meson 𝒟lm ‹insert D 𝒟' ⊆ 𝒟› fmeasurable.finite_Union less.prems(2) finite_subset subset_eq subset_insertI)
          show "measure lebesgue D + measure lebesgue (⋃ 𝒟') ≤ measure lebesgue D + measure lebesgue (⋃ 𝒟' - D)"
            using ‹insert D 𝒟' ⊆ 𝒟› infinite_super less.prems(2) by force
        qed (simp add: 𝒟lm ‹D ∈ 𝒟›)
      qed
      finally show "measure lebesgue (⋃𝒟) / 3 ^ DIM('a) ≤ measure lebesgue (⋃(insert D 𝒟'))"
        by (simp add: field_split_simps)
    qed
  qed
qed


subsection‹A differentiability-like property of the indefinite integral.        ›

proposition integrable_ccontinuous_explicit:
  fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
  assumes "⋀a b::'a. f integrable_on cbox a b"
  obtains N where
       "negligible N"
       "⋀x e. ⟦x ∉ N; 0 < e⟧ ⟹
               ∃d>0. ∀h. 0 < h ∧ h < d ⟶
                         norm(integral (cbox x (x + h *⇩R One)) f /⇩R h ^ DIM('a) - f x) < e"
proof -
  define BOX where "BOX ≡ λh. λx::'a. cbox x (x + h *⇩R One)"
  define BOX2 where "BOX2 ≡ λh. λx::'a. cbox (x - h *⇩R One) (x + h *⇩R One)"
  define i where "i ≡ λh x. integral (BOX h x) f /⇩R h ^ DIM('a)"
  define Ψ where "Ψ ≡ λx r. ∀d>0. ∃h. 0 < h ∧ h < d ∧ r ≤ norm(i h x - f x)"
  let ?N = "{x. ∃e>0. Ψ x e}"
  have "∃N. negligible N ∧ (∀x e. x ∉ N ∧ 0 < e ⟶ ¬ Ψ x e)"
  proof (rule exI ; intro conjI allI impI)
    let ?M =  "⋃n. {x. Ψ x (inverse(real n + 1))}"
    have "negligible ({x. Ψ x μ} ∩ cbox a b)"
      if "μ > 0" for a b μ
    proof (cases "negligible(cbox a b)")
      case True
      then show ?thesis
        by (simp add: negligible_Int)
    next
      case False
      then have "box a b ≠ {}"
        by (simp add: negligible_interval)
      then have ab: "⋀i. i ∈ Basis ⟹ a∙i < b∙i"
        by (simp add: box_ne_empty)
      show ?thesis
        unfolding negligible_outer_le
      proof (intro allI impI)
        fix e::real
        let ?ee = "(e * μ) / 2 / 6 ^ (DIM('a))"
        assume "e > 0"
        then have gt0: "?ee > 0"
          using ‹μ > 0› by auto
        have f': "f integrable_on cbox (a - One) (b + One)"
          using assms by blast
        obtain γ where "gauge γ"
          and γ: "⋀p. ⟦p tagged_partial_division_of (cbox (a - One) (b + One)); γ fine p⟧
                    ⟹ (∑(x, k)∈p. norm (content k *⇩R f x - integral k f)) < ?ee"
          using Henstock_lemma [OF f' gt0] that by auto
        let ?E = "{x. x ∈ cbox a b ∧ Ψ x μ}"
        have "∃h>0. BOX h x ⊆ γ x ∧
                    BOX h x ⊆ cbox (a - One) (b + One) ∧ μ ≤ norm (i h x - f x)"
          if "x ∈ cbox a b" "Ψ x μ" for x
        proof -
          obtain d where "d > 0" and d: "ball x d ⊆ γ x"
            using gaugeD [OF ‹gauge γ›, of x] openE by blast
          then obtain h where "0 < h" "h < 1" and hless: "h < d / real DIM('a)"
                          and mule: "μ ≤ norm (i h x - f x)"
            using ‹Ψ x μ› [unfolded Ψ_def, rule_format, of "min 1 (d / DIM('a))"]
            by auto
          show ?thesis
          proof (intro exI conjI)
            show "0 < h" "μ ≤ norm (i h x - f x)" by fact+
            have "BOX h x ⊆ ball x d"
            proof (clarsimp simp: BOX_def mem_box dist_norm algebra_simps)
              fix y
              assume "∀i∈Basis. x ∙ i ≤ y ∙ i ∧ y ∙ i ≤ h + x ∙ i"
              then have lt: "¦(x - y) ∙ i¦ < d / real DIM('a)" if "i ∈ Basis" for i
                using hless that by (force simp: inner_diff_left)
              have "norm (x - y) ≤ (∑i∈Basis. ¦(x - y) ∙ i¦)"
                using norm_le_l1 by blast
              also have "… < d"
                using sum_bounded_above_strict [of Basis "λi. ¦(x - y) ∙ i¦" "d / DIM('a)", OF lt]
                by auto
              finally show "norm (x - y) < d" .
            qed
            with d show "BOX h x ⊆ γ x"
              by blast
            show "BOX h x ⊆ cbox (a - One) (b + One)"
              using that ‹h < 1›
              by (force simp: BOX_def mem_box algebra_simps intro: subset_box_imp)
          qed
        qed
        then obtain η where h0: "⋀x. x ∈ ?E ⟹ η x > 0"
          and BOX_γ: "⋀x. x ∈ ?E ⟹ BOX (η x) x ⊆ γ x"
          and "⋀x. x ∈ ?E ⟹ BOX (η x) x ⊆ cbox (a - One) (b + One) ∧ μ ≤ norm (i (η x) x - f x)"
          by simp metis
        then have BOX_cbox: "⋀x. x ∈ ?E ⟹ BOX (η x) x ⊆ cbox (a - One) (b + One)"
             and μ_le: "⋀x. x ∈ ?E ⟹ μ ≤ norm (i (η x) x - f x)"
          by blast+
        define γ' where "γ' ≡ λx. if x ∈ cbox a b ∧ Ψ x μ then ball x (η x) else γ x"
        have "gauge γ'"
          using ‹gauge γ› by (auto simp: h0 gauge_def γ'_def)
        obtain 𝒟 where "countable 𝒟"
          and 𝒟: "⋃𝒟 ⊆ cbox a b"
          "⋀K. K ∈ 𝒟 ⟹ interior K ≠ {} ∧ (∃c d. K = cbox c d)"
          and Dcovered: "⋀K. K ∈ 𝒟 ⟹ ∃x. x ∈ cbox a b ∧ Ψ x μ ∧ x ∈ K ∧ K ⊆ γ' x"
          and subUD: "?E ⊆ ⋃𝒟"
          by (rule covering_lemma [of ?E a b γ']) (simp_all add: Bex_def ‹box a b ≠ {}› ‹gauge γ'›)
        then have "𝒟 ⊆ sets lebesgue"
          by fastforce
        show "∃T. {x. Ψ x μ} ∩ cbox a b ⊆ T ∧ T ∈ lmeasurable ∧ measure lebesgue T ≤ e"
        proof (intro exI conjI)
          show "{x. Ψ x μ} ∩ cbox a b ⊆ ⋃𝒟"
            apply auto
            using subUD by auto
          have mUE: "measure lebesgue (⋃ ℰ) ≤ measure lebesgue (cbox a b)"
            if "ℰ ⊆ 𝒟" "finite ℰ" for ℰ
          proof (rule measure_mono_fmeasurable)
            show "⋃ ℰ ⊆ cbox a b"
              using 𝒟(1) that(1) by blast
            show "⋃ ℰ ∈ sets lebesgue"
              by (metis 𝒟(2) fmeasurable.finite_Union fmeasurableD lmeasurable_cbox subset_eq that)
          qed auto
          then show "⋃𝒟 ∈ lmeasurable"
            by (metis 𝒟(2) ‹countable 𝒟› fmeasurable_Union_bound lmeasurable_cbox)
          then have leab: "measure lebesgue (⋃𝒟) ≤ measure lebesgue (cbox a b)"
            by (meson 𝒟(1) fmeasurableD lmeasurable_cbox measure_mono_fmeasurable)
          obtain ℱ where "ℱ ⊆ 𝒟" "finite ℱ"
            and ℱ: "measure lebesgue (⋃𝒟) ≤ 2 * measure lebesgue (⋃ℱ)"
          proof (cases "measure lebesgue (⋃𝒟) = 0")
            case True
            then show ?thesis
              by (force intro: that [where ℱ = "{}"])
          next
            case False
            obtain ℱ where "ℱ ⊆ 𝒟" "finite ℱ"
              and ℱ: "measure lebesgue (⋃𝒟)/2 < measure lebesgue (⋃ℱ)"
            proof (rule measure_countable_Union_approachable [of 𝒟 "measure lebesgue (⋃𝒟) / 2" "content (cbox a b)"])
              show "countable 𝒟"
                by fact
              show "0 < measure lebesgue (⋃ 𝒟) / 2"
                using False by (simp add: zero_less_measure_iff)
              show Dlm: "D ∈ lmeasurable" if "D ∈ 𝒟" for D
                using 𝒟(2) that by blast
              show "measure lebesgue (⋃ ℱ) ≤ content (cbox a b)"
                if "ℱ ⊆ 𝒟" "finite ℱ" for ℱ
              proof -
                have "measure lebesgue (⋃ ℱ) ≤ measure lebesgue (⋃𝒟)"
                proof (rule measure_mono_fmeasurable)
                  show "⋃ ℱ ⊆ ⋃ 𝒟"
                    by (simp add: Sup_subset_mono ‹ℱ ⊆ 𝒟›)
                  show "⋃ ℱ ∈ sets lebesgue"
                    by (meson Dlm fmeasurableD sets.finite_Union subset_eq that)
                  show "⋃ 𝒟 ∈ lmeasurable"
                    by fact
                qed
                also have "… ≤ measure lebesgue (cbox a b)"
                proof (rule measure_mono_fmeasurable)
                  show "⋃ 𝒟 ∈ sets lebesgue"
                    by (simp add: ‹⋃ 𝒟 ∈ lmeasurable› fmeasurableD)
                qed (auto simp:𝒟(1))
                finally show ?thesis
                  by simp
              qed
            qed auto
            then show ?thesis
              using that by auto
          qed
          obtain tag where tag_in_E: "⋀D. D ∈ 𝒟 ⟹ tag D ∈ ?E"
            and tag_in_self: "⋀D. D ∈ 𝒟 ⟹ tag D ∈ D"
            and tag_sub: "⋀D. D ∈ 𝒟 ⟹ D ⊆ γ' (tag D)"
            using Dcovered by simp metis
          then have sub_ball_tag: "⋀D. D ∈ 𝒟 ⟹ D ⊆ ball (tag D) (η (tag D))"
            by (simp add: γ'_def)
          define Φ where "Φ ≡ λD. BOX (η(tag D)) (tag D)"
          define Φ2 where "Φ2 ≡ λD. BOX2 (η(tag D)) (tag D)"
          obtain 𝒞 where "𝒞 ⊆ Φ2 ` ℱ" "pairwise disjnt 𝒞"
            "measure lebesgue (⋃𝒞) ≥ measure lebesgue (⋃(Φ2`ℱ)) / 3 ^ (DIM('a))"
          proof (rule Austin_Lemma)
            show "finite (Φ2`ℱ)"
              using ‹finite ℱ› by blast
            have "∃k a b. Φ2 D = cbox a b ∧ (∀i∈Basis. b ∙ i - a ∙ i = k)" if "D ∈ ℱ" for D
              apply (rule_tac x="2 * η(tag D)" in exI)
              apply (rule_tac x="tag D - η(tag D) *⇩R One" in exI)
              apply (rule_tac x="tag D + η(tag D) *⇩R One" in exI)
              using that
              apply (auto simp: Φ2_def BOX2_def algebra_simps)
              done
            then show "⋀D. D ∈ Φ2 ` ℱ ⟹ ∃k a b. D = cbox a b ∧ (∀i∈Basis. b ∙ i - a ∙ i = k)"
              by blast
          qed auto
          then obtain 𝒢 where "𝒢 ⊆ ℱ" and disj: "pairwise disjnt (Φ2 ` 𝒢)"
            and "measure lebesgue (⋃(Φ2 ` 𝒢)) ≥ measure lebesgue (⋃(Φ2`ℱ)) / 3 ^ (DIM('a))"
            unfolding Φ2_def subset_image_iff
            by (meson empty_subsetI equals0D pairwise_imageI)
          moreover
          have "measure lebesgue (⋃(Φ2 ` 𝒢)) * 3 ^ DIM('a) ≤ e/2"
          proof -
            have "finite 𝒢"
              using ‹finite ℱ› ‹𝒢 ⊆ ℱ› infinite_super by blast
            have BOX2_m: "⋀x. x ∈ tag ` 𝒢 ⟹ BOX2 (η x) x ∈ lmeasurable"
              by (auto simp: BOX2_def)
            have BOX_m: "⋀x. x ∈ tag ` 𝒢 ⟹ BOX (η x) x ∈ lmeasurable"
              by (auto simp: BOX_def)
            have BOX_sub: "BOX (η x) x ⊆ BOX2 (η x) x" for x
              by (auto simp: BOX_def BOX2_def subset_box algebra_simps)
            have DISJ2: "BOX2 (η (tag X)) (tag X) ∩ BOX2 (η (tag Y)) (tag Y) = {}"
              if "X ∈ 𝒢" "Y ∈ 𝒢" "tag X ≠ tag Y" for X Y
            proof -
              obtain i where i: "i ∈ Basis" "tag X ∙ i ≠ tag Y ∙ i"
                using ‹tag X ≠ tag Y› by (auto simp: euclidean_eq_iff [of "tag X"])
              have XY: "X ∈ 𝒟" "Y ∈ 𝒟"
                using ‹ℱ ⊆ 𝒟› ‹𝒢 ⊆ ℱ› that by auto
              then have "0 ≤ η (tag X)" "0 ≤ η (tag Y)"
                by (meson h0 le_cases not_le tag_in_E)+
              with XY i have "BOX2 (η (tag X)) (tag X) ≠ BOX2 (η (tag Y)) (tag Y)"
                unfolding eq_iff
                by (fastforce simp add: BOX2_def subset_box algebra_simps)
              then show ?thesis
                using disj that by (auto simp: pairwise_def disjnt_def Φ2_def)
            qed
            then have BOX2_disj: "pairwise (λx y. negligible (BOX2 (η x) x ∩ BOX2 (η y) y)) (tag ` 𝒢)"
              by (simp add: pairwise_imageI)
            then have BOX_disj: "pairwise (λx y. negligible (BOX (η x) x ∩ BOX (η y) y)) (tag ` 𝒢)"
            proof (rule pairwise_mono)
              show "negligible (BOX (η x) x ∩ BOX (η y) y)"
                if "negligible (BOX2 (η x) x ∩ BOX2 (η y) y)" for x y
                by (metis (no_types, 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 ` 𝒢"
              by (simp add: image_comp)
            have "measure lebesgue (BOX2 (η t) t) * 3 ^ DIM('a)
                = measure lebesgue (BOX (η t) t) * (2*3) ^ DIM('a)"
              if "t ∈ tag ` 𝒢" for t
            proof -
              have "content (cbox (t - η t *⇩R One) (t + η t *⇩R One))
                  = content (cbox t (t + η t *⇩R One)) * 2 ^ DIM('a)"
                using that by (simp add: algebra_simps content_cbox_if box_eq_empty)
              then show ?thesis
                by (simp add: BOX2_def BOX_def flip: power_mult_distrib)
            qed
            then have "measure lebesgue (⋃(Φ2 ` 𝒢)) * 3 ^ DIM('a) = measure lebesgue (⋃(Φ ` 𝒢)) * 6 ^ DIM('a)"
              unfolding Φ_def Φ2_def eq
              by (simp add: measure_negligible_finite_Union_image
                  ‹finite 𝒢› BOX2_m BOX_m BOX2_disj BOX_disj sum_distrib_right
                  del: UN_simps)
            also have "… ≤ e/2"
            proof -
              have "μ * measure lebesgue (⋃D∈𝒢. Φ D) ≤ μ * (∑D ∈ Φ`𝒢. measure lebesgue D)"
                using ‹μ > 0› ‹finite 𝒢› by (force simp: BOX_m Φ_def fmeasurableD intro: measure_Union_le)
              also have "… = (∑D ∈ Φ`𝒢. measure lebesgue D * μ)"
                by (metis mult.commute sum_distrib_right)
              also have "… ≤ (∑(x, K) ∈ (λD. (tag D, Φ D)) ` 𝒢.  norm (content K *⇩R f x - integral K f))"
              proof (rule sum_le_included; clarify?)
                fix D
                assume "D ∈ 𝒢"
                then have "η (tag D) > 0"
                  using ‹ℱ ⊆ 𝒟› ‹𝒢 ⊆ ℱ› h0 tag_in_E by auto
                then have m_Φ: "measure lebesgue (Φ D) > 0"
                  by (simp add: Φ_def BOX_def algebra_simps)
                have "μ ≤ norm (i (η(tag D)) (tag D) - f(tag D))"
                  using μ_le ‹D ∈ 𝒢› ‹ℱ ⊆ 𝒟› ‹𝒢 ⊆ ℱ› tag_in_E by auto
                also have "… = norm ((content (Φ D) *⇩R f(tag D) - integral (Φ D) f) /⇩R measure lebesgue (Φ D))"
                  using m_Φ
                  unfolding i_def Φ_def BOX_def
                  by (simp add: algebra_simps content_cbox_plus norm_minus_commute)
                finally have "measure lebesgue (Φ D) * μ ≤ norm (content (Φ D) *⇩R f(tag D) - integral (Φ D) f)"
                  using m_Φ by simp (simp add: field_simps)
                then show "∃y∈(λD. (tag D, Φ D)) ` 𝒢.
                        snd y = Φ D ∧ measure lebesgue (Φ D) * μ ≤ (case y of (x, k) ⇒ norm (content k *⇩R f x - integral k f))"
                  using ‹D ∈ 𝒢› by auto
              qed (use ‹finite 𝒢› in auto)
              also have "… < ?ee"
              proof (rule γ)
                show "(λD. (tag D, Φ D)) ` 𝒢 tagged_partial_division_of cbox (a - One) (b + One)"
                  unfolding tagged_partial_division_of_def
                proof (intro conjI allI impI ; clarify ?)
                  show "tag D ∈ Φ D"
                    if "D ∈ 𝒢" for D
                    using that ‹ℱ ⊆ 𝒟› ‹𝒢 ⊆ ℱ› h0 tag_in_E
                    by (auto simp: Φ_def BOX_def mem_box algebra_simps eucl_less_le_not_le in_mono)
                  show "y ∈ cbox (a - One) (b + One)" if "D ∈ 𝒢" "y ∈ Φ D" for D y
                    using that BOX_cbox Φ_def ‹ℱ ⊆ 𝒟› ‹𝒢 ⊆ ℱ› tag_in_E by blast
                  show "tag D = tag E ∧ Φ D = Φ E"
                    if "D ∈ 𝒢" "E ∈ 𝒢" and ne: "interior (Φ D) ∩ interior (Φ E) ≠ {}" for D E
                  proof -
                    have "BOX2 (η (tag D)) (tag D) ∩ BOX2 (η (tag E)) (tag E) = {} ∨ tag E = tag D"
                      using DISJ2 ‹D ∈ 𝒢› ‹E ∈ 𝒢› by force
                    then have "BOX (η (tag D)) (tag D) ∩ BOX (η (tag E)) (tag E) = {} ∨ tag E = tag D"
                      using BOX_sub by blast
                    then show "tag D = tag E ∧ Φ D = Φ E"
                      by (metis Φ_def interior_Int interior_empty ne)
                  qed
                qed (use ‹finite 𝒢› Φ_def BOX_def in auto)
                show "γ fine (λD. (tag D, Φ D)) ` 𝒢"
                  unfolding fine_def Φ_def using BOX_γ ‹ℱ ⊆ 𝒟› ‹𝒢 ⊆ ℱ› tag_in_E by blast
              qed
              finally show ?thesis
                using ‹μ > 0› by (auto simp: field_split_simps)
          qed
            finally show ?thesis .
          qed
          moreover
          have "measure lebesgue (⋃ℱ) ≤ measure lebesgue (⋃(Φ2`ℱ))"
          proof (rule measure_mono_fmeasurable)
            have "D ⊆ ball (tag D) (η(tag D))" if "D ∈ ℱ" for D
              using ‹ℱ ⊆ 𝒟› sub_ball_tag that by blast
            moreover have "ball (tag D) (η(tag D)) ⊆ BOX2 (η (tag D)) (tag D)" if "D ∈ ℱ" for D
            proof (clarsimp simp: Φ2_def BOX2_def mem_box algebra_simps dist_norm)
              fix x and i::'a
              assume "norm (tag D - x) < η (tag D)" and "i ∈ Basis"
              then have "¦tag D ∙ i - x ∙ i¦ ≤ η (tag D)"
                by (metis eucl_less_le_not_le inner_commute inner_diff_right norm_bound_Basis_le)
              then show "tag D ∙ i ≤ x ∙ i + η (tag D) ∧ x ∙ i ≤ η (tag D) + tag D ∙ i"
                by (simp add: abs_diff_le_iff)
            qed
            ultimately show "⋃ℱ ⊆ ⋃(Φ2`ℱ)"
              by (force simp: Φ2_def)
            show "⋃ℱ ∈ sets lebesgue"
              using ‹finite ℱ› ‹𝒟 ⊆ sets lebesgue› ‹ℱ ⊆ 𝒟› by blast
            show "⋃(Φ2`ℱ) ∈ lmeasurable"
              unfolding Φ2_def BOX2_def using ‹finite ℱ› by blast
          qed
          ultimately
          have "measure lebesgue (⋃ℱ) ≤ e/2"
            by (auto simp: field_split_simps)
          then show "measure lebesgue (⋃𝒟) ≤ e"
            using ℱ by linarith
        qed
      qed
    qed
    then have "⋀j. negligible {x. Ψ x (inverse(real j + 1))}"
      using negligible_on_intervals
      by (metis (full_types) inverse_positive_iff_positive le_add_same_cancel1 linorder_not_le nat_le_real_less not_add_less1 of_nat_0)
    then have "negligible ?M"
      by auto
    moreover have "?N ⊆ ?M"
    proof (clarsimp simp: dist_norm)
      fix y e
      assume "0 < e"
        and ye [rule_format]: "Ψ y e"
      then obtain k where k: "0 < k" "inverse (real k + 1) < e"
        by (metis One_nat_def add.commute less_add_same_cancel2 less_imp_inverse_less less_trans neq0_conv of_nat_1 of_nat_Suc reals_Archimedean zero_less_one)
      with ye show "∃n. Ψ y (inverse (real n + 1))"
        apply (rule_tac x=k in exI)
        unfolding Ψ_def
        by (force intro: less_le_trans)
    qed
    ultimately show "negligible ?N"
      by (blast intro: negligible_subset)
    show "¬ Ψ x e" if "x ∉ ?N ∧ 0 < e" for x e
      using that by blast
  qed
  with that show ?thesis
    unfolding i_def BOX_def Ψ_def by (fastforce simp add: not_le)
qed


subsection‹HOL Light measurability›

definition measurable_on :: "('a::euclidean_space ⇒ 'b::real_normed_vector) ⇒ 'a set ⇒ bool"
  (infixr "measurable'_on" 46)
  where "f measurable_on S ≡
        ∃N g. negligible N ∧
              (∀n. continuous_on UNIV (g n)) ∧
              (∀x. x ∉ N ⟶ (λn. g n x) ⇢ (if x ∈ S then f x else 0))"

lemma measurable_on_UNIV:
  "(λx.  if x ∈ S then f x else 0) measurable_on UNIV ⟷ f measurable_on S"
  by (auto simp: measurable_on_def)

lemma measurable_on_spike_set:
  assumes f: "f measurable_on S" and neg: "negligible ((S - T) ∪ (T - S))"
  shows "f measurable_on T"
proof -
  obtain N and F
    where N: "negligible N"
      and conF: "⋀n. continuous_on UNIV (F n)"
      and tendsF: "⋀x. x ∉ N ⟹ (λn. F n x) ⇢ (if x ∈ S then f x else 0)"
    using f by (auto simp: measurable_on_def)
  show ?thesis
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "continuous_on UNIV (λx. F n x)" for n
      by (intro conF continuous_intros)
    show "negligible (N ∪ (S - T) ∪ (T - S))"
      by (metis (full_types) N neg negligible_Un_eq)
    show "(λn. F n x) ⇢ (if x ∈ T then f x else 0)"
      if "x ∉ (N ∪ (S - T) ∪ (T - S))" for x
      using that tendsF [of x] by auto
  qed
qed

text‹ Various common equivalent forms of function measurability.                ›

lemma measurable_on_0 [simp]: "(λx. 0) measurable_on S"
  unfolding measurable_on_def
proof (intro exI conjI allI impI)
  show "(λn. 0) ⇢ (if x ∈ S then 0::'b else 0)" for x
    by force
qed auto

lemma measurable_on_scaleR_const:
  assumes f: "f measurable_on S"
  shows "(λx. c *⇩R f x) measurable_on S"
proof -
  obtain NF and F
    where NF: "negligible NF"
      and conF: "⋀n. continuous_on UNIV (F n)"
      and tendsF: "⋀x. x ∉ NF ⟹ (λn. F n x) ⇢ (if x ∈ S then f x else 0)"
    using f by (auto simp: measurable_on_def)
  show ?thesis
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "continuous_on UNIV (λx. c *⇩R F n x)" for n
      by (intro conF continuous_intros)
    show "(λn. c *⇩R F n x) ⇢ (if x ∈ S then c *⇩R f x else 0)"
      if "x ∉ NF" for x
      using tendsto_scaleR [OF tendsto_const tendsF, of x] that by auto
  qed (auto simp: NF)
qed


lemma measurable_on_cmul:
  fixes c :: real
  assumes "f measurable_on S"
  shows "(λx. c * f x) measurable_on S"
  using measurable_on_scaleR_const [OF assms] by simp

lemma measurable_on_cdivide:
  fixes c :: real
  assumes "f measurable_on S"
  shows "(λx. f x / c) measurable_on S"
proof (cases "c=0")
  case False
  then show ?thesis
    using measurable_on_cmul [of f S "1/c"]
    by (simp add: assms)
qed auto


lemma measurable_on_minus:
   "f measurable_on S ⟹ (λx. -(f x)) measurable_on S"
  using measurable_on_scaleR_const [of f S "-1"] by auto


lemma continuous_imp_measurable_on:
   "continuous_on UNIV f ⟹ f measurable_on UNIV"
  unfolding measurable_on_def
  apply (rule_tac x="{}" in exI)
  apply (rule_tac x="λn. f" in exI, auto)
  done

proposition integrable_subintervals_imp_measurable:
  fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
  assumes "⋀a b. f integrable_on cbox a b"
  shows "f measurable_on UNIV"
proof -
  define BOX where "BOX ≡ λh. λx::'a. cbox x (x + h *⇩R One)"
  define i where "i ≡ λh x. integral (BOX h x) f /⇩R h ^ DIM('a)"
  obtain N where "negligible N"
    and k: "⋀x e. ⟦x ∉ N; 0 < e⟧
            ⟹ ∃d>0. ∀h. 0 < h ∧ h < d ⟶
                  norm (integral (cbox x (x + h *⇩R One)) f /⇩R h ^ DIM('a) - f x) < e"
    using integrable_ccontinuous_explicit assms by blast
  show ?thesis
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "continuous_on UNIV ((λn x. i (inverse(Suc n)) x) n)" for n
    proof (clarsimp simp: continuous_on_iff)
      show "∃d>0. ∀x'. dist x' x < d ⟶ dist (i (inverse (1 + real n)) x') (i (inverse (1 + real n)) x) < e"
        if "0 < e"
        for x e
      proof -
        let ?e = "e / (1 + real n) ^ DIM('a)"
        have "?e > 0"
          using ‹e > 0› by auto
        moreover have "x ∈ cbox (x - 2 *⇩R One) (x + 2 *⇩R One)"
          by (simp add: mem_box inner_diff_left inner_left_distrib)
        moreover have "x + One /⇩R real (Suc n) ∈ cbox (x - 2 *⇩R One) (x + 2 *⇩R One)"
          by (auto simp: mem_box inner_diff_left inner_left_distrib field_simps)
        ultimately obtain δ where "δ > 0"
          and δ: "⋀c' d'. ⟦c' ∈ cbox (x - 2 *⇩R One) (x + 2 *⇩R One);
                           d' ∈ cbox (x - 2 *⇩R One) (x + 2 *⇩R One);
                           norm(c' - x) ≤ δ; norm(d' - (x + One /⇩R Suc n)) ≤ δ⟧
                          ⟹ norm(integral(cbox c' d') f - integral(cbox x (x + One /⇩R Suc n)) f) < ?e"
          by (blast intro: indefinite_integral_continuous [of f _ _ x] assms)
        show ?thesis
        proof (intro exI impI conjI allI)
          show "min δ 1 > 0"
            using ‹δ > 0› by auto
          show "dist (i (inverse (1 + real n)) y) (i (inverse (1 + real n)) x) < e"
            if "dist y x < min δ 1" for y
          proof -
            have no: "norm (y - x) < 1"
              using that by (auto simp: dist_norm)
            have le1: "inverse (1 + real n) ≤ 1"
              by (auto simp: field_split_simps)
            have "norm (integral (cbox y (y + One /⇩R real (Suc n))) f
                - integral (cbox x (x + One /⇩R real (Suc n))) f)
                < e / (1 + real n) ^ DIM('a)"
            proof (rule δ)
              show "y ∈ cbox (x - 2 *⇩R One) (x + 2 *⇩R One)"
                using no by (auto simp: mem_box algebra_simps dest: Basis_le_norm [of _ "y-x"])
              show "y + One /⇩R real (Suc n) ∈ cbox (x - 2 *⇩R One) (x + 2 *⇩R One)"
              proof (simp add: dist_norm mem_box algebra_simps, intro ballI conjI)
                fix i::'a
                assume "i ∈ Basis"
                then have 1: "¦y ∙ i - x ∙ i¦ < 1"
                  by (metis inner_commute inner_diff_right no norm_bound_Basis_lt)
                moreover have "… < (2 + inverse (1 + real n))" "1 ≤ 2 - inverse (1 + real n)"
                  by (auto simp: field_simps)
                ultimately show "x ∙ i ≤ y ∙ i + (2 + inverse (1 + real n))"
                                "y ∙ i + inverse (1 + real n) ≤ x ∙ i + 2"
                  by linarith+
              qed
              show "norm (y - x) ≤ δ" "norm (y + One /⇩R real (Suc n) - (x + One /⇩R real (Suc n))) ≤ δ"
                using that by (auto simp: dist_norm)
            qed
            then show ?thesis
              using that by (simp add: dist_norm i_def BOX_def flip: scaleR_diff_right) (simp add: field_simps)
          qed
        qed
      qed
    qed
    show "negligible N"
      by (simp add: ‹negligible N›)
    show "(λn. i (inverse (Suc n)) x) ⇢ (if x ∈ UNIV then f x else 0)"
      if "x ∉ N" for x
      unfolding lim_sequentially
    proof clarsimp
      show "∃no. ∀n≥no. dist (i (inverse (1 + real n)) x) (f x) < e"
        if "0 < e" for e
      proof -
        obtain d where "d > 0"
          and d: "⋀h. ⟦0 < h; h < d⟧ ⟹
              norm (integral (cbox x (x + h *⇩R One)) f /⇩R h ^ DIM('a) - f x) < e"
          using k [of x e] ‹x ∉ N› ‹0 < e› by blast
        then obtain M where M: "M ≠ 0" "0 < inverse (real M)" "inverse (real M) < d"
          using real_arch_invD by auto
        show ?thesis
        proof (intro exI allI impI)
          show "dist (i (inverse (1 + real n)) x) (f x) < e"
            if "M ≤ n" for n
          proof -
            have *: "0 < inverse (1 + real n)" "inverse (1 + real n) ≤ inverse M"
              using that ‹M ≠ 0› by auto
            show ?thesis
              using that M
              apply (simp add: i_def BOX_def dist_norm)
              apply (blast intro: le_less_trans * d)
              done
          qed
        qed
      qed
    qed
  qed
qed


subsection‹Composing continuous and measurable functions; a few variants›

lemma measurable_on_compose_continuous:
   assumes f: "f measurable_on UNIV" and g: "continuous_on UNIV g"
   shows "(g ∘ f) measurable_on UNIV"
proof -
  obtain N and F
    where "negligible N"
      and conF: "⋀n. continuous_on UNIV (F n)"
      and tendsF: "⋀x. x ∉ N ⟹ (λn. F n x) ⇢ f x"
    using f by (auto simp: measurable_on_def)
  show ?thesis
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "negligible N"
      by fact
    show "continuous_on UNIV (g ∘ (F n))" for n
      using conF continuous_on_compose continuous_on_subset g by blast
    show "(λn. (g ∘ F n) x) ⇢ (if x ∈ UNIV then (g ∘ f) x else 0)"
      if "x ∉ N" for x :: 'a
      using that g tendsF by (auto simp: continuous_on_def intro: tendsto_compose)
  qed
qed

lemma measurable_on_compose_continuous_0:
   assumes f: "f measurable_on S" and g: "continuous_on UNIV g" and "g 0 = 0"
   shows "(g ∘ f) measurable_on S"
proof -
  have f': "(λx. if x ∈ S then f x else 0) measurable_on UNIV"
    using f measurable_on_UNIV by blast
  show ?thesis
    using measurable_on_compose_continuous [OF f' g]
    by (simp add: measurable_on_UNIV o_def if_distrib ‹g 0 = 0› cong: if_cong)
qed


lemma measurable_on_compose_continuous_box:
  assumes fm: "f measurable_on UNIV" and fab: "⋀x. f x ∈ box a b"
    and contg: "continuous_on (box a b) g"
  shows "(g ∘ f) measurable_on UNIV"
proof -
  have "∃γ. (∀n. continuous_on UNIV (γ n)) ∧ (∀x. x ∉ N ⟶ (λn. γ n x) ⇢ g (f x))"
    if "negligible N"
      and conth [rule_format]: "∀n. continuous_on UNIV (λx. h n x)"
      and tends [rule_format]: "∀x. x ∉ N ⟶ (λn. h n x) ⇢ f x"
    for N and h :: "nat ⇒ 'a ⇒ 'b"
  proof -
    define θ where "θ ≡ λn x. (∑i∈Basis. (max (a∙i + (b∙i - a∙i) / real (n+2))
                                            (min ((h n x)∙i)
                                                 (b∙i - (b∙i - a∙i) / real (n+2)))) *⇩R i)"
    have aibi: "⋀i. i ∈ Basis ⟹ a ∙ i < b ∙ i"
      using box_ne_empty(2) fab by auto
    then have *: "⋀i n. i ∈ Basis ⟹ a ∙ i + real n * (a ∙ i) < b ∙ i + real n * (b ∙ i)"
      by (meson add_mono_thms_linordered_field(3) less_eq_real_def mult_left_mono of_nat_0_le_iff)
    show ?thesis
    proof (intro exI conjI allI impI)
      show "continuous_on UNIV (g ∘ (θ n))" for n :: nat
        unfolding θ_def
        apply (intro continuous_on_compose2 [OF contg] continuous_intros conth)
        apply (auto simp: aibi * mem_box less_max_iff_disj min_less_iff_disj field_split_simps)
        done
      show "(λn. (g ∘ θ n) x) ⇢ g (f x)"
        if "x ∉ N" for x
        unfolding o_def
      proof (rule isCont_tendsto_compose [where g=g])
        show "isCont g (f x)"
          using contg fab continuous_on_eq_continuous_at by blast
        have "(λn. θ n x) ⇢ (∑i∈Basis. max (a ∙ i) (min (f x ∙ i) (b ∙ i)) *⇩R i)"
          unfolding θ_def
        proof (intro tendsto_intros ‹x ∉ N› tends)
          fix i::'b
          assume "i ∈ Basis"
          have a: "(λn. a ∙ i + (b ∙ i - a ∙ i) / real n) ⇢ a∙i + 0"
            by (intro tendsto_add lim_const_over_n tendsto_const)
          show "(λn. a ∙ i + (b ∙ i - a ∙ i) / real (n + 2)) ⇢ a ∙ i"
            using LIMSEQ_ignore_initial_segment [where k=2, OF a] by simp
          have b: "(λn. b∙i - (b ∙ i - a ∙ i) / (real n)) ⇢ b∙i - 0"
            by (intro tendsto_diff lim_const_over_n tendsto_const)
          show "(λn. b ∙ i - (b ∙ i - a ∙ i) / real (n + 2)) ⇢ b ∙ i"
            using LIMSEQ_ignore_initial_segment [where k=2, OF b] by simp
        qed
        also have "(∑i∈Basis. max (a ∙ i) (min (f x ∙ i) (b ∙ i)) *⇩R i) = (∑i∈Basis. (f x ∙ i) *⇩R i)"
          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)"
      by (simp add: NF NG)
    show "continuous_on UNIV (λx. (F n x, G n x))" for n
      using conF conG continuous_on_Pair by blast
    show "(λn. (F n x, G n x)) ⇢ (if x ∈ S then (f x, g x) else 0)"
      if "x ∉ NF ∪ NG" for x
      using tendsto_Pair [OF tendsF tendsG, of x x] that unfolding zero_prod_def
      by (simp add: split: if_split_asm)
  qed
qed

lemma measurable_on_combine:
  assumes f: "f measurable_on S" and g: "g measurable_on S"
    and h: "continuous_on UNIV (λx. h (fst x) (snd x))" and "h 0 0 = 0"
  shows "(λx. h (f x) (g x)) measurable_on S"
proof -
  have *: "(λx. h (f x) (g x)) = (λx. h (fst x) (snd x)) ∘ (λx. (f x, g x))"
    by auto
  show ?thesis
    unfolding * by (auto simp: measurable_on_compose_continuous_0 measurable_on_Pair assms)
qed

lemma measurable_on_add:
  assumes f: "f measurable_on S" and g: "g measurable_on S"
  shows "(λx. f x + g x) measurable_on S"
  by (intro continuous_intros measurable_on_combine [OF assms]) auto

lemma measurable_on_diff:
  assumes f: "f measurable_on S" and g: "g measurable_on S"
  shows "(λx. f x - g x) measurable_on S"
  by (intro continuous_intros measurable_on_combine [OF assms]) auto

lemma measurable_on_scaleR:
  assumes f: "f measurable_on S" and g: "g measurable_on S"
  shows "(λx. f x *⇩R g x) measurable_on S"
  by (intro continuous_intros measurable_on_combine [OF assms]) auto

lemma measurable_on_sum:
  assumes "finite I" "⋀i. i ∈ I ⟹ f i measurable_on S"
  shows "(λx. sum  (λi. f i x) I) measurable_on S"
  using assms by (induction I) (auto simp: measurable_on_add)

lemma measurable_on_spike:
  assumes f: "f measurable_on T" and "negligible S" and gf: "⋀x. x ∈ T - S ⟹ g x = f x"
  shows "g measurable_on T"
proof -
  obtain NF and F
    where NF: "negligible NF"
      and conF: "⋀n. continuous_on UNIV (F n)"
      and tendsF: "⋀x. x ∉ NF ⟹ (λn. F n x) ⇢ (if x ∈ T then f x else 0)"
    using f by (auto simp: measurable_on_def)
  show ?thesis
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "negligible (NF ∪ S)"
      by (simp add: NF ‹negligible S›)
    show "⋀x. x ∉ NF ∪ S ⟹ (λn. F n x) ⇢ (if x ∈ T then g x else 0)"
      by (metis (full_types) Diff_iff Un_iff gf tendsF)
  qed (auto simp: conF)
qed

proposition indicator_measurable_on:
  assumes "S ∈ sets lebesgue"
  shows "indicat_real S measurable_on UNIV"
proof -
  { fix n::nat
    let ?ε = "(1::real) / (2 * 2^n)"
    have ε: "?ε > 0"
      by auto
    obtain T where "closed T" "T ⊆ S" "S-T ∈ lmeasurable" and ST: "emeasure lebesgue (S - T) < ?ε"
      by (meson ε assms sets_lebesgue_inner_closed)
    obtain U where "open U" "S ⊆ U" "(U - S) ∈ lmeasurable" and US: "emeasure lebesgue (U - S) < ?ε"
      by (meson ε assms sets_lebesgue_outer_open)
    have eq: "-T ∩ U = (S-T) ∪ (U - S)"
      using ‹T ⊆ S› ‹S ⊆ U› by auto
    have "emeasure lebesgue ((S-T) ∪ (U - S)) ≤ emeasure lebesgue (S - T) + emeasure lebesgue (U - S)"
      using ‹S - T ∈ lmeasurable› ‹U - S ∈ lmeasurable› emeasure_subadditive by blast
    also have "… < ?ε + ?ε"
      using ST US add_mono_ennreal by metis
    finally have le: "emeasure lebesgue (-T ∩ U) < ennreal (1 / 2^n)"
      by (simp add: eq)
    have 1: "continuous_on (T ∪ -U) (indicat_real S)"
      unfolding indicator_def 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
      by (simp add: eventually_mono geq)
  qed
  show ?thesis
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "negligible (limsup E)"
      using negligible_iff_null_sets null by blast
    show "continuous_on UNIV (g n)" for n
      using cont by blast
  qed (use tends in auto)
qed

lemma measurable_on_restrict:
  assumes f: "f measurable_on UNIV" and S: "S ∈ sets lebesgue"
  shows "(λx. if x ∈ S then f x else 0) measurable_on UNIV"
proof -
  have "indicat_real S measurable_on UNIV"
    by (simp add: S indicator_measurable_on)
  then show ?thesis
    using measurable_on_scaleR [OF _ f, of "indicat_real S"]
    by (simp add: indicator_scaleR_eq_if)
qed

lemma measurable_on_const_UNIV: "(λx. k) measurable_on UNIV"
  by (simp add: continuous_imp_measurable_on)

lemma measurable_on_const [simp]: "S ∈ sets lebesgue ⟹ (λx. k) measurable_on S"
  using measurable_on_UNIV measurable_on_const_UNIV measurable_on_restrict by blast

lemma simple_function_indicator_representation_real:
  fixes f ::"'a ⇒ real"
  assumes f: "simple_function M f" and x: "x ∈ space M" and nn: "⋀x. f x ≥ 0"
  shows "f x = (∑y ∈ f ` space M. y * indicator (f -` {y} ∩ space M) x)"
proof -
  have f': "simple_function M (ennreal ∘ f)"
    by (simp add: f)
  have *: "f x =
     enn2real
      (∑y∈ ennreal ` f ` space M.
         y * indicator ((ennreal ∘ f) -` {y} ∩ space M) x)"
    using arg_cong [OF simple_function_indicator_representation [OF f' x], of enn2real, simplified nn o_def] nn
    unfolding o_def image_comp
    by (metis enn2real_ennreal)
  have "enn2real (∑y∈ennreal ` f ` space M. if ennreal (f x) = y ∧ x ∈ space M then y else 0)
      = sum (enn2real ∘ (λy. if ennreal (f x) = y ∧ x ∈ space M then y else 0))
            (ennreal ` f ` space M)"
    by (rule enn2real_sum) auto
  also have "… = sum (enn2real ∘ (λy. if ennreal (f x) = y ∧ x ∈ space M then y else 0) ∘ ennreal)
                   (f ` space M)"
    by (rule sum.reindex) (use nn in ‹auto simp: inj_on_def intro: sum.cong›)
  also have "… = (∑y∈f ` space M. if f x = y ∧ x ∈ space M then y else 0)"
    using nn
    by (auto simp: inj_on_def intro: sum.cong)
  finally show ?thesis
    by (subst *) (simp add: enn2real_sum indicator_def 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
      by (simp add: eq indicator_times_eq_if [where f = "λx. a"] add)
  qed
next
  show "simple_function M (λx. (∑y∈u ` space M. y * indicator (u -` {y} ∩ space M) x))"
    apply (subst simple_function_cong)
    apply (rule simple_function_indicator_representation_real[symmetric])
    apply (auto intro: u nn)
    done
qed fact

proposition simple_function_measurable_on_UNIV:
  fixes f :: "'a::euclidean_space ⇒ real"
  assumes f: "simple_function lebesgue f" and nn: "⋀x. f x ≥ 0"
  shows "f measurable_on UNIV"
  using f
proof (induction f)
  case (cong f g)
  then obtain N where "negligible N" "{x. g x ≠ f x} ⊆ N"
    by (auto simp: eventually_ae_filter_negligible eq_commute)
  then show ?case
    by (blast intro: measurable_on_spike cong)
next
  case (set S)
  then show ?case
    by (simp add: indicator_measurable_on)
next
  case (mult u c)
  then show ?case
    by (simp add: measurable_on_cmul)
  case (add u v)
  then show ?case
    by (simp add: measurable_on_add)
qed (auto simp: nn)

lemma simple_function_lebesgue_if:
  fixes f :: "'a::euclidean_space ⇒ real"
  assumes f: "simple_function lebesgue f" and S: "S ∈ sets lebesgue"
  shows "simple_function lebesgue (λx. if x ∈ S then f x else 0)"
proof -
  have ffin: "finite (range f)" and fsets: "∀x. f -` {f x} ∈ sets lebesgue"
    using f by (auto simp: simple_function_def)
  have "finite (f ` S)"
    by (meson finite_subset subset_image_iff ffin top_greatest)
  moreover have "finite ((λx. 0::real) ` T)" for T :: "'a set"
    by (auto simp: image_def)
  moreover have if_sets: "(λx. if x ∈ S then f x else 0) -` {f a} ∈ sets lebesgue" for a
  proof -
    have *: "(λx. if x ∈ S then f x else 0) -` {f a}
           = (if f a = 0 then -S ∪ f -` {f a} else (f -` {f a}) ∩ S)"
      by (auto simp: split: if_split_asm)
    show ?thesis
      unfolding * by (metis Compl_in_sets_lebesgue S sets.Int sets.Un fsets)
  qed
  moreover have "(λx. if x ∈ S then f x else 0) -` {0} ∈ sets lebesgue"
  proof (cases "0 ∈ range f")
    case True
    then show ?thesis
      by (metis (no_types, lifting) if_sets rangeE)
  next
    case False
    then have "(λx. if x ∈ S then f x else 0) -` {0} = -S"
      by auto
    then show ?thesis
      by (simp add: Compl_in_sets_lebesgue S)
  qed
  ultimately show ?thesis
    by (auto simp: simple_function_def)
qed

corollary simple_function_measurable_on:
  fixes f :: "'a::euclidean_space ⇒ real"
  assumes f: "simple_function lebesgue f" and nn: "⋀x. f x ≥ 0" and S: "S ∈ sets lebesgue"
  shows "f measurable_on S"
  by (simp add: measurable_on_UNIV [symmetric, of f] S f simple_function_lebesgue_if nn simple_function_measurable_on_UNIV)

lemma
  fixes f :: "'a::euclidean_space ⇒ 'b::ordered_euclidean_space"
  assumes f: "f measurable_on S" and g: "g measurable_on S"
  shows measurable_on_sup: "(λx. sup (f x) (g x)) measurable_on S"
  and   measurable_on_inf: "(λx. inf (f x) (g x)) measurable_on S"
proof -
  obtain NF and F
    where NF: "negligible NF"
      and conF: "⋀n. continuous_on UNIV (F n)"
      and tendsF: "⋀x. x ∉ NF ⟹ (λn. F n x) ⇢ (if x ∈ S then f x else 0)"
    using f by (auto simp: measurable_on_def)
  obtain NG and G
    where NG: "negligible NG"
      and conG: "⋀n. continuous_on UNIV (G n)"
      and tendsG: "⋀x. x ∉ NG ⟹ (λn. G n x) ⇢ (if x ∈ S then g x else 0)"
    using g by (auto simp: measurable_on_def)
  show "(λx. sup (f x) (g x)) measurable_on S"
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "continuous_on UNIV (λx. sup (F n x) (G n x))" for n
      unfolding sup_max eucl_sup  by (intro conF conG continuous_intros)
    show "(λn. sup (F n x) (G n x)) ⇢ (if x ∈ S then sup (f x) (g x) else 0)"
      if "x ∉ NF ∪ NG" for x
      using tendsto_sup [OF tendsF tendsG, of x x] that by auto
  qed (simp add: NF NG)
  show "(λx. inf (f x) (g x)) measurable_on S"
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "continuous_on UNIV (λx. inf (F n x) (G n x))" for n
      unfolding inf_min eucl_inf  by (intro conF conG continuous_intros)
    show "(λn. inf (F n x) (G n x)) ⇢ (if x ∈ S then inf (f x) (g x) else 0)"
      if "x ∉ NF ∪ NG" for x
      using tendsto_inf [OF tendsF tendsG, of x x] that by auto
  qed (simp add: NF NG)
qed

proposition measurable_on_componentwise_UNIV:
  "f measurable_on UNIV ⟷ (∀i∈Basis. (λx. (f x ∙ i) *⇩R i) measurable_on UNIV)"
  (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  show ?rhs
  proof
    fix i::'b
    assume "i ∈ Basis"
    have cont: "continuous_on UNIV (λx. (x ∙ i) *⇩R i)"
      by (intro continuous_intros)
    show "(λx. (f x ∙ i) *⇩R i) measurable_on UNIV"
      using measurable_on_compose_continuous [OF L cont]
      by (simp add: o_def)
  qed
next
  assume ?rhs
  then have "∃N g. negligible N ∧
              (∀n. continuous_on UNIV (g n)) ∧
              (∀x. x ∉ N ⟶ (λn. g n x) ⇢ (f x ∙ i) *⇩R i)"
    if "i ∈ Basis" for i
    by (simp add: measurable_on_def that)
  then obtain N g where N: "⋀i. i ∈ Basis ⟹ negligible (N i)"
        and cont: "⋀i n. i ∈ Basis ⟹ continuous_on UNIV (g i n)"
        and tends: "⋀i x. ⟦i ∈ Basis; x ∉ N i⟧ ⟹ (λn. g i n x) ⇢ (f x ∙ i) *⇩R i"
    by metis
  show ?lhs
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "negligible (⋃i ∈ Basis. N i)"
      using N eucl.finite_Basis by blast
    show "continuous_on UNIV (λx. (∑i∈Basis. g i n x))" for n
      by (intro continuous_intros cont)
  next
    fix x
    assume "x ∉ (⋃i ∈ Basis. N i)"
    then have "⋀i. i ∈ Basis ⟹ x ∉ N i"
      by auto
    then have "(λn. (∑i∈Basis. g i n x)) ⇢ (∑i∈Basis. (f x ∙ i) *⇩R i)"
      by (intro tends tendsto_intros)
    then show "(λn. (∑i∈Basis. g i n x)) ⇢ (if x ∈ UNIV then f x else 0)"
      by (simp add: euclidean_representation)
  qed
qed

corollary measurable_on_componentwise:
  "f measurable_on S ⟷ (∀i∈Basis. (λx. (f x ∙ i) *⇩R i) measurable_on S)"
  apply (subst measurable_on_UNIV [symmetric])
  apply (subst measurable_on_componentwise_UNIV)
  apply (simp add: measurable_on_UNIV if_distrib [of "λx. inner x _"] if_distrib [of "λx. scaleR x _"] cong: if_cong)
  done


(*FIXME: avoid duplication of proofs WRT borel_measurable_implies_simple_function_sequence*)
lemma✐‹tag important› borel_measurable_implies_simple_function_sequence_real:
  fixes u :: "'a ⇒ real"
  assumes u[measurable]: "u ∈ borel_measurable M" and nn: "⋀x. u x ≥ 0"
  shows "∃f. incseq f ∧ (∀i. simple_function M (f i)) ∧ (∀x. bdd_above (range (λi. f i x))) ∧
             (∀i x. 0 ≤ f i x) ∧ u = (SUP i. f i)"
proof -
  define f where [abs_def]:
    "f i x = real_of_int (floor ((min i (u x)) * 2^i)) / 2^i" for i x

  have [simp]: "0 ≤ f i x" for i x
    by (auto simp: f_def intro!: divide_nonneg_nonneg mult_nonneg_nonneg nn)

  have *: "2^n * real_of_int x = real_of_int (2^n * x)" for n x
    by simp

  have "real_of_int ⌊real i * 2 ^ i⌋ = real_of_int ⌊i * 2 ^ i⌋" for i
    by (intro arg_cong[where f=real_of_int]) simp
  then have [simp]: "real_of_int