Theory HOL-Analysis.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 ⌊real i * 2 ^ iβŒ‹ = i * 2 ^ i" for i
    unfolding floor_of_nat by simp

  have bdd: "bdd_above (range (Ξ»i. f i x))" for x
    by (rule bdd_aboveI [where M = "u x"]) (auto simp: f_def field_simps min_def)

  have "incseq f"
  proof (intro monoI le_funI)
    fix m n :: nat and x assume "m ≀ n"
    moreover
    { fix d :: nat
      have "⌊2^d::realβŒ‹ * ⌊2^m * (min (of_nat m) (u x))βŒ‹ ≀ ⌊2^d * (2^m * (min (of_nat m) (u x)))βŒ‹"
        by (rule le_mult_floor) (auto simp: nn)
      also have "… ≀ ⌊2^d * (2^m *  (min (of_nat d + of_nat m) (u x)))βŒ‹"
        by (intro floor_mono mult_mono min.mono)
           (auto simp: nn min_less_iff_disj of_nat_less_top)
      finally have "f m x ≀ f(m + d) x"
        unfolding f_def
        by (auto simp: field_simps power_add * simp del: of_int_mult) }
    ultimately show "f m x ≀ f n x"
      by (auto simp: le_iff_add)
  qed
  then have inc_f: "incseq (Ξ»i. f i x)" for x
    by (auto simp: incseq_def le_fun_def)
  moreover
  have "simple_function M (f i)" for i
  proof (rule simple_function_borel_measurable)
    have "⌊(min (of_nat i) (u x)) * 2 ^ iβŒ‹ ≀ ⌊int i * 2 ^ iβŒ‹" for x
      by (auto split: split_min intro!: floor_mono)
    then have "f i ` space M βŠ† (Ξ»n. real_of_int n / 2^i) ` {0 .. of_nat i * 2^i}"
      unfolding floor_of_int by (auto simp: f_def nn intro!: imageI)
    then show "finite (f i ` space M)"
      by (rule finite_subset) auto
    show "f i ∈ borel_measurable M"
      unfolding f_def enn2real_def by measurable
  qed
  moreover
  { fix x
    have "(SUP i. (f i x)) = u x"
    proof -
      obtain n where "u x ≀ of_nat n" using real_arch_simple by auto
      then have min_eq_r: "βˆ€F i in sequentially. min (real i) (u x) = u x"
        by (auto simp: eventually_sequentially intro!: exI[of _ n] split: split_min)
      have "(Ξ»i. real_of_int ⌊min (real i) (u x) * 2^iβŒ‹ / 2^i) β‡’ u x"
      proof (rule tendsto_sandwich)
        show "(Ξ»n. u x - (1/2)^n) β‡’ u x"
          by (auto intro!: tendsto_eq_intros LIMSEQ_power_zero)
        show "βˆ€F n in sequentially. real_of_int ⌊min (real n) (u x) * 2 ^ nβŒ‹ / 2 ^ n ≀ u x"
          using min_eq_r by eventually_elim (auto simp: field_simps)
        have *: "u x * (2 ^ n * 2 ^ n) ≀ 2^n + 2^n * real_of_int ⌊u x * 2 ^ nβŒ‹" for n
          using real_of_int_floor_ge_diff_one[of "u x * 2^n", THEN mult_left_mono, of "2^n"]
          by (auto simp: field_simps)
        show "βˆ€F n in sequentially. u x - (1/2)^n ≀ real_of_int ⌊min (real n) (u x) * 2 ^ nβŒ‹ / 2 ^ n"
          using min_eq_r by eventually_elim (insert *, auto simp: field_simps)
      qed auto
      then have "(Ξ»i. (f i x)) β‡’ u x"
        by (simp add: f_def)
      from LIMSEQ_unique LIMSEQ_incseq_SUP [OF bdd inc_f] this
      show ?thesis
        by blast
    qed }
  ultimately show ?thesis
    by (intro exI [of _ "Ξ»i x. f i x"]) (auto simp: β€Ήincseq fβ€Ί bdd image_comp)
qed


lemma homeomorphic_open_interval_UNIV:
  fixes a b:: real
  assumes "a < b"
  shows "{a<..<b} homeomorphic (UNIV::real set)"
proof -
  have "{a<..<b} = ball ((b+a) / 2) ((b-a) / 2)"
    using assms
    by (auto simp: dist_real_def abs_if field_split_simps split: if_split_asm)
  then show ?thesis
    by (simp add: homeomorphic_ball_UNIV assms)
qed

