equal
deleted
inserted
replaced
142 (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel)" |
142 (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel)" |
143 by (subst nn_integral_cmult [symmetric]) |
143 by (subst nn_integral_cmult [symmetric]) |
144 (auto simp: mult_ac ennreal_mult' [symmetric] indicator_def intro!: nn_integral_cong) |
144 (auto simp: mult_ac ennreal_mult' [symmetric] indicator_def intro!: nn_integral_cong) |
145 also have "(\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel) = |
145 also have "(\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel) = |
146 (\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A |
146 (\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A |
147 \<partial>(distr lborel borel (op * (1/r))))" using \<open>r > 0\<close> |
147 \<partial>(distr lborel borel (( * ) (1/r))))" using \<open>r > 0\<close> |
148 by (subst nn_integral_distr) |
148 by (subst nn_integral_distr) |
149 (auto simp: indicator_def field_simps real_sqrt_divide intro!: nn_integral_cong) |
149 (auto simp: indicator_def field_simps real_sqrt_divide intro!: nn_integral_cong) |
150 also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) * |
150 also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) * |
151 (indicator {- 1..1} x * sqrt (1 - x\<^sup>2) ^ card A) \<partial>lborel)" using \<open>r > 0\<close> |
151 (indicator {- 1..1} x * sqrt (1 - x\<^sup>2) ^ card A) \<partial>lborel)" using \<open>r > 0\<close> |
152 by (subst lborel_distr_mult) (auto simp: nn_integral_density ennreal_mult' [symmetric] mult_ac) |
152 by (subst lborel_distr_mult) (auto simp: nn_integral_density ennreal_mult' [symmetric] mult_ac) |