Theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration

(*  Title:      HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
    Author:     Johannes Hölzl, TU München
    Author:     Robert Himmelmann, TU München
    Huge cleanup by LCP
*)

theory Equivalence_Lebesgue_Henstock_Integration
  imports
    Lebesgue_Measure
    Henstock_Kurzweil_Integration
    Complete_Measure
    Set_Integral
    Homeomorphism
    Cartesian_Euclidean_Space
begin

lemma LIMSEQ_if_less: "(λk. if i < k then a else b)  a"
  by (rule_tac k="Suc i" in LIMSEQ_offset) auto

text ‹Note that the rhs is an implication. This lemma plays a specific role in one proof.›
lemma le_left_mono: "x  y  y  a  x  (a::'a::preorder)"
  by (auto intro: order_trans)

lemma ball_trans:
  assumes "y  ball z q" "r + q  s" shows "ball y r  ball z s"
  using assms by metric

lemma has_integral_implies_lebesgue_measurable_cbox:
  fixes f :: "'a :: euclidean_space  real"
  assumes f: "(f has_integral I) (cbox x y)"
  shows "f  lebesgue_on (cbox x y) M borel"
proof (rule cld_measure.borel_measurable_cld)
  let ?L = "lebesgue_on (cbox x y)"
  let  = "emeasure ?L"
  let ?μ' = "outer_measure_of ?L"
  interpret L: finite_measure ?L
  proof
    show " (space ?L)  "
      by (simp add: emeasure_restrict_space space_restrict_space emeasure_lborel_cbox_eq)
  qed

  show "cld_measure ?L"
  proof
    fix B A assume "B  A" "A  null_sets ?L"
    then show "B  sets ?L"
      using null_sets_completion_subset[OF B  A, of lborel]
      by (auto simp add: null_sets_restrict_space sets_restrict_space_iff intro: )
  next
    fix A assume "A  space ?L" "B. B  sets ?L   B <   A  B  sets ?L"
    from this(1) this(2)[of "space ?L"] show "A  sets ?L"
      by (auto simp: Int_absorb2 less_top[symmetric])
  qed auto
  then interpret cld_measure ?L
    .

  have content_eq_L: "A  sets borel  A  cbox x y  content A = measure ?L A" for A
    by (subst measure_restrict_space) (auto simp: measure_def)

  fix E and a b :: real assume "E  sets ?L" "a < b" "0 <  E" " E < "
  then obtain M :: real where " E = M" "0 < M"
    by (cases " E") auto
  define e where "e = M / (4 + 2 / (b - a))"
  from a < b 0<M have "0 < e"
    by (auto intro!: divide_pos_pos simp: field_simps e_def)

  have "e < M / (3 + 2 / (b - a))"
    using a < b 0 < M
    unfolding e_def by (intro divide_strict_left_mono add_strict_right_mono mult_pos_pos) (auto simp: field_simps)
  then have "2 * e < (b - a) * (M - e * 3)"
    using 0<M 0 < e a < b by (simp add: field_simps)

  have e_less_M: "e < M / 1"
    unfolding e_def using a < b 0<M by (intro divide_strict_left_mono) (auto simp: field_simps)

  obtain d
    where "gauge d"
      and integral_f: "p. p tagged_division_of cbox x y  d fine p 
        norm (((x,k)  p. content k *R f x) - I) < e"
    using 0<e f unfolding has_integral by auto

  define C where "C X m = X  {x. ball x (1/Suc m)  d x}" for X m
  have "incseq (C X)" for X
    unfolding C_def [abs_def]
    by (intro monoI Collect_mono conj_mono imp_refl le_left_mono subset_ball divide_left_mono Int_mono) auto

  { fix X assume "X  space ?L" and eq: "?μ' X =  E"
    have "(SUP m. outer_measure_of ?L (C X m)) = outer_measure_of ?L (m. C X m)"
      using X  space ?L by (intro SUP_outer_measure_of_incseq incseq (C X)) (auto simp: C_def)
    also have "(m. C X m) = X"
    proof -
      { fix x
        obtain e where "0 < e" "ball x e  d x"
          using gaugeD[OF gauge d, of x] unfolding open_contains_ball by auto
        moreover
        obtain n where "1 / (1 + real n) < e"
          using reals_Archimedean[OF 0<e] by (auto simp: inverse_eq_divide)
        then have "ball x (1 / (1 + real n))  ball x e"
          by (intro subset_ball) auto
        ultimately have "n. ball x (1 / (1 + real n))  d x"
          by blast }
      then show ?thesis
        by (auto simp: C_def)
    qed
    finally have "(SUP m. outer_measure_of ?L (C X m)) =  E"
      using eq by auto
    also have " > M - e"
      using 0 < M  E = M 0<e by (auto intro!: ennreal_lessI)
    finally have "m. M - e < outer_measure_of ?L (C X m)"
      unfolding less_SUP_iff by auto }
  note C = this

  let ?E = "{xE. f x  a}" and ?F = "{xE. b  f x}"

  have "¬ (?μ' ?E =  E  ?μ' ?F =  E)"
  proof
    assume eq: "?μ' ?E =  E  ?μ' ?F =  E"
    with C[of ?E] C[of ?F] E  sets ?L[THEN sets.sets_into_space] obtain ma mb
      where "M - e < outer_measure_of ?L (C ?E ma)" "M - e < outer_measure_of ?L (C ?F mb)"
      by auto
    moreover define m where "m = max ma mb"
    ultimately have M_minus_e: "M - e < outer_measure_of ?L (C ?E m)" "M - e < outer_measure_of ?L (C ?F m)"
      using
        incseqD[OF incseq (C ?E), of ma m, THEN outer_measure_of_mono]
        incseqD[OF incseq (C ?F), of mb m, THEN outer_measure_of_mono]
      by (auto intro: less_le_trans)
    define d' where "d' x = d x  ball x (1 / (3 * Suc m))" for x
    have "gauge d'"
      unfolding d'_def by (intro gauge_Int gauge d gauge_ball) auto
    then obtain p where p: "p tagged_division_of cbox x y" "d' fine p"
      by (rule fine_division_exists)
    then have "d fine p"
      unfolding d'_def[abs_def] fine_def by auto

    define s where "s = {(x::'a, k). k  (C ?E m)  {}  k  (C ?F m)  {}}"
    define T where "T E k = (SOME x. x  k  C E m)" for E k
    let ?A = "(λ(x, k). (T ?E k, k)) ` (p  s)  (p - s)"
    let ?B = "(λ(x, k). (T ?F k, k)) ` (p  s)  (p - s)"

    { fix X assume X_eq: "X = ?E  X = ?F"
      let ?T = "(λ(x, k). (T X k, k))"
      let ?p = "?T ` (p  s)  (p - s)"

      have in_s: "(x, k)  s  T X k  k  C X m" for x k
        using someI_ex[of "λx. x  k  C X m"] X_eq unfolding ex_in_conv by (auto simp: T_def s_def)

      { fix x k assume "(x, k)  p" "(x, k)  s"
        have k: "k  ball x (1 / (3 * Suc m))"
          using d' fine p[THEN fineD, OF (x, k)  p] by (auto simp: d'_def)
        then have "x  ball (T X k) (1 / (3 * Suc m))"
          using in_s[OF (x, k)  s] by (auto simp: C_def subset_eq dist_commute)
        then have "ball x (1 / (3 * Suc m))  ball (T X k) (1 / Suc m)"
          by (rule ball_trans) (auto simp: field_split_simps)
        with k in_s[OF (x, k)  s] have "k  d (T X k)"
          by (auto simp: C_def) }
      then have "d fine ?p"
        using d fine p by (auto intro!: fineI)
      moreover
      have "?p tagged_division_of cbox x y"
      proof (rule tagged_division_ofI)
        show "finite ?p"
          using p(1) by auto
      next
        fix z k assume *: "(z, k)  ?p"
        then consider "(z, k)  p" "(z, k)  s"
          | x' where "(x', k)  p" "(x', k)  s" "z = T X k"
          by (auto simp: T_def)
        then have "z  k  k  cbox x y  (a b. k = cbox a b)"
          using p(1) by cases (auto dest: in_s)
        then show "z  k" "k  cbox x y" "a b. k = cbox a b"
          by auto
      next
        fix z k z' k' assume "(z, k)  ?p" "(z', k')  ?p" "(z, k)  (z', k')"
        with tagged_division_ofD(5)[OF p(1), of _ k _ k']
        show "interior k  interior k' = {}"
          by (auto simp: T_def dest: in_s)
      next
        have "{k. x. (x, k)  ?p} = {k. x. (x, k)  p}"
          by (auto simp: T_def image_iff Bex_def)
        then show "{k. x. (x, k)  ?p} = cbox x y"
          using p(1) by auto
      qed
      ultimately have I: "norm (((x,k)  ?p. content k *R f x) - I) < e"
        using integral_f by auto

      have "((x,k)  ?p. content k *R f x) =
        ((x,k)  ?T ` (p  s). content k *R f x) + ((x,k)  p - s. content k *R f x)"
        using p(1)[THEN tagged_division_ofD(1)]
        by (safe intro!: sum.union_inter_neutral) (auto simp: s_def T_def)
      also have "((x,k)  ?T ` (p  s). content k *R f x) = ((x,k)  p  s. content k *R f (T X k))"
      proof (subst sum.reindex_nontrivial, safe)
        fix x1 x2 k assume 1: "(x1, k)  p" "(x1, k)  s" and 2: "(x2, k)  p" "(x2, k)  s"
          and eq: "content k *R f (T X k)  0"
        with tagged_division_ofD(5)[OF p(1), of x1 k x2 k] tagged_division_ofD(4)[OF p(1), of x1 k]
        show "x1 = x2"
          by (auto simp: content_eq_0_interior)
      qed (use p in auto intro!: sum.cong)
      finally have eq: "((x,k)  ?p. content k *R f x) =
        ((x,k)  p  s. content k *R f (T X k)) + ((x,k)  p - s. content k *R f x)" .

      have in_T: "(x, k)  s  T X k  X" for x k
        using in_s[of x k] by (auto simp: C_def)

      note I eq in_T }
    note parts = this

    have p_in_L: "(x, k)  p  k  sets ?L" for x k
      using tagged_division_ofD(3, 4)[OF p(1), of x k] by (auto simp: sets_restrict_space)

    have [simp]: "finite p"
      using tagged_division_ofD(1)[OF p(1)] .

    have "(M - 3*e) * (b - a)  ((x,k)  p  s. content k) * (b - a)"
    proof (intro mult_right_mono)
      have fin: " (E  {ksnd`p. k  C X m = {}}) < " for X
        using  E <  by (rule le_less_trans[rotated]) (auto intro!: emeasure_mono E  sets ?L)
      have sets: "(E  {ksnd`p. k  C X m = {}})  sets ?L" for X
        using tagged_division_ofD(1)[OF p(1)] by (intro sets.Diff E  sets ?L sets.finite_Union sets.Int) (auto intro: p_in_L)
      { fix X assume "X  E" "M - e < ?μ' (C X m)"
        have "M - e  ?μ' (C X m)"
          by (rule less_imp_le) fact
        also have "  ?μ' (E - (E  {ksnd`p. k  C X m = {}}))"
        proof (intro outer_measure_of_mono subsetI)
          fix v assume "v  C X m"
          then have "v  cbox x y" "v  E"
            using E  space ?L X  E by (auto simp: space_restrict_space C_def)
          then obtain z k where "(z, k)  p" "v  k"
            using tagged_division_ofD(6)[OF p(1), symmetric] by auto
          then show "v  E - E  ({ksnd`p. k  C X m = {}})"
            using v  C X m v  E by auto
        qed
        also have " =  E -  (E  {ksnd`p. k  C X m = {}})"
          using E  sets ?L fin[of X] sets[of X] by (auto intro!: emeasure_Diff)
        finally have " (E  {ksnd`p. k  C X m = {}})  e"
          using 0 < e e_less_M 
          by (cases " (E  {ksnd`p. k  C X m = {}})") (auto simp add:  E = M ennreal_minus ennreal_le_iff2)
        note this }
      note upper_bound = this

      have " (E  (snd`(p - s))) =
         ((E  {ksnd`p. k  C ?E m = {}})  (E  {ksnd`p. k  C ?F m = {}}))"
        by (intro arg_cong[where f=""]) (auto simp: s_def image_def Bex_def)
      also have "   (E  {ksnd`p. k  C ?E m = {}}) +  (E  {ksnd`p. k  C ?F m = {}})"
        using sets[of ?E] sets[of ?F] M_minus_e by (intro emeasure_subadditive) auto
      also have "  e + ennreal e"
        using upper_bound[of ?E] upper_bound[of ?F] M_minus_e by (intro add_mono) auto
      finally have " E - 2*e   (E - (E  (snd`(p - s))))"
        using 0 < e E  sets ?L tagged_division_ofD(1)[OF p(1)]
        by (subst emeasure_Diff)
           (auto simp: top_unique simp flip: ennreal_plus
                 intro!: sets.Int sets.finite_UN ennreal_mono_minus intro: p_in_L)
      also have "   (xp  s. snd x)"
      proof (safe intro!: emeasure_mono subsetI)
        fix v assume "v  E" and not: "v  (xp  s. snd x)"
        then have "v  cbox x y"
          using E  space ?L by (auto simp: space_restrict_space)
        then obtain z k where "(z, k)  p" "v  k"
          using tagged_division_ofD(6)[OF p(1), symmetric] by auto
        with not show "v  (snd ` (p - s))"
          by (auto intro!: bexI[of _ "(z, k)"] elim: ballE[of _ _ "(z, k)"])
      qed (auto intro!: sets.Int sets.finite_UN ennreal_mono_minus intro: p_in_L)
      also have " = measure ?L (xp  s. snd x)"
        by (auto intro!: emeasure_eq_ennreal_measure)
      finally have "M - 2 * e  measure ?L (xp  s. snd x)"
        unfolding  E = M using 0 < e by (simp add: ennreal_minus)
      also have "measure ?L (xp  s. snd x) = content (xp  s. snd x)"
        using tagged_division_ofD(1,3,4) [OF p(1)]
        by (intro content_eq_L[symmetric])
           (fastforce intro!: sets.finite_UN UN_least del: subsetI)+
      also have "content (xp  s. snd x)  (kp  s. content (snd k))"
        using p(1) by (auto simp: emeasure_lborel_cbox_eq intro!: measure_subadditive_finite
                            dest!: p(1)[THEN tagged_division_ofD(4)])
      finally show "M - 3 * e  ((x, y)p  s. content y)"
        using 0 < e by (simp add: split_beta)
    qed (use a < b in auto)
    also have " = ((x,k)  p  s. content k * (b - a))"
      by (simp add: sum_distrib_right split_beta')
    also have "  ((x,k)  p  s. content k * (f (T ?F k) - f (T ?E k)))"
      using parts(3) by (auto intro!: sum_mono mult_left_mono diff_mono)
    also have " = ((x,k)  p  s. content k * f (T ?F k)) - ((x,k)  p  s. content k * f (T ?E k))"
      by (auto intro!: sum.cong simp: field_simps sum_subtractf[symmetric])
    also have " = ((x,k)  ?B. content k *R f x) - ((x,k)  ?A. content k *R f x)"
      by (subst (1 2) parts) auto
    also have "  norm (((x,k)  ?B. content k *R f x) - ((x,k)  ?A. content k *R f x))"
      by auto
    also have "  e + e"
      using parts(1)[of ?E] parts(1)[of ?F] by (intro norm_diff_triangle_le[of _ I]) auto
    finally show False
      using 2 * e < (b - a) * (M - e * 3) by (auto simp: field_simps)
  qed
  moreover have "?μ' ?E   E" "?μ' ?F   E"
    unfolding outer_measure_of_eq[OF E  sets ?L, symmetric] by (auto intro!: outer_measure_of_mono)
  ultimately show "min (?μ' ?E) (?μ' ?F) <  E"
    unfolding min_less_iff_disj by (auto simp: less_le)
qed

lemma has_integral_implies_lebesgue_measurable_real:
  fixes f :: "'a :: euclidean_space  real"
  assumes f: "(f has_integral I) Ω"
  shows "(λx. f x * indicator Ω x)  lebesgue M borel"
proof -
  define B :: "nat  'a set" where "B n = cbox (- real n *R One) (real n *R One)" for n
  show "(λx. f x * indicator Ω x)  lebesgue M borel"
  proof (rule measurable_piecewise_restrict)
    have "(n. box (- real n *R One) (real n *R One))  (B ` UNIV)"
      unfolding B_def by (intro UN_mono box_subset_cbox order_refl)
    then show "countable (range B)" "space lebesgue  (B ` UNIV)"
      by (auto simp: B_def UN_box_eq_UNIV)
  next
    fix Ω' assume "Ω'  range B"
    then obtain n where Ω': "Ω' = B n" by auto
    then show "Ω'  space lebesgue  sets lebesgue"
      by (auto simp: B_def)

    have "f integrable_on Ω"
      using f by auto
    then have "(λx. f x * indicator Ω x) integrable_on Ω"
      by (auto simp: integrable_on_def cong: has_integral_cong)
    then have "(λx. f x * indicator Ω x) integrable_on (Ω  B n)"
      by (rule integrable_on_superset) auto
    then have "(λx. f x * indicator Ω x) integrable_on B n"
      unfolding B_def by (rule integrable_on_subcbox) auto
    then show "(λx. f x * indicator Ω x)  lebesgue_on Ω' M borel"
      unfolding B_def Ω' by (auto intro: has_integral_implies_lebesgue_measurable_cbox simp: integrable_on_def)
  qed
qed

lemma has_integral_implies_lebesgue_measurable:
  fixes f :: "'a :: euclidean_space  'b :: euclidean_space"
  assumes f: "(f has_integral I) Ω"
  shows "(λx. indicator Ω x *R f x)  lebesgue M borel"
proof (intro borel_measurable_euclidean_space[where 'c='b, THEN iffD2] ballI)
  fix i :: "'b" assume "i  Basis"
  have "(λx. (f x  i) * indicator Ω x)  borel_measurable (completion lborel)"
    using has_integral_linear[OF f bounded_linear_inner_left, of i]
    by (intro has_integral_implies_lebesgue_measurable_real) (auto simp: comp_def)
  then show "(λx. indicator Ω x *R f x  i)  borel_measurable (completion lborel)"
    by (simp add: ac_simps)
qed

subsection ‹Equivalence Lebesgue integral on constlborel and HK-integral›

lemma has_integral_measure_lborel:
  fixes A :: "'a::euclidean_space set"
  assumes A[measurable]: "A  sets borel" and finite: "emeasure lborel A < "
  shows "((λx. 1) has_integral measure lborel A) A"
proof -
  { fix l u :: 'a
    have "((λx. 1) has_integral measure lborel (box l u)) (box l u)"
    proof cases
      assume "bBasis. l  b  u  b"
      then show ?thesis
        using has_integral_const[of "1::real" l u]
        by (simp flip: has_integral_restrict[OF box_subset_cbox] add: has_integral_spike_interior)
    next
      assume "¬ (bBasis. l  b  u  b)"
      then have "box l u = {}"
        unfolding box_eq_empty by (auto simp: not_le intro: less_imp_le)
      then show ?thesis
        by simp
    qed }
  note has_integral_box = this

  { fix a b :: 'a let ?M = "λA. measure lborel (A  box a b)"
    have "Int_stable  (range (λ(a, b). box a b))"
      by (auto simp: Int_stable_def box_Int_box)
    moreover have "(range (λ(a, b). box a b))  Pow UNIV"
      by auto
    moreover have "A  sigma_sets UNIV (range (λ(a, b). box a b))"
       using A unfolding borel_eq_box by simp
    ultimately have "((λx. 1) has_integral ?M A) (A  box a b)"
    proof (induction rule: sigma_sets_induct_disjoint)
      case (basic A) then show ?case
        by (auto simp: box_Int_box has_integral_box)
    next
      case empty then show ?case
        by simp
    next
      case (compl A)
      then have [measurable]: "A  sets borel"
        by (simp add: borel_eq_box)

      have "((λx. 1) has_integral ?M (box a b)) (box a b)"
        by (simp add: has_integral_box)
      moreover have "((λx. if x  A  box a b then 1 else 0) has_integral ?M A) (box a b)"
        by (subst has_integral_restrict) (auto intro: compl)
      ultimately have "((λx. 1 - (if x  A  box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
        by (rule has_integral_diff)
      then have "((λx. (if x  (UNIV - A)  box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
        by (rule has_integral_cong[THEN iffD1, rotated 1]) auto
      then have "((λx. 1) has_integral ?M (box a b) - ?M A) ((UNIV - A)  box a b)"
        by (subst (asm) has_integral_restrict) auto
      also have "?M (box a b) - ?M A = ?M (UNIV - A)"
        by (subst measure_Diff[symmetric]) (auto simp: emeasure_lborel_box_eq Diff_Int_distrib2)
      finally show ?case .
    next
      case (union F)
      then have [measurable]: "i. F i  sets borel"
        by (simp add: borel_eq_box subset_eq)
      have "((λx. if x  (F ` UNIV)  box a b then 1 else 0) has_integral ?M (i. F i)) (box a b)"
      proof (rule has_integral_monotone_convergence_increasing)
        let ?f = "λk x. i<k. if x  F i  box a b then 1 else 0 :: real"
        show "k. (?f k has_integral (i<k. ?M (F i))) (box a b)"
          using union.IH by (auto intro!: has_integral_sum simp del: Int_iff)
        show "k x. ?f k x  ?f (Suc k) x"
          by (intro sum_mono2) auto
        from union(1) have *: "x i j. x  F i  x  F j  j = i"
          by (auto simp add: disjoint_family_on_def)
        show "(λk. ?f k x)  (if x  (F ` UNIV)  box a b then 1 else 0)" for x
          by (auto simp: * sum.If_cases Iio_Int_singleton if_distrib LIMSEQ_if_less cong: if_cong)
        have *: "emeasure lborel ((x. F x)  box a b)  emeasure lborel (box a b)"
          by (intro emeasure_mono) auto

        with union(1) show "(λk. i<k. ?M (F i))  ?M (i. F i)"
          unfolding sums_def[symmetric] UN_extend_simps
          by (intro measure_UNION) (auto simp: disjoint_family_on_def emeasure_lborel_box_eq top_unique)
      qed
      then show ?case
        by (subst (asm) has_integral_restrict) auto
    qed }
  note * = this

  show ?thesis
  proof (rule has_integral_monotone_convergence_increasing)
    let ?B = "λn::nat. box (- real n *R One) (real n *R One) :: 'a set"
    let ?f = "λn::nat. λx. if x  A  ?B n then 1 else 0 :: real"
    let ?M = "λn. measure lborel (A  ?B n)"

    show "n::nat. (?f n has_integral ?M n) A"
      using * by (subst has_integral_restrict) simp_all
    show "k x. ?f k x  ?f (Suc k) x"
      by (auto simp: box_def)
    { fix x assume "x  A"
      moreover have "(λk. indicator (A  ?B k) x :: real)  indicator (k::nat. A  ?B k) x"
        by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def box_def)
      ultimately show "(λk. if x  A  ?B k then 1 else 0::real)  1"
        by (simp add: indicator_def of_bool_def UN_box_eq_UNIV) }

    have "(λn. emeasure lborel (A  ?B n))  emeasure lborel (n::nat. A  ?B n)"
      by (intro Lim_emeasure_incseq) (auto simp: incseq_def box_def)
    also have "(λn. emeasure lborel (A  ?B n)) = (λn. measure lborel (A  ?B n))"
    proof (intro ext emeasure_eq_ennreal_measure)
      fix n have "emeasure lborel (A  ?B n)  emeasure lborel (?B n)"
        by (intro emeasure_mono) auto
      then show "emeasure lborel (A  ?B n)  top"
        by (auto simp: top_unique)
    qed
    finally show "(λn. measure lborel (A  ?B n))  measure lborel A"
      using emeasure_eq_ennreal_measure[of lborel A] finite
      by (simp add: UN_box_eq_UNIV less_top)
  qed
qed

lemma nn_integral_has_integral:
  fixes f::"'a::euclidean_space  real"
  assumes f: "f  borel_measurable borel" "x. 0  f x" "(+x. f x lborel) = ennreal r" "0  r"
  shows "(f has_integral r) UNIV"
using f proof (induct f arbitrary: r rule: borel_measurable_induct_real)
  case (set A)
  then have "((λx. 1) has_integral measure lborel A) A"
    by (intro has_integral_measure_lborel) (auto simp: ennreal_indicator)
  with set show ?case
    by (simp add: ennreal_indicator measure_def) (simp add: indicator_def of_bool_def)
next
  case (mult g c)
  then have "ennreal c * (+ x. g x lborel) = ennreal r"
    by (subst nn_integral_cmult[symmetric]) (auto simp: ennreal_mult)
  with 0  r 0  c
  obtain r' where "(c = 0  r = 0)  (0  r'  (+ x. ennreal (g x) lborel) = ennreal r'  r = c * r')"
    by (cases "+ x. ennreal (g x) lborel" rule: ennreal_cases)
       (auto split: if_split_asm simp: ennreal_mult_top ennreal_mult[symmetric])
  with mult show ?case
    by (auto intro!: has_integral_cmult_real)
next
  case (add g h)
  then have "(+ x. h x + g x lborel) = (+ x. h x lborel) + (+ x. g x lborel)"
    by (simp add: nn_integral_add)
  with add obtain a b where "0  a" "0  b" "(+ x. h x lborel) = ennreal a" "(+ x. g x lborel) = ennreal b" "r = a + b"
    by (cases "+ x. h x lborel" "+ x. g x lborel" rule: ennreal2_cases)
       (auto simp: add_top nn_integral_add top_add simp flip: ennreal_plus)
  with add show ?case
    by (auto intro!: has_integral_add)
next
  case (seq U)
  note seq(1)[measurable] and f[measurable]

  have U_le_f: "U i x  f x" for i x
    by (metis (no_types) LIMSEQ_le_const UNIV_I incseq_def le_fun_def seq.hyps(4) seq.hyps(5) space_borel)

  { fix i
    have "(+x. U i x lborel)  (+x. f x lborel)"
      using seq(2) f(2) U_le_f by (intro nn_integral_mono) simp
    then obtain p where "(+x. U i x lborel) = ennreal p" "p  r" "0  p"
      using seq(6) 0r by (cases "+x. U i x lborel" rule: ennreal_cases) (auto simp: top_unique)
    moreover note seq
    ultimately have "p. (+x. U i x lborel) = ennreal p  0  p  p  r  (U i has_integral p) UNIV"
      by auto }
  then obtain p where p: "i. (+x. ennreal (U i x) lborel) = ennreal (p i)"
    and bnd: "i. p i  r" "i. 0  p i"
    and U_int: "i.(U i has_integral (p i)) UNIV" by metis

  have int_eq: "i. integral UNIV (U i) = p i" using U_int by (rule integral_unique)

  have *: "f integrable_on UNIV  (λk. integral UNIV (U k))  integral UNIV f"
  proof (rule monotone_convergence_increasing)
    show "k. U k integrable_on UNIV" using U_int by auto
    show "k x. xUNIV  U k x  U (Suc k) x" using incseq U by (auto simp: incseq_def le_fun_def)
    then show "bounded (range (λk. integral UNIV (U k)))"
      using bnd int_eq by (auto simp: bounded_real intro!: exI[of _ r])
    show "x. xUNIV  (λk. U k x)  f x"
      using seq by auto
  qed
  moreover have "(λi. (+x. U i x lborel))  (+x. f x lborel)"
    using seq f(2) U_le_f by (intro nn_integral_dominated_convergence[where w=f]) auto
  ultimately have "integral UNIV f = r"
    by (auto simp add: bnd int_eq p seq intro: LIMSEQ_unique)
  with * show ?case
    by (simp add: has_integral_integral)
qed

lemma nn_integral_lborel_eq_integral:
  fixes f::"'a::euclidean_space  real"
  assumes f: "f  borel_measurable borel" "x. 0  f x" "(+x. f x lborel) < "
  shows "(+x. f x lborel) = integral UNIV f"
proof -
  from f(3) obtain r where r: "(+x. f x lborel) = ennreal r" "0  r"
    by (cases "+x. f x lborel" rule: ennreal_cases) auto
  then show ?thesis
    using nn_integral_has_integral[OF f(1,2) r] by (simp add: integral_unique)
qed

lemma nn_integral_integrable_on:
  fixes f::"'a::euclidean_space  real"
  assumes f: "f  borel_measurable borel" "x. 0  f x" "(+x. f x lborel) < "
  shows "f integrable_on UNIV"
proof -
  from f(3) obtain r where r: "(+x. f x lborel) = ennreal r" "0  r"
    by (cases "+x. f x lborel" rule: ennreal_cases) auto
  then show ?thesis
    by (intro has_integral_integrable[where i=r] nn_integral_has_integral[where r=r] f)
qed

lemma nn_integral_has_integral_lborel:
  fixes f :: "'a::euclidean_space  real"
  assumes f_borel: "f  borel_measurable borel" and nonneg: "x. 0  f x"
  assumes I: "(f has_integral I) UNIV"
  shows "integralN lborel f = I"
proof -
  from f_borel have "(λx. ennreal (f x))  borel_measurable lborel" by auto
  from borel_measurable_implies_simple_function_sequence'[OF this]
  obtain F where F: "i. simple_function lborel (F i)" "incseq F"
                 "i x. F i x < top" "x. (SUP i. F i x) = ennreal (f x)"
    by blast
  then have [measurable]: "i. F i  borel_measurable lborel"
    by (metis borel_measurable_simple_function)
  let ?B = "λi::nat. box (- (real i *R One)) (real i *R One) :: 'a set"

  have "0  I"
    using I by (rule has_integral_nonneg) (simp add: nonneg)

  have F_le_f: "enn2real (F i x)  f x" for i x
    using F(3,4)[where x=x] nonneg SUP_upper[of i UNIV "λi. F i x"]
    by (cases "F i x" rule: ennreal_cases) auto
  let ?F = "λi x. F i x * indicator (?B i) x"
  have "(+ x. ennreal (f x) lborel) = (SUP i. integralN lborel (λx. ?F i x))"
  proof (subst nn_integral_monotone_convergence_SUP[symmetric])
    { fix x
      obtain j where j: "x  ?B j"
        using UN_box_eq_UNIV by auto

      have "ennreal (f x) = (SUP i. F i x)"
        using F(4)[of x] nonneg[of x] by (simp add: max_def)
      also have " = (SUP i. ?F i x)"
      proof (rule SUP_eq)
        fix i show "jUNIV. F i x  ?F j x"
          using j F(2)
          by (intro bexI[of _ "max i j"])
             (auto split: split_max split_indicator simp: incseq_def le_fun_def box_def)
      qed (auto intro!: F split: split_indicator)
      finally have "ennreal (f x) =  (SUP i. ?F i x)" . }
    then show "(+ x. ennreal (f x) lborel) = (+ x. (SUP i. ?F i x) lborel)"
      by simp
  qed (insert F, auto simp: incseq_def le_fun_def box_def split: split_indicator)
  also have "  ennreal I"
  proof (rule SUP_least)
    fix i :: nat
    have finite_F: "(+ x. ennreal (enn2real (F i x) * indicator (?B i) x) lborel) < "
    proof (rule nn_integral_bound_simple_function)
      have "emeasure lborel {x  space lborel. ennreal (enn2real (F i x) * indicator (?B i) x)  0} 
        emeasure lborel (?B i)"
        by (intro emeasure_mono)  (auto split: split_indicator)
      then show "emeasure lborel {x  space lborel. ennreal (enn2real (F i x) * indicator (?B i) x)  0} < "
        by (auto simp: less_top[symmetric] top_unique)
    qed (auto split: split_indicator
              intro!: F simple_function_compose1[where g="enn2real"] simple_function_ennreal)

    have int_F: "(λx. enn2real (F i x) * indicator (?B i) x) integrable_on UNIV"
      using F(4) finite_F
      by (intro nn_integral_integrable_on) (auto split: split_indicator simp: enn2real_nonneg)

    have "(+ x. F i x * indicator (?B i) x lborel) =
      (+ x. ennreal (enn2real (F i x) * indicator (?B i) x) lborel)"
      using F(3,4)
      by (intro nn_integral_cong) (auto simp: image_iff eq_commute split: split_indicator)
    also have " = ennreal (integral UNIV (λx. enn2real (F i x) * indicator (?B i) x))"
      using F
      by (intro nn_integral_lborel_eq_integral[OF _ _ finite_F])
         (auto split: split_indicator intro: enn2real_nonneg)
    also have "  ennreal I"
      by (auto intro!: has_integral_le[OF integrable_integral[OF int_F] I] nonneg F_le_f
               simp: 0  I split: split_indicator )
    finally show "(+ x. F i x * indicator (?B i) x lborel)  ennreal I" .
  qed
  finally have "(+ x. ennreal (f x) lborel) < "
    by (auto simp: less_top[symmetric] top_unique)
  from nn_integral_lborel_eq_integral[OF assms(1,2) this] I show ?thesis
    by (simp add: integral_unique)