proposition homeomorphic_box_UNIV:
  fixes a b:: "'a::euclidean_space"
  assumes "box a b β‰  {}"
  shows "box a b homeomorphic (UNIV::'a set)"
proof -
  have "{a βˆ™ i <..<b βˆ™ i} homeomorphic (UNIV::real set)" if "i ∈ Basis" for i
    using assms box_ne_empty that by (blast intro: homeomorphic_open_interval_UNIV)
  then have "βˆƒf g. (βˆ€x. a βˆ™ i < x ∧ x < b βˆ™ i ⟢ g (f x) = x) ∧
                   (βˆ€y. a βˆ™ i < g y ∧ g y < b βˆ™ i ∧ f(g y) = y) ∧
                   continuous_on {a βˆ™ i<..<b βˆ™ i} f ∧
                   continuous_on (UNIV::real set) g"
    if "i ∈ Basis" for i
    using that by (auto simp: homeomorphic_minimal mem_box Ball_def)
  then obtain f g where gf: "β‹€i x. ⟦i ∈ Basis; a βˆ™ i < x; x < b βˆ™ i⟧ ⟹ g i (f i x) = x"
              and fg: "β‹€i y. i ∈ Basis ⟹ a βˆ™ i < g i y ∧ g i y < b βˆ™ i ∧ f i (g i y) = y"
              and contf: "β‹€i. i ∈ Basis ⟹ continuous_on {a βˆ™ i<..<b βˆ™ i} (f i)"
              and contg: "β‹€i. i ∈ Basis ⟹ continuous_on (UNIV::real set) (g i)"
    by metis
  define F where "F ≑ Ξ»x. βˆ‘i∈Basis. (f i (x βˆ™ i)) *R i"
  define G where "G ≑ Ξ»x. βˆ‘i∈Basis. (g i (x βˆ™ i)) *R i"
  show ?thesis
    unfolding homeomorphic_minimal
  proof (intro exI conjI ballI)
    show "G y ∈ box a b" for y
      using fg by (simp add: G_def mem_box)
    show "G (F x) = x" if "x ∈ box a b" for x
      using that by (simp add: F_def G_def gf mem_box euclidean_representation)
    show "F (G y) = y" for y
      by (simp add: F_def G_def fg mem_box euclidean_representation)
    show "continuous_on (box a b) F"
      unfolding F_def
    proof (intro continuous_intros continuous_on_compose2 [OF contf continuous_on_inner])
      show "(Ξ»x. x βˆ™ i) ` box a b βŠ† {a βˆ™ i<..<b βˆ™ i}" if "i ∈ Basis" for i
        using that by (auto simp: mem_box)
    qed
    show "continuous_on UNIV G"
      unfolding G_def
      by (intro continuous_intros continuous_on_compose2 [OF contg continuous_on_inner]) auto
  qed auto
qed



lemma diff_null_sets_lebesgue: "⟦N ∈ null_sets (lebesgue_on S); X-N ∈ sets (lebesgue_on S); N βŠ† X⟧
    ⟹ X ∈ sets (lebesgue_on S)"
  by (metis Int_Diff_Un inf.commute inf.orderE null_setsD2 sets.Un)

lemma borel_measurable_diff_null:
  fixes f :: "'a::euclidean_space β‡’ 'b::euclidean_space"
  assumes N: "N ∈ null_sets (lebesgue_on S)" and S: "S ∈ sets lebesgue"
  shows "f ∈ borel_measurable (lebesgue_on (S-N)) ⟷ f ∈ borel_measurable (lebesgue_on S)"
  unfolding in_borel_measurable space_lebesgue_on sets_restrict_UNIV
proof (intro ball_cong iffI)
  show "f -` T ∩ S ∈ sets (lebesgue_on S)"
    if "f -` T ∩ (S-N) ∈ sets (lebesgue_on (S-N))" for T
  proof -
    have "N ∩ S = N"
      by (metis N S inf.orderE null_sets_restrict_space)
    moreover have "N ∩ S ∈ sets lebesgue"
      by (metis N S inf.orderE null_setsD2 null_sets_restrict_space)
    moreover have "f -` T ∩ S ∩ (f -` T ∩ N) ∈ sets lebesgue"
      by (metis N S completion.complete inf.absorb2 inf_le2 inf_mono null_sets_restrict_space)
    ultimately show ?thesis
      by (metis Diff_Int_distrib Int_Diff_Un S inf_le2 sets.Diff sets.Un sets_restrict_space_iff space_lebesgue_on space_restrict_space that)
  qed
  show "f -` T ∩ (S-N) ∈ sets (lebesgue_on (S-N))"
    if "f -` T ∩ S ∈ sets (lebesgue_on S)" for T
  proof -
    have "(S - N) ∩ f -` T = (S - N) ∩ (f -` T ∩ S)"
      by blast
    then have "(S - N) ∩ f -` T ∈ sets.restricted_space lebesgue (S - N)"
      by (metis S image_iff sets.Int_space_eq2 sets_restrict_space_iff that)
    then show ?thesis
      by (simp add: inf.commute sets_restrict_space)
  qed
