Theory 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<