equal
deleted
inserted
replaced
1271 by (simp add: algebra_simps sum.distrib) |
1271 by (simp add: algebra_simps sum.distrib) |
1272 also have "\<dots> \<le> ?B" |
1272 also have "\<dots> \<le> ?B" |
1273 proof (rule add_mono) |
1273 proof (rule add_mono) |
1274 have "(\<Sum>k\<le>n. real k * e * ?\<mu> (T k)) = (\<Sum>k\<le>n. integral (T k) (\<lambda>x. k * e))" |
1274 have "(\<Sum>k\<le>n. real k * e * ?\<mu> (T k)) = (\<Sum>k\<le>n. integral (T k) (\<lambda>x. k * e))" |
1275 by (simp add: lmeasure_integral [OF meas_t] |
1275 by (simp add: lmeasure_integral [OF meas_t] |
1276 integral_mult_right [symmetric] integral_mult_left [symmetric] |
1276 reorient: integral_mult_right integral_mult_left) |
1277 del: integral_mult_right integral_mult_left) |
|
1278 also have "\<dots> \<le> (\<Sum>k\<le>n. integral (T k) (\<lambda>x. (abs (det (matrix (f' x))))))" |
1277 also have "\<dots> \<le> (\<Sum>k\<le>n. integral (T k) (\<lambda>x. (abs (det (matrix (f' x))))))" |
1279 proof (rule sum_mono) |
1278 proof (rule sum_mono) |
1280 fix k |
1279 fix k |
1281 assume "k \<in> {..n}" |
1280 assume "k \<in> {..n}" |
1282 show "integral (T k) (\<lambda>x. k * e) \<le> integral (T k) (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)" |
1281 show "integral (T k) (\<lambda>x. k * e) \<le> integral (T k) (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)" |