src/HOL/Analysis/Ball_Volume.thy
changeset 67976 75b94eb58c3d
parent 67719 bffb7482faaa
child 67982 7643b005b29a
     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)