qed auto

lemma lebesgue_measurable_diff_null:
  fixes f :: "'a::euclidean_space β‡’ 'b::euclidean_space"
  assumes "N ∈ null_sets lebesgue"
  shows "f ∈ borel_measurable (lebesgue_on (-N)) ⟷ f ∈ borel_measurable lebesgue"
  by (simp add: Compl_eq_Diff_UNIV assms borel_measurable_diff_null lebesgue_on_UNIV_eq)



proposition measurable_on_imp_borel_measurable_lebesgue_UNIV:
  fixes f :: "'a::euclidean_space β‡’ 'b::euclidean_space"
  assumes "f measurable_on UNIV"
  shows "f ∈ borel_measurable lebesgue"
proof -
  obtain N and F
    where NF: "negligible N"
      and conF: "β‹€n. continuous_on UNIV (F n)"
      and tendsF: "β‹€x. x βˆ‰ N ⟹ (Ξ»n. F n x) β‡’ f x"
    using assms by (auto simp: measurable_on_def)
  obtain N where "N ∈ null_sets lebesgue" "f ∈ borel_measurable (lebesgue_on (-N))"
  proof
    show "f ∈ borel_measurable (lebesgue_on (- N))"
    proof (rule borel_measurable_LIMSEQ_metric)
      show "F i ∈ borel_measurable (lebesgue_on (- N))" for i
        by (meson Compl_in_sets_lebesgue NF conF continuous_imp_measurable_on_sets_lebesgue continuous_on_subset negligible_imp_sets subset_UNIV)
      show "(Ξ»i. F i x) β‡’ f x" if "x ∈ space (lebesgue_on (- N))" for x
        using that
        by (simp add: tendsF)
    qed
    show "N ∈ null_sets lebesgue"
      using NF negligible_iff_null_sets by blast
  qed
  then show ?thesis
    using lebesgue_measurable_diff_null by blast
qed

corollary measurable_on_imp_borel_measurable_lebesgue:
  fixes f :: "'a::euclidean_space β‡’ 'b::euclidean_space"
  assumes "f measurable_on S" and S: "S ∈ sets lebesgue"
  shows "f ∈ borel_measurable (lebesgue_on S)"
proof -
  have "(λx. if x ∈ S then f x else 0) measurable_on UNIV"
    using assms(1) measurable_on_UNIV by blast
  then show ?thesis
    by (simp add: borel_measurable_if_D measurable_on_imp_borel_measurable_lebesgue_UNIV)
qed


proposition measurable_on_limit:
  fixes f :: "nat β‡’ 'a::euclidean_space β‡’ 'b::euclidean_space"
  assumes f: "β‹€n. f n measurable_on S" and N: "negligible N"
    and lim: "β‹€x. x ∈ S - N ⟹ (Ξ»n. f n x) β‡’ g x"
  shows "g measurable_on S"