qed

lemma has_integral_iff_emeasure_lborel:
  fixes A :: "'a::euclidean_space set"
  assumes A[measurable]: "A  sets borel" and [simp]: "0  r"
  shows "((λx. 1) has_integral r) A  emeasure lborel A = ennreal r"
proof (cases "emeasure lborel A = ")
  case emeasure_A: True
  have "¬ (λx. 1::real) integrable_on A"
  proof
    assume int: "(λx. 1::real) integrable_on A"
    then have "(indicator A::'a  real) integrable_on UNIV"
      unfolding indicator_def of_bool_def integrable_restrict_UNIV .
    then obtain r where "((indicator A::'areal) has_integral r) UNIV"
      by auto
    from nn_integral_has_integral_lborel[OF _ _ this] emeasure_A show False
      by (simp add: ennreal_indicator)
  qed
  with emeasure_A show ?thesis
    by auto
next
  case False
  then have "((λx. 1) has_integral measure lborel A) A"
    by (simp add: has_integral_measure_lborel less_top)
  with False show ?thesis
    by (auto simp: emeasure_eq_ennreal_measure has_integral_unique)
qed

lemma ennreal_max_0: "ennreal (max 0 x) = ennreal x"
  by (auto simp: max_def ennreal_neg)

lemma has_integral_integral_real:
  fixes f::"'a::euclidean_space  real"
  assumes f: "integrable lborel f"
  shows "(f has_integral (integralL lborel f)) UNIV"
proof -
  from integrableE[OF f] obtain r q
    where "0  r" "0  q"
      and r: "(+ x. ennreal (max 0 (f x)) lborel) = ennreal r"
      and q: "(+ x. ennreal (max 0 (- f x)) lborel) = ennreal q"
      and f: "f  borel_measurable lborel" and eq: "integralL lborel f = r - q"
    unfolding ennreal_max_0 by auto
  then have "((λx. max 0 (f x)) has_integral r) UNIV" "((λx. max 0 (- f x)) has_integral q) UNIV"
    using nn_integral_has_integral[OF _ _ r] nn_integral_has_integral[OF _ _ q] by auto
  note has_integral_diff[OF this]
  moreover have "(λx. max 0 (f x) - max 0 (- f x)) = f"
    by auto
  ultimately show ?thesis
    by (simp add: eq)
qed

lemma has_integral_AE:
  assumes ae: "AE x in lborel. x  Ω  f x = g x"
  shows "(f has_integral x) Ω = (g has_integral x) Ω"
proof -
  from ae obtain N
    where N: "N  sets borel" "emeasure lborel N = 0" "{x. ¬ (x  Ω  f x = g x)}  N"
    by (auto elim!: AE_E)
  then have not_N: "AE x in lborel. x  N"
    by (simp add: AE_iff_measurable)
  show ?thesis
  proof (rule has_integral_spike_eq[symmetric])
    show "x. xΩ - N  f x = g x" using N(3) by auto
    show "negligible N"
      unfolding negligible_def
    proof (intro allI)
      fix a b :: "'a"
      let ?F = "λx::'a. if x  cbox a b then indicator N x else 0 :: real"
      have "integrable lborel ?F = integrable lborel (λx::'a. 0::real)"
        using not_N N(1) by (intro integrable_cong_AE) auto
      moreover have "(LINT x|lborel. ?F x) = (LINT x::'a|lborel. 0::real)"
        using not_N N(1) by (intro integral_cong_AE) auto
      ultimately have "(?F has_integral 0) UNIV"
        using has_integral_integral_real[of ?F] by simp
      then show "(indicator N has_integral (0::real)) (cbox a b)"
        unfolding has_integral_restrict_UNIV .
    qed
  qed
qed

lemma nn_integral_has_integral_lebesgue:
  fixes f :: "'a::euclidean_space  real"
  assumes nonneg: "x. x  Ω  0  f x" and I: "(f has_integral I) Ω"
  shows "integralN lborel (λx. indicator Ω x * f x) = I"
proof -
  from I have "(λx. indicator Ω x *R f x)  lebesgue M borel"
    by (rule has_integral_implies_lebesgue_measurable)
  then obtain f' :: "'a  real"
    where [measurable]: "f'  borel M borel" and eq: "AE x in lborel. indicator Ω x * f x = f' x"
    by (auto dest: completion_ex_borel_measurable_real)

  from I have "((λx. abs (indicator Ω x * f x)) has_integral I) UNIV"
    using nonneg by (simp add: indicator_def of_bool_def if_distrib[of "λx. x * f y" for y] cong: if_cong)
  also have "((λx. abs (indicator Ω x * f x)) has_integral I) UNIV  ((λx. abs (f' x)) has_integral I) UNIV"
    using eq by (intro has_integral_AE) auto
  finally have "integralN lborel (λx. abs (f' x)) = I"
    by (rule nn_integral_has_integral_lborel[rotated 2]) auto
  also have "integralN lborel (λx. abs (f' x)) = integralN lborel (λx. abs (indicator Ω x * f x))"
    using eq by (intro nn_integral_cong_AE) auto
  also have "(λx. abs (indicator Ω x * f x)) = (λx. indicator Ω x * f x)"
    using nonneg by (auto simp: indicator_def fun_eq_iff)
  finally show ?thesis .
qed

lemma has_integral_iff_nn_integral_lebesgue:
  assumes f: "x. 0  f x"
  shows "(f has_integral r) UNIV  (f  lebesgue M borel  integralN lebesgue f = r  0  r)" (is "?I = ?N")
proof
  assume ?I
  have "0  r"
    using has_integral_nonneg[OF ?I] f by auto
  then show ?N
    using nn_integral_has_integral_lebesgue[OF f ?I]
      has_integral_implies_lebesgue_measurable[OF ?I]
    by (auto simp: nn_integral_completion)
next
  assume ?N
  then obtain f' where f': "f'  borel M borel" "AE x in lborel. f x = f' x"
    by (auto dest: completion_ex_borel_measurable_real)
  moreover have "(+ x. ennreal ¦f' x¦ lborel) = (+ x. ennreal ¦f x¦ lborel)"
    using f' by (intro nn_integral_cong_AE) auto
  moreover have "((λx. ¦f' x¦) has_integral r) UNIV  ((λx. ¦f x¦) has_integral r) UNIV"
    using f' by (intro has_integral_AE) auto
  moreover note nn_integral_has_integral[of "λx. ¦f' x¦" r] ?N
  ultimately show ?I
    using f by (auto simp: nn_integral_completion)
qed

lemma set_nn_integral_lborel_eq_integral:
  fixes f::"'a::euclidean_space  real"
  assumes "set_borel_measurable borel A f"
  assumes "x. x  A  0  f x" "(+xA. f x lborel) < "
  shows "(+xA. f x lborel) = integral A f"
proof -
  have eq: "(+xA. f x lborel) = (+x. ennreal (indicator A x * f x) lborel)"
    by (intro nn_integral_cong) (auto simp: indicator_def)
  also have " = integral UNIV (λx. indicator A x * f x)"
    using assms eq by (intro nn_integral_lborel_eq_integral)
                      (auto simp: indicator_def set_borel_measurable_def)
  also have "integral UNIV (λx. indicator A x * f x) = integral A (λx. indicator A x * f x)"
    by (rule integral_spike_set) (auto intro: empty_imp_negligible)
 
  also have " = integral A f"
    by (rule integral_cong) (auto simp: indicator_def)
  finally show ?thesis .
qed

lemma nn_integral_has_integral_lebesgue':
  fixes f :: "'a::euclidean_space  real"
  assumes nonneg: "x. x  Ω  0  f x" and I: "(f has_integral I) Ω"
  shows "integralN lborel (λx. ennreal (f x) * indicator Ω x) = ennreal I"
proof -
  have "integralN lborel (λx. ennreal (f x) * indicator Ω x) =
        integralN lborel (λx. ennreal (indicator Ω x * f x))"
    by (intro nn_integral_cong) (auto simp: indicator_def)
  also have " = ennreal I"
    using assms by (intro nn_integral_has_integral_lebesgue)
  finally show ?thesis .
qed

context
  fixes f::"'a::euclidean_space  'b::euclidean_space"
begin

lemma has_integral_integral_lborel:
  assumes f: "integrable lborel f"
  shows "(f has_integral (integralL lborel f)) UNIV"
proof -
  have "((λx. bBasis. (f x  b) *R b) has_integral (bBasis. integralL lborel (λx. f x  b) *R b)) UNIV"
    using f by (intro has_integral_sum finite_Basis ballI has_integral_scaleR_left has_integral_integral_real) auto
  also have eq_f: "(λx. bBasis. (f x  b) *R b) = f"
    by (simp add: fun_eq_iff euclidean_representation)
  also have "(bBasis. integralL lborel (λx. f x  b) *R b) = integralL lborel f"
    using f by (subst (2) eq_f[symmetric]) simp
  finally show ?thesis .
qed

lemma integrable_on_lborel: "integrable lborel f  f integrable_on UNIV"
  using has_integral_integral_lborel by auto

lemma integral_lborel: "integrable lborel f  integral UNIV f = (x. f x lborel)"
  using has_integral_integral_lborel by auto

end

context
begin

private lemma has_integral_integral_lebesgue_real:
  fixes f :: "'a::euclidean_space  real"
  assumes f: "integrable lebesgue f"
  shows "(f has_integral (integralL lebesgue f)) UNIV"
proof -
  obtain f' where f': "f'  borel M borel" "AE x in lborel. f x = f' x"
    using completion_ex_borel_measurable_real[OF borel_measurable_integrable[OF f]] by auto
  moreover have "(+ x. ennreal (norm (f x)) lborel) = (+ x. ennreal (norm (f' x)) lborel)"
    using f' by (intro nn_integral_cong_AE) auto
  ultimately have "integrable lborel f'"
    using f by (auto simp: integrable_iff_bounded nn_integral_completion cong: nn_integral_cong_AE)
  note has_integral_integral_real[OF this]
  moreover have "integralL lebesgue f = integralL lebesgue f'"
    using f' f by (intro integral_cong_AE) (auto intro: AE_completion measurable_completion)
  moreover have "integralL lebesgue f' = integralL lborel f'"
    using f' by (simp add: integral_completion)
  moreover have "(f' has_integral integralL lborel f') UNIV  (f has_integral integralL lborel f') UNIV"
    using f' by (intro has_integral_AE) auto
  ultimately show ?thesis
    by auto
qed

lemma has_integral_integral_lebesgue:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes f: "integrable lebesgue f"
  shows "(f has_integral (integralL lebesgue f)) UNIV"
proof -
  have "((λx. bBasis. (f x  b) *R b) has_integral (bBasis. integralL lebesgue (λx. f x  b) *R b)) UNIV"
    using f by (intro has_integral_sum finite_Basis ballI has_integral_scaleR_left has_integral_integral_lebesgue_real) auto
  also have eq_f: "(λx. bBasis. (f x  b) *R b) = f"
    by (simp add: fun_eq_iff euclidean_representation)
  also have "(bBasis. integralL lebesgue (λx. f x  b) *R b) = integralL lebesgue f"
    using f by (subst (2) eq_f[symmetric]) simp
  finally show ?thesis .
qed

lemma has_integral_integral_lebesgue_on:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "integrable (lebesgue_on S) f" "S  sets lebesgue"
  shows "(f has_integral (integralL (lebesgue_on S) f)) S"
proof -
  let ?f = "λx. if x  S then f x else 0"
  have "integrable lebesgue (λx. indicat_real S x *R f x)"
    using indicator_scaleR_eq_if [of S _ f] assms
  by (metis (full_types) integrable_restrict_space sets.Int_space_eq2)
  then have "integrable lebesgue ?f"
    using indicator_scaleR_eq_if [of S _ f] assms by auto
  then have "(?f has_integral (integralL lebesgue ?f)) UNIV"
    by (rule has_integral_integral_lebesgue)
  then have "(f has_integral (integralL lebesgue ?f)) S"
    using has_integral_restrict_UNIV by blast
  moreover
  have "S  space lebesgue  sets lebesgue"
    by (simp add: assms)
  then have "(integralL lebesgue ?f) = (integralL (lebesgue_on S) f)"
    by (simp add: integral_restrict_space indicator_scaleR_eq_if)
  ultimately show ?thesis
    by auto
qed

lemma lebesgue_integral_eq_integral:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "integrable (lebesgue_on S) f" "S  sets lebesgue"
  shows "integralL (lebesgue_on S) f = integral S f"
  by (metis has_integral_integral_lebesgue_on assms integral_unique)

lemma integrable_on_lebesgue:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  shows "integrable lebesgue f  f integrable_on UNIV"
  using has_integral_integral_lebesgue by auto

lemma integral_lebesgue:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  shows "integrable lebesgue f  integral UNIV f = (x. f x lebesgue)"
  using has_integral_integral_lebesgue by auto

end

subsection ‹Absolute integrability (this is the same as Lebesgue integrability)›

translations
"LBINT x. f" == "CONST lebesgue_integral CONST lborel (λx. f)"

translations
"LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (λx. f)"

lemma set_integral_reflect:
  fixes S and f :: "real  'a :: {banach, second_countable_topology}"
  shows "(LBINT x : S. f x) = (LBINT x : {x. - x  S}. f (- x))"
  unfolding set_lebesgue_integral_def
  by (subst lborel_integral_real_affine[where c="-1" and t=0])
     (auto intro!: Bochner_Integration.integral_cong split: split_indicator)

lemma borel_integrable_atLeastAtMost':
  fixes f :: "real  'a::{banach, second_countable_topology}"
  assumes f: "continuous_on {a..b} f"
  shows "set_integrable lborel {a..b} f"
  unfolding set_integrable_def
  by (intro borel_integrable_compact compact_Icc f)

lemma integral_FTC_atLeastAtMost:
  fixes f :: "real  'a :: euclidean_space"
  assumes "a  b"
    and F: "x. a  x  x  b  (F has_vector_derivative f x) (at x within {a .. b})"
    and f: "continuous_on {a .. b} f"
  shows "integralL lborel (λx. indicator {a .. b} x *R f x) = F b - F a"
proof -
  let ?f = "λx. indicator {a .. b} x *R f x"
  have "(?f has_integral (x. ?f x lborel)) UNIV"
    using borel_integrable_atLeastAtMost'[OF f]
    unfolding set_integrable_def by (rule has_integral_integral_lborel)
  moreover
  have "(f has_integral F b - F a) {a .. b}"
    by (intro fundamental_theorem_of_calculus ballI assms) auto
  then have "(?f has_integral F b - F a) {a .. b}"
    by (subst has_integral_cong[where g=f]) auto
  then have "(?f has_integral F b - F a) UNIV"
    by (intro has_integral_on_superset[where T=UNIV and S="{a..b}"]) auto
  ultimately show "integralL lborel ?f = F b - F a"
    by (rule has_integral_unique)
qed

lemma set_borel_integral_eq_integral:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "set_integrable lborel S f"
  shows "f integrable_on S" "(LINT x : S | lborel. f x) = integral S f"
proof -
  let ?f = "λx. indicator S x *R f x"
  have "(?f has_integral (LINT x : S | lborel. f x)) UNIV"
    using assms has_integral_integral_lborel
    unfolding set_integrable_def set_lebesgue_integral_def by blast
  hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
    by (simp add: indicator_scaleR_eq_if)
  thus "f integrable_on S"
    by (auto simp add: integrable_on_def)
  with 1 have "(f has_integral (integral S f)) S"
    by (intro integrable_integral, auto simp add: integrable_on_def)
  thus "(LINT x : S | lborel. f x) = integral S f"
    by (intro has_integral_unique [OF 1])
qed

lemma has_integral_set_lebesgue:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes f: "set_integrable lebesgue S f"
  shows "(f has_integral (LINT x:S|lebesgue. f x)) S"
  using has_integral_integral_lebesgue f
  by (fastforce simp add: set_integrable_def set_lebesgue_integral_def indicator_def
    of_bool_def if_distrib[of "λx. x *R f _"] cong: if_cong)

lemma set_lebesgue_integral_eq_integral:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes f: "set_integrable lebesgue S f"
  shows "f integrable_on S" "(LINT x:S | lebesgue. f x) = integral S f"
  using has_integral_set_lebesgue[OF f] by (auto simp: integral_unique integrable_on_def)

lemma lmeasurable_iff_has_integral:
  "S  lmeasurable  ((indicator S) has_integral measure lebesgue S) UNIV"
  by (subst has_integral_iff_nn_integral_lebesgue)
     (auto simp: ennreal_indicator emeasure_eq_measure2 borel_measurable_indicator_iff intro!: fmeasurableI)

abbreviation
  absolutely_integrable_on :: "('a::euclidean_space  'b::{banach, second_countable_topology})  'a set  bool"
  (infixr "absolutely'_integrable'_on" 46)
  where "f absolutely_integrable_on s  set_integrable lebesgue s f"


lemma absolutely_integrable_zero [simp]: "(λx. 0) absolutely_integrable_on S"
    by (simp add: set_integrable_def)

lemma absolutely_integrable_on_def:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  shows "f absolutely_integrable_on S  f integrable_on S  (λx. norm (f x)) integrable_on S"
proof safe
  assume f: "f absolutely_integrable_on S"
  then have nf: "integrable lebesgue (λx. norm (indicator S x *R f x))"
    using integrable_norm set_integrable_def by blast
  show "f integrable_on S"
    by (rule set_lebesgue_integral_eq_integral[OF f])
  have "(λx. norm (indicator S x *R f x)) = (λx. if x  S then norm (f x) else 0)"
    by auto
  with integrable_on_lebesgue[OF nf] show "(λx. norm (f x)) integrable_on S"
    by (simp add: integrable_restrict_UNIV)
next
  assume f: "f integrable_on S" and nf: "(λx. norm (f x)) integrable_on S"
  show "f absolutely_integrable_on S"
    unfolding set_integrable_def
  proof (rule integrableI_bounded)
    show "(λx. indicator S x *R f x)  borel_measurable lebesgue"
      using f has_integral_implies_lebesgue_measurable[of f _ S] by (auto simp: integrable_on_def)
    show "(+ x. ennreal (norm (indicator S x *R f x)) lebesgue) < "
      using nf nn_integral_has_integral_lebesgue[of _ "λx. norm (f x)"]
      by (auto simp: integrable_on_def nn_integral_completion)
  qed
qed

lemma integrable_on_lebesgue_on:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes f: "integrable (lebesgue_on S) f" and S: "S  sets lebesgue"
  shows "f integrable_on S"
proof -
  have "integrable lebesgue (λx. indicator S x *R f x)"
    using S f inf_top.comm_neutral integrable_restrict_space by blast
  then show ?thesis
    using absolutely_integrable_on_def set_integrable_def by blast
qed

lemma absolutely_integrable_imp_integrable:
  assumes "f absolutely_integrable_on S" "S  sets lebesgue"
  shows "integrable (lebesgue_on S) f"
  by (meson assms integrable_restrict_space set_integrable_def sets.Int sets.top)

lemma absolutely_integrable_on_null [intro]:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  shows "content (cbox a b) = 0  f absolutely_integrable_on (cbox a b)"
  by (auto simp: absolutely_integrable_on_def)

lemma absolutely_integrable_on_open_interval:
  fixes f :: "'a :: euclidean_space  'b :: euclidean_space"
  shows "f absolutely_integrable_on box a b 
         f absolutely_integrable_on cbox a b"
  by (auto simp: integrable_on_open_interval absolutely_integrable_on_def)

lemma absolutely_integrable_restrict_UNIV:
  "(λx. if x  S then f x else 0) absolutely_integrable_on UNIV  f absolutely_integrable_on S"
    unfolding set_integrable_def
  by (intro arg_cong2[where f=integrable]) auto

lemma absolutely_integrable_onI:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  shows "f integrable_on S  (λx. norm (f x)) integrable_on S  f absolutely_integrable_on S"
  unfolding absolutely_integrable_on_def by auto

lemma nonnegative_absolutely_integrable_1:
  fixes f :: "'a :: euclidean_space  real"
  assumes f: "f integrable_on A" and "x. x  A  0  f x"
  shows "f absolutely_integrable_on A"
  by (rule absolutely_integrable_onI [OF f]) (use assms in simp add: integrable_eq)

lemma absolutely_integrable_on_iff_nonneg:
  fixes f :: "'a :: euclidean_space  real"
  assumes "x. x  S  0  f x" shows "f absolutely_integrable_on S  f integrable_on S"
proof -
  { assume "f integrable_on S"
    then have "(λx. if x  S then f x else 0) integrable_on UNIV"
      by (simp add: integrable_restrict_UNIV)
    then have "(λx. if x  S then f x else 0) absolutely_integrable_on UNIV"
      using f integrable_on S absolutely_integrable_restrict_UNIV assms nonnegative_absolutely_integrable_1 by blast
    then have "f absolutely_integrable_on S"
      using absolutely_integrable_restrict_UNIV by blast
  }
  then show ?thesis
    unfolding absolutely_integrable_on_def by auto
qed

lemma absolutely_integrable_on_scaleR_iff:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  shows
   "(λx. c *R f x) absolutely_integrable_on S 
      c = 0  f absolutely_integrable_on S"
proof (cases "c=0")
  case False
  then show ?thesis
  unfolding absolutely_integrable_on_def
  by (simp add: norm_mult)
qed auto

lemma absolutely_integrable_spike:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "f absolutely_integrable_on T" and S: "negligible S" "x. x  T - S  g x = f x"
  shows "g absolutely_integrable_on T"
  using assms integrable_spike
  unfolding absolutely_integrable_on_def by metis

lemma absolutely_integrable_negligible:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "negligible S"
  shows "f absolutely_integrable_on S"
  using assms by (simp add: absolutely_integrable_on_def integrable_negligible)

lemma absolutely_integrable_spike_eq:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "negligible S" "x. x  T - S  g x = f x"
  shows "(f absolutely_integrable_on T  g absolutely_integrable_on T)"
  using assms by (blast intro: absolutely_integrable_spike sym)

lemma absolutely_integrable_spike_set_eq:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "negligible {x  S - T. f x  0}" "negligible {x  T - S. f x  0}"
  shows "(f absolutely_integrable_on S  f absolutely_integrable_on T)"
proof -
  have "(λx. if x  S then f x else 0) absolutely_integrable_on UNIV 
        (λx. if x  T then f x else 0) absolutely_integrable_on UNIV"
  proof (rule absolutely_integrable_spike_eq)
    show "negligible ({x  S - T. f x  0}  {x  T - S. f x  0})"
      by (rule negligible_Un [OF assms])
  qed auto
  with absolutely_integrable_restrict_UNIV show ?thesis
    by blast
qed

lemma absolutely_integrable_spike_set:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes f: "f absolutely_integrable_on S" and neg: "negligible {x  S - T. f x  0}" "negligible {x  T - S. f x  0}"
  shows "f absolutely_integrable_on T"
  using absolutely_integrable_spike_set_eq f neg by blast

lemma absolutely_integrable_reflect[simp]:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  shows "(λx. f(-x)) absolutely_integrable_on cbox (-b) (-a)  f absolutely_integrable_on cbox a b"
  unfolding absolutely_integrable_on_def
  by (metis (mono_tags, lifting) integrable_eq integrable_reflect)

lemma absolutely_integrable_reflect_real[simp]:
  fixes f :: "real  'b::euclidean_space"
  shows "(λx. f(-x)) absolutely_integrable_on {-b .. -a}  f absolutely_integrable_on {a..b::real}"
  unfolding box_real[symmetric] by (rule absolutely_integrable_reflect)

lemma absolutely_integrable_on_subcbox:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  shows "f absolutely_integrable_on S; cbox a b  S  f absolutely_integrable_on cbox a b"
  by (meson absolutely_integrable_on_def integrable_on_subcbox)

lemma absolutely_integrable_on_subinterval:
  fixes f :: "real  'b::euclidean_space"
  shows "f absolutely_integrable_on S; {a..b}  S  f absolutely_integrable_on {a..b}"
  using absolutely_integrable_on_subcbox by fastforce

lemma integrable_subinterval:
  fixes f :: "real  'a::euclidean_space"
  assumes "integrable (lebesgue_on {a..b}) f"
    and "{c..d}  {a..b}"
  shows "integrable (lebesgue_on {c..d}) f"
proof (rule absolutely_integrable_imp_integrable)
  show "f absolutely_integrable_on {c..d}"
  proof -
    have "f integrable_on {c..d}"
      using assms integrable_on_lebesgue_on integrable_on_subinterval by fastforce
    moreover have "(λx. norm (f x)) integrable_on {c..d}"
    proof (rule integrable_on_subinterval)
      show "(λx. norm (f x)) integrable_on {a..b}"
        by (simp add: assms integrable_on_lebesgue_on)
    qed (use assms in auto)
    ultimately show ?thesis
      by (auto simp: absolutely_integrable_on_def)
  qed
qed auto

lemma indefinite_integral_continuous_real:
  fixes f :: "real  'a::euclidean_space"
  assumes "integrable (lebesgue_on {a..b}) f"
  shows "continuous_on {a..b} (λx. integralL (lebesgue_on {a..x}) f)"
proof -
  have "f integrable_on {a..b}"
    by (simp add: assms integrable_on_lebesgue_on)
  then have "continuous_on {a..b} (λx. integral {a..x} f)"
    using indefinite_integral_continuous_1 by blast
  moreover have "integralL (lebesgue_on {a..x}) f = integral {a..x} f" if "a  x" "x  b" for x
  proof -
    have "{a..x}  {a..b}"
      using that by auto
    then have "integrable (lebesgue_on {a..x}) f"
      using integrable_subinterval assms by blast
    then show "integralL (lebesgue_on {a..x}) f = integral {a..x} f"
      by (simp add: lebesgue_integral_eq_integral)
  qed
  ultimately show ?thesis
    by (metis (no_types, lifting) atLeastAtMost_iff continuous_on_cong)
qed

lemma lmeasurable_iff_integrable_on: "S  lmeasurable  (λx. 1::real) integrable_on S"
  by (subst absolutely_integrable_on_iff_nonneg[symmetric])
     (simp_all add: lmeasurable_iff_integrable set_integrable_def)

lemma lmeasure_integral_UNIV: "S  lmeasurable  measure lebesgue S = integral UNIV (indicator S)"
  by (simp add: lmeasurable_iff_has_integral integral_unique)

lemma lmeasure_integral: "S  lmeasurable  measure lebesgue S = integral S (λx. 1::real)"
  by (fastforce simp add: lmeasure_integral_UNIV indicator_def [abs_def] of_bool_def lmeasurable_iff_integrable_on)

lemma integrable_on_const: "S  lmeasurable  (λx. c) integrable_on S"
  unfolding lmeasurable_iff_integrable
  by (metis (mono_tags, lifting) integrable_eq integrable_on_scaleR_left lmeasurable_iff_integrable lmeasurable_iff_integrable_on scaleR_one)

lemma integral_indicator:
  assumes "(S  T)  lmeasurable"
  shows "integral T (indicator S) = measure lebesgue (S  T)"
proof -
  have "integral UNIV (indicator (S  T)) = integral UNIV (λa. if a  S  T then 1::real else 0)"
    by (simp add: indicator_def [abs_def] of_bool_def)
  moreover have "(indicator (S  T) has_integral measure lebesgue (S  T)) UNIV"
    using assms by (simp add: lmeasurable_iff_has_integral)
  ultimately have "integral UNIV (λx. if x  S  T then 1 else 0) = measure lebesgue (S  T)"
    by (metis (no_types) integral_unique)
  moreover have "integral T (λa. if a  S then 1::real else 0) = integral (S  T  UNIV) (λa. 1)"
    by (simp add: Henstock_Kurzweil_Integration.integral_restrict_Int)
  moreover have "integral T (indicat_real S) = integral T (λa. if a  S then 1 else 0)"
    by (simp add: indicator_def [abs_def] of_bool_def)
  ultimately show ?thesis
    by (simp add: assms lmeasure_integral)
qed

lemma measurable_integrable:
  fixes S :: "'a::euclidean_space set"
  shows "S  lmeasurable  (indicat_real S) integrable_on UNIV"
  by (auto simp: lmeasurable_iff_integrable absolutely_integrable_on_iff_nonneg [symmetric] set_integrable_def)

lemma integrable_on_indicator:
  fixes S :: "'a::euclidean_space set"
  shows "indicat_real S integrable_on T  (S  T)  lmeasurable"
  unfolding measurable_integrable
  unfolding integrable_restrict_UNIV [of T, symmetric]
  by (fastforce simp add: indicator_def elim: integrable_eq)

lemma
  assumes 𝒟: "𝒟 division_of S"
  shows lmeasurable_division: "S  lmeasurable" (is ?l)
    and content_division: "(k𝒟. measure lebesgue k) = measure lebesgue S" (is ?m)
proof -
  { fix d1 d2 assume *: "d1  𝒟" "d2  𝒟" "d1  d2"
    then obtain a b c d where "d1 = cbox a b" "d2 = cbox c d"
      using division_ofD(4)[OF 𝒟] by blast
    with division_ofD(5)[OF 𝒟 *]
    have "d1  sets lborel" "d2  sets lborel" "d1  d2  (cbox a b - box a b)  (cbox c d - box c d)"
      by auto
    moreover have "(cbox a b - box a b)  (cbox c d - box c d)  null_sets lborel"
      by (intro null_sets.Un null_sets_cbox_Diff_box)
    ultimately have "d1  d2  null_sets lborel"
      by (blast intro: null_sets_subset) }
  then show ?l ?m
    unfolding division_ofD(6)[OF 𝒟, symmetric]
    using division_ofD(1,4)[OF 𝒟]
    by (auto intro!: measure_Union_AE[symmetric] simp: completion.AE_iff_null_sets Int_def[symmetric] pairwise_def null_sets_def)
qed

lemma has_measure_limit:
  assumes "S  lmeasurable" "e > 0"
  obtains B where "B > 0"
    "a b. ball 0 B  cbox a b  ¦measure lebesgue (S  cbox a b) - measure lebesgue S¦ < e"
  using assms unfolding lmeasurable_iff_has_integral has_integral_alt'
  by (force simp: integral_indicator integrable_on_indicator)

lemma lmeasurable_iff_indicator_has_integral:
  fixes S :: "'a::euclidean_space set"
  shows "S  lmeasurable  m = measure lebesgue S  (indicat_real S has_integral m) UNIV"
  by (metis has_integral_iff lmeasurable_iff_has_integral measurable_integrable)

lemma has_measure_limit_iff:
  fixes f :: "'n::euclidean_space  'a::banach"
  shows "S  lmeasurable  m = measure lebesgue S 
          (e>0. B>0. a b. ball 0 B  cbox a b 
            (S  cbox a b)  lmeasurable  ¦measure lebesgue (S  cbox a b) - m¦ < e)" (is "?lhs = ?rhs")
proof
  assume ?lhs then show ?rhs
    by (meson has_measure_limit fmeasurable.Int lmeasurable_cbox)
