author paulson Thu Apr 12 12:16:34 2018 +0100 (13 months ago) changeset 67976 75b94eb58c3d parent 67975 27c8692825f6 child 67977 557ea2740125
Analysis builds using set_borel_measurable_def, etc.
```     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
```