proof -
  have "box (0::'b) One homeomorphic (UNIV::'b set)"
    by (simp add: homeomorphic_box_UNIV)
  then obtain h h':: "'bβ‡’'b" where hh': "β‹€x. x ∈ box 0 One ⟹ h (h' x) = x"
                  and h'im:  "h' ` box 0 One = UNIV"
                  and conth: "continuous_on UNIV h"
                  and conth': "continuous_on (box 0 One) h'"
                  and h'h:   "β‹€y. h' (h y) = y"
                  and rangeh: "range h = box 0 One"
    by (auto simp: homeomorphic_def homeomorphism_def)
  have "norm y ≀ DIM('b)" if y: "y ∈ box 0 One" for y::'b
  proof -
    have y01: "0 < y βˆ™ i" "y βˆ™ i < 1" if "i ∈ Basis" for i
      using that y by (auto simp: mem_box)
    have "norm y ≀ (βˆ‘i∈Basis. Β¦y βˆ™ iΒ¦)"
      using norm_le_l1 by blast
    also have "… ≀ (βˆ‘i::'b∈Basis. 1)"
    proof (rule sum_mono)
      show "Β¦y βˆ™ iΒ¦ ≀ 1" if "i ∈ Basis" for i
        using y01 that by fastforce
    qed
    also have "… ≀ DIM('b)"
      by auto
    finally show ?thesis .
  qed
  then have norm_le: "norm(h y) ≀ DIM('b)" for y
    by (metis UNIV_I image_eqI rangeh)
  have "(h' ∘ (h ∘ (λx. if x ∈ S then g x else 0))) measurable_on UNIV"
  proof (rule measurable_on_compose_continuous_box)
    let ?Ο‡ =  "h ∘ (Ξ»x. if x ∈ S then g x else 0)"
    let ?f = "λn. h ∘ (λx. if x ∈ S then f n x else 0)"
    show "?Ο‡ measurable_on UNIV"
    proof (rule integrable_subintervals_imp_measurable)
      show "?Ο‡ integrable_on cbox a b" for a b
      proof (rule integrable_spike_set)
        show "?Ο‡ integrable_on (cbox a b - N)"
        proof (rule dominated_convergence_integrable)
          show const: "(Ξ»x. DIM('b)) integrable_on cbox a b - N"
            by (simp add: N has_integral_iff integrable_const integrable_negligible integrable_setdiff negligible_diff)
          show "norm ((h ∘ (Ξ»x. if x ∈ S then g x else 0)) x) ≀ DIM('b)" if "x ∈ cbox a b - N" for x
            using that norm_le  by (simp add: o_def)
          show "(Ξ»k. ?f k x) β‡’ ?Ο‡ x" if "x ∈ cbox a b - N" for x
            using that lim [of x] conth
            by (auto simp: continuous_on_def intro: tendsto_compose)
          show "(?f n) absolutely_integrable_on cbox a b - N" for n
          proof (rule measurable_bounded_by_integrable_imp_absolutely_integrable)
            show "?f n ∈ borel_measurable (lebesgue_on (cbox a b - N))"
            proof (rule measurable_on_imp_borel_measurable_lebesgue [OF measurable_on_spike_set])
              show "?f n measurable_on cbox a b"
                unfolding measurable_on_UNIV [symmetric, of _ "cbox a b"]
              proof (rule measurable_on_restrict)
                have f': "(λx. if x ∈ S then f n x else 0) measurable_on UNIV"
                  by (simp add: f measurable_on_UNIV)
                show "?f n measurable_on UNIV"
                  using measurable_on_compose_continuous [OF f' conth] by auto
              qed auto
              show "negligible (sym_diff (cbox a b) (cbox a b - N))"
                by (auto intro: negligible_subset [OF N])
              show "cbox a b - N ∈ sets lebesgue"
                by (simp add: N negligible_imp_sets sets.Diff)
            qed
            show "cbox a b - N ∈ sets lebesgue"
              by (simp add: N negligible_imp_sets sets.Diff)
            show "norm (?f n x) ≀ DIM('b)"
              if "x ∈ cbox a b - N" for x
              using that local.norm_le by simp
          qed (auto simp: const)
        qed
        show "negligible {x ∈ cbox a b - N - cbox a b. ?Ο‡ x β‰  0}"
          by (auto simp: empty_imp_negligible)
        have "{x ∈ cbox a b - (cbox a b - N). ?Ο‡ x β‰  0} βŠ† N"
          by auto
        then show "negligible {x ∈ cbox a b - (cbox a b - N). ?Ο‡ x β‰  0}"
          using N negligible_subset by blast
      qed
    qed
    show "?Ο‡ x ∈ box 0 One" for x
      using rangeh by auto
    show "continuous_on (box 0 One) h'"
      by (rule conth')
  qed
  then show ?thesis
    by (simp add: o_def h'h measurable_on_UNIV)
qed


lemma measurable_on_if_simple_function_limit:
  fixes f :: "'a::euclidean_space β‡’ 'b::euclidean_space"
  shows  "βŸ¦β‹€n. g n measurable_on UNIV; β‹€n. finite (range (g n)); β‹€x. (Ξ»n. g n x) β‡’ f x⟧
   ⟹ f measurable_on UNIV"
  by (force intro: measurable_on_limit [where N="{}"])


lemma lebesgue_measurable_imp_measurable_on_nnreal_UNIV:
  fixes u :: "'a::euclidean_space β‡’ real"
  assumes u: "u ∈ borel_measurable lebesgue" and nn: "β‹€x. u x β‰₯ 0"
  shows "u measurable_on UNIV"
proof -
  obtain f where "incseq f" and f: "βˆ€i. simple_function lebesgue (f i)"
    and bdd: "β‹€x. bdd_above (range (Ξ»i. f i x))"
    and nnf: "β‹€i x. 0 ≀ f i x" and *: "u = (SUP i. f i)"
    using borel_measurable_implies_simple_function_sequence_real nn u by metis
  show ?thesis
    unfolding *
  proof (rule measurable_on_if_simple_function_limit [of concl: "Sup (range f)"])
    show "(f i) measurable_on UNIV" for i
      by (simp add: f nnf simple_function_measurable_on_UNIV)
    show "finite (range (f i))" for i
      by (metis f simple_function_def space_borel space_completion space_lborel)
    show "(Ξ»i. f i x) β‡’ Sup (range f) x" for x
    proof -
      have "incseq (Ξ»i. f i x)"
        using β€Ήincseq fβ€Ί apply (auto simp: incseq_def)
        by (simp add: le_funD)
      then show ?thesis
        by (metis SUP_apply bdd LIMSEQ_incseq_SUP)
    qed
  qed
qed

lemma lebesgue_measurable_imp_measurable_on_nnreal:
  fixes u :: "'a::euclidean_space β‡’ real"
  assumes "u ∈ borel_measurable lebesgue" "β‹€x. u x β‰₯ 0""S ∈ sets lebesgue"
  shows "u measurable_on S"
  unfolding measurable_on_UNIV [symmetric, of u]
  using assms
  by (auto intro: lebesgue_measurable_imp_measurable_on_nnreal_UNIV)

lemma lebesgue_measurable_imp_measurable_on_real:
  fixes u :: "'a::euclidean_space β‡’ real"
  assumes u: "u ∈ borel_measurable lebesgue" and S: "S ∈ sets lebesgue"
  shows "u measurable_on S"
proof -
  let ?f = "λx. ¦u x¦ + u x"
  let ?g = "λx. ¦u x¦ - u x"
  have "?f measurable_on S" "?g measurable_on S"
    using S u by (auto intro: lebesgue_measurable_imp_measurable_on_nnreal)
  then have "(Ξ»x. (?f x - ?g x) / 2) measurable_on S"
    using measurable_on_cdivide measurable_on_diff by blast
  then show ?thesis
    by auto
qed


proposition lebesgue_measurable_imp_measurable_on:
  fixes f :: "'a::euclidean_space β‡’ 'b::euclidean_space"
  assumes f: "f ∈ borel_measurable lebesgue" and S: "S ∈ sets lebesgue"
  shows "f measurable_on S"
  unfolding measurable_on_componentwise [of f]
proof
  fix i::'b
  assume "i ∈ Basis"
  have "(Ξ»x. (f x βˆ™ i)) ∈ borel_measurable lebesgue"
    using β€Ήi ∈ Basisβ€Ί borel_measurable_euclidean_space f by blast
  then have "(Ξ»x. (f x βˆ™ i)) measurable_on S"
    using S lebesgue_measurable_imp_measurable_on_real by blast
  then show "(Ξ»x. (f x βˆ™ i) *R i) measurable_on S"
    by (intro measurable_on_scaleR measurable_on_const S)
qed

proposition measurable_on_iff_borel_measurable:
  fixes f :: "'a::euclidean_space β‡’ 'b::euclidean_space"
  assumes "S ∈ sets lebesgue"
  shows "f measurable_on S ⟷ f ∈ borel_measurable (lebesgue_on S)" (is "?lhs = ?rhs")
proof
  show "f ∈ borel_measurable (lebesgue_on S)"
    if "f measurable_on S"
    using that by (simp add: assms measurable_on_imp_borel_measurable_lebesgue)
next
  assume "f ∈ borel_measurable (lebesgue_on S)"
  then have "(λa. if a ∈ S then f a else 0) measurable_on UNIV"
    by (simp add: assms borel_measurable_if lebesgue_measurable_imp_measurable_on)
  then show "f measurable_on S"
    using measurable_on_UNIV by blast
qed

subsection β€ΉMonotonic functions are Lebesgue integrableβ€Ί

(*Can these be generalised from type real?*)
lemma integrable_mono_on_nonneg:
  fixes f :: "real β‡’ real"
  assumes mon: "mono_on {a..b} f" and 0: "β‹€x. 0 ≀ f x"
  shows "integrable (lebesgue_on {a..b}) f" 
proof -
  have "space lborel = space lebesgue" "sets borel βŠ† sets lebesgue"
    by force+
  then have fborel: "f ∈ borel_measurable (lebesgue_on {a..b})"
    by (metis mon borel_measurable_mono_on_fnc borel_measurable_subalgebra mono_restrict_space space_lborel space_restrict_space)
  then obtain g where g: "incseq g" and simple: "β‹€i. simple_function (lebesgue_on {a..b}) (g i)" 
                and bdd: " (βˆ€x. bdd_above (range (Ξ»i. g i x)))" and nonneg: "βˆ€i x. 0 ≀ g i x"
                and fsup: "f = (SUP i. g i)"
    by (metis borel_measurable_implies_simple_function_sequence_real 0)
  have "f ` {a..b} βŠ† {f a..f b}" 
    using assms by (auto simp: mono_on_def)
  have g_le_f: "g i x ≀ f x" for i x
  proof -
    have "bdd_above ((Ξ»h. h x) ` range g)"
      using bdd cSUP_lessD linorder_not_less by fastforce
    then show ?thesis
      by (metis SUP_apply UNIV_I bdd cSUP_upper fsup)
  qed
  then have gfb: "g i x ≀ f b" if "x ∈ {a..b}" for i x
    by (smt (verit, best) mon atLeastAtMost_iff mono_on_def that)
  have g_le: "g i x ≀ g j x" if "i≀j"  for i j x
    using g by (simp add: incseq_def le_funD that)
  show "integrable (lebesgue_on {a..b}) ( f)"
  proof (rule integrable_dominated_convergence)
    show "f ∈ borel_measurable (lebesgue_on {a..b})"
      using fborel by blast
    have "β‹€x. (Ξ»i. g i x) β‡’ (SUP h ∈ range g. h  x)"
    proof (rule order_tendstoI)
      show "βˆ€F i in sequentially. y < g i x"
        if "y < (SUP h∈range g. h x)" for x y
      proof -
        from that obtain h where h: "h ∈ range g" "y < h x"
          using g_le_f by (subst (asm)less_cSUP_iff) fastforce+
        then show ?thesis
          by (smt (verit, ccfv_SIG) eventually_sequentially g_le imageE)
      qed
      show "βˆ€F i in sequentially. g i x < y"
        if "(SUP h∈range g. h x) < y" for x y
        by (smt (verit, best) that Sup_apply g_le_f always_eventually fsup image_cong)
    qed
    then show "AE x in lebesgue_on {a..b}. (Ξ»i. g i x) β‡’ f x"
      by (simp add: fsup)
    fix i
    show "g i ∈ borel_measurable (lebesgue_on {a..b})"
      using borel_measurable_simple_function simple by blast
    show "AE x in lebesgue_on {a..b}. norm (g i x) ≀ f b"
      by (simp add: gfb nonneg Measure_Space.AE_I' [of "{}"])
  qed auto
qed

lemma integrable_mono_on:
  fixes f :: "real β‡’ real"
  assumes "mono_on {a..b} f"
  shows "integrable (lebesgue_on {a..b}) f" 
proof -
  define f' where "f' ≑ Ξ»x. if x ∈ {a..b} then f x - f a else 0"
  have "mono_on {a..b} f'"
    by (smt (verit, best) assms f'_def mono_on_def)
  moreover have 0: "β‹€x. 0 ≀ f' x"
    by (smt (verit, best) assms atLeastAtMost_iff f'_def mono_on_def)
  ultimately have "integrable (lebesgue_on {a..b}) f'"
    using integrable_mono_on_nonneg by presburger
  then have "integrable (lebesgue_on {a..b}) (Ξ»x. f' x + f a)"
    by force
  moreover have "space lborel = space lebesgue" "sets borel βŠ† sets lebesgue"
    by force+
  then have fborel: "f ∈ borel_measurable (lebesgue_on {a..b})"
    by (metis assms borel_measurable_mono_on_fnc borel_measurable_subalgebra mono_restrict_space space_lborel space_restrict_space)
  ultimately show ?thesis
    by (rule integrable_cong_AE_imp) (auto simp add: f'_def)
qed

lemma integrable_on_mono_on:
  fixes f :: "real β‡’ real"
  assumes "mono_on {a..b} f"
  shows "f integrable_on {a..b}"
  by (simp add: assms integrable_mono_on integrable_on_lebesgue_on) 

subsection β€ΉMeasurability on generalisations of the binary productβ€Ί

lemma measurable_on_bilinear:
  fixes h :: "'a::euclidean_space β‡’ 'b::euclidean_space β‡’ 'c::euclidean_space"
  assumes h: "bilinear h" and f: "f measurable_on S" and g: "g measurable_on S"
  shows "(Ξ»x. h (f x) (g x)) measurable_on S"
proof (rule measurable_on_combine [where h = h])
  show "continuous_on UNIV (Ξ»x. h (fst x) (snd x))"
    by (simp add: bilinear_continuous_on_compose [OF continuous_on_fst continuous_on_snd h])
  show "h 0 0 = 0"
  by (simp add: bilinear_lzero h)
qed (auto intro: assms)

lemma borel_measurable_bilinear:
  fixes h :: "'a::euclidean_space β‡’ 'b::euclidean_space β‡’ 'c::euclidean_space"
  assumes "bilinear h" "f ∈ borel_measurable (lebesgue_on S)" "g ∈ borel_measurable (lebesgue_on S)"
    and S: "S ∈ sets lebesgue"
  shows "(λx. h (f x) (g x)) ∈ borel_measurable (lebesgue_on S)"
  using assms measurable_on_bilinear [of h f S g]
  by (simp flip: measurable_on_iff_borel_measurable)

lemma absolutely_integrable_bounded_measurable_product:
  fixes h :: "'a::euclidean_space β‡’ 'b::euclidean_space β‡’ 'c::euclidean_space"
  assumes "bilinear h" and f: "f ∈ borel_measurable (lebesgue_on S)" "S ∈ sets lebesgue"
    and bou: "bounded (f ` S)" and g: "g absolutely_integrable_on S"
  shows "(Ξ»x. h (f x) (g x)) absolutely_integrable_on S"
proof -
  obtain B where "B > 0" and B: "β‹€x y. norm (h x y) ≀ B * norm x * norm y"
    using bilinear_bounded_pos β€Ήbilinear hβ€Ί by blast
  obtain C where "C > 0" and C: "β‹€x. x ∈ S ⟹ norm (f x) ≀ C"
    using bounded_pos by (metis bou imageI)
  show ?thesis
  proof (rule measurable_bounded_by_integrable_imp_absolutely_integrable [OF _ β€ΉS ∈ sets lebesgueβ€Ί])
    show "norm (h (f x) (g x)) ≀ B * C * norm(g x)" if "x ∈ S" for x
      by (meson less_le mult_left_mono mult_right_mono norm_ge_zero order_trans that β€ΉB > 0β€Ί B C)
    show "(λx. h (f x) (g x)) ∈ borel_measurable (lebesgue_on S)"
      using β€Ήbilinear hβ€Ί f g
      by (blast intro: borel_measurable_bilinear dest: absolutely_integrable_measurable)
    show "(Ξ»x. B * C * norm(g x)) integrable_on S"
      using β€Ή0 < Bβ€Ί β€Ή0 < Cβ€Ί absolutely_integrable_on_def g by auto
  qed
qed

lemma absolutely_integrable_bounded_measurable_product_real:
  fixes f :: "real β‡’ real"
  assumes "f ∈ borel_measurable (lebesgue_on S)" "S ∈ sets lebesgue"
      and "bounded (f ` S)" and "g absolutely_integrable_on S"
  shows "(Ξ»x. f x * g x) absolutely_integrable_on S"
  using absolutely_integrable_bounded_measurable_product bilinear_times assms by blast


lemma borel_measurable_AE:
  fixes f :: "'a::euclidean_space β‡’ 'b::euclidean_space"
  assumes "f ∈ borel_measurable lebesgue" and ae: "AE x in lebesgue. f x = g x"
  shows "g ∈ borel_measurable lebesgue"
proof -
  obtain N where N: "N ∈ null_sets lebesgue" "β‹€x. x βˆ‰ N ⟹ f x = g x"
    using ae unfolding completion.AE_iff_null_sets by auto
  have "f measurable_on UNIV"
    by (simp add: assms lebesgue_measurable_imp_measurable_on)
  then have "g measurable_on UNIV"
    by (metis Diff_iff N measurable_on_spike negligible_iff_null_sets)
  then show ?thesis
    using measurable_on_imp_borel_measurable_lebesgue_UNIV by blast
qed

lemma has_bochner_integral_combine:
  fixes f :: "real β‡’ 'a::euclidean_space"
  assumes "a ≀ c" "c ≀ b"
    and ac: "has_bochner_integral (lebesgue_on {a..c}) f i"
    and cb: "has_bochner_integral (lebesgue_on {c..b}) f j"
  shows "has_bochner_integral (lebesgue_on {a..b}) f(i + j)"
proof -
  have i: "has_bochner_integral lebesgue (Ξ»x. indicator {a..c} x *R f x) i"
   and j: "has_bochner_integral lebesgue (Ξ»x. indicator {c..b} x *R f x) j"
    using assms  by (auto simp: has_bochner_integral_restrict_space)
  have AE: "AE x in lebesgue. indicat_real {a..c} x *R f x + indicat_real {c..b} x *R f x = indicat_real {a..b} x *R f x"
  proof (rule AE_I')
    have eq: "indicat_real {a..c} x *R f x + indicat_real {c..b} x *R f x = indicat_real {a..b} x *R f x" if "x β‰  c" for x
      using assms that by (auto simp: indicator_def)
    then show "{x ∈ space lebesgue. indicat_real {a..c} x *R f x + indicat_real {c..b} x *R f x β‰  indicat_real {a..b} x *R f x} βŠ† {c}"
      by auto
  qed auto
  have "has_bochner_integral lebesgue (Ξ»x. indicator {a..b} x *R f x) (i + j)"
  proof (rule has_bochner_integralI_AE [OF has_bochner_integral_add [OF i j] _ AE])
    have eq: "indicat_real {a..c} x *R f x + indicat_real {c..b} x *R f x = indicat_real {a..b} x *R f x" if "x β‰  c" for x
      using assms that by (auto simp: indicator_def)
    show "(λx. indicat_real {a..b} x *R f x) ∈ borel_measurable lebesgue"
    proof (rule borel_measurable_AE [OF borel_measurable_add AE])
      show "(λx. indicator {a..c} x *R f x) ∈ borel_measurable lebesgue"
           "(λx. indicator {c..b} x *R f x) ∈ borel_measurable lebesgue"
        using i j by auto
    qed
  qed
  then show ?thesis
    by (simp add: has_bochner_integral_restrict_space)
qed

lemma integrable_combine:
  fixes f :: "real β‡’ 'a::euclidean_space"
  assumes "integrable (lebesgue_on {a..c}) f" "integrable (lebesgue_on {c..b}) f"
    and "a ≀ c" "c ≀ b"
  shows "integrable (lebesgue_on {a..b}) f"
  using assms has_bochner_integral_combine has_bochner_integral_iff by blast

lemma integral_combine:
  fixes f :: "real β‡’ 'a::euclidean_space"
  assumes f: "integrable (lebesgue_on {a..b}) f" and "a ≀ c" "c ≀ b"
  shows "integralL (lebesgue_on {a..b}) f = integralL (lebesgue_on {a..c}) f + integralL (lebesgue_on {c..b}) f"
proof -
  have i: "has_bochner_integral (lebesgue_on {a..c}) f(integralL (lebesgue_on {a..c}) f)"
    using integrable_subinterval β€Ήc ≀ bβ€Ί f has_bochner_integral_iff by fastforce
  have j: "has_bochner_integral (lebesgue_on {c..b}) f(integralL (lebesgue_on {c..b}) f)"
    using integrable_subinterval β€Ήa ≀ cβ€Ί f has_bochner_integral_iff by fastforce
  show ?thesis
    by (meson β€Ήa ≀ cβ€Ί β€Ήc ≀ bβ€Ί has_bochner_integral_combine has_bochner_integral_iff i j)
qed

lemma has_bochner_integral_null [intro]:
  fixes f :: "'a::euclidean_space β‡’ 'b::euclidean_space"
  assumes "N ∈ null_sets lebesgue"
  shows "has_bochner_integral (lebesgue_on N) f 0"
  unfolding has_bochner_integral_iff ―‹strange that the proof's so longβ€Ί
proof
  show "integrable (lebesgue_on N) f"
  proof (subst integrable_restrict_space)
    show "N ∩ space lebesgue ∈ sets lebesgue"
      using assms by force
    show "integrable lebesgue (Ξ»x. indicat_real N x *R f x)"
    proof (rule integrable_cong_AE_imp)
      show "integrable lebesgue (Ξ»x. 0)"
        by simp
      show *: "AE x in lebesgue. 0 = indicat_real N x *R f x"
        using assms
        by (simp add: indicator_def completion.null_sets_iff_AE eventually_mono)
      show "(λx. indicat_real N x *R f x) ∈ borel_measurable lebesgue"
        by (auto intro: borel_measurable_AE [OF _ *])
    qed
  qed
  show "integralL (lebesgue_on N) f = 0"
  proof (rule integral_eq_zero_AE)
    show "AE x in lebesgue_on N. f x = 0"
      by (rule AE_I' [where N=N]) (auto simp: assms null_setsD2 null_sets_restrict_space)
  qed
qed

lemma has_bochner_integral_null_eq[simp]:
  fixes f :: "'a::euclidean_space β‡’ 'b::euclidean_space"
  assumes "N ∈ null_sets lebesgue"
  shows "has_bochner_integral (lebesgue_on N) f i ⟷ i = 0"
  using assms has_bochner_integral_eq by blast

end