src/HOL/Analysis/Ball_Volume.thy
changeset 69064 5840724b1d71
parent 68624 205d352ed727
child 69517 dc20f278e8f3
     1.1 --- a/src/HOL/Analysis/Ball_Volume.thy	Sun Sep 23 21:49:31 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Ball_Volume.thy	Mon Sep 24 14:30:09 2018 +0200
     1.3 @@ -147,7 +147,7 @@
     1.4         (auto simp: mult_ac ennreal_mult' [symmetric] indicator_def intro!: nn_integral_cong)
     1.5    also have "(\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel) =
     1.6                 (\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A  
     1.7 -               \<partial>(distr lborel borel (( * ) (1/r))))" using \<open>r > 0\<close>
     1.8 +               \<partial>(distr lborel borel ((*) (1/r))))" using \<open>r > 0\<close>
     1.9      by (subst nn_integral_distr)
    1.10         (auto simp: indicator_def field_simps real_sqrt_divide intro!: nn_integral_cong)
    1.11    also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) *