equal
deleted
inserted
replaced
370 (\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel)" |
370 (\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel)" |
371 by (intro integral_cong) auto |
371 by (intro integral_cong) auto |
372 also have "(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel) = (a + b) / 2" |
372 also have "(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel) = (a + b) / 2" |
373 proof (subst integral_FTC_atLeastAtMost) |
373 proof (subst integral_FTC_atLeastAtMost) |
374 fix x |
374 fix x |
375 show "DERIV (\<lambda>x. x ^ 2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}" |
375 show "DERIV (\<lambda>x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}" |
376 using uniform_distributed_params[OF D] |
376 using uniform_distributed_params[OF D] |
377 by (auto intro!: DERIV_intros) |
377 by (auto intro!: DERIV_intros) |
378 show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x" |
378 show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x" |
379 using uniform_distributed_params[OF D] |
379 using uniform_distributed_params[OF D] |
380 by (auto intro!: isCont_divide) |
380 by (auto intro!: isCont_divide) |