Theory HOL-Analysis.Lebesgue_Integral_Substitution

(*  Title:      HOL/Analysis/Lebesgue_Integral_Substitution.thy
    Author:     Manuel Eberl

    Provides lemmas for integration by substitution for the basic integral types.
    Note that the substitution function must have a nonnegative derivative.
    This could probably be weakened somehow.
*)

section ‹Integration by Substition for the Lebesgue Integral›

theory Lebesgue_Integral_Substitution
imports Interval_Integral
begin


lemma nn_integral_substitution_aux:
  fixes f :: "real  ennreal"
  assumes Mf: "f  borel_measurable borel"
  assumes nonnegf: "x. f x  0"
  assumes derivg: "x. x  {a..b}  (g has_real_derivative g' x) (at x)"
  assumes contg': "continuous_on {a..b} g'"
  assumes derivg_nonneg: "x. x  {a..b}  g' x  0"
  assumes "a < b"
  shows "(+x. f x * indicator {g a..g b} x lborel) =
             (+x. f (g x) * g' x * indicator {a..b} x lborel)"
proof-
  from a < b have [simp]: "a  b" by simp
  from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
  from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and
                             Mg': "set_borel_measurable borel {a..b} g'"
      by (simp_all only: set_measurable_continuous_on_ivl)
  from derivg have derivg': "x. x  {a..b}  (g has_vector_derivative g' x) (at x)"
    by (simp only: has_real_derivative_iff_has_vector_derivative)

  have real_ind[simp]: "A x. enn2real (indicator A x) = indicator A x"
      by (auto split: split_indicator)
  have ennreal_ind[simp]: "A x. ennreal (indicator A x) = indicator A x"
      by (auto split: split_indicator)
  have [simp]: "x A. indicator A (g x) = indicator (g -` A) x"
      by (auto split: split_indicator)

  from derivg derivg_nonneg have monog: "x y. a  x  x  y  y  b  g x  g y"
    by (rule deriv_nonneg_imp_mono) simp_all
  with monog have [simp]: "g a  g b" by (auto intro: mono_onD)

  show ?thesis
  proof (induction rule: borel_measurable_induct[OF Mf, case_names cong set mult add sup])
    case (cong f1 f2)
    from cong.hyps(3) have "f1 = f2" by auto
    with cong show ?case by simp
  next
    case (set A)
    from set.hyps show ?case
    proof (induction rule: borel_set_induct)
      case empty
      thus ?case by simp
    next
      case (interval c d)
      {
        fix u v :: real assume asm: "{u..v}  {g a..g b}" "u  v"

        obtain u' v' where u'v': "{a..b}  g-`{u..v} = {u'..v'}" "u'  v'" "g u' = u" "g v' = v"
             using asm by (rule_tac continuous_interval_vimage_Int[OF contg monog, of u v]) simp_all
        hence "{u'..v'}  {a..b}" "{u'..v'}  g -` {u..v}" by blast+
        with u'v'(2) have "u'  g -` {u..v}" "v'  g -` {u..v}" by auto
        from u'v'(1) have [simp]: "{a..b}  g -` {u..v}  sets borel" by simp

        have A: "continuous_on {min u' v'..max u' v'} g'"
            by (simp only: u'v' max_absorb2 min_absorb1)
               (intro continuous_on_subset[OF contg'], insert u'v', auto)
        have "x. x  {u'..v'}  (g has_real_derivative g' x) (at x within {u'..v'})"
           using asm by (intro has_field_derivative_subset[OF derivg] subsetD[OF {u'..v'}  {a..b}]) auto
        hence B: "x. min u' v'  x  x  max u' v' 
                      (g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})"
            by (simp only: u'v' max_absorb2 min_absorb1)
               (auto simp: has_real_derivative_iff_has_vector_derivative)
          have "integrable lborel (λx. indicator ({a..b}  g -` {u..v}) x *R g' x)"
            using set_integrable_subset borel_integrable_atLeastAtMost'[OF contg']
            by (metis {u'..v'}  {a..b} eucl_ivals(5) set_integrable_def sets_lborel u'v'(1))
        hence "(+x. ennreal (g' x) * indicator ({a..b}  g-` {u..v}) x lborel) =
                   (LBINT x:{a..b}  g-`{u..v}. g' x)"
          unfolding set_lebesgue_integral_def
          by (subst nn_integral_eq_integral[symmetric])
             (auto intro!: derivg_nonneg nn_integral_cong split: split_indicator)
        also from interval_integral_FTC_finite[OF A B]
            have "(LBINT x:{a..b}  g-`{u..v}. g' x) = v - u"
                by (simp add: u'v' interval_integral_Icc u  v)
        finally have "(+ x. ennreal (g' x) * indicator ({a..b}  g -` {u..v}) x lborel) =
                           ennreal (v - u)" .
      } note A = this

      have "(+x. indicator {c..d} (g x) * ennreal (g' x) * indicator {a..b} x lborel) =
               (+ x. ennreal (g' x) * indicator ({a..b}  g -` {c..d}) x lborel)"
        by (intro nn_integral_cong) (simp split: split_indicator)
      also have "{a..b}  g-`{c..d} = {a..b}  g-`{max (g a) c..min (g b) d}"
        using a  b c  d
        by (auto intro!: monog intro: order.trans)
      also have "(+ x. ennreal (g' x) * indicator ... x lborel) =
        (if max (g a) c  min (g b) d then min (g b) d - max (g a) c else 0)"
         using c  d by (simp add: A)
      also have "... = (+ x. indicator ({g a..g b}  {c..d}) x lborel)"
        by (subst nn_integral_indicator) (auto intro!: measurable_sets Mg simp:)
      also have "... = (+ x. indicator {c..d} x * indicator {g a..g b} x lborel)"
        by (intro nn_integral_cong) (auto split: split_indicator)
      finally show ?case ..

      next

      case (compl A)
      note A  sets borel[measurable]
      from emeasure_mono[of "A  {g a..g b}" "{g a..g b}" lborel]
      have [simp]: "emeasure lborel (A  {g a..g b})  top" by (auto simp: top_unique)
      have [simp]: "g -` A  {a..b}  sets borel"
        by (rule set_borel_measurable_sets[OF Mg]) auto
      have [simp]: "g -` (-A)  {a..b}  sets borel"
        by (rule set_borel_measurable_sets[OF Mg]) auto

      have "(+x. indicator (-A) x * indicator {g a..g b} x lborel) =
                (+x. indicator (-A  {g a..g b}) x lborel)"
        by (rule nn_integral_cong) (simp split: split_indicator)
      also from compl have "... = emeasure lborel ({g a..g b} - A)" using derivg_nonneg
        by (simp add: vimage_Compl diff_eq Int_commute[of "-A"])
      also have "{g a..g b} - A = {g a..g b} - A  {g a..g b}" by blast
      also have "emeasure lborel ... = g b - g a - emeasure lborel (A  {g a..g b})"
             using A  sets borel by (subst emeasure_Diff) auto
     also have "emeasure lborel (A  {g a..g b}) =
                    +x. indicator A x * indicator {g a..g b} x lborel"
       using A  sets borel
       by (subst nn_integral_indicator[symmetric], simp, intro nn_integral_cong)
          (simp split: split_indicator)
      also have "... = + x. indicator (g-`A  {a..b}) x * ennreal (g' x * indicator {a..b} x) lborel" (is "_ = ?I")
        by (subst compl.IH, intro nn_integral_cong) (simp split: split_indicator)
      also have "g b - g a = (LBINT x:{a..b}. g' x)" using derivg'
        unfolding set_lebesgue_integral_def
        by (intro integral_FTC_atLeastAtMost[symmetric])
           (auto intro: continuous_on_subset[OF contg'] has_field_derivative_subset[OF derivg]
                 has_vector_derivative_at_within)
      also have "ennreal ... = (+ x. g' x * indicator {a..b} x lborel)"
        using borel_integrable_atLeastAtMost'[OF contg'] unfolding set_lebesgue_integral_def
        by (subst nn_integral_eq_integral)
           (simp_all add: mult.commute derivg_nonneg set_integrable_def split: split_indicator)
      also have Mg'': "(λx. indicator (g -` A  {a..b}) x * ennreal (g' x * indicator {a..b} x))
                             borel_measurable borel" using Mg'
        by (intro borel_measurable_times_ennreal borel_measurable_indicator)
           (simp_all add: mult.commute set_borel_measurable_def)
      have le: "(+x. indicator (g-`A  {a..b}) x * ennreal (g' x * indicator {a..b} x) lborel) 
                        (+x. ennreal (g' x) * indicator {a..b} x lborel)"
         by (intro nn_integral_mono) (simp split: split_indicator add: derivg_nonneg)
      note integrable = borel_integrable_atLeastAtMost'[OF contg']
      with le have notinf: "(+x. indicator (g-`A  {a..b}) x * ennreal (g' x * indicator {a..b} x) lborel)  top"
          by (auto simp: real_integrable_def nn_integral_set_ennreal mult.commute top_unique set_integrable_def)
      have "(+ x. g' x * indicator {a..b} x lborel) - ?I =
                  + x. ennreal (g' x * indicator {a..b} x) -
                        indicator (g -` A  {a..b}) x * ennreal (g' x * indicator {a..b} x) lborel"
        apply (intro nn_integral_diff[symmetric])
        apply (insert Mg', simp add: mult.commute set_borel_measurable_def) []
        apply (insert Mg'', simp) []
        apply (simp split: split_indicator add: derivg_nonneg)
        apply (rule notinf)
        apply (simp split: split_indicator add: derivg_nonneg)
        done
      also have "... = + x. indicator (-A) (g x) * ennreal (g' x) * indicator {a..b} x lborel"
        by (intro nn_integral_cong) (simp split: split_indicator)
      finally show ?case .

    next
      case (union f)
      then have [simp]: "i. {a..b}  g -` f i  sets borel"
        by (subst Int_commute, intro set_borel_measurable_sets[OF Mg]) auto
      have "g -` (i. f i)  {a..b} = (i. {a..b}  g -` f i)" by auto
      hence "g -` (i. f i)  {a..b}  sets borel" by (auto simp del: UN_simps)

      have "(+x. indicator (i. f i) x * indicator {g a..g b} x lborel) =
                +x. indicator (i. {g a..g b}  f i) x lborel"
          by (intro nn_integral_cong) (simp split: split_indicator)
      also from union have "... = emeasure lborel (i. {g a..g b}  f i)" by simp
      also from union have "... = (i. emeasure lborel ({g a..g b}  f i))"
        by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def)
      also from union have "... = (i. +x. indicator ({g a..g b}  f i) x lborel)" by simp
      also have "(λi. +x. indicator ({g a..g b}  f i) x lborel) =
                           (λi. +x. indicator (f i) x * indicator {g a..g b} x lborel)"
        by (intro ext nn_integral_cong) (simp split: split_indicator)
      also from union.IH have "(i. +x. indicator (f i) x * indicator {g a..g b} x lborel) =
          (i. + x. indicator (f i) (g x) * ennreal (g' x) * indicator {a..b} x lborel)" by simp
      also have "(λi. + x. indicator (f i) (g x) * ennreal (g' x) * indicator {a..b} x lborel) =
                         (λi. + x. ennreal (g' x * indicator {a..b} x) * indicator ({a..b}  g -` f i) x lborel)"
        by (intro ext nn_integral_cong) (simp split: split_indicator)
      also have "(i. ... i) = + x. (i. ennreal (g' x * indicator {a..b} x) * indicator ({a..b}  g -` f i) x) lborel"
        using Mg'
        apply (intro nn_integral_suminf[symmetric])
        apply (rule borel_measurable_times_ennreal, simp add: mult.commute set_borel_measurable_def)
        apply (rule borel_measurable_indicator, subst sets_lborel)
        apply (simp_all split: split_indicator add: derivg_nonneg)
        done
      also have "(λx i. ennreal (g' x * indicator {a..b} x) * indicator ({a..b}  g -` f i) x) =
                      (λx i. ennreal (g' x * indicator {a..b} x) * indicator (g -` f i) x)"
        by (intro ext) (simp split: split_indicator)
      also have "(+ x. (i. ennreal (g' x * indicator {a..b} x) * indicator (g -` f i) x) lborel) =
                     + x. ennreal (g' x * indicator {a..b} x) * (i. indicator (g -` f i) x) lborel"
        by (intro nn_integral_cong) (auto split: split_indicator simp: derivg_nonneg)
      also from union have "(λx. i. indicator (g -` f i) x :: ennreal) = (λx. indicator (i. g -` f i) x)"
        by (intro ext suminf_indicator) (auto simp: disjoint_family_on_def)
      also have "(+x. ennreal (g' x * indicator {a..b} x) * ... x lborel) =
                    (+x. indicator (i. f i) (g x) * ennreal (g' x) * indicator {a..b} x lborel)"
       by (intro nn_integral_cong) (simp split: split_indicator)
      finally show ?case .
  qed

next
  case (mult f c)
    note Mf[measurable] = f  borel_measurable borel
    let ?I = "indicator {a..b}"
    have "(λx. f (g x * ?I x) * ennreal (g' x * ?I x))  borel_measurable borel" using Mg Mg'
      by (intro borel_measurable_times_ennreal measurable_compose[OF _ Mf])
         (simp_all add: mult.commute set_borel_measurable_def)
    also have "(λx. f (g x * ?I x) * ennreal (g' x * ?I x)) = (λx. f (g x) * ennreal (g' x) * ?I x)"
      by (intro ext) (simp split: split_indicator)
    finally have Mf': "(λx. f (g x) * ennreal (g' x) * ?I x)  borel_measurable borel" .
    with mult show ?case
      by (subst (1 2 3) mult_ac, subst (1 2) nn_integral_cmult) (simp_all add: mult_ac)

next
  case (add f2 f1)
    let ?I = "indicator {a..b}"
    {
      fix f :: "real  ennreal" assume Mf: "f  borel_measurable borel"
      have "(λx. f (g x * ?I x) * ennreal (g' x * ?I x))  borel_measurable borel" using Mg Mg'
        by (intro borel_measurable_times_ennreal measurable_compose[OF _ Mf])
           (simp_all add:  mult.commute set_borel_measurable_def)
      also have "(λx. f (g x * ?I x) * ennreal (g' x * ?I x)) = (λx. f (g x) * ennreal (g' x) * ?I x)"
        by (intro ext) (simp split: split_indicator)
      finally have "(λx. f (g x) * ennreal (g' x) * ?I x)  borel_measurable borel" .
    } note Mf' = this[OF f1  borel_measurable borel] this[OF f2  borel_measurable borel]

    have "(+ x. (f1 x + f2 x) * indicator {g a..g b} x lborel) =
             (+ x. f1 x * indicator {g a..g b} x + f2 x * indicator {g a..g b} x lborel)"
      by (intro nn_integral_cong) (simp split: split_indicator)
    also from add have "... = (+ x. f1 (g x) * ennreal (g' x) * indicator {a..b} x lborel) +
                                (+ x. f2 (g x) * ennreal (g' x) * indicator {a..b} x lborel)"
      by (simp_all add: nn_integral_add)
    also from add have "... = (+ x. f1 (g x) * ennreal (g' x) * indicator {a..b} x +
                                      f2 (g x) * ennreal (g' x) * indicator {a..b} x lborel)"
      by (intro nn_integral_add[symmetric])
         (auto simp add: Mf' derivg_nonneg split: split_indicator)
    also have "... = + x. (f1 (g x) + f2 (g x)) * ennreal (g' x) * indicator {a..b} x lborel"
      by (intro nn_integral_cong) (simp split: split_indicator add: distrib_right)
    finally show ?case .

next
  case (sup F)
  {
    fix i
    let ?I = "indicator {a..b}"
    have "(λx. F i (g x * ?I x) * ennreal (g' x * ?I x))  borel_measurable borel" using Mg Mg'
      by (rule_tac borel_measurable_times_ennreal, rule_tac measurable_compose[OF _ sup.hyps(1)])
         (simp_all add: mult.commute set_borel_measurable_def)
    also have "(λx. F i (g x * ?I x) * ennreal (g' x * ?I x)) = (λx. F i (g x) * ennreal (g' x) * ?I x)"
      by (intro ext) (simp split: split_indicator)
     finally have "...  borel_measurable borel" .
  } note Mf' = this

    have "(+x. (SUP i. F i x) * indicator {g a..g b} x lborel) =
               +x. (SUP i. F i x* indicator {g a..g b} x) lborel"
      by (intro nn_integral_cong) (simp split: split_indicator)
    also from sup have "... = (SUP i. +x. F i x* indicator {g a..g b} x lborel)"
      by (intro nn_integral_monotone_convergence_SUP)
         (auto simp: incseq_def le_fun_def split: split_indicator)
    also from sup have "... = (SUP i. +x. F i (g x) * ennreal (g' x) * indicator {a..b} x lborel)"
      by simp
    also from sup have "... =  +x. (SUP i. F i (g x) * ennreal (g' x) * indicator {a..b} x) lborel"
      by (intro nn_integral_monotone_convergence_SUP[symmetric])
         (auto simp: incseq_def le_fun_def derivg_nonneg Mf' split: split_indicator
               intro!: mult_right_mono)
    also from sup have "... = +x. (SUP i. F i (g x)) * ennreal (g' x) * indicator {a..b} x lborel"
      by (subst mult.assoc, subst mult.commute, subst SUP_mult_left_ennreal)
         (auto split: split_indicator simp: derivg_nonneg mult_ac)
    finally show ?case by (simp add: image_comp)
  qed
qed

theorem nn_integral_substitution:
  fixes f :: "real  real"
  assumes Mf[measurable]: "set_borel_measurable borel {g a..g b} f"
  assumes derivg: "x. x  {a..b}  (g has_real_derivative g' x) (at x)"
  assumes contg': "continuous_on {a..b} g'"
  assumes derivg_nonneg: "x. x  {a..b}  g' x  0"
  assumes "a  b"
  shows "(+x. f x * indicator {g a..g b} x lborel) =
             (+x. f (g x) * g' x * indicator {a..b} x lborel)"
proof (cases "a = b")
  assume "a  b"
  with a  b have "a < b" by auto
  let ?f' = "λx. f x * indicator {g a..g b} x"

  from derivg derivg_nonneg have monog: "x y. a  x  x  y  y  b  g x  g y"
    by (rule deriv_nonneg_imp_mono) simp_all
  have bounds: "x. x  a  x  b  g x  g a" "x. x  a  x  b  g x  g b"
    by (auto intro: monog)

  from derivg_nonneg have nonneg:
    "f x. x  a  x  b  g' x  0  f x * ennreal (g' x)  0  f x  0"
    by (force simp: field_simps)
  have nonneg': "x. a  x  x  b  ¬ 0  f (g x)  0  f (g x) * g' x  g' x = 0"
    by (metis atLeastAtMost_iff derivg_nonneg eq_iff mult_eq_0_iff mult_le_0_iff)

  have "(+x. f x * indicator {g a..g b} x lborel) =
            (+x. ennreal (?f' x) * indicator {g a..g b} x lborel)"
    by (intro nn_integral_cong)
       (auto split: split_indicator split_max simp: zero_ennreal.rep_eq ennreal_neg)
  also have "... = + x. ?f' (g x) * ennreal (g' x) * indicator {a..b} x lborel" using Mf
    by (subst nn_integral_substitution_aux[OF _ _ derivg contg' derivg_nonneg a < b])
       (auto simp add: mult.commute set_borel_measurable_def)
  also have "... = + x. f (g x) * ennreal (g' x) * indicator {a..b} x lborel"
    by (intro nn_integral_cong) (auto split: split_indicator simp: max_def dest: bounds)
  also have "... = +x. ennreal (f (g x) * g' x * indicator {a..b} x) lborel"
    by (intro nn_integral_cong) (auto simp: mult.commute derivg_nonneg ennreal_mult' split: split_indicator)
  finally show ?thesis .
qed auto

theorem integral_substitution:
  assumes integrable: "set_integrable lborel {g a..g b} f"
  assumes derivg: "x. x  {a..b}  (g has_real_derivative g' x) (at x)"
  assumes contg': "continuous_on {a..b} g'"
  assumes derivg_nonneg: "x. x  {a..b}  g' x  0"
  assumes "a  b"
  shows "set_integrable lborel {a..b} (λx. f (g x) * g' x)"
    and "(LBINT x. f x * indicator {g a..g b} x) = (LBINT x. f (g x) * g' x * indicator {a..b} x)"
proof-
  from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
  with contg' have Mg: "set_borel_measurable borel {a..b} g"
    and Mg': "set_borel_measurable borel {a..b} g'"
    by (simp_all only: set_measurable_continuous_on_ivl)
  from derivg derivg_nonneg have monog: "x y. a  x  x  y  y  b  g x  g y"
    by (rule deriv_nonneg_imp_mono) simp_all

  have "(λx. ennreal (f x) * indicator {g a..g b} x) =
           (λx. ennreal (f x * indicator {g a..g b} x))"
    by (intro ext) (simp split: split_indicator)
  with integrable have M1: "(λx. f x * indicator {g a..g b} x)  borel_measurable borel"
    by (force simp: mult.commute set_integrable_def)
  from integrable have M2: "(λx. -f x * indicator {g a..g b} x)  borel_measurable borel"
    by (force simp: mult.commute set_integrable_def)

  have "(LBINT x. (f x :: real) * indicator {g a..g b} x) =
          enn2real (+ x. ennreal (f x) * indicator {g a..g b} x lborel) -
          enn2real (+ x. ennreal (- (f x)) * indicator {g a..g b} x lborel)" using integrable
    unfolding set_integrable_def
    by (subst real_lebesgue_integral_def) (simp_all add: nn_integral_set_ennreal mult.commute)
  also have *: "(+x. ennreal (f x) * indicator {g a..g b} x lborel) =
      (+x. ennreal (f x * indicator {g a..g b} x) lborel)"
    by (intro nn_integral_cong) (simp split: split_indicator)
  also from M1 * have A: "(+ x. ennreal (f x * indicator {g a..g b} x) lborel) =
                            (+ x. ennreal (f (g x) * g' x * indicator {a..b} x) lborel)"
    by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg a  b])
       (auto simp: nn_integral_set_ennreal mult.commute set_borel_measurable_def)
  also have **: "(+ x. ennreal (- (f x)) * indicator {g a..g b} x lborel) =
      (+ x. ennreal (- (f x) * indicator {g a..g b} x) lborel)"
    by (intro nn_integral_cong) (simp split: split_indicator)
  also from M2 ** have B: "(+ x. ennreal (- (f x) * indicator {g a..g b} x) lborel) =
        (+ x. ennreal (- (f (g x)) * g' x * indicator {a..b} x) lborel)"
    by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg a  b])
       (auto simp: nn_integral_set_ennreal mult.commute set_borel_measurable_def)

  also {
    from integrable have Mf: "set_borel_measurable borel {g a..g b} f"
      unfolding set_borel_measurable_def set_integrable_def by simp
    from measurable_compose Mg Mf Mg' borel_measurable_times
    have "(λx. f (g x * indicator {a..b} x) * indicator {g a..g b} (g x * indicator {a..b} x) *
                     (g' x * indicator {a..b} x))  borel_measurable borel"  (is "?f  _")
      by (simp add: mult.commute set_borel_measurable_def)
    also have "?f = (λx. f (g x) * g' x * indicator {a..b} x)"
      using monog by (intro ext) (auto split: split_indicator)
    finally show "set_integrable lborel {a..b} (λx. f (g x) * g' x)"
      using A B integrable unfolding real_integrable_def set_integrable_def
      by (simp_all add: nn_integral_set_ennreal mult.commute)
  } note integrable' = this

  have "enn2real (+ x. ennreal (f (g x) * g' x * indicator {a..b} x) lborel) -
                  enn2real (+ x. ennreal (-f (g x) * g' x * indicator {a..b} x) lborel) =
                (LBINT x. f (g x) * g' x * indicator {a..b} x)" 
    using integrable' unfolding set_integrable_def
    by (subst real_lebesgue_integral_def) (simp_all add: field_simps)
  finally show "(LBINT x. f x * indicator {g a..g b} x) =
                     (LBINT x. f (g x) * g' x * indicator {a..b} x)" .
qed

theorem interval_integral_substitution:
  assumes integrable: "set_integrable lborel {g a..g b} f"
  assumes derivg: "x. x  {a..b}  (g has_real_derivative g' x) (at x)"
  assumes contg': "continuous_on {a..b} g'"
  assumes derivg_nonneg: "x. x  {a..b}  g' x  0"
  assumes "a  b"
  shows "set_integrable lborel {a..b} (λx. f (g x) * g' x)"
    and "(LBINT x=g a..g b. f x) = (LBINT x=a..b. f (g x) * g' x)"
  apply (rule integral_substitution[OF assms], simp, simp)
  apply (subst (1 2) interval_integral_Icc, fact)
  apply (rule deriv_nonneg_imp_mono[OF derivg derivg_nonneg], simp, simp, fact)
  using integral_substitution(2)[OF assms]
  apply (simp add: mult.commute set_lebesgue_integral_def)
  done

lemma set_borel_integrable_singleton[simp]: "set_integrable lborel {x} (f :: real  real)"
  unfolding set_integrable_def
  by (subst integrable_discrete_difference[where X="{x}" and g="λ_. 0"]) auto

end