src/HOL/Probability/Distributions.thy
changeset 63886 685fb01256af
parent 63540 f8652d0534fa
child 63918 6bf55e6e0b75
     1.1 --- a/src/HOL/Probability/Distributions.thy	Thu Sep 15 22:41:05 2016 +0200
     1.2 +++ b/src/HOL/Probability/Distributions.thy	Fri Sep 16 13:56:51 2016 +0200
     1.3 @@ -608,7 +608,7 @@
     1.4      using D by (rule entropy_distr) simp
     1.5    also have "(\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel) =
     1.6      (\<integral> x. (ln l * exponential_density l x - l * (exponential_density l x * x)) / ln b \<partial>lborel)"
     1.7 -    by (intro integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps)
     1.8 +    by (intro Bochner_Integration.integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps)
     1.9    also have "\<dots> = (ln l - 1) / ln b"
    1.10      by simp
    1.11    finally show ?thesis
    1.12 @@ -750,7 +750,7 @@
    1.13      uniform_distributed_bounds[of X a b]
    1.14      uniform_distributed_measure[of X a b]
    1.15      distributed_measurable[of M lborel X]
    1.16 -  by (auto intro!: uniform_distrI_borel_atLeastAtMost)
    1.17 +  by (auto intro!: uniform_distrI_borel_atLeastAtMost simp del: content_real_if)
    1.18  
    1.19  lemma (in prob_space) uniform_distributed_expectation:
    1.20    fixes a b :: real
    1.21 @@ -762,13 +762,13 @@
    1.22  
    1.23    have "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) =
    1.24      (\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel)"
    1.25 -    by (intro integral_cong) auto
    1.26 +    by (intro Bochner_Integration.integral_cong) auto
    1.27    also have "(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel) = (a + b) / 2"
    1.28    proof (subst integral_FTC_Icc_real)
    1.29      fix x
    1.30      show "DERIV (\<lambda>x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}"
    1.31        using uniform_distributed_params[OF D]
    1.32 -      by (auto intro!: derivative_eq_intros)
    1.33 +      by (auto intro!: derivative_eq_intros simp del: content_real_if)
    1.34      show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x"
    1.35        using uniform_distributed_params[OF D]
    1.36        by (auto intro!: isCont_divide)
    1.37 @@ -791,12 +791,12 @@
    1.38    have [arith]: "a < b" using uniform_distributed_bounds[OF D] .
    1.39    let ?\<mu> = "expectation X" let ?D = "\<lambda>x. indicator {a..b} (x + ?\<mu>) / measure lborel {a..b}"
    1.40    have "(\<integral>x. x\<^sup>2 * (?D x) \<partial>lborel) = (\<integral>x. x\<^sup>2 * (indicator {a - ?\<mu> .. b - ?\<mu>} x) / measure lborel {a .. b} \<partial>lborel)"
    1.41 -    by (intro integral_cong) (auto split: split_indicator)
    1.42 +    by (intro Bochner_Integration.integral_cong) (auto split: split_indicator)
    1.43    also have "\<dots> = (b - a)\<^sup>2 / 12"
    1.44      by (simp add: integral_power uniform_distributed_expectation[OF D])
    1.45         (simp add: eval_nat_numeral field_simps )
    1.46    finally show "(\<integral>x. x\<^sup>2 * ?D x \<partial>lborel) = (b - a)\<^sup>2 / 12" .
    1.47 -qed (auto intro: D simp: measure_nonneg)
    1.48 +qed (auto intro: D simp del: content_real_if)
    1.49  
    1.50  subsection \<open>Normal distribution\<close>
    1.51  
    1.52 @@ -949,7 +949,7 @@
    1.53      proof (intro filterlim_cong refl eventually_at_top_linorder[THEN iffD2] exI[of _ 0] allI impI)
    1.54        fix b :: real assume b: "0 \<le> b"
    1.55        have "Suc k * (\<integral>x. indicator {0..b} x *\<^sub>R ?M k x \<partial>lborel) = (\<integral>x. indicator {0..b} x *\<^sub>R (exp (- x\<^sup>2) * ((Suc k) * x ^ k)) \<partial>lborel)"
    1.56 -        unfolding integral_mult_right_zero[symmetric] by (intro integral_cong) auto
    1.57 +        unfolding integral_mult_right_zero[symmetric] by (intro Bochner_Integration.integral_cong) auto
    1.58        also have "\<dots> = exp (- b\<^sup>2) * b ^ (Suc k) - exp (- 0\<^sup>2) * 0 ^ (Suc k) -
    1.59            (\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * x * exp (- x\<^sup>2) * x ^ (Suc k)) \<partial>lborel)"
    1.60          by (rule integral_by_parts')
    1.61 @@ -957,7 +957,7 @@
    1.62                   simp: diff_Suc of_nat_Suc field_simps split: nat.split)
    1.63        also have "(\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * x * exp (- x\<^sup>2) * x ^ (Suc k)) \<partial>lborel) =
    1.64          (\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * (exp (- x\<^sup>2) * x ^ (k + 2))) \<partial>lborel)"
    1.65 -        by (intro integral_cong) auto
    1.66 +        by (intro Bochner_Integration.integral_cong) auto
    1.67        finally have "Suc k * (\<integral>x. indicator {0..b} x *\<^sub>R ?M k x \<partial>lborel) =
    1.68          exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\<integral>x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \<partial>lborel)"
    1.69          by (simp del: real_scaleR_def integral_mult_right add: integral_mult_right[symmetric])
    1.70 @@ -1361,10 +1361,10 @@
    1.71    have "entropy b lborel X = - (\<integral> x. normal_density \<mu> \<sigma> x * log b (normal_density \<mu> \<sigma> x) \<partial>lborel)"
    1.72      using D by (rule entropy_distr) simp
    1.73    also have "\<dots> = - (\<integral> x. normal_density \<mu> \<sigma> x * (- ln (2 * pi * \<sigma>\<^sup>2) - (x - \<mu>)\<^sup>2 / \<sigma>\<^sup>2) / (2 * ln b) \<partial>lborel)"
    1.74 -    by (intro arg_cong[where f="uminus"] integral_cong)
    1.75 +    by (intro arg_cong[where f="uminus"] Bochner_Integration.integral_cong)
    1.76         (auto simp: normal_density_def field_simps ln_mult log_def ln_div ln_sqrt)
    1.77    also have "\<dots> = - (\<integral>x. - (normal_density \<mu> \<sigma> x * (ln (2 * pi * \<sigma>\<^sup>2)) + (normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2) / \<sigma>\<^sup>2) / (2 * ln b) \<partial>lborel)"
    1.78 -    by (intro arg_cong[where f="uminus"] integral_cong) (auto simp: divide_simps field_simps)
    1.79 +    by (intro arg_cong[where f="uminus"] Bochner_Integration.integral_cong) (auto simp: divide_simps field_simps)
    1.80    also have "\<dots> = (\<integral>x. normal_density \<mu> \<sigma> x * (ln (2 * pi * \<sigma>\<^sup>2)) + (normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2) / \<sigma>\<^sup>2 \<partial>lborel) / (2 * ln b)"
    1.81      by (simp del: minus_add_distrib)
    1.82    also have "\<dots> = (ln (2 * pi * \<sigma>\<^sup>2) + 1) / (2 * ln b)"