Analysis builds using set_borel_measurable_def, etc.
authorpaulson <lp15@cam.ac.uk>
Thu Apr 12 12:16:34 2018 +0100 (13 months ago)
changeset 6797675b94eb58c3d
parent 67975 27c8692825f6
child 67977 557ea2740125
Analysis builds using set_borel_measurable_def, etc.
src/HOL/Analysis/Ball_Volume.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Gamma_Function.thy
src/HOL/Analysis/Lebesgue_Integral_Substitution.thy
     1.1 --- a/src/HOL/Analysis/Ball_Volume.thy	Wed Apr 11 16:34:52 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Ball_Volume.thy	Thu Apr 12 12:16:34 2018 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4    also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (x\<^sup>2 powr - (1 / 2) * (1 - x\<^sup>2) powr (real n / 2) * (2 * x) *
     1.5                            indicator {0..1} x) \<partial>lborel)"
     1.6      by (subst nn_integral_substitution[where g = "\<lambda>x. x ^ 2" and g' = "\<lambda>x. 2 * x"])
     1.7 -       (auto intro!: derivative_eq_intros continuous_intros)
     1.8 +       (auto intro!: derivative_eq_intros continuous_intros simp: set_borel_measurable_def)
     1.9    also have "\<dots> = (\<integral>\<^sup>+ x. 2 * ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
    1.10      by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"]) 
    1.11         (auto simp: indicator_def powr_minus powr_half_sqrt divide_simps ennreal_mult' mult_ac)
     2.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Wed Apr 11 16:34:52 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Apr 12 12:16:34 2018 +0100
     2.3 @@ -1545,7 +1545,7 @@
     2.4      using that by (subst Ln_minus) (auto simp: Ln_of_real)
     2.5    have **: "Ln (of_real x) = of_real (ln (-x)) + \<i> * pi" if "x < 0" for x
     2.6      using *[of "-x"] that by simp
     2.7 -  have cont: "set_borel_measurable borel (- \<real>\<^sub>\<le>\<^sub>0) Ln"
     2.8 +  have cont: "(\<lambda>x. indicat_real (- \<real>\<^sub>\<le>\<^sub>0) x *\<^sub>R Ln x) \<in> borel_measurable borel"
     2.9      by (intro borel_measurable_continuous_on_indicator continuous_intros) auto
    2.10    have "(\<lambda>x. if x \<in> \<real>\<^sub>\<le>\<^sub>0 then ln (-Re x) + \<i> * pi else indicator (-\<real>\<^sub>\<le>\<^sub>0) x *\<^sub>R Ln x) \<in> borel \<rightarrow>\<^sub>M borel"
    2.11      (is "?f \<in> _") by (rule measurable_If_set[OF _ cont]) auto
     3.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Wed Apr 11 16:34:52 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Thu Apr 12 12:16:34 2018 +0100
     3.3 @@ -876,9 +876,9 @@
     3.4       using of_nat_neq_0[of "2*n"] by (simp only: of_nat_Suc) (simp add: add_ac)
     3.5    hence nz': "of_nat n + (1/2::'a) \<noteq> 0" by (simp add: field_simps)
     3.6    have "Digamma (of_nat (Suc n) + 1/2 :: 'a) = Digamma (of_nat n + 1/2 + 1)" by simp
     3.7 -  also from nz' have "\<dots> = Digamma (of_nat n + 1 / 2) + 1 / (of_nat n + 1 / 2)"
     3.8 +  also from nz' have "\<dots> = Digamma (of_nat n + 1/2) + 1 / (of_nat n + 1/2)"
     3.9      by (rule Digamma_plus1)
    3.10 -  also from nz nz' have "1 / (of_nat n + 1 / 2 :: 'a) = 2 / (2 * of_nat n + 1)"
    3.11 +  also from nz nz' have "1 / (of_nat n + 1/2 :: 'a) = 2 / (2 * of_nat n + 1)"
    3.12      by (subst divide_eq_eq) simp_all
    3.13    also note Suc
    3.14    finally show ?case by (simp add: add_ac)
    3.15 @@ -2048,7 +2048,7 @@
    3.16    from assms double_in_nonpos_Ints_imp[of z] have z': "2 * z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto
    3.17    from fraction_not_in_ints[of 2 1] have "(1/2 :: 'a) \<notin> \<int>\<^sub>\<le>\<^sub>0"
    3.18      by (intro not_in_Ints_imp_not_in_nonpos_Ints) simp_all
    3.19 -  with lim[of "1/2 :: 'a"] have "?h \<longlonglongrightarrow> 2 * Gamma (1 / 2 :: 'a)" by (simp add: exp_of_real)
    3.20 +  with lim[of "1/2 :: 'a"] have "?h \<longlonglongrightarrow> 2 * Gamma (1/2 :: 'a)" by (simp add: exp_of_real)
    3.21    from LIMSEQ_unique[OF this lim[OF assms]] z' show ?thesis
    3.22      by (simp add: divide_simps Gamma_eq_zero_iff ring_distribs exp_diff exp_of_real ac_simps)
    3.23  qed
    3.24 @@ -2735,11 +2735,12 @@
    3.25    have "?f absolutely_integrable_on ({0<..x0} \<union> {x0..})"
    3.26    proof (rule set_integrable_Un)
    3.27      show "?f absolutely_integrable_on {0<..x0}"
    3.28 +      unfolding set_integrable_def
    3.29      proof (rule Bochner_Integration.integrable_bound [OF _ _ AE_I2])
    3.30 -      show "set_integrable lebesgue {0<..x0} (\<lambda>x. x powr (Re z - 1))" using x0(1) assms
    3.31 -        by (intro nonnegative_absolutely_integrable_1 integrable_on_powr_from_0') auto
    3.32 -      show "set_borel_measurable lebesgue {0<..x0}
    3.33 -              (\<lambda>x. complex_of_real x powr (z - 1) / complex_of_real (exp (a * x)))"
    3.34 +      show "integrable lebesgue (\<lambda>x. indicat_real {0<..x0} x *\<^sub>R x powr (Re z - 1))"         
    3.35 +        using x0(1) assms
    3.36 +        by (intro nonnegative_absolutely_integrable_1 [unfolded set_integrable_def] integrable_on_powr_from_0') auto
    3.37 +      show "(\<lambda>x. indicat_real {0<..x0} x *\<^sub>R (x powr (z - 1) / exp (a * x))) \<in> borel_measurable lebesgue"
    3.38          by (intro measurable_completion)
    3.39             (auto intro!: borel_measurable_continuous_on_indicator continuous_intros)
    3.40        fix x :: real 
    3.41 @@ -2751,11 +2752,11 @@
    3.42      qed
    3.43    next
    3.44      show "?f absolutely_integrable_on {x0..}"
    3.45 +      unfolding set_integrable_def
    3.46      proof (rule Bochner_Integration.integrable_bound [OF _ _ AE_I2])
    3.47 -      show "set_integrable lebesgue {x0..} (\<lambda>x. exp (-(a/2) * x))" using assms
    3.48 -        by (intro nonnegative_absolutely_integrable_1 integrable_on_exp_minus_to_infinity) auto
    3.49 -      show "set_borel_measurable lebesgue {x0..}
    3.50 -              (\<lambda>x. complex_of_real x powr (z - 1) / complex_of_real (exp (a * x)))" using x0(1)
    3.51 +      show "integrable lebesgue (\<lambda>x. indicat_real {x0..} x *\<^sub>R exp (- (a / 2) * x))" using assms
    3.52 +        by (intro nonnegative_absolutely_integrable_1 [unfolded set_integrable_def] integrable_on_exp_minus_to_infinity) auto
    3.53 +      show "(\<lambda>x. indicat_real {x0..} x *\<^sub>R (x powr (z - 1) / exp (a * x))) \<in> borel_measurable lebesgue" using x0(1)
    3.54          by (intro measurable_completion)
    3.55             (auto intro!: borel_measurable_continuous_on_indicator continuous_intros)
    3.56        fix x :: real 
    3.57 @@ -3015,14 +3016,15 @@
    3.58    qed (insert that, auto simp: max.coboundedI1 max.coboundedI2 powr_mono2' powr_mono2 D_def)
    3.59    have [simp]: "C \<ge> 0" "D \<ge> 0" by (simp_all add: C_def D_def)
    3.60  
    3.61 -  have I1: "set_integrable lborel {0..1 / 2} (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
    3.62 +  have I1: "set_integrable lborel {0..1/2} (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
    3.63 +    unfolding set_integrable_def
    3.64    proof (rule Bochner_Integration.integrable_bound[OF _ _ AE_I2])
    3.65 -    have "(\<lambda>t. t powr (a - 1)) integrable_on {0..1 / 2}"
    3.66 +    have "(\<lambda>t. t powr (a - 1)) integrable_on {0..1/2}"
    3.67        by (rule integrable_on_powr_from_0) (use assms in auto)
    3.68 -    hence "(\<lambda>t. t powr (a - 1)) absolutely_integrable_on {0..1 / 2}"
    3.69 +    hence "(\<lambda>t. t powr (a - 1)) absolutely_integrable_on {0..1/2}"
    3.70        by (subst absolutely_integrable_on_iff_nonneg) auto
    3.71 -    from integrable_mult_right[OF this, of C]
    3.72 -      show "set_integrable lborel {0..1 / 2} (\<lambda>t. C * t powr (a - 1))"
    3.73 +    from integrable_mult_right[OF this [unfolded set_integrable_def], of C]
    3.74 +    show "integrable lborel (\<lambda>x. indicat_real {0..1/2} x *\<^sub>R (C * x powr (a - 1)))"
    3.75        by (subst (asm) integrable_completion) (auto simp: mult_ac)
    3.76    next
    3.77      fix x :: real
    3.78 @@ -3033,7 +3035,8 @@
    3.79        by (auto simp: indicator_def abs_mult mult_ac)
    3.80    qed (auto intro!: AE_I2 simp: indicator_def)
    3.81  
    3.82 -  have I2: "set_integrable lborel {1 / 2..1} (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
    3.83 +  have I2: "set_integrable lborel {1/2..1} (\<lambda>t. t powr (a - 1) * (1 - t) powr (b - 1))"
    3.84 +    unfolding set_integrable_def
    3.85    proof (rule Bochner_Integration.integrable_bound[OF _ _ AE_I2])
    3.86      have "(\<lambda>t. t powr (b - 1)) integrable_on {0..1/2}"
    3.87        by (rule integrable_on_powr_from_0) (use assms in auto)
    3.88 @@ -3042,8 +3045,8 @@
    3.89        have "(\<lambda>t. (1 - t) powr (b - 1)) integrable_on {1/2..1}" by simp
    3.90      hence "(\<lambda>t. (1 - t) powr (b - 1)) absolutely_integrable_on {1/2..1}"
    3.91        by (subst absolutely_integrable_on_iff_nonneg) auto
    3.92 -    from integrable_mult_right[OF this, of D]
    3.93 -      show "set_integrable lborel {1 / 2..1} (\<lambda>t. D * (1 - t) powr (b - 1))"
    3.94 +    from integrable_mult_right[OF this [unfolded set_integrable_def], of D]
    3.95 +    show "integrable lborel (\<lambda>x. indicat_real {1/2..1} x *\<^sub>R (D * (1 - x) powr (b - 1)))"
    3.96        by (subst (asm) integrable_completion) (auto simp: mult_ac)
    3.97    next
    3.98      fix x :: real
    3.99 @@ -3204,9 +3207,9 @@
   3.100  proof -
   3.101    from tendsto_inverse[OF tendsto_mult[OF
   3.102           sin_product_formula_real[of "1/2"] tendsto_const[of "2/pi"]]]
   3.103 -    have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) \<longlonglongrightarrow> pi/2"
   3.104 +    have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1/2)\<^sup>2 / (real k)\<^sup>2))) \<longlonglongrightarrow> pi/2"
   3.105      by (simp add: prod_inversef [symmetric])
   3.106 -  also have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) =
   3.107 +  also have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1/2)\<^sup>2 / (real k)\<^sup>2))) =
   3.108                 (\<lambda>n. (\<Prod>k=1..n. (4*real k^2)/(4*real k^2 - 1)))"
   3.109      by (intro ext prod.cong refl) (simp add: divide_simps)
   3.110    finally show ?thesis .
     4.1 --- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Wed Apr 11 16:34:52 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Thu Apr 12 12:16:34 2018 +0100
     4.3 @@ -74,10 +74,12 @@
     4.4                        (g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})"
     4.5              by (simp only: u'v' max_absorb2 min_absorb1)
     4.6                 (auto simp: has_field_derivative_iff_has_vector_derivative)
     4.7 -        have "integrable lborel (\<lambda>x. indicator ({a..b} \<inter> g -` {u..v}) x *\<^sub>R g' x)"
     4.8 -          by (rule set_integrable_subset[OF borel_integrable_atLeastAtMost'[OF contg']]) simp_all
     4.9 +          have "integrable lborel (\<lambda>x. indicator ({a..b} \<inter> g -` {u..v}) x *\<^sub>R g' x)"
    4.10 +            using set_integrable_subset borel_integrable_atLeastAtMost'[OF contg']
    4.11 +            by (metis \<open>{u'..v'} \<subseteq> {a..b}\<close> eucl_ivals(5) set_integrable_def sets_lborel u'v'(1))
    4.12          hence "(\<integral>\<^sup>+x. ennreal (g' x) * indicator ({a..b} \<inter> g-` {u..v}) x \<partial>lborel) =
    4.13                     LBINT x:{a..b} \<inter> g-`{u..v}. g' x"
    4.14 +          unfolding set_lebesgue_integral_def
    4.15            by (subst nn_integral_eq_integral[symmetric])
    4.16               (auto intro!: derivg_nonneg nn_integral_cong split: split_indicator)
    4.17          also from interval_integral_FTC_finite[OF A B]
    4.18 @@ -129,28 +131,29 @@
    4.19        also have "... = \<integral>\<^sup>+ x. indicator (g-`A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel" (is "_ = ?I")
    4.20          by (subst compl.IH, intro nn_integral_cong) (simp split: split_indicator)
    4.21        also have "g b - g a = LBINT x:{a..b}. g' x" using derivg'
    4.22 +        unfolding set_lebesgue_integral_def
    4.23          by (intro integral_FTC_atLeastAtMost[symmetric])
    4.24             (auto intro: continuous_on_subset[OF contg'] has_field_derivative_subset[OF derivg]
    4.25                   has_vector_derivative_at_within)
    4.26        also have "ennreal ... = \<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel"
    4.27 -        using borel_integrable_atLeastAtMost'[OF contg']
    4.28 +        using borel_integrable_atLeastAtMost'[OF contg'] unfolding set_lebesgue_integral_def
    4.29          by (subst nn_integral_eq_integral)
    4.30 -           (simp_all add: mult.commute derivg_nonneg split: split_indicator)
    4.31 +           (simp_all add: mult.commute derivg_nonneg set_integrable_def split: split_indicator)
    4.32        also have Mg'': "(\<lambda>x. indicator (g -` A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x))
    4.33                              \<in> borel_measurable borel" using Mg'
    4.34          by (intro borel_measurable_times_ennreal borel_measurable_indicator)
    4.35 -           (simp_all add: mult.commute)
    4.36 +           (simp_all add: mult.commute set_borel_measurable_def)
    4.37        have le: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel) \<le>
    4.38                          (\<integral>\<^sup>+x. ennreal (g' x) * indicator {a..b} x \<partial>lborel)"
    4.39           by (intro nn_integral_mono) (simp split: split_indicator add: derivg_nonneg)
    4.40        note integrable = borel_integrable_atLeastAtMost'[OF contg']
    4.41        with le have notinf: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel) \<noteq> top"
    4.42 -          by (auto simp: real_integrable_def nn_integral_set_ennreal mult.commute top_unique)
    4.43 +          by (auto simp: real_integrable_def nn_integral_set_ennreal mult.commute top_unique set_integrable_def)
    4.44        have "(\<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel) - ?I =
    4.45                    \<integral>\<^sup>+ x. ennreal (g' x * indicator {a..b} x) -
    4.46                          indicator (g -` A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel"
    4.47          apply (intro nn_integral_diff[symmetric])
    4.48 -        apply (insert Mg', simp add: mult.commute) []
    4.49 +        apply (insert Mg', simp add: mult.commute set_borel_measurable_def) []
    4.50          apply (insert Mg'', simp) []
    4.51          apply (simp split: split_indicator add: derivg_nonneg)
    4.52          apply (rule notinf)
    4.53 @@ -185,7 +188,7 @@
    4.54        also have "(\<Sum>i. ... i) = \<integral>\<^sup>+ x. (\<Sum>i. ennreal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x) \<partial>lborel"
    4.55          using Mg'
    4.56          apply (intro nn_integral_suminf[symmetric])
    4.57 -        apply (rule borel_measurable_times_ennreal, simp add: mult.commute)
    4.58 +        apply (rule borel_measurable_times_ennreal, simp add: mult.commute set_borel_measurable_def)
    4.59          apply (rule borel_measurable_indicator, subst sets_lborel)
    4.60          apply (simp_all split: split_indicator add: derivg_nonneg)
    4.61          done
    4.62 @@ -209,7 +212,7 @@
    4.63      let ?I = "indicator {a..b}"
    4.64      have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
    4.65        by (intro borel_measurable_times_ennreal measurable_compose[OF _ Mf])
    4.66 -         (simp_all add: mult.commute)
    4.67 +         (simp_all add: mult.commute set_borel_measurable_def)
    4.68      also have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) = (\<lambda>x. f (g x) * ennreal (g' x) * ?I x)"
    4.69        by (intro ext) (simp split: split_indicator)
    4.70      finally have Mf': "(\<lambda>x. f (g x) * ennreal (g' x) * ?I x) \<in> borel_measurable borel" .
    4.71 @@ -223,7 +226,7 @@
    4.72        fix f :: "real \<Rightarrow> ennreal" assume Mf: "f \<in> borel_measurable borel"
    4.73        have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
    4.74          by (intro borel_measurable_times_ennreal measurable_compose[OF _ Mf])
    4.75 -           (simp_all add:  mult.commute)
    4.76 +           (simp_all add:  mult.commute set_borel_measurable_def)
    4.77        also have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) = (\<lambda>x. f (g x) * ennreal (g' x) * ?I x)"
    4.78          by (intro ext) (simp split: split_indicator)
    4.79        finally have "(\<lambda>x. f (g x) * ennreal (g' x) * ?I x) \<in> borel_measurable borel" .
    4.80 @@ -250,7 +253,7 @@
    4.81      let ?I = "indicator {a..b}"
    4.82      have "(\<lambda>x. F i (g x * ?I x) * ennreal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
    4.83        by (rule_tac borel_measurable_times_ennreal, rule_tac measurable_compose[OF _ sup.hyps(1)])
    4.84 -         (simp_all add: mult.commute)
    4.85 +         (simp_all add: mult.commute set_borel_measurable_def)
    4.86      also have "(\<lambda>x. F i (g x * ?I x) * ennreal (g' x * ?I x)) = (\<lambda>x. F i (g x) * ennreal (g' x) * ?I x)"
    4.87        by (intro ext) (simp split: split_indicator)
    4.88       finally have "... \<in> borel_measurable borel" .
    4.89 @@ -306,7 +309,7 @@
    4.90         (auto split: split_indicator split_max simp: zero_ennreal.rep_eq ennreal_neg)
    4.91    also have "... = \<integral>\<^sup>+ x. ?f' (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel" using Mf
    4.92      by (subst nn_integral_substitution_aux[OF _ _ derivg contg' derivg_nonneg \<open>a < b\<close>])
    4.93 -       (auto simp add: mult.commute)
    4.94 +       (auto simp add: mult.commute set_borel_measurable_def)
    4.95    also have "... = \<integral>\<^sup>+ x. f (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel"
    4.96      by (intro nn_integral_cong) (auto split: split_indicator simp: max_def dest: bounds)
    4.97    also have "... = \<integral>\<^sup>+x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel"
    4.98 @@ -334,13 +337,14 @@
    4.99             (\<lambda>x. ennreal (f x * indicator {g a..g b} x))"
   4.100      by (intro ext) (simp split: split_indicator)
   4.101    with integrable have M1: "(\<lambda>x. f x * indicator {g a..g b} x) \<in> borel_measurable borel"
   4.102 -    unfolding real_integrable_def by (force simp: mult.commute)
   4.103 +    by (force simp: mult.commute set_integrable_def)
   4.104    from integrable have M2: "(\<lambda>x. -f x * indicator {g a..g b} x) \<in> borel_measurable borel"
   4.105 -    unfolding real_integrable_def by (force simp: mult.commute)
   4.106 +    by (force simp: mult.commute set_integrable_def)
   4.107  
   4.108    have "LBINT x. (f x :: real) * indicator {g a..g b} x =
   4.109            enn2real (\<integral>\<^sup>+ x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) -
   4.110            enn2real (\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel)" using integrable
   4.111 +    unfolding set_integrable_def
   4.112      by (subst real_lebesgue_integral_def) (simp_all add: nn_integral_set_ennreal mult.commute)
   4.113    also have *: "(\<integral>\<^sup>+x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) =
   4.114        (\<integral>\<^sup>+x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel)"
   4.115 @@ -348,32 +352,33 @@
   4.116    also from M1 * have A: "(\<integral>\<^sup>+ x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel) =
   4.117                              (\<integral>\<^sup>+ x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel)"
   4.118      by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \<open>a \<le> b\<close>])
   4.119 -       (auto simp: nn_integral_set_ennreal mult.commute)
   4.120 +       (auto simp: nn_integral_set_ennreal mult.commute set_borel_measurable_def)
   4.121    also have **: "(\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel) =
   4.122        (\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel)"
   4.123      by (intro nn_integral_cong) (simp split: split_indicator)
   4.124    also from M2 ** have B: "(\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel) =
   4.125          (\<integral>\<^sup>+ x. ennreal (- (f (g x)) * g' x * indicator {a..b} x) \<partial>lborel)"
   4.126      by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \<open>a \<le> b\<close>])
   4.127 -       (auto simp: nn_integral_set_ennreal mult.commute)
   4.128 +       (auto simp: nn_integral_set_ennreal mult.commute set_borel_measurable_def)
   4.129  
   4.130    also {
   4.131      from integrable have Mf: "set_borel_measurable borel {g a..g b} f"
   4.132 -      unfolding real_integrable_def by simp
   4.133 -    from borel_measurable_times[OF measurable_compose[OF Mg Mf] Mg']
   4.134 -      have "(\<lambda>x. f (g x * indicator {a..b} x) * indicator {g a..g b} (g x * indicator {a..b} x) *
   4.135 +      unfolding set_borel_measurable_def set_integrable_def by simp
   4.136 +    from measurable_compose Mg Mf Mg' borel_measurable_times
   4.137 +    have "(\<lambda>x. f (g x * indicator {a..b} x) * indicator {g a..g b} (g x * indicator {a..b} x) *
   4.138                       (g' x * indicator {a..b} x)) \<in> borel_measurable borel"  (is "?f \<in> _")
   4.139 -      by (simp add: mult.commute)
   4.140 +      by (simp add: mult.commute set_borel_measurable_def)
   4.141      also have "?f = (\<lambda>x. f (g x) * g' x * indicator {a..b} x)"
   4.142        using monog by (intro ext) (auto split: split_indicator)
   4.143      finally show "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)"
   4.144 -      using A B integrable unfolding real_integrable_def
   4.145 +      using A B integrable unfolding real_integrable_def set_integrable_def
   4.146        by (simp_all add: nn_integral_set_ennreal mult.commute)
   4.147    } note integrable' = this
   4.148  
   4.149    have "enn2real (\<integral>\<^sup>+ x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel) -
   4.150                    enn2real (\<integral>\<^sup>+ x. ennreal (-f (g x) * g' x * indicator {a..b} x) \<partial>lborel) =
   4.151 -                (LBINT x. f (g x) * g' x * indicator {a..b} x)" using integrable'
   4.152 +                (LBINT x. f (g x) * g' x * indicator {a..b} x)" 
   4.153 +    using integrable' unfolding set_integrable_def
   4.154      by (subst real_lebesgue_integral_def) (simp_all add: field_simps)
   4.155    finally show "(LBINT x. f x * indicator {g a..g b} x) =
   4.156                       (LBINT x. f (g x) * g' x * indicator {a..b} x)" .
   4.157 @@ -391,11 +396,11 @@
   4.158    apply (subst (1 2) interval_integral_Icc, fact)
   4.159    apply (rule deriv_nonneg_imp_mono[OF derivg derivg_nonneg], simp, simp, fact)
   4.160    using integral_substitution(2)[OF assms]
   4.161 -  apply (simp add: mult.commute)
   4.162 +  apply (simp add: mult.commute set_lebesgue_integral_def)
   4.163    done
   4.164  
   4.165 -lemma set_borel_integrable_singleton[simp]:
   4.166 -  "set_integrable lborel {x} (f :: real \<Rightarrow> real)"
   4.167 +lemma set_borel_integrable_singleton[simp]: "set_integrable lborel {x} (f :: real \<Rightarrow> real)"
   4.168 +  unfolding set_integrable_def
   4.169    by (subst integrable_discrete_difference[where X="{x}" and g="\<lambda>_. 0"]) auto
   4.170  
   4.171  end