next
  assume RHS [rule_format]: ?rhs
  then show ?lhs
    apply (simp add: lmeasurable_iff_indicator_has_integral has_integral' [where i=m])
    by (metis (full_types) integral_indicator integrable_integral integrable_on_indicator)
qed

subsection‹Applications to Negligibility›

lemma negligible_iff_null_sets: "negligible S  S  null_sets lebesgue"
proof
  assume "negligible S"
  then have "(indicator S has_integral (0::real)) UNIV"
    by (auto simp: negligible)
  then show "S  null_sets lebesgue"
    by (subst (asm) has_integral_iff_nn_integral_lebesgue)
        (auto simp: borel_measurable_indicator_iff nn_integral_0_iff_AE AE_iff_null_sets indicator_eq_0_iff)
next
  assume S: "S  null_sets lebesgue"
  show "negligible S"
    unfolding negligible_def
  proof (safe intro!: has_integral_iff_nn_integral_lebesgue[THEN iffD2]
                      has_integral_restrict_UNIV[where s="cbox _ _", THEN iffD1])
    fix a b
    show "(λx. if x  cbox a b then indicator S x else 0)  lebesgue M borel"
      using S by (auto intro!: measurable_If)
    then show "(+ x. ennreal (if x  cbox a b then indicator S x else 0) lebesgue) = ennreal 0"
      using S[THEN AE_not_in] by (auto intro!: nn_integral_0_iff_AE[THEN iffD2])
  qed auto
qed

corollary eventually_ae_filter_negligible:
  "eventually P (ae_filter lebesgue)  (N. negligible N  {x. ¬ P x}  N)"
  by (auto simp: completion.AE_iff_null_sets negligible_iff_null_sets null_sets_completion_subset)

lemma starlike_negligible:
  assumes "closed S"
      and eq1: "c x. (a + c *R x)  S  0  c  a + x  S  c = 1"
    shows "negligible S"
proof -
  have "negligible ((+) (-a) ` S)"
  proof (subst negligible_on_intervals, intro allI)
    fix u v
    show "negligible ((+) (- a) ` S  cbox u v)"
      using closed S eq1 by (auto simp add: negligible_iff_null_sets algebra_simps
        intro!: closed_translation_subtract starlike_negligible_compact cong: image_cong_simp)
        (metis add_diff_eq diff_add_cancel scale_right_diff_distrib)
  qed
  then show ?thesis
    by (rule negligible_translation_rev)
qed

lemma starlike_negligible_strong:
  assumes "closed S"
      and star: "c x. 0  c; c < 1; a+x  S  a + c *R x  S"
    shows "negligible S"
proof -
  show ?thesis
  proof (rule starlike_negligible [OF closed S, of a])
    fix c x
    assume cx: "a + c *R x  S" "0  c" "a + x  S"
    with star have "¬ (c < 1)" by auto
    moreover have "¬ (c > 1)"
      using star [of "1/c" "c *R x"] cx by force
    ultimately show "c = 1" by arith
  qed
qed

lemma negligible_hyperplane:
  assumes "a  0  b  0" shows "negligible {x. a  x = b}"
proof -
  obtain x where x: "a  x  b"
    using assms by (metis euclidean_all_zero_iff inner_zero_right)
  moreover have "c = 1" if "a  (x + c *R w) = b" "a  (x + w) = b" for c w
    using that
    by (metis (no_types, opaque_lifting) add_diff_eq diff_0 diff_minus_eq_add inner_diff_right inner_scaleR_right mult_cancel_right2 right_minus_eq x)
  ultimately
  show ?thesis
    using starlike_negligible [OF closed_hyperplane, of x] by simp
qed

lemma negligible_lowdim:
  fixes S :: "'N :: euclidean_space set"
  assumes "dim S < DIM('N)"
    shows "negligible S"
proof -
  obtain a where "a  0" and a: "span S  {x. a  x = 0}"
    using lowdim_subset_hyperplane [OF assms] by blast
  have "negligible (span S)"
    using a  0 a negligible_hyperplane by (blast intro: negligible_subset)
  then show ?thesis
    using span_base by (blast intro: negligible_subset)
qed

proposition negligible_convex_frontier:
  fixes S :: "'N :: euclidean_space set"
  assumes "convex S"
    shows "negligible(frontier S)"
proof -
  have nf: "negligible(frontier S)" if "convex S" "0  S" for S :: "'N set"
  proof -
    obtain B where "B  S" and indB: "independent B"
               and spanB: "S  span B" and cardB: "card B = dim S"
      by (metis basis_exists)
    consider "dim S < DIM('N)" | "dim S = DIM('N)"
      using dim_subset_UNIV le_eq_less_or_eq by auto
    then show ?thesis
    proof cases
      case 1
      show ?thesis
        by (rule negligible_subset [of "closure S"])
           (simp_all add: frontier_def negligible_lowdim 1)
    next
      case 2
      obtain a where "a  interior (convex hull insert 0 B)"
      proof (rule interior_simplex_nonempty [OF indB])
        show "finite B"
          by (simp add: indB independent_imp_finite)
        show "card B = DIM('N)"
          by (simp add: cardB 2)
      qed
      then have a: "a  interior S"
        by (metis B  S 0  S convex S insert_absorb insert_subset interior_mono subset_hull)
      show ?thesis
      proof (rule starlike_negligible_strong [where a=a])
        fix c::real and x
        have eq: "a + c *R x = (a + x) - (1 - c) *R ((a + x) - a)"
          by (simp add: algebra_simps)
        assume "0  c" "c < 1" "a + x  frontier S"
        then show "a + c *R x  frontier S"
          using eq mem_interior_closure_convex_shrink [OF convex S a, of _ "1-c"]
          unfolding frontier_def
          by (metis Diff_iff add_diff_cancel_left' add_diff_eq diff_gt_0_iff_gt group_cancel.rule0 not_le)
      qed auto
    qed
  qed
  show ?thesis
  proof (cases "S = {}")
    case True then show ?thesis by auto
  next
    case False
    then obtain a where "a  S" by auto
    show ?thesis
      using nf [of "(λx. -a + x) ` S"]
      by (metis a  S add.left_inverse assms convex_translation_eq frontier_translation
                image_eqI negligible_translation_rev)
  qed
qed

corollary negligible_sphere: "negligible (sphere a e)"
  using frontier_cball negligible_convex_frontier convex_cball
  by (blast intro: negligible_subset)

lemma non_negligible_UNIV [simp]: "¬ negligible UNIV"
  unfolding negligible_iff_null_sets by (auto simp: null_sets_def)

lemma negligible_interval:
  "negligible (cbox a b)  box a b = {}" "negligible (box a b)  box a b = {}"
   by (auto simp: negligible_iff_null_sets null_sets_def prod_nonneg inner_diff_left box_eq_empty
                  not_le emeasure_lborel_cbox_eq emeasure_lborel_box_eq
            intro: eq_refl antisym less_imp_le)

proposition open_not_negligible:
  assumes "open S" "S  {}"
  shows "¬ negligible S"
proof
  assume neg: "negligible S"
  obtain a where "a  S"
    using S  {} by blast
  then obtain e where "e > 0" "cball a e  S"
    using open S open_contains_cball_eq by blast
  let ?p = "a - (e / DIM('a)) *R One" let ?q = "a + (e / DIM('a)) *R One"
  have "cbox ?p ?q  cball a e"
  proof (clarsimp simp: mem_box dist_norm)
    fix x
    assume "iBasis. ?p  i  x  i  x  i  ?q  i"
    then have ax: "¦(a - x)  i¦  e / real DIM('a)" if "i  Basis" for i
      using that by (auto simp: algebra_simps)
    have "norm (a - x)  (iBasis. ¦(a - x)  i¦)"
      by (rule norm_le_l1)
    also have "  DIM('a) * (e / real DIM('a))"
      by (intro sum_bounded_above ax)
    also have " = e"
      by simp
    finally show "norm (a - x)  e" .
  qed
  then have "negligible (cbox ?p ?q)"
    by (meson cball a e  S neg negligible_subset)
  with e > 0 show False
    by (simp add: negligible_interval box_eq_empty algebra_simps field_split_simps mult_le_0_iff)
qed

lemma negligible_convex_interior:
   "convex S  (negligible S  interior S = {})"
  by (metis Diff_empty closure_subset frontier_def interior_subset negligible_convex_frontier negligible_subset open_interior open_not_negligible)

lemma measure_eq_0_null_sets: "S  null_sets M  measure M S = 0"
  by (auto simp: measure_def null_sets_def)

lemma negligible_imp_measure0: "negligible S  measure lebesgue S = 0"
  by (simp add: measure_eq_0_null_sets negligible_iff_null_sets)

lemma negligible_iff_emeasure0: "S  sets lebesgue  (negligible S  emeasure lebesgue S = 0)"
  by (auto simp: measure_eq_0_null_sets negligible_iff_null_sets)

lemma negligible_iff_measure0: "S  lmeasurable  (negligible S  measure lebesgue S = 0)"
  by (metis (full_types) completion.null_sets_outer negligible_iff_null_sets negligible_imp_measure0 order_refl)

lemma negligible_imp_sets: "negligible S  S  sets lebesgue"
  by (simp add: negligible_iff_null_sets null_setsD2)

lemma negligible_imp_measurable: "negligible S  S  lmeasurable"
  by (simp add: fmeasurableI_null_sets negligible_iff_null_sets)

lemma negligible_iff_measure: "negligible S  S  lmeasurable  measure lebesgue S = 0"
  by (fastforce simp: negligible_iff_measure0 negligible_imp_measurable dest: negligible_imp_measure0)

lemma negligible_outer:
  "negligible S  (e>0. T. S  T  T  lmeasurable  measure lebesgue T < e)" (is "_ = ?rhs")
proof
  assume "negligible S" then show ?rhs
    by (metis negligible_iff_measure order_refl)
next
  assume ?rhs then show "negligible S"
  by (meson completion.null_sets_outer negligible_iff_null_sets)
qed

lemma negligible_outer_le:
     "negligible S  (e>0. T. S  T  T  lmeasurable  measure lebesgue T  e)" (is "_ = ?rhs")
proof
  assume "negligible S" then show ?rhs
    by (metis dual_order.strict_implies_order negligible_imp_measurable negligible_imp_measure0 order_refl)
next
  assume ?rhs then show "negligible S"
    by (metis le_less_trans negligible_outer field_lbound_gt_zero)
qed

lemma negligible_UNIV: "negligible S  (indicat_real S has_integral 0) UNIV" (is "_=?rhs")
  by (metis lmeasurable_iff_indicator_has_integral negligible_iff_measure)

lemma sets_negligible_symdiff:
   "S  sets lebesgue; negligible((S - T)  (T - S))  T  sets lebesgue"
  by (metis Diff_Diff_Int Int_Diff_Un inf_commute negligible_Un_eq negligible_imp_sets sets.Diff sets.Un)

lemma lmeasurable_negligible_symdiff:
   "S  lmeasurable; negligible((S - T)  (T - S))  T  lmeasurable"
  using integrable_spike_set_eq lmeasurable_iff_integrable_on by blast


lemma measure_Un3_negligible:
  assumes meas: "S  lmeasurable" "T  lmeasurable" "U  lmeasurable"
  and neg: "negligible(S  T)" "negligible(S  U)" "negligible(T  U)" and V: "S  T  U = V"
shows "measure lebesgue V = measure lebesgue S + measure lebesgue T + measure lebesgue U"
proof -
  have [simp]: "measure lebesgue (S  T) = 0"
    using neg(1) negligible_imp_measure0 by blast
  have [simp]: "measure lebesgue (S  U  T  U) = 0"
    using neg(2) neg(3) negligible_Un negligible_imp_measure0 by blast
  have "measure lebesgue V = measure lebesgue (S  T  U)"
    using V by simp
  also have " = measure lebesgue S + measure lebesgue T + measure lebesgue U"
    by (simp add: measure_Un3 meas fmeasurable.Un Int_Un_distrib2)
  finally show ?thesis .
qed

lemma measure_translate_add:
  assumes meas: "S  lmeasurable" "T  lmeasurable"
    and U: "S  ((+)a ` T) = U" and neg: "negligible(S  ((+)a ` T))"
  shows "measure lebesgue S + measure lebesgue T = measure lebesgue U"
proof -
  have [simp]: "measure lebesgue (S  (+) a ` T) = 0"
    using neg negligible_imp_measure0 by blast
  have "measure lebesgue (S  ((+)a ` T)) = measure lebesgue S + measure lebesgue T"
    by (simp add: measure_Un3 meas measurable_translation measure_translation fmeasurable.Un)
  then show ?thesis
    using U by auto
qed

lemma measure_negligible_symdiff:
  assumes S: "S  lmeasurable"
    and neg: "negligible (S - T  (T - S))"
  shows "measure lebesgue T = measure lebesgue S"
proof -
  have "measure lebesgue (S - T) = 0"
    using neg negligible_Un_eq negligible_imp_measure0 by blast
  then show ?thesis
    by (metis S Un_commute add.right_neutral lmeasurable_negligible_symdiff measure_Un2 neg negligible_Un_eq negligible_imp_measure0)
qed

lemma measure_closure:
  assumes "bounded S" and neg: "negligible (frontier S)"
  shows "measure lebesgue (closure S) = measure lebesgue S"
proof -
  have "measure lebesgue (frontier S) = 0"
    by (metis neg negligible_imp_measure0)
  then show ?thesis
    by (metis assms lmeasurable_iff_integrable_on eq_iff_diff_eq_0 has_integral_interior integrable_on_def integral_unique lmeasurable_interior lmeasure_integral measure_frontier)
qed

lemma measure_interior:
   "bounded S; negligible(frontier S)  measure lebesgue (interior S) = measure lebesgue S"
  using measure_closure measure_frontier negligible_imp_measure0 by fastforce

lemma measurable_Jordan:
  assumes "bounded S" and neg: "negligible (frontier S)"
  shows "S  lmeasurable"
proof -
  have "closure S  lmeasurable"
    by (metis lmeasurable_closure bounded S)
  moreover have "interior S  lmeasurable"
    by (simp add: lmeasurable_interior bounded S)
  moreover have "interior S  S"
    by (simp add: interior_subset)
  ultimately show ?thesis
    using assms by (metis (full_types) closure_subset completion.complete_sets_sandwich_fmeasurable measure_closure measure_interior)
qed

lemma measurable_convex: "convex S; bounded S  S  lmeasurable"
  by (simp add: measurable_Jordan negligible_convex_frontier)

lemma content_cball_conv_ball: "content (cball c r) = content (ball c r)"
proof -
  have "ball c r - cball c r  (cball c r - ball c r) = sphere c r"
    by auto
  hence "measure lebesgue (cball c r) = measure lebesgue (ball c r)"
    using negligible_sphere[of c r] by (intro measure_negligible_symdiff) simp_all
  thus ?thesis by simp
qed

subsection‹Negligibility of image under non-injective linear map›

lemma negligible_Union_nat:
  assumes "n::nat. negligible(S n)"
  shows "negligible(n. S n)"
proof -
  have "negligible (mk. S m)" for k
    using assms by blast
  then have 0:  "integral UNIV (indicat_real (mk. S m)) = 0"
    and 1: "(indicat_real (mk. S m)) integrable_on UNIV" for k
    by (auto simp: negligible has_integral_iff)
  have 2: "k x. indicat_real (mk. S m) x  (indicat_real (mSuc k. S m) x)"
    by (auto simp add: indicator_def)
  have 3: "x. (λk. indicat_real (mk. S m) x)  (indicat_real (n. S n) x)"
    by (force simp: indicator_def eventually_sequentially intro: tendsto_eventually)
  have 4: "bounded (range (λk. integral UNIV (indicat_real (mk. S m))))"
    by (simp add: 0)
  have *: "indicat_real (n. S n) integrable_on UNIV 
        (λk. integral UNIV (indicat_real (mk. S m)))  (integral UNIV (indicat_real (n. S n)))"
    by (intro monotone_convergence_increasing 1 2 3 4)
  then have "integral UNIV (indicat_real (n. S n)) = (0::real)"
    using LIMSEQ_unique by (auto simp: 0)
  then show ?thesis
    using * by (simp add: negligible_UNIV has_integral_iff)
qed


lemma negligible_linear_singular_image:
  fixes f :: "'n::euclidean_space  'n"
  assumes "linear f" "¬ inj f"
  shows "negligible (f ` S)"
proof -
  obtain a where "a  0" "S. f ` S  {x. a  x = 0}"
    using assms linear_singular_image_hyperplane by blast
  then show "negligible (f ` S)"
    by (metis negligible_hyperplane negligible_subset)
qed

lemma measure_negligible_finite_Union:
  assumes "finite "
    and meas: "S. S    S  lmeasurable"
    and djointish: "pairwise (λS T. negligible (S  T)) "
  shows "measure lebesgue () = (S. measure lebesgue S)"
  using assms
proof (induction)
  case empty
  then show ?case
    by auto
next
  case (insert S )
  then have "S  lmeasurable" "  lmeasurable" "pairwise (λS T. negligible (S  T)) "
    by (simp_all add: fmeasurable.finite_Union insert.hyps(1) insert.prems(1) pairwise_insert subsetI)
  then show ?case
  proof (simp add: measure_Un3 insert)
    have *: "T. T  (∩) S `   negligible T"
      using insert by (force simp: pairwise_def)
    have "negligible(S  )"
      unfolding Int_Union
      by (rule negligible_Union) (simp_all add: * insert.hyps(1))
    then show "measure lebesgue (S  ) = 0"
      using negligible_imp_measure0 by blast
  qed
qed

lemma measure_negligible_finite_Union_image:
  assumes "finite S"
    and meas: "x. x  S  f x  lmeasurable"
    and djointish: "pairwise (λx y. negligible (f x  f y)) S"
  shows "measure lebesgue ((f ` S)) = (xS. measure lebesgue (f x))"
proof -
  have "measure lebesgue ((f ` S)) = sum (measure lebesgue) (f ` S)"
    using assms by (auto simp: pairwise_mono pairwise_image intro: measure_negligible_finite_Union)
  also have " = sum (measure lebesgue  f) S"
    using djointish [unfolded pairwise_def] by (metis inf.idem negligible_imp_measure0 sum.reindex_nontrivial [OF finite S])
  also have " = (xS. measure lebesgue (f x))"
    by simp
  finally show ?thesis .
qed

subsection ‹Negligibility of a Lipschitz image of a negligible set›

text‹The bound will be eliminated by a sort of onion argument›
lemma locally_Lipschitz_negl_bounded:
  fixes f :: "'M::euclidean_space  'N::euclidean_space"
  assumes MleN: "DIM('M)  DIM('N)" "0 < B" "bounded S" "negligible S"
      and lips: "x. x  S
                       T. open T  x  T 
                              (y  S  T. norm(f y - f x)  B * norm(y - x))"
  shows "negligible (f ` S)"
  unfolding negligible_iff_null_sets
proof (clarsimp simp: completion.null_sets_outer)
  fix e::real
  assume "0 < e"
  have "S  lmeasurable"
    using negligible S by (simp add: negligible_iff_null_sets fmeasurableI_null_sets)
  then have "S  sets lebesgue"
    by blast
  have e22: "0 < e/2 / (2 * B * real DIM('M)) ^ DIM('N)"
    using 0 < e 0 < B by (simp add: field_split_simps)
  obtain T where "open T" "S  T" "(T - S)  lmeasurable"
                 "measure lebesgue (T - S) < e/2 / (2 * B * DIM('M)) ^ DIM('N)"
    using sets_lebesgue_outer_open [OF S  sets lebesgue e22]
    by (metis emeasure_eq_measure2 ennreal_leI linorder_not_le)
  then have T: "measure lebesgue T  e/2 / (2 * B * DIM('M)) ^ DIM('N)"
    using negligible S by (simp add: measure_Diff_null_set negligible_iff_null_sets)
  have "r. 0 < r  r  1/2 
            (x  S  (y. norm(y - x) < r
                        y  T  (y  S  norm(f y - f x)  B * norm(y - x))))"
        for x
  proof (cases "x  S")
    case True
    obtain U where "open U" "x  U" and U: "y. y  S  U  norm(f y - f x)  B * norm(y - x)"
      using lips [OF x  S] by auto
    have "x  T  U"
      using S  T x  U x  S by auto
    then obtain ε where "0 < ε" "ball x ε  T  U"
      by (metis open T open U openE open_Int)
    then show ?thesis
      by (rule_tac x="min (1/2) ε" in exI) (simp add: U dist_norm norm_minus_commute subset_iff)
  next
    case False
    then show ?thesis
      by (rule_tac x="1/4" in exI) auto
  qed
  then obtain R where R12: "x. 0 < R x  R x  1/2"
                and RT: "x y. x  S; norm(y - x) < R x  y  T"
                and RB: "x y. x  S; y  S; norm(y - x) < R x  norm(f y - f x)  B * norm(y - x)"
    by metis+
  then have gaugeR: "gauge (λx. ball x (R x))"
    by (simp add: gauge_def)
  obtain c where c: "S  cbox (-c *R One) (c *R One)" "box (-c *R One:: 'M) (c *R One)  {}"
  proof -
    obtain B where B: "x. x  S  norm x  B"
      using bounded S bounded_iff by blast
    show ?thesis
    proof (rule_tac c = "abs B + 1" in that)
      show "S  cbox (- (¦B¦ + 1) *R One) ((¦B¦ + 1) *R One)"
        using norm_bound_Basis_le Basis_le_norm
        by (fastforce simp: mem_box dest!: B intro: order_trans)
      show "box (- (¦B¦ + 1) *R One) ((¦B¦ + 1) *R One)  {}"
        by (simp add: box_eq_empty(1))
    qed
  qed
  obtain 𝒟 where "countable 𝒟"
     and Dsub: "𝒟  cbox (-c *R One) (c *R One)"
     and cbox: "K. K  𝒟  interior K  {}  (c d. K = cbox c d)"
     and pw:   "pairwise (λA B. interior A  interior B = {}) 𝒟"
     and Ksub: "K. K  𝒟  x  S  K. K  (λx. ball x (R x)) x"
     and exN:  "u v. cbox u v  𝒟  n. i  Basis. v  i - u  i = (2*c) / 2^n"
     and "S  𝒟"
    using covering_lemma [OF c gaugeR]  by force
  have "u v z. K = cbox u v  box u v  {}  z  S  z  cbox u v 
                cbox u v  ball z (R z)" if "K  𝒟" for K
  proof -
    obtain u v where "K = cbox u v"
      using K  𝒟 cbox by blast
    with that show ?thesis
      by (metis Int_iff interior_cbox cbox Ksub)
  qed
  then obtain uf vf zf
    where uvz: "K. K  𝒟 
                K = cbox (uf K) (vf K)  box (uf K) (vf K)  {}  zf K  S 
                zf K  cbox (uf K) (vf K)  cbox (uf K) (vf K)  ball (zf K) (R (zf K))"
    by metis
  define prj1 where "prj1  λx::'M. x  (SOME i. i  Basis)"
  define fbx where "fbx  λD. cbox (f(zf D) - (B * DIM('M) * (prj1(vf D - uf D))) *R One::'N)
                                    (f(zf D) + (B * DIM('M) * prj1(vf D - uf D)) *R One)"
  have vu_pos: "0 < prj1 (vf X - uf X)" if "X  𝒟" for X
    using uvz [OF that] by (simp add: prj1_def box_ne_empty SOME_Basis inner_diff_left)
  have prj1_idem: "prj1 (vf X - uf X) = (vf X - uf X)  i" if  "X  𝒟" "i  Basis" for X i
  proof -
    have "cbox (uf X) (vf X)  𝒟"
      using uvz X  𝒟 by auto
    with exN obtain n where "i. i  Basis  vf X  i - uf X  i = (2*c) / 2^n"
      by blast
    then show ?thesis
      by (simp add: i  Basis SOME_Basis inner_diff prj1_def)
  qed
  have countbl: "countable (fbx ` 𝒟)"
    using countable 𝒟 by blast
  have "(kfbx`𝒟'. measure lebesgue k)  e/2" if "𝒟'  𝒟" "finite 𝒟'" for 𝒟'
  proof -
    have BM_ge0: "0  B * (DIM('M) * prj1 (vf X - uf X))" if "X  𝒟'" for X
      using 0 < B 𝒟'  𝒟 that vu_pos by fastforce
    have "{}  𝒟'"
      using cbox 𝒟'  𝒟 interior_empty by blast
    have "(kfbx`𝒟'. measure lebesgue k)  sum (measure lebesgue o fbx) 𝒟'"
      by (rule sum_image_le [OF finite 𝒟']) (force simp: fbx_def)
    also have "  (X𝒟'. (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X)"
    proof (rule sum_mono)
      fix X assume "X  𝒟'"
      then have "X  𝒟" using 𝒟'  𝒟 by blast
      then have ufvf: "cbox (uf X) (vf X) = X"
        using uvz by blast
      have "prj1 (vf X - uf X) ^ DIM('M) = (i::'M  Basis. prj1 (vf X - uf X))"
        by (rule prod_constant [symmetric])
      also have " = (iBasis. vf X  i - uf X  i)"
        by (simp add: X  𝒟 inner_diff_left prj1_idem cong: prod.cong)
      finally have prj1_eq: "prj1 (vf X - uf X) ^ DIM('M) = (iBasis. vf X  i - uf X  i)" .
      have "uf X  cbox (uf X) (vf X)" "vf X  cbox (uf X) (vf X)"
        using uvz [OF X  𝒟] by (force simp: mem_box)+
      moreover have "cbox (uf X) (vf X)  ball (zf X) (1/2)"
        by (meson R12 order_trans subset_ball uvz [OF X  𝒟])
      ultimately have "uf X  ball (zf X) (1/2)"  "vf X  ball (zf X) (1/2)"
        by auto
      then have "dist (vf X) (uf X)  1"
        unfolding mem_ball
        by (metis dist_commute dist_triangle_half_l dual_order.order_iff_strict)
      then have 1: "prj1 (vf X - uf X)  1"
        unfolding prj1_def dist_norm using Basis_le_norm SOME_Basis order_trans by fastforce
      have 0: "0  prj1 (vf X - uf X)"
        using X  𝒟 prj1_def vu_pos by fastforce
      have "(measure lebesgue  fbx) X  (2 * B * DIM('M)) ^ DIM('N) * content (cbox (uf X) (vf X))"
        apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 X  𝒟' 0 < B flip: prj1_eq)
        using MleN 0 1 uvz X  𝒟
        by (fastforce simp add: box_ne_empty power_decreasing)
      also have " = (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X"
        by (subst (3) ufvf[symmetric]) simp
      finally show "(measure lebesgue  fbx) X  (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X" .
    qed
    also have " = (2 * B * DIM('M)) ^ DIM('N) * sum (measure lebesgue) 𝒟'"
      by (simp add: sum_distrib_left)
    also have "  e/2"
    proof -
      have "K. K  𝒟'  a b. K = cbox a b"
        using cbox that by blast
      then have div: "𝒟' division_of 𝒟'"
        using pairwise_subset [OF pw 𝒟'  𝒟] unfolding pairwise_def
        by (force simp: finite 𝒟' {}  𝒟' division_of_def)
      have le_meaT: "measure lebesgue (𝒟')  measure lebesgue T"
      proof (rule measure_mono_fmeasurable)
        show "(𝒟')  sets lebesgue"
          using div lmeasurable_division by auto
        have "𝒟'  𝒟"
          using 𝒟'  𝒟 by blast
        also have "...  T"
        proof (clarify)
          fix x D
          assume "x  D" "D  𝒟"
          show "x  T"
            using Ksub [OF D  𝒟]
            by (metis x  D Int_iff dist_norm mem_ball norm_minus_commute subsetD RT)
        qed
        finally show "𝒟'  T" .
        show "T  lmeasurable"
          using S  lmeasurable S  T T - S  lmeasurable fmeasurable_Diff_D by blast
      qed
      have "sum (measure lebesgue) 𝒟' = sum content 𝒟'"
        using  𝒟'  𝒟 cbox by (force intro: sum.cong)
      then have "(2 * B * DIM('M)) ^ DIM('N) * sum (measure lebesgue) 𝒟' =
                 (2 * B * real DIM('M)) ^ DIM('N) * measure lebesgue (𝒟')"
        using content_division [OF div] by auto
      also have "  (2 * B * real DIM('M)) ^ DIM('N) * measure lebesgue T"
        using 0 < B 
        by (intro mult_left_mono [OF le_meaT]) (force simp add: algebra_simps)
      also have "  e/2"
        using T 0 < B by (simp add: field_simps)
      finally show ?thesis .
    qed
    finally show ?thesis .
  qed
  then have e2: "sum (measure lebesgue) 𝒢  e/2" if "𝒢  fbx ` 𝒟" "finite 𝒢" for 𝒢
    by (metis finite_subset_image that)
  show "Wlmeasurable. f ` S  W  measure lebesgue W < e"
  proof (intro bexI conjI)
    have "X𝒟. f y  fbx X" if "y  S" for y
    proof -
      obtain X where "y  X" "X  𝒟"
        using S  𝒟 y  S by auto
      then have y: "y  ball(zf X) (R(zf X))"
        using uvz by fastforce
      have conj_le_eq: "z - b  y  y  z + b  abs(y - z)  b" for z y b::real
        by auto
      have yin: "y  cbox (uf X) (vf X)" and zin: "(zf X)  cbox (uf X) (vf X)"
        using uvz X  𝒟 y  X by auto
      have "norm (y - zf X)  (iBasis. ¦(y - zf X)  i¦)"
        by (rule norm_le_l1)
      also have "  real DIM('M) * prj1 (vf X - uf X)"
      proof (rule sum_bounded_above)
        fix j::'M assume j: "j  Basis"
        show "¦(y - zf X)  j¦  prj1 (vf X - uf X)"
          using yin zin j
          by (fastforce simp add: mem_box prj1_idem [OF X  𝒟 j] inner_diff_left)
      qed
      finally have nole: "norm (y - zf X)  DIM('M) * prj1 (vf X - uf X)"
        by simp
      have fle: "¦f y  i - f(zf X)  i¦  B * DIM('M) * prj1 (vf X - uf X)" if "i  Basis" for i
      proof -
        have "¦f y  i - f (zf X)  i¦ = ¦(f y - f (zf X))  i¦"
          by (simp add: algebra_simps)
        also have "  norm (f y - f (zf X))"
          by (simp add: Basis_le_norm that)
        also have "  B * norm(y - zf X)"
          by (metis uvz RB X  𝒟 dist_commute dist_norm mem_ball y  S y)
        also have "  B * real DIM('M) * prj1 (vf X - uf X)"
          using 0 < B by (simp add: nole)
        finally show ?thesis .
      qed
      show ?thesis
        by (rule_tac x=X in bexI)
           (auto simp: fbx_def prj1_idem mem_box conj_le_eq inner_add inner_diff fle X  𝒟)
    qed
    then show "f ` S  (D𝒟. fbx D)" by auto
  next
    have 1: "D. D  𝒟  fbx D  lmeasurable"
      by (auto simp: fbx_def)
    have 2: "I'  𝒟  finite I'  measure lebesgue (DI'. fbx D)  e/2" for I'
      by (rule order_trans[OF measure_Union_le e2]) (auto simp: fbx_def)
    show "(D𝒟. fbx D)  lmeasurable"
      by (intro fmeasurable_UN_bound[OF countable 𝒟 1 2])
    have "measure lebesgue (D𝒟. fbx D)  e/2"
      by (intro measure_UN_bound[OF countable 𝒟 1 2])
    then show "measure lebesgue (D𝒟. fbx D) < e"
      using 0 < e by linarith
  qed
qed

proposition negligible_locally_Lipschitz_image:
  fixes f :: "'M::euclidean_space  'N::euclidean_space"
  assumes MleN: "DIM('M)  DIM('N)" "negligible S"
      and lips: "x. x  S
                       T B. open T  x  T 
                              (y  S  T. norm(f y - f x)  B * norm(y - x))"
    shows "negligible (f ` S)"
proof -
  let ?S = "λn. ({x  S. norm x  n 
                          (T. open T  x  T 
                               (yS  T. norm (f y - f x)  (real n + 1) * norm (y - x)))})"
  have negfn: "f ` ?S n  null_sets lebesgue" for n::nat
    unfolding negligible_iff_null_sets[symmetric]
    apply (rule_tac B = "real n + 1" in locally_Lipschitz_negl_bounded)
    by (auto simp: MleN bounded_iff intro: negligible_subset [OF negligible S])
  have "S = (n. ?S n)"
  proof (intro set_eqI iffI)
    fix x assume "x  S"
    with lips obtain T B where T: "open T" "x  T"
                           and B: "y. y  S  T  norm(f y - f x)  B * norm(y - x)"
      by metis+
    have no: "norm (f y - f x)  (nat max B (norm x) + 1) * norm (y - x)" if "y  S  T" for y
    proof -
      have "B * norm(y - x)  (nat max B (norm x) + 1) * norm (y - x)"
        by (meson max.cobounded1 mult_right_mono nat_ceiling_le_eq nat_le_iff_add norm_ge_zero order_trans)
      then show ?thesis
        using B order_trans that by blast
    qed
    have "norm x  real (nat max B (norm x))"
      by linarith
    then have "x  ?S (nat (ceiling (max B (norm x))))"
      using T no by (force simp: x  S algebra_simps)
    then show "x  (n. ?S n)" by force
  qed auto
  then show ?thesis
    by (rule ssubst) (auto simp: image_Union negligible_iff_null_sets intro: negfn)
qed

corollary negligible_differentiable_image_negligible:
  fixes f :: "'M::euclidean_space  'N::euclidean_space"
  assumes MleN: "DIM('M)  DIM('N)" "negligible S"
      and diff_f: "f differentiable_on S"
    shows "negligible (f ` S)"
proof -
  have "T B. open T  x  T  (y  S  T. norm(f y - f x)  B * norm(y - x))"
        if "x  S" for x
  proof -
    obtain f' where "linear f'"
       and f': "e. e>0 
                        d>0. yS. norm (y - x) < d 
                                    norm (f y - f x - f' (y - x))  e * norm (y - x)"
      using diff_f x  S
      by (auto simp: linear_linear differentiable_on_def differentiable_def has_derivative_within_alt)
    obtain B where "B > 0" and B: "x. norm (f' x)  B * norm x"
      using linear_bounded_pos linear f' by blast
    obtain d where "d>0"
              and d: "y. y  S; norm (y - x) < d 
                          norm (f y - f x - f' (y - x))  norm (y - x)"
      using f' [of 1] by (force simp:)
    show ?thesis
    proof (intro exI conjI ballI)
      show "norm (f y - f x)  (B + 1) * norm (y - x)"
        if "y  S  ball x d" for y
      proof -
        have "norm (f y - f x) - B * norm (y - x)  norm (f y - f x) - norm (f' (y - x))"
          by (simp add: B)
        also have "  norm (f y - f x - f' (y - x))"
          by (rule norm_triangle_ineq2)
        also have "...  norm (y - x)"
          by (metis IntE d dist_norm mem_ball norm_minus_commute that)
        finally show ?thesis
          by (simp add: algebra_simps)
      qed
    qed (use d>0 in auto)
  qed
  with negligible_locally_Lipschitz_image assms show ?thesis by metis
qed

corollary negligible_differentiable_image_lowdim:
  fixes f :: "'M::euclidean_space  'N::euclidean_space"
  assumes MlessN: "DIM('M) < DIM('N)" and diff_f: "f differentiable_on S"
    shows "negligible (f ` S)"
proof -
  have "x  DIM('M)  x  DIM('N)" for x
    using MlessN by linarith
  obtain lift :: "'M * real  'N" and drop :: "'N  'M * real" and j :: 'N
    where "linear lift" "linear drop" and dropl [simp]: "z. drop (lift z) = z"
      and "j  Basis" and j: "x. lift(x,0)  j = 0"
    using lowerdim_embeddings [OF MlessN] by metis
  have "negligible ((λx. lift (x, 0)) ` S)"
  proof -
    have "negligible {x. xj = 0}"
      by (metis j  Basis negligible_standard_hyperplane)
    moreover have "(λm. lift (m, 0)) ` S  {n. n  j = 0}"
      using j by force
    ultimately show ?thesis
      using negligible_subset by auto
  qed
  moreover
  have "f  fst  drop differentiable_on (λx. lift (x, 0)) ` S"
    using diff_f
    apply (clarsimp simp add: differentiable_on_def)
    apply (intro differentiable_chain_within linear_imp_differentiable [OF linear drop]
             linear_imp_differentiable [OF linear_fst])
    apply (force simp: image_comp o_def)
    done
  moreover
  have "f = f  fst  drop  (λx. lift (x, 0))"
    by (simp add: o_def)
  ultimately show ?thesis
    by (metis (no_types) image_comp negligible_differentiable_image_negligible order_refl)
qed

subsection‹Measurability of countable unions and intersections of various kinds.›

lemma
  assumes S: "n. S n  lmeasurable"
    and leB: "n. measure lebesgue (S n)  B"
    and nest: "n. S n  S(Suc n)"
  shows measurable_nested_Union: "(n. S n)  lmeasurable"
  and measure_nested_Union:  "(λn. measure lebesgue (S n))  measure lebesgue (n. S n)" (is ?Lim)
proof -
  have "indicat_real ( (range S)) integrable_on UNIV 
    (λn. integral UNIV (indicat_real (S n)))
     integral UNIV (indicat_real ( (range S)))"
  proof (rule monotone_convergence_increasing)
    show "n. (indicat_real (S n)) integrable_on UNIV"
      using S measurable_integrable by blast
    show "n x::'a. indicat_real (S n) x  (indicat_real (S (Suc n)) x)"
      by (simp add: indicator_leI nest rev_subsetD)
    have "x. (n. x  S n)  (F n in sequentially. x  S n)"
      by (metis eventually_sequentiallyI lift_Suc_mono_le nest subsetCE)
    then
    show "x. (λn. indicat_real (S n) x)  (indicat_real ((S ` UNIV)) x)"
      by (simp add: indicator_def tendsto_eventually)
    show "bounded (range (λn. integral UNIV (indicat_real (S n))))"
      using leB by (auto simp: lmeasure_integral_UNIV [symmetric] S bounded_iff)
  qed
  then have "(n. S n)  lmeasurable  ?Lim"
    by (simp add: lmeasure_integral_UNIV S cong: conj_cong) (simp add: measurable_integrable)
  then show "(n. S n)  lmeasurable" "?Lim"
    by auto
qed

lemma
  assumes S: "n. S n  lmeasurable"
    and djointish: "pairwise (λm n. negligible (S m  S n)) UNIV"
    and leB: "n. (kn. measure lebesgue (S k))  B"
  shows measurable_countable_negligible_Union: "(n. S n)  lmeasurable"
  and   measure_countable_negligible_Union:    "(λn. (measure lebesgue (S n))) sums measure lebesgue (n. S n)" (is ?Sums)
proof -
  have 1: " (S ` {..n})  lmeasurable" for n
    using S by blast
  have 2: "measure lebesgue ( (S ` {..n}))  B" for n
  proof -
    have "measure lebesgue ( (S ` {..n}))  (kn. measure lebesgue (S k))"
      by (simp add: S fmeasurableD measure_UNION_le)
    with leB show ?thesis
      using order_trans by blast
  qed
  have 3: "n.  (S ` {..n})   (S ` {..Suc n})"
    by (simp add: SUP_subset_mono)
  have eqS: "(n. S n) = (n.  (S ` {..n}))"
    using atLeastAtMost_iff by blast
  also have "(n.  (S ` {..n}))  lmeasurable"
    by (intro measurable_nested_Union [OF 1 2] 3)
  finally show "(n. S n)  lmeasurable" .
  have eqm: "(in. measure lebesgue (S i)) = measure lebesgue ( (S ` {..n}))" for n
    using assms by (simp add: measure_negligible_finite_Union_image pairwise_mono)
  have "(λn. (measure lebesgue (S n))) sums measure lebesgue (n.  (S ` {..n}))"
    by (simp add: sums_def' eqm atLeast0AtMost) (intro measure_nested_Union [OF 1 2] 3)
  then show ?Sums
    by (simp add: eqS)
qed

lemma negligible_countable_Union [intro]:
  assumes "countable " and meas: "S. S    negligible S"
  shows "negligible ()"
proof (cases " = {}")
  case False
  then show ?thesis
    by (metis from_nat_into range_from_nat_into assms negligible_Union_nat)
qed simp

lemma
  assumes S: "n. (S n)  lmeasurable"
    and djointish: "pairwise (λm n. negligible (S m  S n)) UNIV"
    and bo: "bounded (n. S n)"
  shows measurable_countable_negligible_Union_bounded: "(n. S n)  lmeasurable"
  and   measure_countable_negligible_Union_bounded:    "(λn. (measure lebesgue (S n))) sums measure lebesgue (n. S n)" (is ?Sums)
proof -
  obtain a b where ab: "(n. S n)  cbox a b"
    using bo bounded_subset_cbox_symmetric by metis
  then have B: "(kn. measure lebesgue (S k))  measure lebesgue (cbox a b)" for n
  proof -
    have "(kn. measure lebesgue (S k)) = measure lebesgue ( (S ` {..n}))"
      using measure_negligible_finite_Union_image [OF _ _ pairwise_subset] djointish
      by (metis S finite_atMost subset_UNIV)
    also have "  measure lebesgue (cbox a b)"
    proof (rule measure_mono_fmeasurable)
      show " (S ` {..n})  sets lebesgue" using S by blast
    qed (use ab in auto)
    finally show ?thesis .
  qed
  show "(n. S n)  lmeasurable"
    by (rule measurable_countable_negligible_Union [OF S djointish B])
  show ?Sums
    by (rule measure_countable_negligible_Union [OF S djointish B])
qed

lemma measure_countable_Union_approachable:
  assumes "countable 𝒟" "e > 0" and measD: "d. d  𝒟  d  lmeasurable"
      and B: "D'. D'  𝒟; finite D'  measure lebesgue (D')  B"
    obtains D' where "D'  𝒟" "finite D'" "measure lebesgue (𝒟) - e < measure lebesgue (D')"
proof (cases "𝒟 = {}")
  case True
  then show ?thesis
    by (simp add: e > 0 that)
next
  case False
  let ?S = "λn. k  n. from_nat_into 𝒟 k"
  have "(λn. measure lebesgue (?S n))  measure lebesgue (n. ?S n)"
  proof (rule measure_nested_Union)
    show "?S n  lmeasurable" for n
      by (simp add: False fmeasurable.finite_UN from_nat_into measD)
    show "measure lebesgue (?S n)  B" for n
      by (metis (mono_tags, lifting) B False finite_atMost finite_imageI from_nat_into image_iff subsetI)
    show "?S n  ?S (Suc n)" for n
      by force
  qed
  then obtain N where N: "n. n  N  dist (measure lebesgue (?S n)) (measure lebesgue (n. ?S n)) < e"
    using metric_LIMSEQ_D e > 0 by blast
  show ?thesis
  proof
    show "from_nat_into 𝒟 ` {..N}  𝒟"
      by (auto simp: False from_nat_into)
    have eq: "(n. kn. from_nat_into 𝒟 k) = (𝒟)"
      using countable 𝒟 False
      by (auto intro: from_nat_into dest: from_nat_into_surj [OF countable 𝒟])
    show "measure lebesgue (𝒟) - e < measure lebesgue ( (from_nat_into 𝒟 ` {..N}))"
      using N [OF order_refl]
      by (auto simp: eq algebra_simps dist_norm)
  qed auto
qed


subsection‹Negligibility is a local property›

lemma locally_negligible_alt:
    "negligible S  (x  S. U. openin (top_of_set S) U  x  U  negligible U)"
     (is "_ = ?rhs")
proof
  assume "negligible S"
  then show ?rhs
    using openin_subtopology_self by blast
next
  assume ?rhs
  then obtain U where ope: "x. x  S  openin (top_of_set S) (U x)"
    and cov: "x. x  S  x  U x"
    and neg: "x. x  S  negligible (U x)"
    by metis
  obtain  where "  U ` S" "countable " and eq: " = (U ` S)"
    using ope by (force intro: Lindelof_openin [of "U ` S" S])
  then have "negligible ()"
    by (metis imageE neg negligible_countable_Union subset_eq)
  with eq have "negligible ((U ` S))"
    by metis
  moreover have "S  (U ` S)"
    using cov by blast
  ultimately show "negligible S"
    using negligible_subset by blast
qed

lemma locally_negligible: "locally negligible S  negligible S"
  unfolding locally_def
  by (metis locally_negligible_alt negligible_subset openin_imp_subset openin_subtopology_self)


subsection‹Integral bounds›

lemma set_integral_norm_bound:
  fixes f :: "_  'a :: {banach, second_countable_topology}"
  shows "set_integrable M k f  norm (LINT x:k|M. f x)  (LINT x:k|M. norm (f x))"
  using integral_norm_bound[of M "λx. indicator k x *R f x"] by (simp add: set_lebesgue_integral_def)

lemma set_integral_finite_UN_AE:
  fixes f :: "_  _ :: {banach, second_countable_topology}"
  assumes "finite I"
    and ae: "i j. i  I  j  I  AE x in M. (x  A i  x  A j)  i = j"
    and [measurable]: "i. i  I  A i  sets M"
    and f: "i. i  I  set_integrable M (A i) f"
  shows "(LINT x:(iI. A i)|M. f x) = (iI. LINT x:A i|M. f x)"
  using finite I order_refl[of I]
proof (induction I rule: finite_subset_induct')
  case (insert i I')
  have "AE x in M. (jI'. x  A i  x  A j)"
  proof (intro AE_ball_countable[THEN iffD2] ballI)
    fix j assume "j  I'"
    with I'  I i  I' have "i  j" "j  I"
      by auto
    then show "AE x in M. x  A i  x  A j"
      using ae[of i j] i  I by auto
  qed (use finite I' in rule countable_finite)
  then have "AE xA i in M. xaI'. x  A xa "
    by auto
  with insert.hyps insert.IH[symmetric]
  show ?case
    by (auto intro!: set_integral_Un_AE sets.finite_UN f set_integrable_UN)
qed (simp add: set_lebesgue_integral_def)

lemma set_integrable_norm:
  fixes f :: "'a  'b::{banach, second_countable_topology}"
  assumes f: "set_integrable M k f" shows "set_integrable M k (λx. norm (f x))"
  using integrable_norm f by (force simp add: set_integrable_def)

lemma absolutely_integrable_bounded_variation:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes f: "f absolutely_integrable_on UNIV"
  obtains B where "d. d division_of (d)  sum (λk. norm (integral k f)) d  B"
proof (rule that[of "integral UNIV (λx. norm (f x))"]; safe)
  fix d :: "'a set set" assume d: "d division_of d"
  have *: "k  d  f absolutely_integrable_on k" for k
    using f[THEN set_integrable_subset, of k] division_ofD(2,4)[OF d, of k] by auto
  note d' = division_ofD[OF d]
  have "(kd. norm (integral k f)) = (kd. norm (LINT x:k|lebesgue. f x))"
    by (intro sum.cong refl arg_cong[where f=norm] set_lebesgue_integral_eq_integral(2)[symmetric] *)
  also have "  (kd. LINT x:k|lebesgue. norm (f x))"
    by (intro sum_mono set_integral_norm_bound *)
  also have " = (kd. integral k (λx. norm (f x)))"
    by (intro sum.cong refl set_lebesgue_integral_eq_integral(2) set_integrable_norm *)
  also have "  integral (d) (λx. norm (f x))"
    using integrable_on_subdivision[OF d] assms f unfolding absolutely_integrable_on_def
    by (subst integral_combine_division_topdown[OF _ d]) auto
  also have "  integral UNIV (λx. norm (f x))"
    using integrable_on_subdivision[OF d] assms unfolding absolutely_integrable_on_def
    by (intro integral_subset_le) auto
  finally show "(kd. norm (integral k f))  integral UNIV (λx. norm (f x))" .
qed

lemma absdiff_norm_less:
  assumes "sum (λx. norm (f x - g x)) S < e"
  shows "¦sum (λx. norm(f x)) S - sum (λx. norm(g x)) S¦ < e" (is "?lhs < e")
proof -
  have "?lhs  (iS. ¦norm (f i) - norm (g i)¦)"
    by (metis (no_types) sum_abs sum_subtractf)
  also have "...  (xS. norm (f x - g x))"
    by (simp add: norm_triangle_ineq3 sum_mono)
  also have "... < e"
    using assms(1) by blast
  finally show ?thesis .
qed

proposition bounded_variation_absolutely_integrable_interval:
  fixes f :: "'n::euclidean_space  'm::euclidean_space"
  assumes f: "f integrable_on cbox a b"
    and *: "d. d division_of (cbox a b)  sum (λK. norm(integral K f)) d  B"
  shows "f absolutely_integrable_on cbox a b"
proof -
  let ?f = "λd. Kd. norm (integral K f)" and ?D = "{d. d division_of (cbox a b)}"
  have D_1: "?D  {}"
    by (rule elementary_interval[of a b]) auto
  have D_2: "bdd_above (?f`?D)"
    by (metis * mem_Collect_eq bdd_aboveI2)
  note D = D_1 D_2
  let ?S = "SUP x?D. ?f x"
  have *: "γ. gauge γ 
             (p. p tagged_division_of cbox a b 
                  γ fine p 
                  norm (((x,k)  p. content k *R norm (f x)) - ?S) < e)"
    if e: "e > 0" for e
  proof -
    have "?S - e/2 < ?S" using e > 0 by simp
    then obtain d where d: "d division_of (cbox a b)" "?S - e/2 < (kd. norm (integral k f))"
      unfolding less_cSUP_iff[OF D] by auto
    note d' = division_ofD[OF this(1)]

    have "e>0. id. x  i  ball x e  i = {}" for x
    proof -
      have "d'>0. x'{i  d. x  i}. d'  dist x x'"
      proof (rule separate_point_closed)
        show "closed ({i  d. x  i})"
          using d' by force
        show "x  {i  d. x  i}"
          by auto
      qed
      then show ?thesis
        by force
    qed
    then obtain k where k: "x. 0 < k x" "i x. i  d; x  i  ball x (k x)  i = {}"
      by metis
    have "e/2 > 0"
      using e by auto
    with Henstock_lemma[OF f]
    obtain γ where g: "gauge γ"
      "p. p tagged_partial_division_of cbox a b; γ fine p
                 ((x,k)  p. norm (content k *R f x - integral k f)) < e/2"
      by (metis (no_types, lifting))
    let ?g = "λx. γ x  ball x (k x)"
    show ?thesis
    proof (intro exI conjI allI impI)
      show "gauge ?g"
        using g(1) k(1) by (auto simp: gauge_def)
    next
      fix p
      assume "p tagged_division_of (cbox a b)  ?g fine p"
      then have p: "p tagged_division_of cbox a b" "γ fine p" "(λx. ball x (k x)) fine p"
        by (auto simp: fine_Int)
      note p' = tagged_division_ofD[OF p(1)]
      define p' where "p' = {(x,k) | x k. i l. x  i  i  d  (x,l)  p  k = i  l}"
      have gp': "γ fine p'"
        using p(2) by (auto simp: p'_def fine_def)
      have p'': "p' tagged_division_of (cbox a b)"
      proof (rule tagged_division_ofI)
        show "finite p'"
        proof (rule finite_subset)
          show "p'  (λ(k, x, l). (x, k  l)) ` (d × p)"
            by (force simp: p'_def image_iff)
          show "finite ((λ(k, x, l). (x, k  l)) ` (d × p))"
            by (simp add: d'(1) p'(1))
        qed
      next
        fix x K
        assume "(x, K)  p'"
        then have "i l. x  i  i  d  (x, l)  p  K = i  l"
          unfolding p'_def by auto
        then obtain i l where il: "x  i" "i  d" "(x, l)  p" "K = i  l" by blast
        show "x  K" and "K  cbox a b"
          using p'(2-3)[OF il(3)] il by auto
        show "a b. K = cbox a b"
          unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)] by (meson Int_interval)
      next
        fix x1 K1
        assume "(x1, K1)  p'"
        then have "i l. x1  i  i  d  (x1, l)  p  K1 = i  l"
          unfolding p'_def by auto
        then obtain i1 l1 where il1: "x1  i1" "i1  d" "(x1, l1)  p" "K1 = i1  l1" by blast
        fix x2 K2
        assume "(x2,K2)  p'"
        then have "i l. x2  i  i  d  (x2, l)  p  K2 = i  l"
          unfolding p'_def by auto
        then obtain i2 l2 where il2: "x2  i2" "i2  d" "(x2, l2)  p" "K2 = i2  l2" by blast
        assume "(x1, K1)  (x2, K2)"
        then have "interior i1  interior i2 = {}  interior l1  interior l2 = {}"
          using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)]  by (auto simp: il1 il2)
        then show "interior K1  interior K2 = {}"
          unfolding il1 il2 by auto
      next
        have *: "(x, X)  p'. X  cbox a b"
          unfolding p'_def using d' by blast
        show "{K. x. (x, K)  p'} = cbox a b"
        proof
          show "{k. x. (x, k)  p'}  cbox a b"
            using * by auto
        next
          show "cbox a b  {k. x. (x, k)  p'}"
          proof
            fix y
            assume y: "y  cbox a b"
            obtain x L where xl: "(x, L)  p" "y  L"
              using y unfolding p'(6)[symmetric] by auto
            obtain I where i: "I  d" "y  I"
              using y unfolding d'(6)[symmetric] by auto
            have "x  I"
              using fineD[OF p(3) xl(1)] using k(2) i xl by auto
            then show "y  {K. x. (x, K)  p'}"
            proof -
              obtain x l where xl: "(x, l)  p" "y  l"
                using y unfolding p'(6)[symmetric] by auto
              obtain i where i: "i  d" "y  i"
                using y unfolding d'(6)[symmetric] by auto
              have "x  i"
                using fineD[OF p(3) xl(1)] using k(2) i xl by auto
              then show ?thesis
                unfolding p'_def by (rule_tac X="i  l" in UnionI) (use i xl in auto)
            qed
          qed
        qed
      qed
      then have sum_less_e2: "((x,K)  p'. norm (content K *R f x - integral K f)) < e/2"
        using g(2) gp' tagged_division_of_def by blast

      have in_p': "(x, I  L)  p'" if x: "(x, L)  p" "I  d" and y: "y  I" "y  L"
        for x I L y
      proof -
        have "x  I"
          using fineD[OF p(3) that(1)] k(2)[OF I  d] y by auto
        with x have "(i l. x  i  i  d  (x, l)  p  I  L = i  l)"
          by blast
        then have "(x, I  L)  p'"
          by (simp add: p'_def)
        with y show ?thesis by auto
      qed
      moreover 
      have Ex_p_p': "y i l. (x, K) = (y, i  l)  (y, l)  p  i  d  i  l  {}"
        if xK: "(x,K)  p'" for x K
      proof -
        obtain i l where il: "x  i" "i  d" "(x, l)  p" "K = i  l"
          using xK unfolding p'_def by auto
        then show ?thesis
          using p'(2) by fastforce
      qed
      ultimately have p'alt: "p' = {(x, I  L) | x I L. (x,L)  p  I  d  I  L  {}}"
        by auto
      have sum_p': "((x,K)  p'. norm (integral K f)) = (ksnd ` p'. norm (integral k f))"
      proof (rule sum.over_tagged_division_lemma[OF p''])
        show "u v. box u v = {}  norm (integral (cbox u v) f) = 0"
          by (auto intro: integral_null simp: content_eq_0_interior)
      qed
      have snd_p_div: "snd ` p division_of cbox a b"
        by (rule division_of_tagged_division[OF p(1)])
      note snd_p = division_ofD[OF snd_p_div]
      have fin_d_sndp: "finite (d × snd ` p)"
        by (simp add: d'(1) snd_p(1))

      have *: "sni sni' sf sf'. ¦sf' - sni'¦ < e/2; ?S - e/2 < sni; sni'  ?S;
                       sni  sni'; sf' = sf  ¦sf - ?S¦ < e"
        by arith
      show "norm (((x,k)  p. content k *R norm (f x)) - ?S) < e"
        unfolding real_norm_def
      proof (rule *)
        show "¦((x,K)p'. norm (content K *R f x)) - ((x,k)p'. norm (integral k f))¦ < e/2"
          using p'' sum_less_e2 unfolding split_def by (force intro!: absdiff_norm_less)
        show "((x,k)  p'. norm (integral k f)) ?S"
          by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper)
        show "(kd. norm (integral k f))  ((x,k)  p'. norm (integral k f))"
        proof -
          have *: "{k  l | k l. k  d  l  snd ` p} = (λ(k,l). k  l) ` (d × snd ` p)"
            by auto
          have "(Kd. norm (integral K f))  (id. lsnd ` p. norm (integral (i  l) f))"
          proof (rule sum_mono)
            fix K assume k: "K  d"
            from d'(4)[OF this] obtain u v where uv: "K = cbox u v" by metis
            define d' where "d' = {cbox u v  l |l. l  snd ` p   cbox u v  l  {}}"
            have uvab: "cbox u v  cbox a b"
              using d(1) k uv by blast
            have d'_div: "d' division_of cbox u v"
              unfolding d'_def by (rule division_inter_1 [OF snd_p_div uvab])
            moreover have "norm (id'. integral i f)  (kd'. norm (integral k f))"
              by (simp add: sum_norm_le)
            moreover have "f integrable_on K"
              using f integrable_on_subcbox uv uvab by blast
            moreover have "d' division_of K"
              using d'_div uv by blast
            ultimately have "norm (integral K f)  sum (λk. norm (integral k f)) d'"
              by (simp add: integral_combine_division_topdown)
            also have " = (I{K  L |L. L  snd ` p}. norm (integral I f))"
            proof (rule sum.mono_neutral_left)
              show "finite {K  L |L. L  snd ` p}"
                by (simp add: snd_p(1))
              show "i{K  L |L. L  snd ` p} - d'. norm (integral i f) = 0"
                "d'  {K  L |L. L  snd ` p}"
                using d'_def image_eqI uv by auto
            qed
            also have " = (lsnd ` p. norm (integral (K  l) f))"
              unfolding Setcompr_eq_image
            proof (rule sum.reindex_nontrivial [unfolded o_def])
              show "finite (snd ` p)"
                using snd_p(1) by blast
              show "norm (integral (K  l) f) = 0"
                if "l  snd ` p" "y  snd ` p" "l  y" "K  l = K  y" for l y
              proof -
                have "interior (K  l)  interior (l  y)"
                  by (metis Int_lower2 interior_mono le_inf_iff that(4))
                then have "interior (K  l) = {}"
                  by (simp add: snd_p(5) that)
                moreover from d'(4)[OF k] snd_p(4)[OF that(1)]
                obtain u1 v1 u2 v2
                  where uv: "K = cbox u1 u2" "l = cbox v1 v2" by metis
                ultimately show ?thesis
                  using that integral_null
                  unfolding uv Int_interval content_eq_0_interior
                  by (metis (mono_tags, lifting) norm_eq_zero)
              qed
            qed
            finally show "norm (integral K f)  (lsnd ` p. norm (integral (K  l) f))" .
          qed
          also have " = ((i,l)  d × snd ` p. norm (integral (il) f))"
            by (simp add: sum.cartesian_product)
          also have " = (x  d × snd ` p. norm (integral (case_prod (∩) x) f))"
            by (force simp: split_def intro!: sum.cong)
          also have " = (k{i  l |i l. i  d  l  snd ` p}. norm (integral k f))"
          proof -
            have eq0: " (integral (l1  k1) f) = 0"
              if "l1  k1 = l2  k2" "(l1, k1)  (l2, k2)"
                 "l1  d" "(j1,k1)  p" "l2  d" "(j2,k2)  p"
              for l1 l2 k1 k2 j1 j2
            proof -
              obtain u1 v1 u2 v2 where uv: "l1 = cbox u1 u2" "k1 = cbox v1 v2"
                using (j1, k1)  p l1  d d'(4) p'(4) by blast
              have "l1  l2  k1  k2"
                using that by auto
              then have "interior k1  interior k2 = {}  interior l1  interior l2 = {}"
                by (meson d'(5) old.prod.inject p'(5) that(3) that(4) that(5) that(6))
              moreover have "interior (l1  k1) = interior (l2  k2)"
                by (simp add: that(1))
              ultimately have "interior(l1  k1) = {}"
                by auto
              then show ?thesis
                unfolding uv Int_interval content_eq_0_interior[symmetric] by auto
            qed
            show ?thesis
              unfolding *
              apply (rule sum.reindex_nontrivial [OF fin_d_sndp, symmetric, unfolded o_def])
              apply clarsimp
              by (metis eq0 fst_conv snd_conv)
          qed
          also have " = ((x,k)  p'. norm (integral k f))"
            unfolding sum_p'
          proof (rule sum.mono_neutral_right)
            show "finite {i  l |i l. i  d  l  snd ` p}"
              by (metis * finite_imageI[OF fin_d_sndp])
            show "snd ` p'  {i  l |i l. i  d  l  snd ` p}"
              by (clarsimp simp: p'_def) (metis image_eqI snd_conv)
            show "i{i  l |i l. i  d  l  snd ` p} - snd ` p'. norm (integral i f) = 0"
              by clarsimp (metis Henstock_Kurzweil_Integration.integral_empty disjoint_iff image_eqI in_p' snd_conv)
          qed
          finally show ?thesis .
        qed
        show "((x,k)  p'. norm (content k *R f x)) = ((x,k)  p. content k *R norm (f x))"
        proof -
          let ?S = "{(x, i  l) |x i l. (x, l)  p  i  d}"
          have *: "?S = (λ(xl,i). (fst xl, snd xl  i)) ` (p × d)"
            by force
          have fin_pd: "finite (p × d)"
            using finite_cartesian_product[OF p'(1) d'(1)] by metis
          have "((x,k)  p'. norm (content k *R f x)) = ((x,k)  ?S. ¦content k¦ * norm (f x))"
            unfolding norm_scaleR
          proof (rule sum.mono_neutral_left)
            show "finite {(x, i  l) |x i l. (x, l)  p  i  d}"
              by (simp add: "*" fin_pd)
          qed (use p'alt in force+)
          also have " = (((x,l),i)p × d. ¦content (l  i)¦ * norm (f x))"
          proof -
            have "¦content (l1  k1)¦ * norm (f x1) = 0"
              if "(x1, l1)  p" "(x2, l2)  p" "k1  d" "k2  d"
                "x1 = x2" "l1  k1 = l2  k2" "x1  x2  l1  l2  k1  k2"
              for x1 l1 k1 x2 l2 k2
            proof -
              obtain u1 v1 u2 v2 where uv: "k1 = cbox u1 u2" "l1 = cbox v1 v2"
                by (meson (x1, l1)  p k1  d d(1) division_ofD(4) p'(4))
              have "l1  l2  k1  k2"
                using that by auto
              then have "interior k1  interior k2 = {}  interior l1  interior l2 = {}"
                using that p'(5) d'(5) by (metis snd_conv)
              moreover have "interior (l1  k1) = interior (l2  k2)"
                unfolding that ..
              ultimately have "interior (l1  k1) = {}"
                by auto
              then show "¦content (l1  k1)¦ * norm (f x1) = 0"
                unfolding uv Int_interval content_eq_0_interior[symmetric] by auto
            qed
            then show ?thesis
              unfolding *
              apply (subst sum.reindex_nontrivial [OF fin_pd])
              unfolding split_paired_all o_def split_def prod.inject
              by force+
          qed
          also have " = ((x,k)  p. content k *R norm (f x))"
          proof -
            have sumeq: "(id. content (l  i) * norm (f x)) = content l * norm (f x)"
              if "(x, l)  p" for x l
            proof -
              note xl = p'(2-4)[OF that]
              then obtain u v where uv: "l = cbox u v" by blast
              have "(id. ¦content (l  i)¦) = (kd. content (k  cbox u v))"
                by (simp add: Int_commute uv)
              also have " = sum content {k  cbox u v| k. k  d}"
              proof -
                have eq0: "content (k  cbox u v) = 0"
                  if "k  d" "y  d" "k  y" and eq: "k  cbox u v = y  cbox u v" for k y
                proof -
                  from d'(4)[OF that(1)] d'(4)[OF that(2)]
                  obtain α β where α: "k  cbox u v = cbox α β"
                    by (meson Int_interval)
                  have "{} = interior ((k  y)  cbox u v)"
                    by (simp add: d'(5) that)
                  also have " = interior (y  (k  cbox u v))"
                    by auto
                  also have " = interior (k  cbox u v)"
                    unfolding eq by auto
                  finally show ?thesis
                    unfolding α content_eq_0_interior ..
                qed
                then show ?thesis
                  unfolding Setcompr_eq_image
                  by (fastforce intro: sum.reindex_nontrivial [OF finite d, unfolded o_def, symmetric])
              qed
              also have " = sum content {cbox u v  k |k. k  d  cbox u v  k  {}}"
              proof (rule sum.mono_neutral_right)
                show "finite {k  cbox u v |k. k  d}"
                  by (simp add: d'(1))
              qed (fastforce simp: inf.commute)+
              finally have "(id. ¦content (l  i)¦) = content (cbox u v)"
                using additive_content_division[OF division_inter_1[OF d(1)]] uv xl(2) by auto
              then show "(id. content (l  i) * norm (f x)) = content l * norm (f x)"              
                unfolding sum_distrib_right[symmetric] using uv by auto
            qed
            show ?thesis
              by (subst sum_Sigma_product[symmetric]) (auto intro!: sumeq sum.cong p' d')
          qed
          finally show ?thesis .
        qed
      qed (rule d)
    qed
  qed
  then show ?thesis
    using absolutely_integrable_onI [OF f has_integral_integrable] has_integral[of _ ?S]
    by blast
qed


lemma bounded_variation_absolutely_integrable:
  fixes f :: "'n::euclidean_space  'm::euclidean_space"
  assumes "f integrable_on UNIV"
    and "d. d division_of (d)  sum (λk. norm (integral k f)) d  B"
  shows "f absolutely_integrable_on UNIV"
proof (rule absolutely_integrable_onI, fact)
  let ?f = "λD. kD. norm (integral k f)" and ?D = "{d. d division_of (d)}"
  define SDF where "SDF  SUP d?D. ?f d"
  have D_1: "?D  {}"
    by (rule elementary_interval) auto
  have D_2: "bdd_above (?f`?D)"
    using assms(2) by auto
  have f_int: "a b. f absolutely_integrable_on cbox a b"
    using assms integrable_on_subcbox 
    by (blast intro!: bounded_variation_absolutely_integrable_interval)
  have "B>0. a b. ball 0 B  cbox a b 
                    ¦integral (cbox a b) (λx. norm (f x)) - SDF¦ < e"
    if "0 < e" for e
  proof -
    have "y  ?f ` ?D. ¬ y  SDF - e"
    proof (rule ccontr)
      assume "¬ ?thesis"
      then have "SDF  SDF - e"
        unfolding SDF_def
        by (metis (mono_tags) D_1 cSUP_least image_eqI)
      then show False
        using that by auto
    qed
    then obtain d K where ddiv: "d division_of d" and "K = ?f d" "SDF - e < K"
      by (auto simp add: image_iff not_le)
    then have d: "SDF - e < ?f d"
      by auto
    note d'=division_ofD[OF ddiv]
    have "bounded (d)"
      using ddiv by blast
    then obtain K where K: "0 < K" "xd. norm x  K"
      using bounded_pos by blast
    show ?thesis
    proof (intro conjI impI allI exI)
      fix a b :: 'n
      assume ab: "ball 0 (K + 1)  cbox a b"
      have *: "s s1. SDF - e < s1; s1  s; s < SDF + e  ¦s - SDF¦ < e"
        by arith
      show "¦integral (cbox a b) (λx. norm (f x)) - SDF¦ < e"
        unfolding real_norm_def
      proof (rule * [OF d])
        have "?f d  sum (λk. integral k (λx. norm (f x))) d"
        proof (intro sum_mono)
          fix k assume "k  d"
          with d'(4) f_int show "norm (integral k f)  integral k (λx. norm (f x))"
            by (force simp: absolutely_integrable_on_def integral_norm_bound_integral)
        qed
        also have " = integral (d) (λx. norm (f x))"
          by (metis (full_types) absolutely_integrable_on_def d'(4) ddiv f_int integral_combine_division_bottomup)
        also have "  integral (cbox a b) (λx. norm (f x))"
        proof -
          have "d  cbox a b"
            using K(2) ab by fastforce
          then show ?thesis
            using integrable_on_subdivision[OF ddiv] f_int[of a b] unfolding absolutely_integrable_on_def
            by (auto intro!: integral_subset_le)
        qed
        finally show "?f d  integral (cbox a b) (λx. norm (f x))" .
      next
        have "e/2>0"
          using e > 0 by auto
        moreover
        have f: "f integrable_on cbox a b" "(λx. norm (f x)) integrable_on cbox a b"
          using f_int by (auto simp: absolutely_integrable_on_def)
        ultimately obtain d1 where "gauge d1"
           and d1: "p. p tagged_division_of (cbox a b); d1 fine p 
            norm (((x,k)  p. content k *R norm (f x)) - integral (cbox a b) (λx. norm (f x))) < e/2"
          unfolding has_integral_integral has_integral by meson
        obtain d2 where "gauge d2"
          and d2: "p. p tagged_partial_division_of (cbox a b); d2 fine p 
            ((x,k)  p. norm (content k *R f x - integral k f)) < e/2"
          by (blast intro: Henstock_lemma [OF f(1) e/2>0])
        obtain p where
          p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
          by (rule fine_division_exists [OF gauge_Int [OF gauge d1 gauge d2], of a b])
            (auto simp add: fine_Int)
        have *: "sf sf' si di. sf' = sf; si  SDF; ¦sf - si¦ < e/2;
                      ¦sf' - di¦ < e/2  di < SDF + e"
          by arith
        have "integral (cbox a b) (λx. norm (f x)) < SDF + e"
        proof (rule *)
          show "¦((x,k)p. norm (content k *R f x)) - ((x,k)p. norm (integral k f))¦ < e/2"
            unfolding split_def
          proof (rule absdiff_norm_less)
            show "(pp. norm (content (snd p) *R f (fst p) - integral (snd p) f)) < e/2"
              using d2[of p] p(1,3) by (auto simp: tagged_division_of_def split_def)
          qed
          show "¦((x,k)  p. content k *R norm (f x)) - integral (cbox a b) (λx. norm(f x))¦ < e/2"
            using d1[OF p(1,2)] by (simp only: real_norm_def)
          show "((x,k)  p. content k *R norm (f x)) = ((x,k)  p. norm (content k *R f x))"
            by (auto simp: split_paired_all sum.cong [OF refl])
          have "((x,k)  p. norm (integral k f)) = (ksnd ` p. norm (integral k f))"
            apply (rule sum.over_tagged_division_lemma[OF p(1)])
            by (metis Henstock_Kurzweil_Integration.integral_empty integral_open_interval norm_zero)
          also have "...  SDF"
            using partial_division_of_tagged_division[of p "cbox a b"] p(1)
            by (auto simp: SDF_def tagged_partial_division_of_def intro!: cSUP_upper2 D_1 D_2)
          finally show "((x,k)  p. norm (integral k f))  SDF" .
        qed
        then show "integral (cbox a b) (λx. norm (f x)) < SDF + e"
          by simp
      qed
    qed (use K in auto)
  qed
  moreover have "a b. (λx. norm (f x)) integrable_on cbox a b"
    using absolutely_integrable_on_def f_int by auto
  ultimately
  have "((λx. norm (f x)) has_integral SDF) UNIV"
    by (auto simp: has_integral_alt')
  then show "(λx. norm (f x)) integrable_on UNIV"
    by blast
qed


subsection‹Outer and inner approximation of measurable sets by well-behaved sets.›

proposition measurable_outer_intervals_bounded:
  assumes "S  lmeasurable" "S  cbox a b" "e > 0"
  obtains 𝒟
  where "countable 𝒟"
        "K. K  𝒟  K  cbox a b  K  {}  (c d. K = cbox c d)"
        "pairwise (λA B. interior A  interior B = {}) 𝒟"
        "u v. cbox u v  𝒟  n. i  Basis. v  i - u  i = (b  i - a  i)/2^n"
        "K. K  𝒟; box a b  {}  interior K  {}"
        "S  𝒟" "𝒟  lmeasurable" "measure lebesgue (𝒟)  measure lebesgue S + e"
proof (cases "box a b = {}")
  case True
  show ?thesis
  proof (cases "cbox a b = {}")
    case True
    with assms have [simp]: "S = {}"
      by auto
    show ?thesis
    proof
      show "countable {}"
        by simp
    qed (use e > 0 in auto)
  next
    case False
    show ?thesis
    proof
      show "countable {cbox a b}"
        by simp
      show "u v. cbox u v  {cbox a b}  n. iBasis. v  i - u  i = (b  i - a  i)/2 ^ n"
        using False by (force simp: eq_cbox intro: exI [where x=0])
      show "measure lebesgue ({cbox a b})  measure lebesgue S + e"
        using assms by (simp add: sum_content.box_empty_imp [OF True])
    qed (use assms cbox a b  {} in auto)
  qed
next
  case False
  let  = "measure lebesgue"
  have "S  cbox a b  lmeasurable"
    using S  lmeasurable by blast
  then have indS_int: "(indicator S has_integral ( S)) (cbox a b)"
    by (metis integral_indicator S  cbox a b has_integral_integrable_integral inf.orderE integrable_on_indicator)
  with e > 0 obtain γ where "gauge γ" and γ:
    "𝒟. 𝒟 tagged_division_of (cbox a b); γ fine 𝒟  norm (((x,K)𝒟. content(K) *R indicator S x) -  S) < e"
    by (force simp: has_integral)
  have inteq: "integral (cbox a b) (indicat_real S) = integral UNIV (indicator S)"
    using assms by (metis has_integral_iff indS_int lmeasure_integral_UNIV)
  obtain 𝒟 where 𝒟: "countable 𝒟"  "𝒟  cbox a b"
            and cbox: "K. K  𝒟  interior K  {}  (c d. K = cbox c d)"
            and djointish: "pairwise (λA B. interior A  interior B = {}) 𝒟"
            and covered: "K. K  𝒟  x  S  K. K  γ x"
            and close: "u v. cbox u v  𝒟  n. i  Basis. vi - ui = (bi - ai)/2^n"
            and covers: "S  𝒟"
    using covering_lemma [of S a b γ] gauge γ box a b  {} assms by force
  show ?thesis
  proof
    show "K. K  𝒟  K  cbox a b  K  {}  (c d. K = cbox c d)"
      by (meson Sup_le_iff 𝒟(2) cbox interior_empty)
    have negl_int: "negligible(K  L)" if "K  𝒟" "L  𝒟" "K  L" for K L
    proof -
      have "interior K  interior L = {}"
        using djointish pairwiseD that by fastforce
      moreover obtain u v x y where "K = cbox u v" "L = cbox x y"
        using cbox K  𝒟 L  𝒟 by blast
      ultimately show ?thesis
        by (simp add: Int_interval box_Int_box negligible_interval(1))
    qed
    have fincase: "  lmeasurable   ()   S + e" if "finite " "  𝒟" for 
    proof -
      obtain t where t: "K. K    t K  S  K  K  γ(t K)"
        using covered   𝒟 subsetD by metis
      have "K  . L  . K  L  interior K  interior L = {}"
        using that djointish by (simp add: pairwise_def) (metis subsetD)
      with cbox that 𝒟 have ℱdiv: " division_of ()"
        by (fastforce simp: division_of_def dest: cbox)
      then have 1: "  lmeasurable"
        by blast
      have norme: "p. p tagged_division_of cbox a b; γ fine p
           norm (((x,K)p. content K * indicator S x) - integral (cbox a b) (indicator S)) < e"
        by (auto simp: lmeasure_integral_UNIV assms inteq dest: γ)
      have "x K y L. (x,K)  (λK. (t K,K)) `   (y,L)  (λK. (t K,K)) `   (x,K)  (y,L)              interior K  interior L = {}"
        using that djointish  by (clarsimp simp: pairwise_def) (metis subsetD)
      with that 𝒟 have tagged: "(λK. (t K, K)) `  tagged_partial_division_of cbox a b"
        by (auto simp: tagged_partial_division_of_def dest: t cbox)
      have fine: "γ fine (λK. (t K, K)) ` "
        using t by (auto simp: fine_def)
      have *: "y   S  ¦x - y¦  e  x   S + e" for x y
        by arith
      have " ()   S + e"
      proof (rule *)
        have "(K.  (K  S)) =  (C. C  S)"
        proof (rule measure_negligible_finite_Union_image [OF finite , symmetric])
          show "K. K    K  S  lmeasurable"
            using ℱdiv S  lmeasurable by blast
          show "pairwise (λK y. negligible (K  S  (y  S))) "
            unfolding pairwise_def
            by (metis inf.commute inf_sup_aci(3) negligible_Int subsetCE negl_int   𝒟)
        qed
        also have " =  (  S)"
          by simp
        also have "   S"
          by (simp add: "1" S  lmeasurable fmeasurableD measure_mono_fmeasurable sets.Int)
        finally show "(K.  (K  S))   S" .
      next
        have " () = sum  "
          by (metis ℱdiv content_division)
        also have " = (K. content K)"
          using ℱdiv by (force intro: sum.cong)
        also have " = (x. content x * indicator S (t x))"
          using t by auto
        finally have eq1: " () = (x. content x * indicator S (t x))" .
        have eq2: "(K.  (K  S)) = (K. integral K (indicator S))"
          apply (rule sum.cong [OF refl])
          by (metis integral_indicator ℱdiv S  lmeasurable division_ofD(4) fmeasurable.Int inf.commute lmeasurable_cbox)
        have "¦(x,K)(λK. (t K, K)) ` . content K * indicator S x - integral K (indicator S)¦  e"
          using Henstock_lemma_part1 [of "indicator S::'areal", OF _ e > 0 gauge γ _ tagged fine]
            indS_int norme by auto
        then show "¦ () - (K.  (K  S))¦  e"
          by (simp add: eq1 eq2 comm_monoid_add_class.sum.reindex inj_on_def sum_subtractf)
      qed
      with 1 show ?thesis by blast
    qed
    have "𝒟  lmeasurable   (𝒟)   S + e"
    proof (cases "finite 𝒟")
      case True
      with fincase show ?thesis
        by blast
    next
      case False
      let ?T = "from_nat_into 𝒟"
      have T: "bij_betw ?T UNIV 𝒟"
        by (simp add: False 𝒟(1) bij_betw_from_nat_into)
      have TM: "n. ?T n  lmeasurable"
        by (metis False cbox finite.emptyI from_nat_into lmeasurable_cbox)
      have TN: "m n. m  n  negligible (?T m  ?T n)"
        by (simp add: False 𝒟(1) from_nat_into infinite_imp_nonempty negl_int)
      have TB: "(kn.  (?T k))   S + e" for n
      proof -
        have "(kn.  (?T k)) =  ( (?T ` {..n}))"
          by (simp add: pairwise_def TM TN measure_negligible_finite_Union_image)
        also have " ( (?T ` {..n}))   S + e"
          using fincase [of "?T ` {..n}"] T by (auto simp: bij_betw_def)
        finally show ?thesis .
      qed
      have "𝒟  lmeasurable"
        by (metis lmeasurable_compact T 𝒟(2) bij_betw_def cbox compact_cbox countable_Un_Int(1) fmeasurableD fmeasurableI2 rangeI)
      moreover
      have " (x. from_nat_into 𝒟 x)   S + e"
      proof (rule measure_countable_Union_le [OF TM])
        show " (xn. from_nat_into 𝒟 x)   S + e" for n
          by (metis (mono_tags, lifting) False fincase finite.emptyI finite_atMost finite_imageI from_nat_into imageE subsetI)
      qed
      ultimately show ?thesis by (metis T bij_betw_def)
    qed
    then show "𝒟  lmeasurable" "measure lebesgue (𝒟)   S + e" by blast+
  qed (use 𝒟 cbox djointish close covers in auto)
qed


subsection‹Transformation of measure by linear maps›

lemma emeasure_lebesgue_ball_conv_unit_ball:
  fixes c :: "'a :: euclidean_space"
  assumes "r  0"
  shows "emeasure lebesgue (ball c r) =
           ennreal (r ^ DIM('a)) * emeasure lebesgue (ball (0 :: 'a) 1)"
proof (cases "r = 0")
  case False
  with assms have r: "r > 0" by auto
  have "emeasure lebesgue ((λx. c + x) ` (λx. r *R x) ` ball (0 :: 'a) 1) =
          r ^ DIM('a) * emeasure lebesgue (ball (0 :: 'a) 1)"
    unfolding image_image using emeasure_lebesgue_affine[of r c "ball 0 1"] assms
    by (simp add: add_ac)
  also have "(λx. r *R x) ` ball 0 1 = ball (0 :: 'a) r"
    using r by (subst ball_scale) auto
  also have "(λx. c + x) `  = ball c r"
    by (subst image_add_ball) (simp_all add: algebra_simps)
  finally show ?thesis by simp
qed auto

lemma content_ball_conv_unit_ball:
  fixes c :: "'a :: euclidean_space"
  assumes "r  0"
  shows "content (ball c r) = r ^ DIM('a) * content (ball (0 :: 'a) 1)"
proof -
  have "ennreal (content (ball c r)) = emeasure lebesgue (ball c r)"
    using emeasure_lborel_ball_finite[of c r] by (subst emeasure_eq_ennreal_measure) auto
  also have " = ennreal (r ^ DIM('a)) * emeasure lebesgue (ball (0 :: 'a) 1)"
    using assms by (intro emeasure_lebesgue_ball_conv_unit_ball) auto
  also have " = ennreal (r ^ DIM('a) * content (ball (0::'a) 1))"
    using emeasure_lborel_ball_finite[of "0::'a" 1] assms
    by (subst emeasure_eq_ennreal_measure) (auto simp: ennreal_mult')
  finally show ?thesis 
    using assms by (subst (asm) ennreal_inj) auto
qed

lemma measurable_linear_image_interval:
   "linear f  f ` (cbox a b)  lmeasurable"
  by (metis bounded_linear_image linear_linear bounded_cbox closure_bounded_linear_image closure_cbox compact_closure lmeasurable_compact)

proposition measure_linear_sufficient:
  fixes f :: "'n::euclidean_space  'n"
  assumes "linear f" and S: "S  lmeasurable"
    and im: "a b. measure lebesgue (f ` (cbox a b)) = m * measure lebesgue (cbox a b)"
  shows "f ` S  lmeasurable  m * measure lebesgue S = measure lebesgue (f ` S)"
  using le_less_linear [of 0 m]
proof
  assume "m < 0"
  then show ?thesis
    using im [of 0 One] by auto
next
  assume "m  0"
  let  = "measure lebesgue"
  show ?thesis
  proof (cases "inj f")
    case False
    then have " (f ` S) = 0"
      using linear f negligible_imp_measure0 negligible_linear_singular_image by blast
    then have "m *  (cbox 0 (One)) = 0"
      by (metis False linear f cbox_borel content_unit im measure_completion negligible_imp_measure0 negligible_linear_singular_image sets_lborel)
    then show ?thesis
      using linear f negligible_linear_singular_image negligible_imp_measure0 False
      by (auto simp: lmeasurable_iff_has_integral negligible_UNIV)
  next
    case True
    then obtain h where "linear h" and hf: "x. h (f x) = x" and fh: "x. f (h x) = x"
      using linear f linear_injective_isomorphism by blast
    have fBS: "(f ` S)  lmeasurable  m *  S =  (f ` S)"
      if "bounded S" "S  lmeasurable" for S
    proof -
      obtain a b where "S  cbox a b"
        using bounded S bounded_subset_cbox_symmetric by metis
      have fUD: "(f ` 𝒟)  lmeasurable   (f ` 𝒟) = (m *  (𝒟))"
        if "countable 𝒟"
          and cbox: "K. K  𝒟  K  cbox a b  K  {}  (c d. K = cbox c d)"
          and intint: "pairwise (λA B. interior A  interior B = {}) 𝒟"
        for 𝒟
      proof -
        have conv: "K. K  𝒟  convex K"
          using cbox convex_box(1) by blast
        have neg: "negligible (g ` K  g ` L)" if "linear g" "K  𝒟" "L  𝒟" "K  L"
          for K L and g :: "'n'n"
        proof (cases "inj g")
          case True
          have "negligible (frontier(g ` K  g ` L)  interior(g ` K  g ` L))"
          proof (rule negligible_Un)
            show "negligible (frontier (g ` K  g ` L))"
              by (simp add: negligible_convex_frontier convex_Int conv convex_linear_image that)
          next
            have "p N. pairwise p N = (Na. (Na::'n set)  N  (Nb. Nb  N  Na  Nb  p Na Nb))"
              by (metis pairwise_def)
            then have "interior K  interior L = {}"
              using intint that(2) that(3) that(4) by presburger
            then show "negligible (interior (g ` K  g ` L))"
              by (metis True empty_imp_negligible image_Int image_empty interior_Int interior_injective_linear_image that(1))
          qed
          moreover have "g ` K  g ` L  frontier (g ` K  g ` L)  interior (g ` K  g ` L)"
            by (metis Diff_partition Int_commute calculation closure_Un_frontier frontier_def inf.absorb_iff2 inf_bot_right inf_sup_absorb negligible_Un_eq open_interior open_not_negligible sup_commute)
          ultimately show ?thesis
            by (rule negligible_subset)
        next
          case False
          then show ?thesis
            by (simp add: negligible_Int negligible_linear_singular_image linear g)
        qed
        have negf: "negligible ((f ` K)  (f ` L))"
        and negid: "negligible (K  L)" if "K  𝒟" "L  𝒟" "K  L" for K L
          using neg [OF linear f] neg [OF linear_id] that by auto
        show ?thesis
        proof (cases "finite 𝒟")
          case True
          then have " (x𝒟. f ` x) = (x𝒟.  (f ` x))"
            using linear f cbox measurable_linear_image_interval negf
            by (blast intro: measure_negligible_finite_Union_image [unfolded pairwise_def])
          also have " = (k𝒟. m *  k)"
            by (metis (no_types, lifting) cbox im sum.cong)
          also have " = m *  (𝒟)"
            unfolding sum_distrib_left [symmetric]
            by (metis True cbox lmeasurable_cbox measure_negligible_finite_Union [unfolded pairwise_def] negid)
          finally show ?thesis
            by (metis True linear f cbox image_Union fmeasurable.finite_UN measurable_linear_image_interval)
        next
          case False
          with countable 𝒟 obtain X :: "nat  'n set" where S: "bij_betw X UNIV 𝒟"
            using bij_betw_from_nat_into by blast
          then have eq: "(𝒟) = (n. X n)" "(f ` 𝒟) = (n. f ` X n)"
            by (auto simp: bij_betw_def)
          have meas: "K. K  𝒟  K  lmeasurable"
            using cbox by blast
          with S have 1: "n. X n  lmeasurable"
            by (auto simp: bij_betw_def)
          have 2: "pairwise (λm n. negligible (X m  X n)) UNIV"
            using S unfolding bij_betw_def pairwise_def by (metis injD negid range_eqI)
          have "bounded (𝒟)"
            by (meson Sup_least bounded_cbox bounded_subset cbox)
          then have 3: "bounded (n. X n)"
            using S unfolding bij_betw_def by blast
          have "(n. X n)  lmeasurable"
            by (rule measurable_countable_negligible_Union_bounded [OF 1 2 3])
          with S have f1: "n. f ` (X n)  lmeasurable"
            unfolding bij_betw_def by (metis assms(1) cbox measurable_linear_image_interval rangeI)
          have f2: "pairwise (λm n. negligible (f ` (X m)  f ` (X n))) UNIV"
            using S unfolding bij_betw_def pairwise_def by (metis injD negf rangeI)
          have "bounded (𝒟)"
            by (meson Sup_least bounded_cbox bounded_subset cbox)
          then have f3: "bounded (n. f ` X n)"
            using S unfolding bij_betw_def
            by (metis bounded_linear_image linear_linear assms(1) image_Union range_composition)
          have "(λn.  (X n)) sums  (n. X n)"
            by (rule measure_countable_negligible_Union_bounded [OF 1 2 3])
          have meq: " (n. f ` X n) = m *  ((X ` UNIV))"
          proof (rule sums_unique2 [OF measure_countable_negligible_Union_bounded [OF f1 f2 f3]])
            have m: "n.  (f ` X n) = (m *  (X n))"
              using S unfolding bij_betw_def by (metis cbox im rangeI)
            show "(λn.  (f ` X n)) sums (m *  ((X ` UNIV)))"
              unfolding m
              using measure_countable_negligible_Union_bounded [OF 1 2 3] sums_mult by blast
          qed
          show ?thesis
            using measurable_countable_negligible_Union_bounded [OF f1 f2 f3] meq
            by (auto simp: eq [symmetric])
        qed
      qed
      show ?thesis
        unfolding completion.fmeasurable_measure_inner_outer_le
      proof (intro conjI allI impI)
        fix e :: real
        assume "e > 0"
        have 1: "cbox a b - S  lmeasurable"
          by (simp add: fmeasurable.Diff that)
        have 2: "0 < e / (1 + ¦m¦)"
          using e > 0 by (simp add: field_split_simps abs_add_one_gt_zero)
        obtain 𝒟
          where "countable 𝒟"
            and cbox: "K. K  𝒟  K  cbox a b  K  {}  (c d. K = cbox c d)"
            and intdisj: "pairwise (λA B. interior A  interior B = {}) 𝒟"
            and DD: "cbox a b - S  𝒟" "𝒟  lmeasurable"
            and le: " (𝒟)   (cbox a b - S) + e/(1 + ¦m¦)"
          by (rule measurable_outer_intervals_bounded [of "cbox a b - S" a b "e/(1 + ¦m¦)"]; use 1 2 pairwise_def in force)
        show "T  lmeasurable. T  f ` S  m *  S - e   T"
        proof (intro bexI conjI)
          show "f ` (cbox a b) - f ` (𝒟)  f ` S"
            using cbox a b - S  𝒟 by force
          have "m *  S - e  m * ( S - e / (1 + ¦m¦))"
            using m  0 e > 0 by (simp add: field_simps)
          also have "   (f ` cbox a b) -  (f ` (𝒟))"
          proof -
            have " (cbox a b - S) =  (cbox a b) -  S"
              by (simp add: measurable_measure_Diff S  cbox a b fmeasurableD that(2))
            then have "( S - e / (1 + m))  (content (cbox a b) -  ( 𝒟))"
              using m  0 le by auto
            then show ?thesis
              using m  0 e > 0
              by (simp add: mult_left_mono im fUD [OF countable 𝒟 cbox intdisj] flip: right_diff_distrib)
          qed
          also have " =  (f ` cbox a b - f ` 𝒟)"
          proof (rule measurable_measure_Diff [symmetric])
            show "f ` cbox a b  lmeasurable"
              by (simp add: assms(1) measurable_linear_image_interval)
            show "f `  𝒟  sets lebesgue"
              by (simp add: countable 𝒟 cbox fUD fmeasurableD intdisj)
            show "f `  𝒟  f ` cbox a b"
              by (simp add: Sup_le_iff cbox image_mono)
          qed
          finally show "m *  S - e   (f ` cbox a b - f ` 𝒟)" .
          show "f ` cbox a b - f ` 𝒟  lmeasurable"
            by (simp add: fUD countable 𝒟 linear f cbox fmeasurable.Diff intdisj measurable_linear_image_interval)
        qed
      next
        fix e :: real
        assume "e > 0"
        have em: "0 < e / (1 + ¦m¦)"
          using e > 0 by (simp add: field_split_simps abs_add_one_gt_zero)
        obtain 𝒟
          where "countable 𝒟"
            and cbox: "K. K  𝒟  K  cbox a b  K  {}  (c d. K = cbox c d)"
            and intdisj: "pairwise (λA B. interior A  interior B = {}) 𝒟"
            and DD: "S  𝒟" "𝒟  lmeasurable"
            and le: " (𝒟)   S + e/(1 + ¦m¦)"
          by (rule measurable_outer_intervals_bounded [of S a b "e/(1 + ¦m¦)"]; use S  lmeasurable S  cbox a b em in force)
        show "U  lmeasurable. f ` S  U   U  m *  S + e"
        proof (intro bexI conjI)
          show "f ` S  f ` (𝒟)"
            by (simp add: DD(1) image_mono)
          have " (f ` 𝒟)  m * ( S + e / (1 + ¦m¦))"
            using m  0 le mult_left_mono
            by (auto simp: fUD countable 𝒟 linear f cbox fmeasurable.Diff intdisj measurable_linear_image_interval)
          also have "  m *  S + e"
            using m  0 e > 0 by (simp add: fUD [OF countable 𝒟 cbox intdisj] field_simps)
          finally show " (f ` 𝒟)  m *  S + e" .
          show "f ` 𝒟  lmeasurable"
            by (simp add: countable 𝒟 cbox fUD intdisj)
        qed
      qed
    qed
    show ?thesis
      unfolding has_measure_limit_iff
    proof (intro allI impI)
      fix e :: real
      assume "e > 0"
      obtain B where "B > 0" and B:
        "a b. ball 0 B  cbox a b  ¦ (S  cbox a b) -  S¦ < e / (1 + ¦m¦)"
        using has_measure_limit [OF S] e > 0 by (metis abs_add_one_gt_zero zero_less_divide_iff)
      obtain c d::'n where cd: "ball 0 B  cbox c d"
        by (metis bounded_subset_cbox_symmetric bounded_ball)
      with B have less: "¦ (S  cbox c d) -  S¦ < e / (1 + ¦m¦)" .
      obtain D where "D > 0" and D: "cbox c d  ball 0 D"
        by (metis bounded_cbox bounded_subset_ballD)
      obtain C where "C > 0" and C: "x. norm (f x)  C * norm x"
        using linear_bounded_pos linear f by blast
      have "f ` S  cbox a b  lmeasurable 
            ¦ (f ` S  cbox a b) - m *  S¦ < e"
        if "ball 0 (D*C)  cbox a b" for a b
      proof -
        have "bounded (S  h ` cbox a b)"
          by (simp add: bounded_linear_image linear_linear linear h bounded_Int)
        moreover have Shab: "S  h ` cbox a b  lmeasurable"
          by (simp add: S linear h fmeasurable.Int measurable_linear_image_interval)
        moreover have fim: "f ` (S  h ` (cbox a b)) = (f ` S)  cbox a b"
          by (auto simp: hf rev_image_eqI fh)
        ultimately have 1: "(f ` S)  cbox a b  lmeasurable"
              and 2: " ((f ` S)  cbox a b) = m *  (S  h ` cbox a b)"
          using fBS [of "S  (h ` (cbox a b))"] by auto
        have *: "¦z - m¦ < e; z  w; w  m  ¦w - m¦  e"
          for w z m and e::real by auto
        have meas_adiff: "¦ (S  h ` cbox a b) -  S¦  e / (1 + ¦m¦)"
        proof (rule * [OF less])
          show " (S  cbox c d)   (S  h ` cbox a b)"
          proof (rule measure_mono_fmeasurable [OF _ _ Shab])
            have "f ` ball 0 D  ball 0 (C * D)"
              using C C > 0
              apply (clarsimp simp: algebra_simps)
              by (meson le_less_trans linordered_comm_semiring_strict_class.comm_mult_strict_left_mono)
            then have "f ` ball 0 D  cbox a b"
              by (metis mult.commute order_trans that)
            have "ball 0 D  h ` cbox a b"
              by (metis f ` ball 0 D  cbox a b hf image_subset_iff subsetI)
            then show "S  cbox c d  S  h ` cbox a b"
              using D by blast
          next
            show "S  cbox c d  sets lebesgue"
              using S fmeasurable_cbox by blast
          qed
        next
          show " (S  h ` cbox a b)   S"
            by (simp add: S Shab fmeasurableD measure_mono_fmeasurable)
        qed
        have "¦ (f ` S  cbox a b) - m *  S¦  ¦ S -  (S  h ` cbox a b)¦ * m"
          by (metis "2" m  0 abs_minus_commute abs_mult_pos mult.commute order_refl right_diff_distrib')
        also have "  e / (1 + m) * m"
          by (metis m  0 abs_minus_commute abs_of_nonneg meas_adiff mult.commute mult_left_mono)
        also have " < e"
          using e > 0 m  0 by (simp add: field_simps)
        finally have "¦ (f ` S  cbox a b) - m *  S¦ < e" .
        with 1 show ?thesis by auto
      qed
      then show "B>0. a b. ball 0 B  cbox a b 
                         f ` S  cbox a b  lmeasurable 
                         ¦ (f ` S  cbox a b) - m *  S¦ < e"
        using C>0 D>0 by (metis mult_zero_left mult_less_cancel_right_pos)
    qed
  qed
qed

subsection‹Lemmas about absolute integrability›

lemma absolutely_integrable_linear:
  fixes f :: "'m::euclidean_space  'n::euclidean_space"
    and h :: "'n::euclidean_space  'p::euclidean_space"
  shows "f absolutely_integrable_on s  bounded_linear h  (h  f) absolutely_integrable_on s"
  using integrable_bounded_linear[of h lebesgue "λx. indicator s x *R f x"]
  by (simp add: linear_simps[of h] set_integrable_def)

lemma absolutely_integrable_sum:
  fixes f :: "'a  'n::euclidean_space  'm::euclidean_space"
  assumes "finite T" and "a. a  T  (f a) absolutely_integrable_on S"
  shows "(λx. sum (λa. f a x) T) absolutely_integrable_on S"
  using assms by induction auto

lemma absolutely_integrable_integrable_bound:
  fixes f :: "'n::euclidean_space  'm::euclidean_space"
  assumes le: "x. xS  norm (f x)  g x" and f: "f integrable_on S" and g: "g integrable_on S"
  shows "f absolutely_integrable_on S"
    unfolding set_integrable_def
proof (rule Bochner_Integration.integrable_bound)
  have "g absolutely_integrable_on S"
    unfolding absolutely_integrable_on_def
  proof
    show "(λx. norm (g x)) integrable_on S"
      using le norm_ge_zero[of "f _"]
      by (intro integrable_spike_finite[OF _ _ g, of "{}"])
         (auto intro!: abs_of_nonneg intro: order_trans simp del: norm_ge_zero)
  qed fact
  then show "integrable lebesgue (λx. indicat_real S x *R g x)"
    by (simp add: set_integrable_def)
  show "(λx. indicat_real S x *R f x)  borel_measurable lebesgue"
    using f by (auto intro: has_integral_implies_lebesgue_measurable simp: integrable_on_def)
qed (use le in force intro!: always_eventually split: split_indicator)

corollary absolutely_integrable_on_const [simp]:
  fixes c :: "'a::euclidean_space"
  assumes "S  lmeasurable"
  shows "(λx. c) absolutely_integrable_on S"
  by (metis (full_types) assms absolutely_integrable_integrable_bound integrable_on_const order_refl)

lemma absolutely_integrable_continuous:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  shows "continuous_on (cbox a b) f  f absolutely_integrable_on cbox a b"
  using absolutely_integrable_integrable_bound
  by (simp add: absolutely_integrable_on_def continuous_on_norm integrable_continuous)

lemma absolutely_integrable_continuous_real:
  fixes f :: "real  'b::euclidean_space"
  shows "continuous_on {a..b} f  f absolutely_integrable_on {a..b}"
  by (metis absolutely_integrable_continuous box_real(2))

lemma continuous_imp_integrable:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "continuous_on (cbox a b) f"
  shows "integrable (lebesgue_on (cbox a b)) f"
proof -
  have "f absolutely_integrable_on cbox a b"
    by (simp add: absolutely_integrable_continuous assms)
  then show ?thesis
    by (simp add: integrable_restrict_space set_integrable_def)
qed

lemma continuous_imp_integrable_real:
  fixes f :: "real  'b::euclidean_space"
  assumes "continuous_on {a..b} f"
  shows "integrable (lebesgue_on {a..b}) f"
  by (metis assms continuous_imp_integrable interval_cbox)



subsection ‹Componentwise›

proposition absolutely_integrable_componentwise_iff:
  shows "f absolutely_integrable_on A  (bBasis. (λx. f x  b) absolutely_integrable_on A)"
proof -
  have *: "(λx. norm (f x)) integrable_on A  (bBasis. (λx. norm (f x  b)) integrable_on A)" (is "?lhs = ?rhs")
    if "f integrable_on A"
  proof
    assume ?lhs
    then show ?rhs
      by (metis absolutely_integrable_on_def Topology_Euclidean_Space.norm_nth_le absolutely_integrable_integrable_bound integrable_component that)
  next
    assume R: ?rhs
    have "f absolutely_integrable_on A"
    proof (rule absolutely_integrable_integrable_bound)
      show "(λx. iBasis. norm (f x  i)) integrable_on A"
        using R by (force intro: integrable_sum)
    qed (use that norm_le_l1 in auto)
    then show ?lhs
      using absolutely_integrable_on_def by auto
  qed
  show ?thesis
    unfolding absolutely_integrable_on_def
    by (simp add:  integrable_componentwise_iff [symmetric] ball_conj_distrib * cong: conj_cong)
qed

lemma absolutely_integrable_componentwise:
  shows "(b. b  Basis  (λx. f x  b) absolutely_integrable_on A)  f absolutely_integrable_on A"
  using absolutely_integrable_componentwise_iff by blast

lemma absolutely_integrable_component:
  "f absolutely_integrable_on A  (λx. f x  (b :: 'b :: euclidean_space)) absolutely_integrable_on A"
  by (drule absolutely_integrable_linear[OF _ bounded_linear_inner_left[of b]]) (simp add: o_def)


lemma absolutely_integrable_scaleR_left:
  fixes f :: "'n::euclidean_space  'm::euclidean_space"
    assumes "f absolutely_integrable_on S"
  shows "(λx. c *R f x) absolutely_integrable_on S"
proof -
  have "(λx. c *R x) o f absolutely_integrable_on S"
    by (simp add: absolutely_integrable_linear assms bounded_linear_scaleR_right)
  then show ?thesis
    using assms by blast
qed

lemma absolutely_integrable_scaleR_right:
  assumes "f absolutely_integrable_on S"
  shows "(λx. f x *R c) absolutely_integrable_on S"
  using assms by blast

lemma absolutely_integrable_norm:
  fixes f :: "'a :: euclidean_space  'b :: euclidean_space"
  assumes "f absolutely_integrable_on S"
  shows "(norm o f) absolutely_integrable_on S"
  using assms by (simp add: absolutely_integrable_on_def o_def)

lemma absolutely_integrable_abs:
  fixes f :: "'a :: euclidean_space  'b :: euclidean_space"
  assumes "f absolutely_integrable_on S"
  shows "(λx. iBasis. ¦f x  i¦ *R i) absolutely_integrable_on S"
        (is "?g absolutely_integrable_on S")
proof -
  have *: "(λy. jBasis. if j = i then y *R j else 0) 
           (λx. norm (jBasis. if j = i then (x  i) *R j else 0))  f
           absolutely_integrable_on S"
        if "i  Basis" for i
  proof -
    have "bounded_linear (λy. jBasis. if j = i then y *R j else 0)"
      by (simp add: linear_linear algebra_simps linearI)
    moreover have "(λx. norm (jBasis. if j = i then (x  i) *R j else 0))  f
                   absolutely_integrable_on S"
      using assms i  Basis
      unfolding o_def
      by (intro absolutely_integrable_norm [unfolded o_def])
         (auto simp: algebra_simps dest: absolutely_integrable_component)
    ultimately show ?thesis
      by (subst comp_assoc) (blast intro: absolutely_integrable_linear)
  qed
  have eq: "?g =
        (λx. iBasis. ((λy. jBasis. if j = i then y *R j else 0) 
               (λx. norm(jBasis. if j = i then (x  i) *R j else 0))  f) x)"
    by (simp)
  show ?thesis
    unfolding eq
    by (rule absolutely_integrable_sum) (force simp: intro!: *)+
qed

lemma abs_absolutely_integrableI_1:
  fixes f :: "'a :: euclidean_space  real"
  assumes f: "f integrable_on A" and "(λx. ¦f x¦) integrable_on A"
  shows "f absolutely_integrable_on A"
  by (rule absolutely_integrable_integrable_bound [OF _ assms]) auto


lemma abs_absolutely_integrableI:
  assumes f: "f integrable_on S" and fcomp: "(λx. iBasis. ¦f x  i¦ *R i) integrable_on S"
  shows "f absolutely_integrable_on S"
proof -
  have "(λx. (f x  i) *R i) absolutely_integrable_on S" if "i  Basis" for i
  proof -
    have "(λx. ¦f x  i¦) integrable_on S"
      using assms integrable_component [OF fcomp, where y=i] that by simp
    then have "(λx. f x  i) absolutely_integrable_on S"
      using abs_absolutely_integrableI_1 f integrable_component by blast
    then show ?thesis
      by (rule absolutely_integrable_scaleR_right)
  qed
  then have "(λx. iBasis. (f x  i) *R i) absolutely_integrable_on S"
    by (simp add: absolutely_integrable_sum)
  then show ?thesis
    by (simp add: euclidean_representation)
qed


lemma absolutely_integrable_abs_iff:
   "f absolutely_integrable_on S 
    f integrable_on S  (λx. iBasis. ¦f x  i¦ *R i) integrable_on S"
    (is "?lhs = ?rhs")
proof
  assume ?lhs then show ?rhs
    using absolutely_integrable_abs absolutely_integrable_on_def by blast
next
  assume ?rhs
  moreover
  have "(λx. if x  S then iBasis. ¦f x  i¦ *R i else 0) = (λx. iBasis. ¦(if x  S then f x else 0)  i¦ *R i)"
    by force
  ultimately show ?lhs
    by (simp only: absolutely_integrable_restrict_UNIV [of S, symmetric] integrable_restrict_UNIV [of S, symmetric] abs_absolutely_integrableI)
qed

lemma absolutely_integrable_max:
  fixes f :: "'n::euclidean_space  'm::euclidean_space"
  assumes "f absolutely_integrable_on S" "g absolutely_integrable_on S"
   shows "(λx. iBasis. max (f x  i) (g x  i) *R i)
            absolutely_integrable_on S"
proof -
  have "(λx. iBasis. max (f x  i) (g x  i) *R i) =
        (λx. (1/2) *R (f x + g x + (iBasis. ¦f x  i - g x  i¦ *R i)))"
  proof (rule ext)
    fix x
    have "(iBasis. max (f x  i) (g x  i) *R i) = (iBasis. ((f x  i + g x  i + ¦f x  i - g x  i¦) / 2) *R i)"
      by (force intro: sum.cong)
    also have "... = (1 / 2) *R (iBasis. (f x  i + g x  i + ¦f x  i - g x  i¦) *R i)"
      by (simp add: scaleR_right.sum)
    also have "... = (1 / 2) *R (f x + g x + (iBasis. ¦f x  i - g x  i¦ *R i))"
      by (simp add: sum.distrib algebra_simps euclidean_representation)
    finally
    show "(iBasis. max (f x  i) (g x  i) *R i) =
         (1 / 2) *R (f x + g x + (iBasis. ¦f x  i - g x  i¦ *R i))" .
  qed
  moreover have "(λx. (1 / 2) *R (f x + g x + (iBasis. ¦f x  i - g x  i¦ *R i)))
                 absolutely_integrable_on S"
    using absolutely_integrable_abs [OF set_integral_diff(1) [OF assms]]
    by (intro set_integral_add absolutely_integrable_scaleR_left assms) (simp add: algebra_simps)
  ultimately show ?thesis by metis
qed

corollary absolutely_integrable_max_1:
  fixes f :: "'n::euclidean_space  real"
  assumes "f absolutely_integrable_on S" "g absolutely_integrable_on S"
   shows "(λx. max (f x) (g x)) absolutely_integrable_on S"
  using absolutely_integrable_max [OF assms] by simp

lemma absolutely_integrable_min:
  fixes f :: "'n::euclidean_space  'm::euclidean_space"
  assumes "f absolutely_integrable_on S" "g absolutely_integrable_on S"
   shows "(λx. iBasis. min (f x  i) (g x  i) *R i)
            absolutely_integrable_on S"
proof -
  have "(λx. iBasis. min (f x  i) (g x  i) *R i) =
        (λx. (1/2) *R (f x + g x - (iBasis. ¦f x  i - g x  i¦ *R i)))"
  proof (rule ext)
    fix x
    have "(iBasis. min (f x  i) (g x  i) *R i) = (iBasis. ((f x  i + g x  i - ¦f x  i - g x  i¦) / 2) *R i)"
      by (force intro: sum.cong)
    also have "... = (1 / 2) *R (iBasis. (f x  i + g x  i - ¦f x  i - g x  i¦) *R i)"
      by (simp add: scaleR_right.sum)
    also have "... = (1 / 2) *R (f x + g x - (iBasis. ¦f x  i - g x  i¦ *R i))"
      by (simp add: sum.distrib sum_subtractf algebra_simps euclidean_representation)
    finally
    show "(iBasis. min (f x  i) (g x  i) *R i) =
         (1 / 2) *R (f x + g x - (iBasis. ¦f x  i - g x  i¦ *R i))" .
  qed
  moreover have "(λx. (1 / 2) *R (f x + g x - (iBasis. ¦f x  i - g x  i¦ *R i)))
                 absolutely_integrable_on S"
    using absolutely_integrable_abs [OF set_integral_diff(1) [OF assms]]
    by (intro set_integral_add set_integral_diff absolutely_integrable_scaleR_left assms)
       (simp add: algebra_simps)
  ultimately show ?thesis by metis
qed

corollary absolutely_integrable_min_1:
  fixes f :: "'n::euclidean_space  real"
  assumes "f absolutely_integrable_on S" "g absolutely_integrable_on S"
   shows "(λx. min (f x) (g x)) absolutely_integrable_on S"
  using absolutely_integrable_min [OF assms] by simp

lemma nonnegative_absolutely_integrable:
  fixes f :: "'a :: euclidean_space  'b :: euclidean_space"
  assumes "f integrable_on A" and comp: "x b. x  A; b  Basis  0  f x  b"
  shows "f absolutely_integrable_on A"
proof -
  have "(λx. (f x  i) *R i) absolutely_integrable_on A" if "i  Basis" for i
  proof -
    have "(λx. f x  i) integrable_on A"
      by (simp add: assms(1) integrable_component)
    then have "(λx. f x  i) absolutely_integrable_on A"
      by (metis that comp nonnegative_absolutely_integrable_1)
    then show ?thesis
      by (rule absolutely_integrable_scaleR_right)
  qed
  then have "(λx. iBasis. (f x  i) *R i) absolutely_integrable_on A"
    by (simp add: absolutely_integrable_sum)
  then show ?thesis
    by (simp add: euclidean_representation)
qed

lemma absolutely_integrable_component_ubound:
  fixes f :: "'a :: euclidean_space  'b :: euclidean_space"
  assumes f: "f integrable_on A" and g: "g absolutely_integrable_on A"
      and comp: "x b. x  A; b  Basis  f x  b  g x  b"
  shows "f absolutely_integrable_on A"
proof -
  have "(λx. g x - (g x - f x)) absolutely_integrable_on A"
  proof (rule set_integral_diff [OF g nonnegative_absolutely_integrable])
    show "(λx. g x - f x) integrable_on A"
      using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g by blast
  qed (simp add: comp inner_diff_left)
  then show ?thesis
    by simp
qed

lemma absolutely_integrable_component_lbound:
  fixes f :: "'a :: euclidean_space  'b :: euclidean_space"
  assumes f: "f absolutely_integrable_on A" and g: "g integrable_on A"
      and comp: "x b. x  A; b  Basis  f x  b  g x  b"
  shows "g absolutely_integrable_on A"
proof -
  have "(λx. f x + (g x - f x)) absolutely_integrable_on A"
  proof (rule set_integral_add [OF f nonnegative_absolutely_integrable])
    show "(λx. g x - f x) integrable_on A"
      using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g by blast
  qed (simp add: comp inner_diff_left)
  then show ?thesis
    by simp
qed

lemma integrable_on_1_iff:
  fixes f :: "'a::euclidean_space  real^1"
  shows "f integrable_on S  (λx. f x $ 1) integrable_on S"
  by (auto simp: integrable_componentwise_iff [of f] Basis_vec_def cart_eq_inner_axis)

lemma integral_on_1_eq:
  fixes f :: "'a::euclidean_space  real^1"
  shows "integral S f = vec (integral S (λx. f x $ 1))"
by (cases "f integrable_on S") (simp_all add: integrable_on_1_iff vec_eq_iff not_integrable_integral)

lemma absolutely_integrable_on_1_iff:
  fixes f :: "'a::euclidean_space  real^1"
  shows "f absolutely_integrable_on S  (λx. f x $ 1) absolutely_integrable_on S"
  unfolding absolutely_integrable_on_def
  by (auto simp: integrable_on_1_iff norm_real)

lemma absolutely_integrable_absolutely_integrable_lbound:
  fixes f :: "'m::euclidean_space  real"
  assumes f: "f integrable_on S" and g: "g absolutely_integrable_on S"
    and *: "x. x  S  g x  f x"
  shows "f absolutely_integrable_on S"
  by (rule absolutely_integrable_component_lbound [OF g f]) (simp add: *)

lemma absolutely_integrable_absolutely_integrable_ubound:
  fixes f :: "'m::euclidean_space  real"
  assumes fg: "f integrable_on S" "g absolutely_integrable_on S"
    and *: "x. x  S  f x  g x"
  shows "f absolutely_integrable_on S"
  by (rule absolutely_integrable_component_ubound [OF fg]) (simp add: *)

lemma has_integral_vec1_I_cbox:
  fixes f :: "real^1  'a::real_normed_vector"
  assumes "(f has_integral y) (cbox a b)"
  shows "((f  vec) has_integral y) {a$1..b$1}"
proof -
  have "((λx. f(vec x)) has_integral (1 / 1) *R y) ((λx. x $ 1) ` cbox a b)"
  proof (rule has_integral_twiddle)
    show "w z::real^1. vec ` cbox u v = cbox w z"
         "content (vec ` cbox u v :: (real^1) set) = 1 * content (cbox u v)" for u v
      unfolding vec_cbox_1_eq
      by (auto simp: content_cbox_if_cart interval_eq_empty_cart)
    show "w z. (λx. x $ 1) ` cbox u v = cbox w z" for u v :: "real^1"
      using vec_nth_cbox_1_eq by blast
  qed (auto simp: continuous_vec assms)
  then show ?thesis
    by (simp add: o_def)
qed

lemma has_integral_vec1_I:
  fixes f :: "real^1  'a::real_normed_vector"
  assumes "(f has_integral y) S"
  shows "(f  vec has_integral y) ((λx. x $ 1) ` S)"
proof -
  have *: "z. ((λx. if x  (λx. x $ 1) ` S then (f  vec) x else 0) has_integral z) {a..b}  norm (z - y) < e"
    if int: "a b. ball 0 B  cbox a b 
                    (z. ((λx. if x  S then f x else 0) has_integral z) (cbox a b)  norm (z - y) < e)"
      and B: "ball 0 B  {a..b}" for e B a b
  proof -
    have [simp]: "(yS. x = y $ 1)  vec x  S" for x
      by force
    have B': "ball (0::real^1) B  cbox (vec a) (vec b)"
      using B by (simp add: Basis_vec_def cart_eq_inner_axis [symmetric] mem_box norm_real subset_iff)
    show ?thesis
      using int [OF B'] by (auto simp: image_iff o_def cong: if_cong dest!: has_integral_vec1_I_cbox)
  qed
  show ?thesis
    using assms
    apply (subst has_integral_alt)
    apply (subst (asm) has_integral_alt)
    apply (simp add: has_integral_vec1_I_cbox split: if_split_asm)
    subgoal by (metis vector_one_nth)
    subgoal
      apply (erule all_forward imp_forward ex_forward asm_rl)+
      by (blast intro!: *)+
    done
qed

lemma has_integral_vec1_nth_cbox:
  fixes f :: "real  'a::real_normed_vector"
  assumes "(f has_integral y) {a..b}"
  shows "((λx::real^1. f(x$1)) has_integral y) (cbox (vec a) (vec b))"
proof -
  have "((λx::real^1. f(x$1)) has_integral (1 / 1) *R y) (vec ` cbox a b)"
  proof (rule has_integral_twiddle)
    show "w z::real. (λx. x $ 1) ` cbox u v = cbox w z"
         "content ((λx. x $ 1) ` cbox u v) = 1 * content (cbox u v)" for u v::"real^1"
      unfolding vec_cbox_1_eq by (auto simp: content_cbox_if_cart interval_eq_empty_cart)
    show "w z::real^1. vec ` cbox u v = cbox w z" for u v :: "real"
      using vec_cbox_1_eq by auto
  qed (auto simp: continuous_vec assms)
  then show ?thesis
    using vec_cbox_1_eq by auto
qed

lemma has_integral_vec1_D_cbox:
  fixes f :: "real^1  'a::real_normed_vector"
  assumes "((f  vec) has_integral y) {a$1..b$1}"
  shows "(f has_integral y) (cbox a b)"
  by (metis (mono_tags, lifting) assms comp_apply has_integral_eq has_integral_vec1_nth_cbox vector_one_nth)

lemma has_integral_vec1_D:
  fixes f :: "real^1  'a::real_normed_vector"
  assumes "((f  vec) has_integral y) ((λx. x $ 1) ` S)"
  shows "(f has_integral y) S"
proof -
  have *: "z. ((λx. if x  S then f x else 0) has_integral z) (cbox a b)  norm (z - y) < e"
    if int: "a b. ball 0 B  {a..b} 
                             (z. ((λx. if x  (λx. x $ 1) ` S then (f  vec) x else 0) has_integral z) {a..b}  norm (z - y) < e)"
      and B: "ball 0 B  cbox a b" for e B and a b::"real^1"
  proof -
    have B': "ball 0 B  {a$1..b$1}"
    proof (clarsimp)
      fix t
      assume "¦t¦ < B" then show "a $ 1  t  t  b $ 1"
        using subsetD [OF B]
        by (metis (mono_tags, opaque_lifting) mem_ball_0 mem_box_cart(2) norm_real vec_component)
    qed
    have eq: "(λx. if vec x  S then f (vec x) else 0) = (λx. if x  S then f x else 0)  vec"
      by force
    have [simp]: "(yS. x = y $ 1)  vec x  S" for x
      by force
    show ?thesis
      using int [OF B'] by (auto simp: image_iff eq cong: if_cong dest!: has_integral_vec1_D_cbox)
qed
  show ?thesis
    using assms
    apply (subst has_integral_alt)
    apply (subst (asm) has_integral_alt)
    apply (simp add: has_integral_vec1_D_cbox eq_cbox split: if_split_asm, blast)
    apply (intro conjI impI)
    subgoal by (metis vector_one_nth)
    apply (erule thin_rl)
    apply (erule all_forward ex_forward conj_forward)+
      by (blast intro!: *)+
qed


lemma integral_vec1_eq:
  fixes f :: "real^1  'a::real_normed_vector"
  shows "integral S f = integral ((λx. x $ 1) ` S) (f  vec)"
  using has_integral_vec1_I [of f] has_integral_vec1_D [of f]
  by (metis has_integral_iff not_integrable_integral)

lemma absolutely_integrable_drop:
  fixes f :: "real^1  'b::euclidean_space"
  shows "f absolutely_integrable_on S  (f  vec) absolutely_integrable_on (λx. x $ 1) ` S"
  unfolding absolutely_integrable_on_def integrable_on_def
proof safe
  fix y r
  assume "(f has_integral y) S" "((λx. norm (f x)) has_integral r) S"
  then show "y. (f  vec has_integral y) ((λx. x $ 1) ` S)"
            "y. ((λx. norm ((f  vec) x)) has_integral y) ((λx. x $ 1) ` S)"
    by (force simp: o_def dest!: has_integral_vec1_I)+
next
  fix y :: "'b" and r :: "real"
  assume "(f  vec has_integral y) ((λx. x $ 1) ` S)"
         "((λx. norm ((f  vec) x)) has_integral r) ((λx. x $ 1) ` S)"
  then show "y. (f has_integral y) S"  "y. ((λx. norm (f x)) has_integral y) S"
    by (force simp: o_def intro: has_integral_vec1_D)+
qed

subsection ‹Dominated convergence›

lemma dominated_convergence:
  fixes f :: "nat  'n::euclidean_space  'm::euclidean_space"
  assumes f: "k. (f k) integrable_on S" and h: "h integrable_on S"
    and le: "k x. x  S  norm (f k x)  h x"
    and conv: "x. x  S  (λk. f k x)  g x"
  shows "g integrable_on S" "(λk. integral S (f k))  integral S g"
proof -
  have 3: "h absolutely_integrable_on S"
    unfolding absolutely_integrable_on_def
  proof
    show "(λx. norm (h x)) integrable_on S"
    proof (intro integrable_spike_finite[OF _ _ h, of "{}"] ballI)
      fix x assume "x  S - {}" then show "norm (h x) = h x"
        by (metis Diff_empty abs_of_nonneg bot_set_def le norm_ge_zero order_trans real_norm_def)
    qed auto
  qed fact
  have 2: "set_borel_measurable lebesgue S (f k)" for k
    unfolding set_borel_measurable_def
    using f by (auto intro: has_integral_implies_lebesgue_measurable simp: integrable_on_def)
  then have 1: "set_borel_measurable lebesgue S g"
    unfolding set_borel_measurable_def
    by (rule borel_measurable_LIMSEQ_metric) (use conv in auto split: split_indicator)
  have 4: "AE x in lebesgue. (λi. indicator S x *R f i x)  indicator S x *R g x"
    "AE x in lebesgue. norm (indicator S x *R f k x)  indicator S x *R h x" for k
    using conv le by (auto intro!: always_eventually split: split_indicator)
  have g: "g absolutely_integrable_on S"
    using 1 2 3 4 unfolding set_borel_measurable_def set_integrable_def
    by (rule integrable_dominated_convergence)
  then show "g integrable_on S"
    by (auto simp: absolutely_integrable_on_def)
  have "(λk. (LINT x:S|lebesgue. f k x))  (LINT x:S|lebesgue. g x)"
    unfolding set_borel_measurable_def set_lebesgue_integral_def
    using 1 2 3 4 unfolding set_borel_measurable_def set_lebesgue_integral_def set_integrable_def
    by (rule integral_dominated_convergence)
  then show "(λk. integral S (f k))  integral S g"
    using g absolutely_integrable_integrable_bound[OF le f h]
    by (subst (asm) (1 2) set_lebesgue_integral_eq_integral) auto
qed

lemma has_integral_dominated_convergence:
  fixes f :: "nat  'n::euclidean_space  'm::euclidean_space"
  assumes "k. (f k has_integral y k) S" "h integrable_on S"
    "k. xS. norm (f k x)  h x" "xS. (λk. f k x)  g x"
    and x: "y  x"
  shows "(g has_integral x) S"
proof -
  have int_f: "k. (f k) integrable_on S"
    using assms by (auto simp: integrable_on_def)
  have "(g has_integral (integral S g)) S"
    by (metis assms(2-4) dominated_convergence(1) has_integral_integral int_f)
  moreover have "integral S g = x"
  proof (rule LIMSEQ_unique)
    show "(λi. integral S (f i))  x"
      using integral_unique[OF assms(1)] x by simp
    show "(λi. integral S (f i))  integral S g"
      by (metis assms(2) assms(3) assms(4) dominated_convergence(2) int_f)
  qed
  ultimately show ?thesis
    by simp
qed

lemma dominated_convergence_integrable_1:
  fixes f :: "nat  'n::euclidean_space  real"
  assumes f: "k. f k absolutely_integrable_on S"
    and h: "h integrable_on S"
    and normg: "x. x  S  norm(g x)  (h x)"
    and lim: "x. x  S  (λk. f k x)  g x"
 shows "g integrable_on S"
proof -
  have habs: "h absolutely_integrable_on S"
    using h normg nonnegative_absolutely_integrable_1 norm_ge_zero order_trans by blast
  let ?f = "λn x. (min (max (- h x) (f n x)) (h x))"
  have h0: "h x  0" if "x  S" for x
    using normg that by force
  have leh: "norm (?f k x)  h x" if "x  S" for k x
    using h0 that by force
  have limf: "(λk. ?f k x)  g x" if "x  S" for x
  proof -
    have "e y. ¦f y x - g x¦ < e  ¦min (max (- h x) (f y x)) (h x) - g x¦ < e"
      using h0 [OF that] normg [OF that] by simp
    then show ?thesis
      using lim [OF that] by (auto simp add: tendsto_iff dist_norm elim!: eventually_mono)
  qed
  show ?thesis
  proof (rule dominated_convergence [of ?f S h g])
    have "(λx. - h x) absolutely_integrable_on S"
      using habs unfolding set_integrable_def by auto
    then show "?f k integrable_on S" for k
      by (intro set_lebesgue_integral_eq_integral absolutely_integrable_min_1 absolutely_integrable_max_1 f habs)
  qed (use assms leh limf in auto)
qed

lemma dominated_convergence_integrable:
  fixes f :: "nat  'n::euclidean_space  'm::euclidean_space"
  assumes f: "k. f k absolutely_integrable_on S"
    and h: "h integrable_on S"
    and normg: "x. x  S  norm(g x)  (h x)"
    and lim: "x. x  S  (λk. f k x)  g x"
  shows "g integrable_on S"
  using f
  unfolding integrable_componentwise_iff [of g] absolutely_integrable_componentwise_iff [where f = "f k" for k]
proof clarify
  fix b :: "'m"
  assume fb [rule_format]: "k. bBasis. (λx. f k x  b) absolutely_integrable_on S" and b: "b  Basis"
  show "(λx. g x  b) integrable_on S"
  proof (rule dominated_convergence_integrable_1 [OF fb h])
    fix x
    assume "x  S"
    show "norm (g x  b)  h x"
      using norm_nth_le x  S b normg order.trans by blast
    show "(λk. f k x  b)  g x  b"
      using x  S b lim tendsto_componentwise_iff by fastforce
  qed (use b in auto)
qed

lemma dominated_convergence_absolutely_integrable:
  fixes f :: "nat  'n::euclidean_space  'm::euclidean_space"
  assumes f: "k. f k absolutely_integrable_on S"
    and h: "h integrable_on S"
    and normg: "x. x  S  norm(g x)  (h x)"
    and lim: "x. x  S  (λk. f k x)  g x"
  shows "g absolutely_integrable_on S"
proof -
  have "g integrable_on S"
    by (rule dominated_convergence_integrable [OF assms])
  with assms show ?thesis
    by (blast intro:  absolutely_integrable_integrable_bound [where g=h])
qed


proposition integral_countable_UN:
  fixes f :: "real^'m  real^'n"
  assumes f: "f absolutely_integrable_on ((range s))"
    and s: "m. s m  sets lebesgue"
  shows "n. f absolutely_integrable_on (mn. s m)"
    and "(λn. integral (mn. s m) f)  integral ((s ` UNIV)) f" (is "?F  ?I")
proof -
  show fU: "f absolutely_integrable_on (mn. s m)" for n
    using assms by (blast intro: set_integrable_subset [OF f])
  have fint: "f integrable_on ( (range s))"
    using absolutely_integrable_on_def f by blast
  let ?h = "λx. if x  (s ` UNIV) then norm(f x) else 0"
  have "(λn. integral UNIV (λx. if x  (mn. s m) then f x else 0))
         integral UNIV (λx. if x  (s ` UNIV) then f x else 0)"
  proof (rule dominated_convergence)
    show "(λx. if x  (mn. s m) then f x else 0) integrable_on UNIV" for n
      unfolding integrable_restrict_UNIV
      using fU absolutely_integrable_on_def by blast
    show "(λx. if x  (s ` UNIV) then norm(f x) else 0) integrable_on UNIV"
      by (metis (no_types) absolutely_integrable_on_def f integrable_restrict_UNIV)
    show "x. (λn. if x  (mn. s m) then f x else 0)
          (if x  (s ` UNIV) then f x else 0)"
      by (force intro: tendsto_eventually eventually_sequentiallyI)
  qed auto
  then show "?F  ?I"
    by (simp only: integral_restrict_UNIV)
qed


subsection ‹Fundamental Theorem of Calculus for the Lebesgue integral›

text ‹

For the positive integral we replace continuity with Borel-measurability.

›

lemma
  fixes f :: "real  real"
  assumes [measurable]: "f  borel_measurable borel"
  assumes f: "x. x  {a..b}  DERIV F x :> f x" "x. x  {a..b}  0  f x" and "a  b"
  shows nn_integral_FTC_Icc: "(+x. ennreal (f x) * indicator {a .. b} x lborel) = F b - F a" (is ?nn)
    and has_bochner_integral_FTC_Icc_nonneg:
      "has_bochner_integral lborel (λx. f x * indicator {a .. b} x) (F b - F a)" (is ?has)
    and integral_FTC_Icc_nonneg: "(x. f x * indicator {a .. b} x lborel) = F b - F a" (is ?eq)
    and integrable_FTC_Icc_nonneg: "integrable lborel (λx. f x * indicator {a .. b} x)" (is ?int)
proof -
  have *: "(λx. f x * indicator {a..b} x)  borel_measurable borel" "x. 0  f x * indicator {a..b} x"
    using f(2) by (auto split: split_indicator)

  have F_mono: "a  x  x  y  y  b F x  F y" for x y
    using f by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)

  have "(f has_integral F b - F a) {a..b}"
    by (intro fundamental_theorem_of_calculus)
       (auto simp: has_real_derivative_iff_has_vector_derivative[symmetric]
             intro: has_field_derivative_subset[OF f(1)] a  b)
  then have i: "((λx. f x * indicator {a .. b} x) has_integral F b - F a) UNIV"
    unfolding indicator_def of_bool_def if_distrib[where f="λx. a * x" for a]
    by (simp cong del: if_weak_cong del: atLeastAtMost_iff)
  then have nn: "(+x. f x * indicator {a .. b} x lborel) = F b - F a"
    by (rule nn_integral_has_integral_lborel[OF *])
  then show ?has
    by (rule has_bochner_integral_nn_integral[rotated 3]) (simp_all add: * F_mono a  b)
  then show ?eq ?int
    unfolding has_bochner_integral_iff by auto
  show ?nn
    by (subst nn[symmetric])
       (auto intro!: nn_integral_cong simp add: ennreal_mult f split: split_indicator)
qed

lemma
  fixes f :: "real  'a :: euclidean_space"
  assumes "a  b"
  assumes "x. a  x  x  b  (F has_vector_derivative f x) (at x within {a .. b})"
  assumes cont: "continuous_on {a .. b} f"
  shows has_bochner_integral_FTC_Icc:
      "has_bochner_integral lborel (λx. indicator {a .. b} x *R f x) (F b - F a)" (is ?has)
    and integral_FTC_Icc: "(x. indicator {a .. b} x *R f x lborel) = F b - F a" (is ?eq)
proof -
  let ?f = "λx. indicator {a .. b} x *R f x"
  have int: "integrable lborel ?f"
    using borel_integrable_compact[OF _ cont] by auto
  have "(f has_integral F b - F a) {a..b}"
    using assms(1,2) by (intro fundamental_theorem_of_calculus) auto
  moreover
  have "(f has_integral integralL lborel ?f) {a..b}"
    using has_integral_integral_lborel[OF int]
    unfolding indicator_def of_bool_def if_distrib[where f="λx. x *R a" for a]
    by (simp cong del: if_weak_cong del: atLeastAtMost_iff)
  ultimately show ?eq
    by (auto dest: has_integral_unique)
  then show ?has
    using int by (auto simp: has_bochner_integral_iff)
qed

lemma
  fixes f :: "real  real"
  assumes "a  b"
  assumes deriv: "x. a  x  x  b  DERIV F x :> f x"
  assumes cont: "x. a  x  x  b  isCont f x"
  shows has_bochner_integral_FTC_Icc_real:
      "has_bochner_integral lborel (λx. f x * indicator {a .. b} x) (F b - F a)" (is ?has)
    and integral_FTC_Icc_real: "(x. f x * indicator {a .. b} x lborel) = F b - F a" (is ?eq)
proof -
  have 1: "x. a  x  x  b  (F has_vector_derivative f x) (at x within {a .. b})"
    unfolding has_real_derivative_iff_has_vector_derivative[symmetric]
    using deriv by (auto intro: DERIV_subset)
  have 2: "continuous_on {a .. b} f"
    using cont by (intro continuous_at_imp_continuous_on) auto
  show ?has ?eq
    using has_bochner_integral_FTC_Icc[OF a  b 1 2] integral_FTC_Icc[OF a  b 1 2]
    by (auto simp: mult.commute)
qed

lemma nn_integral_FTC_atLeast:
  fixes f :: "real  real"
  assumes f_borel: "f  borel_measurable borel"
  assumes f: "x. a  x  DERIV F x :> f x"
  assumes nonneg: "x. a  x  0  f x"
  assumes lim: "(F  T) at_top"
  shows "(+x. ennreal (f x) * indicator {a ..} x lborel) = T - F a"
proof -
  let ?f = "λ(i::nat) (x::real). ennreal (f x) * indicator {a..a + real i} x"
  let ?fR = "λx. ennreal (f x) * indicator {a ..} x"

  have F_mono: "a  x  x  y  F x  F y" for x y
    using f nonneg by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
  then have F_le_T: "a  x  F x  T" for x
    by (intro tendsto_lowerbound[OF lim])
       (auto simp: eventually_at_top_linorder)

  have "(SUP i. ?f i x) = ?fR x" for x
  proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
    obtain n where "x - a < real n"
      using reals_Archimedean2[of "x - a"] ..
    then have "eventually (λn. ?f n x = ?fR x) sequentially"
      by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator)
    then show "(λn. ?f n x)  ?fR x"
      by (rule tendsto_eventually)
  qed (auto simp: nonneg incseq_def le_fun_def split: split_indicator)
  then have "integralN lborel ?fR = (+ x. (SUP i. ?f i x) lborel)"
    by simp
  also have " = (SUP i. (+ x. ?f i x lborel))"
  proof (rule nn_integral_monotone_convergence_SUP)
    show "incseq ?f"
      using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator)
    show "i. (?f i)  borel_measurable lborel"
      using f_borel by auto
  qed
  also have " = (SUP i. ennreal (F (a + real i) - F a))"
    by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto
  also have " = T - F a"
  proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
     have "(λx. F (a + real x))  T"
       by (auto intro: filterlim_compose[OF lim filterlim_tendsto_add_at_top] filterlim_real_sequentially)
    then show "(λn. ennreal (F (a + real n) - F a))  ennreal (T - F a)"
      by (simp add: F_mono F_le_T tendsto_diff)
  qed (auto simp: incseq_def intro!: ennreal_le_iff[THEN iffD2] F_mono)
  finally show ?thesis .
qed

lemma integral_power:
  "a  b  (x. x^k * indicator {a..b} x lborel) = (b^Suc k - a^Suc k) / Suc k"
proof (subst integral_FTC_Icc_real)
  fix x show "DERIV (λx. x^Suc k / Suc k) x :> x^k"
    by (intro derivative_eq_intros) auto
qed (auto simp: field_simps simp del: of_nat_Suc)

subsection ‹Integration by parts›

lemma integral_by_parts_integrable:
  fixes f g F G::"real  real"
  assumes "a  b"
  assumes cont_f[intro]: "!!x. a x  xb  isCont f x"
  assumes cont_g[intro]: "!!x. a x  xb  isCont g x"
  assumes [intro]: "!!x. DERIV F x :> f x"
  assumes [intro]: "!!x. DERIV G x :> g x"
  shows  "integrable lborel (λx.((F x) * (g x) + (f x) * (G x)) * indicator {a .. b} x)"
  by (auto intro!: borel_integrable_atLeastAtMost continuous_intros) (auto intro!: DERIV_isCont)

lemma integral_by_parts:
  fixes f g F G::"real  real"
  assumes [arith]: "a  b"
  assumes cont_f[intro]: "!!x. a x  xb  isCont f x"
  assumes cont_g[intro]: "!!x. a x  xb  isCont g x"
  assumes [intro]: "!!x. DERIV F x :> f x"
  assumes [intro]: "!!x. DERIV G x :> g x"
  shows "(x. (F x * g x) * indicator {a .. b} x lborel)
            =  F b * G b - F a * G a - x. (f x * G x) * indicator {a .. b} x lborel"
proof-
  have "(x. (F x * g x + f x * G x) * indicator {a .. b} x lborel) 
      = (LBINT x. F x * g x * indicat_real {a..b} x + f x * G x * indicat_real {a..b} x)"
    by (meson vector_space_over_itself.scale_left_distrib)
  also have "... = (x. (F x * g x) * indicator {a .. b} x lborel) + x. (f x * G x) * indicator {a .. b} x lborel"
  proof (intro Bochner_Integration.integral_add borel_integrable_atLeastAtMost cont_f cont_g continuous_intros)
    show "x. a  x; x  b  isCont F x" "x. a  x; x  b  isCont G x"
      using DERIV_isCont by blast+
  qed
  finally have "(x. (F x * g x + f x * G x) * indicator {a .. b} x lborel) =
                (x. (F x * g x) * indicator {a .. b} x lborel) + x. (f x * G x) * indicator {a .. b} x lborel" .
  moreover have "(x. (F x * g x + f x * G x) * indicator {a .. b} x lborel) = F b * G b - F a * G a"
  proof (intro integral_FTC_Icc_real derivative_eq_intros cont_f cont_g continuous_intros)
    show "x. a  x; x  b  isCont F x" "x. a  x; x  b  isCont G x"
      using DERIV_isCont by blast+
  qed auto
  ultimately show ?thesis by auto
qed

lemma integral_by_parts':
  fixes f g F G::"real  real"
  assumes "a  b"
  assumes "!!x. a x  xb  isCont f x"
  assumes "!!x. a x  xb  isCont g x"
  assumes "!!x. DERIV F x :> f x"
  assumes "!!x. DERIV G x :> g x"
  shows "(x. indicator {a .. b} x *R (F x * g x) lborel)
            =  F b * G b - F a * G a - x. indicator {a .. b} x *R (f x * G x) lborel"
  using integral_by_parts[OF assms] by (simp add: ac_simps)

lemma has_bochner_integral_even_function:
  fixes f :: "real  'a :: {banach, second_countable_topology}"
  assumes f: "has_bochner_integral lborel (λx. indicator {0..} x *R f x) x"
  assumes even: "x. f (- x) = f x"
  shows "has_bochner_integral lborel f (2 *R x)"
proof -
  have indicator: "x::real. indicator {..0} (- x) = indicator {0..} x"
    by (auto split: split_indicator)
  have "has_bochner_integral lborel (λx. indicator {.. 0} x *R f x) x"
    by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
       (auto simp: indicator even f)
  with f have "has_bochner_integral lborel (λx. indicator {0..} x *R f x + indicator {.. 0} x *R f x) (x + x)"
    by (rule has_bochner_integral_add)
  then have "has_bochner_integral lborel f (x + x)"
    by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
       (auto split: split_indicator)
  then show ?thesis
    by (simp add: scaleR_2)
qed

lemma has_bochner_integral_odd_function:
  fixes f :: "real  'a :: {banach, second_countable_topology}"
  assumes f: "has_bochner_integral lborel (λx. indicator {0..} x *R f x) x"
  assumes odd: "x. f (- x) = - f x"
  shows "has_bochner_integral lborel f 0"
proof -
  have indicator: "x::real. indicator {..0} (- x) = indicator {0..} x"
    by (auto split: split_indicator)
  have "has_bochner_integral lborel (λx. - indicator {.. 0} x *R f x) x"
    by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
       (auto simp: indicator odd f)
  from has_bochner_integral_minus[OF this]
  have "has_bochner_integral lborel (λx. indicator {.. 0} x *R f x) (- x)"
    by simp
  with f have "has_bochner_integral lborel (λx. indicator {0..} x *R f x + indicator {.. 0} x *R f x) (x + - x)"
    by (rule has_bochner_integral_add)
  then have "has_bochner_integral lborel f (x + - x)"
    by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
       (auto split: split_indicator)
  then show ?thesis
    by simp
qed

subsection ‹A non-negative continuous function whose integral is zero must be zero›

lemma has_integral_0_closure_imp_0:
  fixes f :: "'a::euclidean_space  real"
  assumes f: "continuous_on (closure S) f"
    and nonneg_interior: "x. x  S  0  f x"
    and pos: "0 < emeasure lborel S"
    and finite: "emeasure lborel S < "
    and regular: "emeasure lborel (closure S) = emeasure lborel S"
    and opn: "open S"
  assumes int: "(f has_integral 0) (closure S)"
  assumes x: "x  closure S"
  shows "f x = 0"
proof -
  have zero: "emeasure lborel (frontier S) = 0"
    using finite closure_subset regular
    unfolding frontier_def
    by (subst emeasure_Diff) (auto simp: frontier_def interior_open open S )
  have nonneg: "0  f x" if "x  closure S" for x
    using continuous_ge_on_closure[OF f that nonneg_interior] by simp
  have "0 = integral (closure S) f"
    by (blast intro: int sym)
  also
  note intl = has_integral_integrable[OF int]
  have af: "f absolutely_integrable_on (closure S)"
    using nonneg
    by (intro absolutely_integrable_onI intl integrable_eq[OF intl]) simp
  then have "integral (closure S) f = set_lebesgue_integral lebesgue (closure S) f"
    by (intro set_lebesgue_integral_eq_integral(2)[symmetric])
  also have " = 0  (AE x in lebesgue. indicator (closure S) x *R f x = 0)"
    unfolding set_lebesgue_integral_def
  proof (rule integral_nonneg_eq_0_iff_AE)
    show "integrable lebesgue (λx. indicat_real (closure S) x *R f x)"
      by (metis af set_integrable_def)
  qed (use nonneg in auto simp: indicator_def)
  also have "  (AE x in lebesgue. x  {x. x  closure S  f x = 0})"
    by (auto simp: indicator_def)
  finally have "(AE x in lebesgue. x  {x. x  closure S  f x = 0})" by simp
  moreover have "(AE x in lebesgue. x  - frontier S)"
    using zero
    by (auto simp: eventually_ae_filter null_sets_def intro!: exI[where x="frontier S"])
  ultimately have ae: "AE x  S in lebesgue. x  {x  closure S. f x = 0}" (is ?th)
    by eventually_elim (use closure_subset in auto simp:)
  have "closed {0::real}" by simp
  with continuous_on_closed_vimage[OF closed_closure, of S f] f
  have "closed (f -` {0}  closure S)" by blast
  then have "closed {x  closure S. f x = 0}" by (auto simp: vimage_def Int_def conj_commute)
  with open S have "x  {x  closure S. f x = 0}" if "x  S" for x using ae that
    by (rule mem_closed_if_AE_lebesgue_open)
  then have "f x = 0" if "x  S" for x using that by auto
  from continuous_constant_on_closure[OF f this x  closure S]
  show "f x = 0" .
qed

lemma has_integral_0_cbox_imp_0:
  fixes f :: "'a::euclidean_space  real"
  assumes "continuous_on (cbox a b) f" and "x. x  box a b  0  f x"
  assumes "(f has_integral 0) (cbox a b)"
  assumes ne: "box a b  {}"
  assumes x: "x  cbox a b"
  shows "f x = 0"
proof -
  have "0 < emeasure lborel (box a b)"
    using ne x unfolding emeasure_lborel_box_eq
    by (force intro!: prod_pos simp: mem_box algebra_simps)
  then show ?thesis using assms
    by (intro has_integral_0_closure_imp_0[of "box a b" f x])
      (auto simp: emeasure_lborel_box_eq emeasure_lborel_cbox_eq algebra_simps mem_box)
qed

corollary integral_cbox_eq_0_iff:
  fixes f :: "'a::euclidean_space  real"
  assumes "continuous_on (cbox a b) f" and "box a b  {}"
    and "x. x  cbox a b  f x  0"
  shows "integral (cbox a b) f = 0  (x  cbox a b. f x = 0)" (is "?lhs = ?rhs")
proof
  assume int0: ?lhs
  show ?rhs
    using has_integral_0_cbox_imp_0 [of a b f] assms
    by (metis box_subset_cbox eq_integralD int0 integrable_continuous subsetD) 
next
  assume ?rhs then show ?lhs
    by (meson has_integral_is_0_cbox integral_unique)
qed

lemma integral_eq_0_iff:
  fixes f :: "real  real"
  assumes "continuous_on {a..b} f" and "a < b"
    and "x. x  {a..b}  f x  0"
  shows "integral {a..b} f = 0  (x  {a..b}. f x = 0)" 
  using integral_cbox_eq_0_iff [of a b f] assms by simp

lemma integralL_eq_0_iff:
  fixes f :: "real  real"
  assumes contf: "continuous_on {a..b} f" and "a < b"
    and "x. x  {a..b}  f x  0"
  shows "integralL (lebesgue_on {a..b}) f = 0  (x  {a..b}. f x = 0)" 
  using integral_eq_0_iff [OF assms]
  by (simp add: contf continuous_imp_integrable_real lebesgue_integral_eq_integral)

text ‹In fact, strict inequality is required only at a single point within the box.›
lemma integral_less:
  fixes f :: "'n::euclidean_space  real"
  assumes cont: "continuous_on (cbox a b) f" "continuous_on (cbox a b) g" and "box a b  {}"
    and fg: "x. x  box a b  f x < g x"
  shows "integral (cbox a b) f < integral (cbox a b) g"
proof -
  obtain int: "f integrable_on (cbox a b)" "g integrable_on (cbox a b)"
    using cont integrable_continuous by blast
  then have "integral (cbox a b) f  integral (cbox a b) g"
    by (metis fg integrable_on_open_interval integral_le integral_open_interval less_eq_real_def)
  moreover have "integral (cbox a b) f  integral (cbox a b) g"
  proof (rule ccontr)
    assume "¬ integral (cbox a b) f  integral (cbox a b) g"
    then have 0: "((λx. g x - f x) has_integral 0) (cbox a b)"
      by (metis (full_types) cancel_comm_monoid_add_class.diff_cancel has_integral_diff int integrable_integral)
    have cgf: "continuous_on (cbox a b) (λx. g x - f x)"
      using cont continuous_on_diff by blast
    show False
      using has_integral_0_cbox_imp_0 [OF cgf _ 0] assms(3) box_subset_cbox fg less_eq_real_def by fastforce
  qed
  ultimately show ?thesis
    by linarith
qed

lemma integral_less_real:
  fixes f :: "real  real"
  assumes "continuous_on {a..b} f" "continuous_on {a..b} g" and "{a<..<b}  {}"
    and "x. x  {a<..<b}  f x < g x"
  shows "integral {a..b} f < integral {a..b} g"
  by (metis assms box_real integral_less)

subsection‹Various common equivalent forms of function measurability›

lemma indicator_sum_eq:
  fixes m::real and f :: "'a  real"
  assumes "¦m¦  2 ^ (2*n)" "m/2^n  f x" "f x < (m+1)/2^n" "m  "
  shows   "(k::real | k    ¦k¦  2 ^ (2*n).
            k/2^n * indicator {y. k/2^n  f y  f y < (k+1)/2^n} x)  = m/2^n"
          (is "sum ?f ?S = _")
proof -
  have "sum ?f ?S = sum (λk. k/2^n * indicator {y. k/2^n  f y  f y < (k+1)/2^n} x) {m}"
  proof (rule comm_monoid_add_class.sum.mono_neutral_right)
    show "finite ?S"
      by (rule finite_abs_int_segment)
    show "{m}  {k  . ¦k¦  2 ^ (2*n)}"
      using assms by auto
    show "i{k  . ¦k¦  2 ^ (2*n)} - {m}. ?f i = 0"
      using assms by (auto simp: indicator_def Ints_def abs_le_iff field_split_simps)
  qed
  also have " = m/2^n"
    using assms by (auto simp: indicator_def not_less)
  finally show ?thesis .
qed

lemma measurable_on_sf_limit_lemma1:
  fixes f :: "'a::euclidean_space  real"
  assumes "a b. {x  S. a  f x  f x < b}  sets (lebesgue_on S)"
  obtains g where "n. g n  borel_measurable (lebesgue_on S)"
                  "n. finite(range (g n))"
                  "x. (λn. g n x)  f x"
proof
  show "(λx. sum (λk::real. k/2^n * indicator {y. k/2^n  f y  f y < (k+1)/2^n} x)
                 {k  . ¦k¦  2 ^ (2*n)})  borel_measurable (lebesgue_on S)"
        (is "?g  _")  for n
  proof -
    have "k. k  ; ¦k¦  2 ^ (2*n)
          Measurable.pred (lebesgue_on S) (λx. k / (2^n)  f x  f x < (k+1) / (2^n))"
      using assms by (force simp: pred_def space_restrict_space)
    then show ?thesis
      by (simp add: field_class.field_divide_inverse)
  qed
  show "finite (range (?g n))" for n
  proof -
    have "range (?g n)  (λk. k/2^n) ` {k  . ¦k¦  2 ^ (2*n)}"
    proof clarify
      fix x
      show "?g n x   (λk. k/2^n) ` {k  . ¦k¦  2 ^ (2*n)}"
      proof (cases "k::real. k    ¦k¦  2 ^ (2*n)  k/2^n  (f x)  (f x) < (k+1)/2^n")
        case True
        then show ?thesis
          apply clarify
          by (subst indicator_sum_eq) auto
      next
        case False
        then have "?g n x = 0" by auto
        then show ?thesis by force
      qed
    qed
    moreover have "finite ((λk::real. (k/2^n)) ` {k  . ¦k¦  2 ^ (2*n)})"
      by (simp add: finite_abs_int_segment)
    ultimately show ?thesis
      using finite_subset by blast
  qed
  show "(λn. ?g n x)  f x" for x
  proof (rule LIMSEQ_I)
    fix e::real
    assume "e > 0"
    obtain N1 where N1: "¦f x¦ < 2 ^ N1"
      using real_arch_pow by fastforce
    obtain N2 where N2: "(1/2) ^ N2 < e"
      using real_arch_pow_inv e > 0 by force
    have "norm (?g n x - f x) < e" if n: "n  max N1 N2" for n
    proof -
      define m where "m  floor(2^n * (f x))"
      have "1  ¦2^n¦ * e"
        using n N2 e > 0 less_eq_real_def less_le_trans by (fastforce simp add: field_split_simps)
      then have *: "x  y; y < x + 1  abs(x - y) < ¦2^n¦ * e" for x y::real
        by linarith
      have "¦2^n¦ * ¦m/2^n - f x¦ = ¦2^n * (m/2^n - f x)¦"
        by (simp add: abs_mult)
      also have " = ¦real_of_int 2^n * f x - f x * 2^n¦"
        by (simp add: algebra_simps m_def)
      also have " < ¦2^n¦ * e"
        by (rule *; simp add: mult.commute)
      finally have "¦2^n¦ * ¦m/2^n - f x¦ < ¦2^n¦ * e" .
      then have me: "¦m/2^n - f x¦ < e"
        by simp
      have "¦real_of_int m¦  2 ^ (2*n)"
      proof (cases "f x < 0")
        case True
        then have "-f x  (2::real) ^ N1"
          using N1 le_floor_iff minus_le_iff by fastforce
        with n True have "¦real_of_intf x¦  2 ^ N1"
          by linarith
        also have "  2^n"
          using n by (simp add: m_def)
        finally have "¦real_of_int f x¦ * 2^n  2^n * 2^n"
          by simp
        moreover
        have "¦real_of_int 2^n * f x¦  ¦real_of_int f x¦ * 2^n"
        proof -
          have "¦real_of_int 2^n * f x¦ = - (real_of_int 2^n * f x)"
            using True by (simp add: abs_if mult_less_0_iff)
          also have "  - (real_of_int ((2::real) ^ n * f x))"
            using le_mult_floor_Ints [of "(2::real)^n"] by simp
          also have "  ¦real_of_int f x¦ * 2^n"
            using True
            by simp
          finally show ?thesis .
        qed
        ultimately show ?thesis
          by (metis (no_types, opaque_lifting) m_def order_trans power2_eq_square power_even_eq)
      next
        case False
        with n N1 have "f x  2^n"
          by (simp add: not_less) (meson less_eq_real_def one_le_numeral order_trans power_increasing)
        moreover have "0  m"
          using False m_def by force
        ultimately show ?thesis
          by (metis abs_of_nonneg floor_mono le_floor_iff m_def of_int_0_le_iff power2_eq_square power_mult mult_le_cancel_right_pos zero_less_numeral mult.commute zero_less_power)
      qed
      then have "?g n x = m/2^n"
        by (rule indicator_sum_eq) (auto simp add: m_def field_split_simps, linarith)
      then have "norm (?g n x - f x) = norm (m/2^n - f x)"
        by simp
      also have " < e"
        by (simp add: me)
      finally show ?thesis .
    qed
    then show "no. nno. norm (?g n x - f x) < e"
      by blast
  qed
qed


lemma borel_measurable_simple_function_limit:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  shows "f  borel_measurable (lebesgue_on S) 
         (g. (n. (g n)  borel_measurable (lebesgue_on S)) 
              (n. finite (range (g n)))  (x. (λn. g n x)  f x))"
proof -
  have "g. (n. (g n)  borel_measurable (lebesgue_on S)) 
            (n. finite (range (g n)))  (x. (λn. g n x)  f x)"
       if f: "a i. i  Basis  {x  S. f x  i < a}  sets (lebesgue_on S)"
  proof -
    have "g. (n. (g n)  borel_measurable (lebesgue_on S)) 
                  (n. finite(image (g n) UNIV)) 
                  (x. ((λn. g n x)  f x  i))" if "i  Basis" for i
    proof (rule measurable_on_sf_limit_lemma1 [of S "λx. f x  i"])
      show "{x  S. a  f x  i  f x  i < b}  sets (lebesgue_on S)" for a b
      proof -
        have "{x  S. a  f x  i  f x  i < b} = {x  S. f x  i < b} - {x  S. a > f x  i}"
          by auto
        also have "  sets (lebesgue_on S)"
          using f that by blast
        finally show ?thesis .
      qed
    qed blast
    then obtain g where g:
          "i n. i  Basis  g i n  borel_measurable (lebesgue_on S)"
          "i n. i  Basis  finite(range (g i n))"
          "i x. i  Basis  ((λn. g i n x)  f x  i)"
      by metis
    show ?thesis
    proof (intro conjI allI exI)
      show "(λx. iBasis. g i n x *R i)  borel_measurable (lebesgue_on S)" for n
        by (intro borel_measurable_sum borel_measurable_scaleR) (auto intro: g)
      show "finite (range (λx. iBasis. g i n x *R i))" for n
      proof -
        have "range (λx. iBasis. g i n x *R i)  (λh. iBasis. h i *R i) ` PiE Basis (λi. range (g i n))"
        proof clarify
          fix x
          show "(iBasis. g i n x *R i)  (λh. iBasis. h i *R i) ` (ΠE iBasis. range (g i n))"
            by (rule_tac x="λiBasis. g i n x" in image_eqI) auto
        qed
        moreover have "finite(PiE Basis (λi. range (g i n)))"
          by (simp add: g finite_PiE)
        ultimately show ?thesis
          by (metis (mono_tags, lifting) finite_surj)
      qed
      show "(λn. iBasis. g i n x *R i)  f x" for x
      proof -
        have "(λn. iBasis. g i n x *R i)  (iBasis. (f x  i) *R i)"
          by (auto intro!: tendsto_sum tendsto_scaleR g)
        moreover have "(iBasis. (f x  i) *R i) = f x"
          using euclidean_representation by blast
        ultimately show ?thesis
          by metis
      qed
    qed
  qed
  moreover have "f  borel_measurable (lebesgue_on S)"
              if meas_g: "n. g n  borel_measurable (lebesgue_on S)"
                 and fin: "n. finite (range (g n))"
                 and to_f: "x. (λn. g n x)  f x" for  g
    by (rule borel_measurable_LIMSEQ_metric [OF meas_g to_f])
  ultimately show ?thesis
    using borel_measurable_vimage_halfspace_component_lt by blast
qed

subsection ‹Lebesgue sets and continuous images›

proposition lebesgue_regular_inner:
 assumes "S  sets lebesgue"
 obtains K C where "negligible K" "n::nat. compact(C n)" "S = (n. C n)  K"
proof -
  have "T. closed T  T  S  (S - T)  lmeasurable  emeasure lebesgue (S - T) < ennreal ((1/2)^n)" for n
    using sets_lebesgue_inner_closed assms
    by (metis sets_lebesgue_inner_closed zero_less_divide_1_iff zero_less_numeral zero_less_power)
  then obtain C where clo: "n. closed (C n)" and subS: "n. C n  S"
    and mea: "n. (S - C n)  lmeasurable"
    and less: "n. emeasure lebesgue (S - C n) < ennreal ((1/2)^n)"
    by metis
  have "F. (n::nat. compact(F n))  (n. F n) = C m" for m::nat
    by (metis clo closed_Union_compact_subsets)
  then obtain D :: "[nat,nat]  'a set" where D: "m n. compact(D m n)" "m. (n. D m n) = C m"
    by metis
  let ?C = "from_nat_into (m. range (D m))"
  have "countable (m. range (D m))"
    by blast
  have "range (from_nat_into (m. range (D m))) = (m. range (D m))"
    using range_from_nat_into by simp
  then have CD: "m n. ?C k = D m n"  for k
    by (metis (mono_tags, lifting) UN_iff rangeE range_eqI)
  show thesis
  proof
    show "negligible (S - (n. C n))"
    proof (clarsimp simp: negligible_outer_le)
      fix e :: "real"
      assume "e > 0"
      then obtain n where n: "(1/2)^n < e"
        using real_arch_pow_inv [of e "1/2"] by auto
      show "T. S - (n. C n)  T  T  lmeasurable  measure lebesgue T  e"
      proof (intro exI conjI)
        show "S - (n. C n)  S - C n"
          by blast
        show "S - C n  lmeasurable"
          by (simp add: mea)
        show "measure lebesgue (S - C n)  e"
          using less [of n] n
          by (simp add: emeasure_eq_measure2 less_le mea)
      qed
    qed
    show "compact (?C n)" for n
      using CD D by metis
    show "S = (n. ?C n)  (S - (n. C n))" (is "_ = ?rhs")
    proof
      show "S  ?rhs"
        using D by fastforce
      show "?rhs  S"
        using subS D CD by auto (metis Sup_upper range_eqI subsetCE)
    qed
  qed
qed

lemma sets_lebesgue_continuous_image:
  assumes T: "T  sets lebesgue" and contf: "continuous_on S f"
    and negim: "T. negligible T; T  S  negligible(f ` T)" and "T  S"
 shows "f ` T  sets lebesgue"
proof -
  obtain K C where "negligible K" and com: "n::nat. compact(C n)" and Teq: "T = (n. C n)  K"
    using lebesgue_regular_inner [OF T] by metis
  then have comf: "n::nat. compact(f ` C n)"
    by (metis Un_subset_iff Union_upper T  S compact_continuous_image contf continuous_on_subset rangeI)
  have "((n. f ` C n)  f ` K)  sets lebesgue"
  proof (rule sets.Un)
    have "K  S"
      using Teq T  S by blast
    show "(n. f ` C n)  sets lebesgue"
    proof (rule sets.countable_Union)
      show "range (λn. f ` C n)  sets lebesgue"
        using borel_compact comf by (auto simp: borel_compact)
    qed auto
    show "f ` K  sets lebesgue"
      by (simp add: K  S negligible K negim negligible_imp_sets)
  qed
  then show ?thesis
    by (simp add: Teq image_Un image_Union)
qed

lemma differentiable_image_in_sets_lebesgue:
  fixes f :: "'m::euclidean_space  'n::euclidean_space"
  assumes S: "S  sets lebesgue" and dim: "DIM('m)  DIM('n)" and f: "f differentiable_on S"
  shows "f`S  sets lebesgue"
proof (rule sets_lebesgue_continuous_image [OF S])
  show "continuous_on S f"
    by (meson differentiable_imp_continuous_on f)
  show "T. negligible T; T  S  negligible (f ` T)"
    using differentiable_on_subset f
    by (auto simp: intro!: negligible_differentiable_image_negligible [OF dim])
qed auto

lemma sets_lebesgue_on_continuous_image:
  assumes S: "S  sets lebesgue" and X: "X  sets (lebesgue_on S)" and contf: "continuous_on S f"
    and negim: "T. negligible T; T  S  negligible(f ` T)"
  shows "f ` X  sets (lebesgue_on (f ` S))"
proof -
  have "X  S"
    by (metis S X sets.Int_space_eq2 sets_restrict_space_iff)
  moreover have "f ` S  sets lebesgue"
    using S contf negim sets_lebesgue_continuous_image by blast
  moreover have "f ` X  sets lebesgue"
    by (metis S X contf negim sets_lebesgue_continuous_image sets_restrict_space_iff space_restrict_space space_restrict_space2)
  ultimately show ?thesis
    by (auto simp: sets_restrict_space_iff)
qed

lemma differentiable_image_in_sets_lebesgue_on:
  fixes f :: "'m::euclidean_space  'n::euclidean_space"
  assumes S: "S  sets lebesgue" and X: "X  sets (lebesgue_on S)" and dim: "DIM('m)  DIM('n)"
       and f: "f differentiable_on S"
     shows "f ` X  sets (lebesgue_on (f`S))"
proof (rule sets_lebesgue_on_continuous_image [OF S X])
  show "continuous_on S f"
    by (meson differentiable_imp_continuous_on f)
  show "T. negligible T; T  S  negligible (f ` T)"
    using differentiable_on_subset f
    by (auto simp: intro!: negligible_differentiable_image_negligible [OF dim])
qed

subsection ‹Affine lemmas›

lemma borel_measurable_affine:
  fixes f :: "'a :: euclidean_space  'b :: euclidean_space"
  assumes f: "f  borel_measurable lebesgue" and "c  0"
  shows "(λx. f(t + c *R x))  borel_measurable lebesgue"
proof -
  { fix a b
    have "{x. f x  cbox a b}  sets lebesgue"
      using f cbox_borel lebesgue_measurable_vimage_borel by blast
    then have "(λx. (x - t) /R c) ` {x. f x  cbox a b}  sets lebesgue"
    proof (rule differentiable_image_in_sets_lebesgue)
      show "(λx. (x - t) /R c) differentiable_on {x. f x  cbox a b}"
        unfolding differentiable_on_def differentiable_def
        by (rule c  0 derivative_eq_intros strip exI | simp)+
    qed auto
    moreover
    have "{x. f(t + c *R x)  cbox a b} = (λx. (x-t) /R c) ` {x. f x  cbox a b}"
      using c  0 by (auto simp: image_def)
    ultimately have "{x. f(t + c *R x)  cbox a b}  sets lebesgue"
      by (auto simp: borel_measurable_vimage_closed_interval) }
  then show ?thesis
    by (subst lebesgue_on_UNIV_eq [symmetric]; auto simp: borel_measurable_vimage_closed_interval)
qed
    
lemma lebesgue_integrable_real_affine:
  fixes f :: "real  'a :: euclidean_space"
  assumes f: "integrable lebesgue f" and "c  0"
  shows "integrable lebesgue (λx. f(t + c * x))"
proof -
  have "(λx. norm (f x))  borel_measurable lebesgue"
    by (simp add: borel_measurable_integrable f)
  then show ?thesis
    using assms borel_measurable_affine [of f c]
    unfolding integrable_iff_bounded
    by (subst (asm) nn_integral_real_affine_lebesgue[where c=c and t=t])  (auto simp: ennreal_mult_less_top)
qed

lemma lebesgue_integrable_real_affine_iff:
  fixes f :: "real  'a :: euclidean_space"
  shows "c  0  integrable lebesgue (λx. f(t + c * x))  integrable lebesgue f"
  using lebesgue_integrable_real_affine[of f c t]
        lebesgue_integrable_real_affine[of "λx. f(t + c * x)" "1/c" "-t/c"]
  by (auto simp: field_simps)

lemmatag important› lebesgue_integral_real_affine:
  fixes f :: "real  'a :: euclidean_space" and c :: real
  assumes c: "c  0" shows "(x. f x  lebesgue) = ¦c¦ *R (x. f(t + c * x) lebesgue)"
proof cases
  have "(λx. t + c * x)  lebesgue M lebesgue"
    using lebesgue_affine_measurable[where c= "λx::real. c"] c  0 by simp
  moreover
  assume "integrable lebesgue f"
  ultimately show ?thesis
    by (subst lebesgue_real_affine[OF c, of t]) (auto simp: integral_density integral_distr)
next
  assume "¬ integrable lebesgue f" with c show ?thesis
    by (simp add: lebesgue_integrable_real_affine_iff not_integrable_integral_eq)
qed

lemma has_bochner_integral_lebesgue_real_affine_iff:
  fixes i :: "'a :: euclidean_space"
  shows "c  0 
    has_bochner_integral lebesgue f i 
    has_bochner_integral lebesgue (λx. f(t + c * x)) (i /R ¦c¦)"
  unfolding has_bochner_integral_iff lebesgue_integrable_real_affine_iff
  by (simp_all add: lebesgue_integral_real_affine[symmetric] divideR_right cong: conj_cong)

lemma has_bochner_integral_reflect_real_lemma[intro]:
  fixes f :: "real  'a::euclidean_space"
  assumes "has_bochner_integral (lebesgue_on {a..b}) f i"
  shows "has_bochner_integral (lebesgue_on {-b..-a}) (λx. f(-x)) i"
proof -
  have eq: "indicat_real {a..b} (- x) *R f(- x) = indicat_real {- b..- a} x *R f(- x)" for x
    by (auto simp: indicator_def)
  have i: "has_bochner_integral lebesgue (λx. indicator {a..b} x *R f x) i"
    using assms by (auto simp: has_bochner_integral_restrict_space)
  then have "has_bochner_integral lebesgue (λx. indicator {-b..-a} x *R f(-x)) i"
    using has_bochner_integral_lebesgue_real_affine_iff [of "-1" "(λx. indicator {a..b} x *R f x)" i 0]
    by (auto simp: eq)
  then show ?thesis
    by (auto simp: has_bochner_integral_restrict_space)
qed

lemma has_bochner_integral_reflect_real[simp]:
  fixes f :: "real  'a::euclidean_space"
  shows "has_bochner_integral (lebesgue_on {-b..-a}) (λx. f(-x)) i  has_bochner_integral (lebesgue_on {a..b}) f i"
  by (auto simp: dest: has_bochner_integral_reflect_real_lemma)

lemma integrable_reflect_real[simp]:
  fixes f :: "real  'a::euclidean_space"
  shows "integrable (lebesgue_on {-b..-a}) (λx. f(-x))  integrable (lebesgue_on {a..b}) f"
  by (metis has_bochner_integral_iff has_bochner_integral_reflect_real)

lemma integral_reflect_real[simp]:
  fixes f :: "real  'a::euclidean_space"
  shows "integralL (lebesgue_on {-b .. -a}) (λx. f(-x)) = integralL (lebesgue_on {a..b::real}) f"
  using has_bochner_integral_reflect_real [of b a f]
  by (metis has_bochner_integral_iff not_integrable_integral_eq)

subsection‹More results on integrability›

lemma integrable_on_all_intervals_UNIV:
  fixes f :: "'a::euclidean_space  'b::banach"
  assumes intf: "a b. f integrable_on cbox a b"
    and normf: "x. norm(f x)  g x" and g: "g integrable_on UNIV"
  shows "f integrable_on UNIV"
proof -
have intg: "(a b. g integrable_on cbox a b)"
    and gle_e: "e>0. B>0. a b c d.
                    ball 0 B  cbox a b  cbox a b  cbox c d 
                    ¦integral (cbox a b) g - integral (cbox c d) g¦
                    < e"
    using g
    by (auto simp: integrable_alt_subset [of _ UNIV] intf)
  have le: "norm (integral (cbox a b) f - integral (cbox c d) f)  ¦integral (cbox a b) g - integral (cbox c d) g¦"
    if "cbox a b  cbox c d" for a b c d
  proof -
    have "norm (integral (cbox a b) f - integral (cbox c d) f) = norm (integral (cbox c d - cbox a b) f)"
      using intf that by (simp add: norm_minus_commute integral_setdiff)
    also have "  integral (cbox c d - cbox a b) g"
    proof (rule integral_norm_bound_integral [OF _ _ normf])
      show "f integrable_on cbox c d - cbox a b" "g integrable_on cbox c d - cbox a b"
        by (meson integrable_integral integrable_setdiff intf intg negligible_setdiff that)+
    qed
    also have " = integral (cbox c d) g - integral (cbox a b) g"
      using intg that by (simp add: integral_setdiff)
    also have "  ¦integral (cbox a b) g - integral (cbox c d) g¦"
      by simp
    finally show ?thesis .
  qed
  show ?thesis
    using gle_e
    apply (simp add: integrable_alt_subset [of _ UNIV] intf)
    apply (erule imp_forward all_forward ex_forward asm_rl)+
    by (meson not_less order_trans le)
qed

lemma integrable_on_all_intervals_integrable_bound:
  fixes f :: "'a::euclidean_space  'b::banach"
  assumes intf: "a b. (λx. if x  S then f x else 0) integrable_on cbox a b"
    and normf: "x. x  S  norm(f x)  g x" and g: "g integrable_on S"
  shows "f integrable_on S"
  using integrable_on_all_intervals_UNIV [OF intf, of "(λx. if x  S then g x else 0)"]
  by (simp add: g integrable_restrict_UNIV normf)

lemma measurable_bounded_lemma:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes f: "f  borel_measurable lebesgue" and g: "g integrable_on cbox a b"
    and normf: "x. x  cbox a b  norm(f x)  g x"
  shows "f integrable_on cbox a b"
proof -
  have "g absolutely_integrable_on cbox a b"
    by (metis (full_types) add_increasing g le_add_same_cancel1 nonnegative_absolutely_integrable_1 norm_ge_zero normf)
  then have "integrable (lebesgue_on (cbox a b)) g"
    by (simp add: integrable_restrict_space set_integrable_def)
  then have "integrable (lebesgue_on (cbox a b)) f"
  proof (rule Bochner_Integration.integrable_bound)
    show "AE x in lebesgue_on (cbox a b). norm (f x)  norm (g x)"
      by (rule AE_I2) (auto intro: normf order_trans)
  qed (simp add: f measurable_restrict_space1)
  then show ?thesis
    by (simp add: integrable_on_lebesgue_on)
qed

proposition measurable_bounded_by_integrable_imp_integrable:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes f: "f  borel_measurable (lebesgue_on S)" and g: "g integrable_on S"
    and normf: "x. x  S  norm(f x)  g x" and S: "S  sets lebesgue"
  shows "f integrable_on S"
proof (rule integrable_on_all_intervals_integrable_bound [OF _ normf g])
  show "(λx. if x  S then f x else 0) integrable_on cbox a b" for a b
  proof (rule measurable_bounded_lemma)
    show "(λx. if x  S then f x else 0)  borel_measurable lebesgue"
      by (simp add: S borel_measurable_if f)
    show "(λx. if x  S then g x else 0) integrable_on cbox a b"
      by (simp add: g integrable_altD(1))
    show "norm (if x  S then f x else 0)  (if x  S then g x else 0)" for x
      using normf by simp
  qed
qed

lemma measurable_bounded_by_integrable_imp_lebesgue_integrable:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes f: "f  borel_measurable (lebesgue_on S)" and g: "integrable (lebesgue_on S) g"
    and normf: "x. x  S  norm(f x)  g x" and S: "S  sets lebesgue"
  shows "integrable (lebesgue_on S) f"
proof -
  have "f absolutely_integrable_on S"
    by (metis (no_types) S absolutely_integrable_integrable_bound f g integrable_on_lebesgue_on measurable_bounded_by_integrable_imp_integrable normf)
  then show ?thesis
    by (simp add: S integrable_restrict_space set_integrable_def)
qed

lemma measurable_bounded_by_integrable_imp_integrable_real:
  fixes f :: "'a::euclidean_space  real"
  assumes "f  borel_measurable (lebesgue_on S)" "g integrable_on S" "x. x  S  abs(f x)  g x" "S  sets lebesgue"
  shows "f integrable_on S"
  using measurable_bounded_by_integrable_imp_integrable [of f S g] assms by simp

subsection‹ Relation between Borel measurability and integrability.›

lemma integrable_imp_measurable_weak:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "S  sets lebesgue" "f integrable_on S"
  shows "f  borel_measurable (lebesgue_on S)"
  by (metis (mono_tags, lifting) assms has_integral_implies_lebesgue_measurable borel_measurable_restrict_space_iff integrable_on_def sets.Int_space_eq2)

lemma integrable_imp_measurable:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "f integrable_on S"
  shows "f  borel_measurable (lebesgue_on S)"
proof -
  have "(UNIV::'a set)  sets lborel"
    by simp
  then show ?thesis
    by (metis (mono_tags, lifting) assms borel_measurable_if_D integrable_imp_measurable_weak integrable_restrict_UNIV lebesgue_on_UNIV_eq sets_lebesgue_on_refl)
qed

lemma integrable_iff_integrable_on:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "S  sets lebesgue" "(+ x. ennreal (norm (f x)) lebesgue_on S) < "
  shows "integrable (lebesgue_on S) f  f integrable_on S"
  using assms integrable_iff_bounded integrable_imp_measurable integrable_on_lebesgue_on by blast

lemma absolutely_integrable_measurable:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "S  sets lebesgue"
  shows "f absolutely_integrable_on S  f  borel_measurable (lebesgue_on S)  integrable (lebesgue_on S) (norm  f)"
    (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  then have "f  borel_measurable (lebesgue_on S)"
    by (simp add: absolutely_integrable_on_def integrable_imp_measurable)
  then show ?rhs
    using assms set_integrable_norm [of lebesgue S f] L
    by (simp add: integrable_restrict_space set_integrable_def)
next
  assume ?rhs then show ?lhs
    using assms integrable_on_lebesgue_on
    by (metis absolutely_integrable_integrable_bound comp_def eq_iff measurable_bounded_by_integrable_imp_integrable)
qed

lemma absolutely_integrable_measurable_real:
  fixes f :: "'a::euclidean_space  real"
  assumes "S  sets lebesgue"
  shows "f absolutely_integrable_on S 
         f  borel_measurable (lebesgue_on S)  integrable (lebesgue_on S) (λx. ¦f x¦)"
  by (simp add: absolutely_integrable_measurable assms o_def)

lemma absolutely_integrable_measurable_real':
  fixes f :: "'a::euclidean_space  real"
  assumes "S  sets lebesgue"
  shows "f absolutely_integrable_on S  f  borel_measurable (lebesgue_on S)  (λx. ¦f x¦) integrable_on S"
  by (metis abs_absolutely_integrableI_1 absolutely_integrable_measurable_real assms 
            measurable_bounded_by_integrable_imp_integrable order_refl real_norm_def set_integrable_abs set_lebesgue_integral_eq_integral(1))

lemma absolutely_integrable_imp_borel_measurable:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "f absolutely_integrable_on S" "S  sets lebesgue"
  shows "f  borel_measurable (lebesgue_on S)"
  using absolutely_integrable_measurable assms by blast

lemma measurable_bounded_by_integrable_imp_absolutely_integrable:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "f  borel_measurable (lebesgue_on S)" "S  sets lebesgue"
    and "g integrable_on S" and "x. x  S  norm(f x)  (g x)"
  shows "f absolutely_integrable_on S"
  using assms absolutely_integrable_integrable_bound measurable_bounded_by_integrable_imp_integrable by blast

proposition negligible_differentiable_vimage:
  fixes f :: "'a  'a::euclidean_space"
  assumes "negligible T"
    and f': "x. x  S  inj(f' x)"
    and derf: "x. x  S  (f has_derivative f' x) (at x within S)"
  shows "negligible {x  S. f x  T}"
proof -
  define U where
    "U  λn::nat. {x  S. y. y  S  norm(y - x) < 1/n
                      norm(y - x)  n * norm(f y - f x)}"
  have "negligible {x  U n. f x  T}" if "n > 0" for n
  proof (subst locally_negligible_alt, clarify)
    fix a
    assume a: "a  U n" and fa: "f a  T"
    define V where "V  {x. x  U n  f x  T}  ball a (1 / n / 2)"
    show "V. openin (top_of_set {x  U n. f x  T}) V  a  V  negligible V"
    proof (intro exI conjI)
      have noxy: "norm(x - y)  n * norm(f x - f y)" if "x  V" "y  V" for x y
        using that unfolding U_def V_def mem_Collect_eq Int_iff mem_ball dist_norm
        by (meson norm_triangle_half_r)
      then have "inj_on f V"
        by (force simp: inj_on_def)
      then obtain g where g: "x. x  V  g(f x) = x"
        by (metis inv_into_f_f)
      have "T' B. open T'  f x  T' 
                   (yf ` V  T  T'. norm (g y - g (f x))  B * norm (y - f x))"
        if "f x  T" "x  V" for x
        using that noxy 
        by (rule_tac x = "ball (f x) 1" in exI) (force simp: g)
      then have "negligible (g ` (f ` V  T))"
        by (force simp: negligible T negligible_Int intro!: negligible_locally_Lipschitz_image)
      moreover have "V  g ` (f ` V  T)"
        by (force simp: g image_iff V_def)
      ultimately show "negligible V"
        by (rule negligible_subset)
    qed (use a fa V_def that in auto)
  qed
  with negligible_countable_Union have "negligible (n  {0<..}. {x. x  U n  f x  T})"
    by auto
  moreover have "{x  S. f x  T}  (n  {0<..}. {x. x  U n  f x  T})"
  proof clarsimp
    fix x
    assume "x  S" and "f x  T"
    then obtain inj: "inj(f' x)" and der: "(f has_derivative f' x) (at x within S)"
      using assms by metis
    moreover have "linear(f' x)"
      and eps: "ε. ε > 0  δ>0. yS. norm (y - x) < δ 
                      norm (f y - f x - f' x (y - x))  ε * norm (y - x)"
      using der by (auto simp: has_derivative_within_alt linear_linear)
    ultimately obtain g where "linear g" and g: "g  f' x = id"
      using linear_injective_left_inverse by metis
    then obtain B where "B > 0" and B: "z. B * norm z  norm(f' x z)"
      using linear_invertible_bounded_below_pos linear (f' x) by blast
    then obtain i where "i  0" and i: "1 / real i < B"
      by (metis (full_types) inverse_eq_divide real_arch_invD)
    then obtain δ where "δ > 0"
         and δ: "y. yS; norm (y - x) < δ 
                  norm (f y - f x - f' x (y - x))  (B - 1 / real i) * norm (y - x)"
      using eps [of "B - 1/i"] by auto
    then obtain j where "j  0" and j: "inverse (real j) < δ"
      using real_arch_inverse by blast
    have "norm (y - x)/(max i j)  norm (f y - f x)"
      if "y  S" and less: "norm (y - x) < 1 / (max i j)" for y
    proof -
      have "1 / real (max i j) < δ"
        using j j  0 0 < δ
        by (auto simp: field_split_simps max_mult_distrib_left of_nat_max)
    then have "norm (y - x) < δ"
      using less by linarith
    with δ y  S have le: "norm (f y - f x - f' x (y - x))  B * norm (y - x) - norm (y - x)/i"
      by (auto simp: algebra_simps)
    have "norm (y - x) / real (max i j)  norm (y - x) / real i"
      using i  0 j  0 by (simp add: field_split_simps max_mult_distrib_left of_nat_max less_max_iff_disj)
    also have "...  norm (f y - f x)"
      using B [of "y-x"] le norm_triangle_ineq3 [of "f y - f x" "f' x (y - x)"]
      by linarith 
    finally show ?thesis .
  qed
  with x  S i  0 j  0 show "n{0<..}. x  U n"
    by (rule_tac x="max i j" in bexI) (auto simp: field_simps U_def less_max_iff_disj)
qed
  ultimately show ?thesis
    by (rule negligible_subset)
qed

lemma absolutely_integrable_Un:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes S: "f absolutely_integrable_on S" and T: "f absolutely_integrable_on T"
  shows "f absolutely_integrable_on (S  T)"
proof -
  have [simp]: "{x. (if x  A then f x else 0)  0} = {x  A. f x  0}" for A
    by auto
  let ?ST = "{x  S. f x  0}  {x  T. f x  0}"
  have "?ST  sets lebesgue"
  proof (rule Sigma_Algebra.sets.Int)
    have "f integrable_on S"
      using S absolutely_integrable_on_def by blast
    then have "(λx. if x  S then f x else 0) integrable_on UNIV"
      by (simp add: integrable_restrict_UNIV)
    then have borel: "(λx. if x  S then f x else 0)  borel_measurable (lebesgue_on UNIV)"
      using integrable_imp_measurable lebesgue_on_UNIV_eq by blast
    then show "{x  S. f x  0}  sets lebesgue"
      unfolding borel_measurable_vimage_open
      by (rule allE [where x = "-{0}"]) auto
  next
    have "f integrable_on T"
      using T absolutely_integrable_on_def by blast
    then have "(λx. if x  T then f x else 0) integrable_on UNIV"
      by (simp add: integrable_restrict_UNIV)
    then have borel: "(λx. if x  T then f x else 0)  borel_measurable (lebesgue_on UNIV)"
      using integrable_imp_measurable lebesgue_on_UNIV_eq by blast
    then show "{x  T. f x  0}  sets lebesgue"
      unfolding borel_measurable_vimage_open
      by (rule allE [where x = "-{0}"]) auto
  qed
  then have "f absolutely_integrable_on ?ST"
    by (rule set_integrable_subset [OF S]) auto
  then have Int: "(λx. if x  ?ST then f x else 0) absolutely_integrable_on UNIV"
    using absolutely_integrable_restrict_UNIV by blast
  have "(λx. if x  S then f x else 0) absolutely_integrable_on UNIV"
       "(λx. if x  T then f x else 0) absolutely_integrable_on UNIV"
    using S T absolutely_integrable_restrict_UNIV by blast+
  then have "(λx. (if x  S then f x else 0) + (if x  T then f x else 0)) absolutely_integrable_on UNIV"
    by (rule set_integral_add)
  then have "(λx. ((if x  S then f x else 0) + (if x  T then f x else 0)) - (if x  ?ST then f x else 0)) absolutely_integrable_on UNIV"
    using Int by (rule set_integral_diff)
  then have "(λx. if x  S  T then f x else 0) absolutely_integrable_on UNIV"
    by (rule absolutely_integrable_spike) (auto intro: empty_imp_negligible)
  then show ?thesis
    unfolding absolutely_integrable_restrict_UNIV .
qed

lemma absolutely_integrable_on_combine:
  fixes f :: "real  'a::euclidean_space"
  assumes "f absolutely_integrable_on {a..c}"
    and "f absolutely_integrable_on {c..b}"
    and "a  c"
    and "c  b"
  shows "f absolutely_integrable_on {a..b}"
  by (metis absolutely_integrable_Un assms ivl_disj_un_two_touch(4))

lemma uniform_limit_set_lebesgue_integral_at_top:
  fixes f :: "'a  real  'b::{banach, second_countable_topology}"
    and g :: "real  real"
  assumes bound: "x y. x  A  y  a  norm (f x y)  g y"
  assumes integrable: "set_integrable M {a..} g"
  assumes measurable: "x. x  A  set_borel_measurable M {a..} (f x)"
  assumes "sets borel  sets M"
  shows   "uniform_limit A (λb x. LINT y:{a..b}|M. f x y) (λx. LINT y:{a..}|M. f x y) at_top"
proof (cases "A = {}")
  case False
  then obtain x where x: "x  A" by auto
  have g_nonneg: "g y  0" if "y  a" for y
  proof -
    have "0  norm (f x y)" by simp
    also have "  g y" using bound[OF x that] by simp
    finally show ?thesis .
  qed

  have integrable': "set_integrable M {a..} (λy. f x y)" if "x  A" for x
    unfolding set_integrable_def
  proof (rule Bochner_Integration.integrable_bound)
    show "integrable M (λx. indicator {a..} x * g x)"
      using integrable by (simp add: set_integrable_def)
    show "(λy. indicat_real {a..} y *R f x y)  borel_measurable M" using measurable[OF that]
      by (simp add: set_borel_measurable_def)
    show "AE y in M. norm (indicat_real {a..} y *R f x y)  norm (indicat_real {a..} y * g y)"
      using bound[OF that] by (intro AE_I2) (auto simp: indicator_def g_nonneg)
  qed

  show ?thesis
  proof (rule uniform_limitI)
    fix e :: real assume e: "e > 0"
    have sets [intro]: "A  sets M" if "A  sets borel" for A
      using that assms by blast

    have "((λb. LINT y:{a..b}|M. g y)  (LINT y:{a..}|M. g y)) at_top"
      by (intro tendsto_set_lebesgue_integral_at_top assms sets) auto
    with e obtain b0 :: real where b0: "bb0. ¦(LINT y:{a..}|M. g y) - (LINT y:{a..b}|M. g y)¦ < e"
      by (auto simp: tendsto_iff eventually_at_top_linorder dist_real_def abs_minus_commute)
    define b where "b = max a b0"
    have "a  b" by (simp add: b_def)
    from b0 have "¦(LINT y:{a..}|M. g y) - (LINT y:{a..b}|M. g y)¦ < e"
      by (auto simp: b_def)
    also have "{a..} = {a..b}  {b<..}" by (auto simp: b_def)
    also have "¦(LINT y:|M. g y) - (LINT y:{a..b}|M. g y)¦ = ¦(LINT y:{b<..}|M. g y)¦"
      using a  b by (subst set_integral_Un) (auto intro!: set_integrable_subset[OF integrable])
    also have "(LINT y:{b<..}|M. g y)  0"
      using g_nonneg a  b unfolding set_lebesgue_integral_def
      by (intro Bochner_Integration.integral_nonneg) (auto simp: indicator_def)
    hence "¦(LINT y:{b<..}|M. g y)¦ = (LINT y:{b<..}|M. g y)" by simp
    finally have less: "(LINT y:{b<..}|M. g y) < e" .

    have "eventually (λb. b  b0) at_top" by (rule eventually_ge_at_top)
    moreover have "eventually (λb. b  a) at_top" by (rule eventually_ge_at_top)
    ultimately show "eventually (λb. xA.
                       dist (LINT y:{a..b}|M. f x y) (LINT y:{a..}|M. f x y) < e) at_top"
    proof eventually_elim
      case (elim b)
      show ?case
      proof
        fix x assume x: "x  A"
        have "dist (LINT y:{a..b}|M. f x y) (LINT y:{a..}|M. f x y) =
                norm ((LINT y:{a..}|M. f x y) - (LINT y:{a..b}|M. f x y))"
          by (simp add: dist_norm norm_minus_commute)
        also have "{a..} = {a..b}  {b<..}" using elim by auto
        also have "(LINT y:|M. f x y) - (LINT y:{a..b}|M. f x y) = (LINT y:{b<..}|M. f x y)"
          using elim x
          by (subst set_integral_Un) (auto intro!: set_integrable_subset[OF integrable'])
        also have "norm   (LINT y:{b<..}|M. norm (f x y))" using elim x
          by (intro set_integral_norm_bound set_integrable_subset[OF integrable']) auto
        also have "  (LINT y:{b<..}|M. g y)" using elim x bound g_nonneg
          by (intro set_integral_mono set_integrable_norm set_integrable_subset[OF integrable']
                    set_integrable_subset[OF integrable]) auto
        also have "(LINT y:{b<..}|M. g y)  0"
          using g_nonneg a  b unfolding set_lebesgue_integral_def
          by (intro Bochner_Integration.integral_nonneg) (auto simp: indicator_def)
        hence "(LINT y:{b<..}|M. g y) = ¦(LINT y:{b<..}|M. g y)¦" by simp
        also have " = ¦(LINT y:{a..b}  {b<..}|M. g y) - (LINT y:{a..b}|M. g y)¦"
          using elim by (subst set_integral_Un) (auto intro!: set_integrable_subset[OF integrable])
        also have "{a..b}  {b<..} = {a..}" using elim by auto
        also have "¦(LINT y:{a..}|M. g y) - (LINT y:{a..b}|M. g y)¦ < e"
          using b0 elim by blast
        finally show "dist (LINT y:{a..b}|M. f x y) (LINT y:{a..}|M. f x y) < e" .
      qed
    qed
  qed
qed auto



subsubsection‹Differentiability of inverse function (most basic form)›

proposition has_derivative_inverse_within:
  fixes f :: "'a::real_normed_vector  'b::euclidean_space"
  assumes der_f: "(f has_derivative f') (at a within S)"
    and cont_g: "continuous (at (f a) within f ` S) g"
    and "a  S" "linear g'" and id: "g'  f' = id"
    and gf: "x. x  S  g(f x) = x"
  shows "(g has_derivative g') (at (f a) within f ` S)"
proof -
  have [simp]: "g' (f' x) = x" for x
    by (simp add: local.id pointfree_idE)
  have "bounded_linear f'"
    and f': "e. e>0  d>0. yS. norm (y - a) < d 
                        norm (f y - f a - f' (y - a))  e * norm (y - a)"
    using der_f by (auto simp: has_derivative_within_alt)
  obtain C where "C > 0" and C: "x. norm (g' x)  C * norm x"
    using linear_bounded_pos [OF linear g'] by metis
  obtain B k where "B > 0" "k > 0"
    and Bk: "x. x  S; norm(f x - f a) < k  norm(x - a)  B * norm(f x - f a)"
  proof -
    obtain B where "B > 0" and B: "x. B * norm x  norm (f' x)"
      using linear_inj_bounded_below_pos [of f'] linear g' id der_f has_derivative_linear
        linear_invertible_bounded_below_pos by blast
    then obtain d where "d>0"
      and d: "y. y  S; norm (y - a) < d 
                    norm (f y - f a - f' (y - a))  B / 2 * norm (y - a)"
      using f' [of "B/2"] by auto
    then obtain e where "e > 0"
      and e: "x. x  S; norm (f x - f a) < e  norm (g (f x) - g (f a)) < d"
      using cont_g by (auto simp: continuous_within_eps_delta dist_norm)
    show thesis
    proof
      show "2/B > 0"
        using B > 0 by simp
      show "norm (x - a)  2 / B * norm (f x - f a)"
        if "x  S" "norm (f x - f a) < e" for x
      proof -
        have xa: "norm (x - a) < d"
          using e [OF that] gf by (simp add: a  S that)
        have *: "norm(y - f')  B / 2 * norm x; B * norm x  norm f'
                  norm y  B / 2 * norm x" for y f'::'b and x::'a
          using norm_triangle_ineq3 [of y f'] by linarith
        show ?thesis
          using * [OF d [OF x  S xa] B] B > 0 by (simp add: field_simps)
      qed
    qed (use e > 0 in auto)
  qed
  show ?thesis
    unfolding has_derivative_within_alt
  proof (intro conjI impI allI)
    show "bounded_linear g'"
      using linear g' by (simp add: linear_linear)
  next
    fix e :: "real"
    assume "e > 0"
    then obtain d where "d>0"
      and d: "y. y  S; norm (y - a) < d 
                    norm (f y - f a - f' (y - a))  e / (B * C) * norm (y - a)"
      using f' [of "e / (B * C)"] B > 0 C > 0 by auto
    have "norm (x - a - g' (f x - f a))  e * norm (f x - f a)"
      if "x  S" and lt_k: "norm (f x - f a) < k" and lt_dB: "norm (f x - f a) < d/B" for x
    proof -
      have "norm (x - a)  B * norm(f x - f a)"
        using Bk lt_k x  S by blast
      also have " < d"
        by (metis 0 < B lt_dB mult.commute pos_less_divide_eq)
      finally have lt_d: "norm (x - a) < d" .
      have "norm (x - a - g' (f x - f a))  norm(g'(f x - f a - (f' (x - a))))"
        by (simp add: linear_diff [OF linear g'] norm_minus_commute)
      also have "  C * norm (f x - f a - f' (x - a))"
        using C by blast
      also have "  e * norm (f x - f a)"
      proof -
        have "norm (f x - f a - f' (x - a))  e / (B * C) * norm (x - a)"
          using d [OF x  S lt_d] .
        also have "  (norm (f x - f a) * e) / C"
          using B > 0 C > 0 e > 0 by (simp add: field_simps Bk lt_k x  S)
        finally show ?thesis
          using C > 0 by (simp add: field_simps)
      qed
    finally show ?thesis .
    qed
    with k > 0 B > 0 d > 0 a  S 
    show "d>0. yf ` S.
               norm (y - f a) < d 
               norm (g y - g (f a) - g' (y - f a))  e * norm (y - f a)"
      by (rule_tac x="min k (d / B)" in exI) (auto simp: gf)
  qed
qed

end