Quelle  Distributions.thy   Sprache: Isabelle

(x in M. X x \ a) = erlang_CDF k l a"
proof -
  have "emeasure M {x \ space M. X x \ a } = emeasure (distr M lborel X) {.. a}"
    using distributed_measurable[OF D]
    by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure])
  also have "\ = emeasure (density lborel (erlang_density k l)) {.. a}"
    unfolding distributed_distr_eq_density[OF D] ..
  also have "\ = erlang_CDF k l a"
    by (auto intro!: emeasure_erlang_density)
  finally show ?thesis
    by (auto simp: emeasure_eq_measure measure_nonneg)
qed

lemma (in prob_space) erlang_distributed_gt:
  assumes D[simp]: "distributed M lborel X (erlang_density k l)"
  assumes [arith]: "0 < l" "0 \ a"
  shows "\

(x in M. a < X x ) = 1 - (erlang_CDF k l a)"
proof -
  have " 1 - (erlang_CDF k l a) = 1 - \

(x in M. X x \ a)" by (subst erlang_distributed_le) auto
  also have "\ = prob (space M - {x \ space M. X x \ a })"
    using distributed_measurable[OF D] by (auto simp: prob_compl)
  also have "\ = \

(x in M. a < X x )" by (auto intro!: arg_cong[where f=prob] simp: not_le)
  finally show ?thesis by simp
qed

lemma erlang_CDF_at0: "erlang_CDF k l 0 = 0"
  by (induction k) (auto simp: erlang_CDF_def)

lemma erlang_distributedI:
  assumes X[measurable]: "X \ borel_measurable M" and [arith]: "0 < l"
    and X_distr: "\a. 0 \ a \ emeasure M {x\space M. X x \ a} = erlang_CDF k l a"
  shows "distributed M lborel X (erlang_density k l)"
proof (rule distributedI_borel_atMost)
  fix a :: real
  { assume "a \ 0"
    with X have "emeasure M {x\space M. X x \ a} \ emeasure M {x\space M. X x \ 0}"
      by (intro emeasure_mono) auto
    also have "... = 0"  by (auto intro!: erlang_CDF_at0 simp: X_distr[of 0])
    finally have "emeasure M {x\space M. X x \ a} \ 0" by simp
    then have "emeasure M {x\space M. X x \ a} = 0" by simp
  }
  note eq_0 = this

  show "(\\<^sup>+ x. erlang_density k l x * indicator {..a} x \lborel) = ennreal (erlang_CDF k l a)"
    using nn_integral_erlang_density[of l k a]
    by (simp add: ennreal_indicator ennreal_mult)

  show "emeasure M {x\space M. X x \ a} = ennreal (erlang_CDF k l a)"
    using X_distr[of a] eq_0 by (auto simp: one_ennreal_def erlang_CDF_def)
qed simp_all

lemma (in prob_space) erlang_distributed_iff:
  assumes [arith]: "0
  shows "distributed M lborel X (erlang_density k l) \
    (X \<in> borel_measurable M \<and> 0 < l \<and>  (\<forall>a\<ge>0. \<P>(x in M. X x \<le> a) = erlang_CDF k l a ))"
  using
    distributed_measurable[of M lborel X "erlang_density k l"]
    emeasure_erlang_density[of l]
    erlang_distributed_le[of X k l]
  by (auto intro!: erlang_distributedI simp: one_ennreal_def emeasure_eq_measure)

lemma (in prob_space) erlang_distributed_mult_const:
  assumes erlX: "distributed M lborel X (erlang_density k l)"
  assumes a_pos[arith]: "0 < \" "0 < l"
  shows  "distributed M lborel (\x. \ * X x) (erlang_density k (l / \))"
proof (subst erlang_distributed_iff, safe)
  have [measurable]: "random_variable borel X"  and  [arith]: "0 < l "
  and  [simp]: "\a. 0 \ a \ prob {x \ space M. X x \ a} = erlang_CDF k l a"
    by(insert erlX, auto simp: erlang_distributed_iff)

  show "random_variable borel (\x. \ * X x)" "0 < l / \" "0 < l / \"
    by (auto simp:field_simps)

  fix a:: real assume [arith]: "0 \ a"
  obtain b:: real  where [simp, arith]: "b = a/ \" by blast

  have [arith]: "0 \ b" by (auto simp: divide_nonneg_pos)

  have "prob {x \ space M. \ * X x \ a} = prob {x \ space M. X x \ b}"
    by (rule arg_cong[where f= prob]) (auto simp:field_simps)

  moreover have "prob {x \ space M. X x \ b} = erlang_CDF k l b" by auto
  moreover have "erlang_CDF k (l / \) a = erlang_CDF k l b" unfolding erlang_CDF_def by auto
  ultimately show "prob {x \ space M. \ * X x \ a} = erlang_CDF k (l / \) a" by fastforce
qed

lemma (in prob_space) has_bochner_integral_erlang_ith_moment:
  fixes k i :: nat and l :: real
  assumes [arith]: "0 < l" and D: "distributed M lborel X (erlang_density k l)"
  shows "has_bochner_integral M (\x. X x ^ i) (fact (k + i) / (fact k * l ^ i))"
proof (rule has_bochner_integral_nn_integral)
  show "AE x in M. 0 \ X x ^ i"
    by (subst distributed_AE2[OF D]) (auto simp: erlang_density_def)
  show "(\\<^sup>+ x. ennreal (X x ^ i) \M) = ennreal (fact (k + i) / (fact k * l ^ i))"
    using nn_integral_erlang_ith_moment[of l k i]
    by (subst distributed_nn_integral[symmetric, OF D]) (auto simp: ennreal_mult')
qed (insert distributed_measurable[OF D], auto)

lemma (in prob_space) erlang_ith_moment_integrable:
  "0 < l \ distributed M lborel X (erlang_density k l) \ integrable M (\x. X x ^ i)"
  by rule (rule has_bochner_integral_erlang_ith_moment)

lemma (in prob_space) erlang_ith_moment:
  "0 < l \ distributed M lborel X (erlang_density k l) \
    expectation (\<lambda>x. X x ^ i) = fact (k + i) / (fact k * l ^ i)"
  by (rule has_bochner_integral_integral_eq) (rule has_bochner_integral_erlang_ith_moment)

lemma (in prob_space) erlang_distributed_variance:
  assumes [arith]: "0 < l" and "distributed M lborel X (erlang_density k l)"
  shows "variance X = (k + 1) / l\<^sup>2"
proof (subst variance_eq)
  show "integrable M X" "integrable M (\x. (X x)\<^sup>2)"
    using erlang_ith_moment_integrable[OF assms, of 1] erlang_ith_moment_integrable[OF assms, of 2]
    by auto

  show "expectation (\x. (X x)\<^sup>2) - (expectation X)\<^sup>2 = real (k + 1) / l\<^sup>2"
    using erlang_ith_moment[OF assms, of 1] erlang_ith_moment[OF assms, of 2]
    by simp (auto simp: power2_eq_square field_simps of_nat_Suc)
qed

subsection \<open>Exponential distribution\<close>

abbreviation exponential_density :: "real \ real \ real" where
  "exponential_density \ erlang_density 0"

lemma exponential_density_def:
  "exponential_density l x = (if x < 0 then 0 else l * exp (- x * l))"
  by (simp add: fun_eq_iff erlang_density_def)

lemma erlang_CDF_0: "erlang_CDF 0 l a = (if 0 \ a then 1 - exp (- l * a) else 0)"
  by (simp add: erlang_CDF_def)

lemma prob_space_exponential_density: "0 < l \ prob_space (density lborel (exponential_density l))"
  by (rule prob_space_erlang_density)

lemma (in prob_space) exponential_distributedD_le:
  assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \ a" and l: "0 < l"
  shows "\

(x in M. X x \ a) = 1 - exp (- a * l)"
  using erlang_distributed_le[OF D l a] a by (simp add: erlang_CDF_def)

lemma (in prob_space) exponential_distributedD_gt:
  assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \ a" and l: "0 < l"
  shows "\

(x in M. a < X x ) = exp (- a * l)"
  using erlang_distributed_gt[OF D l a] a by (simp add: erlang_CDF_def)

lemma (in prob_space) exponential_distributed_memoryless:
  assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \ a" and l: "0 < l" and t: "0 \ t"
  shows "\

(x in M. a + t < X x \ a < X x) = \

(x in M. t < X x)"
proof -
  have "\

(x in M. a + t < X x \ a < X x) = \

(x in M. a + t < X x) / \

(x in M. a < X x)"
    using \<open>0 \<le> t\<close> by (auto simp: cond_prob_def intro!: arg_cong[where f=prob] arg_cong2[where f="(/)"])
  also have "\ = exp (- (a + t) * l) / exp (- a * l)"
    using a t by (simp add: exponential_distributedD_gt[OF D _ l])
  also have "\ = exp (- t * l)"
    using l by (auto simp: field_simps exp_add[symmetric])
  finally show ?thesis
    using t by (simp add: exponential_distributedD_gt[OF D _ l])
qed

lemma exponential_distributedI:
  assumes X[measurable]: "X \ borel_measurable M" and [arith]: "0 < l"
    and X_distr: "\a. 0 \ a \ emeasure M {x\space M. X x \ a} = 1 - exp (- a * l)"
  shows "distributed M lborel X (exponential_density l)"
proof (rule erlang_distributedI)
  fix a :: real assume "0 \ a" then show "emeasure M {x \ space M. X x \ a} = ennreal (erlang_CDF 0 l a)"
    using X_distr[of a] by (simp add: erlang_CDF_def ennreal_minus ennreal_1[symmetric] del: ennreal_1)
qed fact+

lemma (in prob_space) exponential_distributed_iff:
  assumes "0 < l"
  shows "distributed M lborel X (exponential_density l) \
    (X \<in> borel_measurable M \<and> (\<forall>a\<ge>0. \<P>(x in M. X x \<le> a) = 1 - exp (- a * l)))"
  using assms erlang_distributed_iff[of l X 0] by (auto simp: erlang_CDF_0)


lemma (in prob_space) exponential_distributed_expectation:
  "0 < l \ distributed M lborel X (exponential_density l) \ expectation X = 1 / l"
  using erlang_ith_moment[of l X 0 1] by simp

lemma exponential_density_nonneg: "0 < l \ 0 \ exponential_density l x"
  by (auto simp: exponential_density_def)

lemma (in prob_space) exponential_distributed_min:
  assumes "0 < l" "0 < u"
  assumes expX: "distributed M lborel X (exponential_density l)"
  assumes expY: "distributed M lborel Y (exponential_density u)"
  assumes ind: "indep_var borel X borel Y"
  shows "distributed M lborel (\x. min (X x) (Y x)) (exponential_density (l + u))"
proof (subst exponential_distributed_iff, safe)
  have randX: "random_variable borel X"
    using expX \<open>0 < l\<close> by (simp add: exponential_distributed_iff)
  moreover have randY: "random_variable borel Y"
    using expY \<open>0 < u\<close> by (simp add: exponential_distributed_iff)
  ultimately show "random_variable borel (\x. min (X x) (Y x))" by auto

  show " 0 < l + u"
    using \<open>0 < l\<close> \<open>0 < u\<close> by auto

  fix a::real assume a[arith]: "0 \ a"
  have gt1[simp]: "\

(x in M. a < X x ) = exp (- a * l)"
    by (rule exponential_distributedD_gt[OF expX a]) fact
  have gt2[simp]: "\

(x in M. a < Y x ) = exp (- a * u)"
    by (rule exponential_distributedD_gt[OF expY a]) fact

  have "\

(x in M. a < (min (X x) (Y x)) ) = \

(x in M. a < (X x) \ a < (Y x))" by (auto intro!:arg_cong[where f=prob])

  also have " ... = \

(x in M. a < (X x)) * \

(x in M. a< (Y x) )"
    using prob_indep_random_variable[OF ind, of "{a <..}" "{a <..}"] by simp
  also have " ... = exp (- a * (l + u))" by (auto simp:field_simps mult_exp_exp)
  finally have indep_prob: "\

(x in M. a < (min (X x) (Y x)) ) = exp (- a * (l + u))" .

  have "{x \ space M. (min (X x) (Y x)) \a } = (space M - {x \ space M. a<(min (X x) (Y x)) })"
    by auto
  then have "1 - prob {x \ space M. a < (min (X x) (Y x))} = prob {x \ space M. (min (X x) (Y x)) \ a}"
    using randX randY by (auto simp: prob_compl)
  then show "prob {x \ space M. (min (X x) (Y x)) \ a} = 1 - exp (- a * (l + u))"
    using indep_prob by auto
qed

lemma (in prob_space) exponential_distributed_Min:
  assumes finI: "finite I"
  assumes A: "I \ {}"
  assumes l: "\i. i \ I \ 0 < l i"
  assumes expX: "\i. i \ I \ distributed M lborel (X i) (exponential_density (l i))"
  assumes ind: "indep_vars (\i. borel) X I"
  shows "distributed M lborel (\x. Min ((\i. X i x)`I)) (exponential_density (\i\I. l i))"
using assms
proof (induct rule: finite_ne_induct)
  case (singleton i) then show ?case by simp
next
  case (insert i I)
  then have "distributed M lborel (\x. min (X i x) (Min ((\i. X i x)`I))) (exponential_density (l i + (\i\I. l i)))"
      by (intro exponential_distributed_min indep_vars_Min insert)
         (auto intro: indep_vars_subset sum_pos)
  then show ?case
    using insert by simp
qed

lemma (in prob_space) exponential_distributed_variance:
  "0 < l \ distributed M lborel X (exponential_density l) \ variance X = 1 / l\<^sup>2"
  using erlang_distributed_variance[of l X 0] by simp

lemma nn_integral_zero': "AE x in M. f x = 0 \ (\\<^sup>+x. f x \M) = 0"
  by (simp cong: nn_integral_cong_AE)

lemma convolution_erlang_density:
  fixes k\<^sub>1 k\<^sub>2 :: nat
  assumes [simp, arith]: "0 < l"
  shows "(\x. \\<^sup>+y. ennreal (erlang_density k\<^sub>1 l (x - y)) * ennreal (erlang_density k\<^sub>2 l y) \lborel) =
    (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)"
      (is "?LHS = ?RHS")
proof
  fix x :: real
  have "x \ 0 \ 0 < x"
    by arith
  then show "?LHS x = ?RHS x"
  proof
    assume "x \ 0" then show ?thesis
      apply (subst nn_integral_zero')
      apply (rule AE_I[where N="{0}"])
      apply (auto simp add: erlang_density_def not_less)
      done
  next
    note zero_le_mult_iff[simp] zero_le_divide_iff[simp]

    have I_eq1: "integral\<^sup>N lborel (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l) = 1"
      using nn_integral_erlang_ith_moment[of l "Suc k\<^sub>1 + Suc k\<^sub>2 - 1" 0] by (simp del: fact_Suc)

    have 1: "(\\<^sup>+ x. ennreal (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l x * indicator {0<..} x) \lborel) = 1"
      apply (subst I_eq1[symmetric])
      unfolding erlang_density_def
      by (auto intro!: nn_integral_cong split:split_indicator)

    have "prob_space (density lborel ?LHS)"
      by (intro prob_space_convolution_density)
         (auto intro!: prob_space_erlang_density erlang_density_nonneg)
    then have 2: "integral\<^sup>N lborel ?LHS = 1"
      by (auto dest!: prob_space.emeasure_space_1 simp: emeasure_density)

    let ?I = "(integral\<^sup>N lborel (\y. ennreal ((1 - y)^ k\<^sub>1 * y^k\<^sub>2 * indicator {0..1} y)))"
    let ?C = "(fact (Suc (k\<^sub>1 + k\<^sub>2))) / ((fact k\<^sub>1) * (fact k\<^sub>2))"
    let ?s = "Suc k\<^sub>1 + Suc k\<^sub>2 - 1"
    let ?L = "(\x. \\<^sup>+y. ennreal (erlang_density k\<^sub>1 l (x- y) * erlang_density k\<^sub>2 l y * indicator {0..x} y) \lborel)"

    { fix x :: real assume [arith]: "0 < x"
      have *: "\x y n. (x - y * x::real)^n = x^n * (1 - y)^n"
        unfolding power_mult_distrib[symmetric] by (simp add: field_simps)

      have "?LHS x = ?L x"
        unfolding erlang_density_def
        by (auto intro!: nn_integral_cong simp: ennreal_mult split:split_indicator)
      also have "... = (\x. ennreal ?C * ?I * erlang_density ?s l x) x"
        apply (subst nn_integral_real_affine[where c=x and t = 0])
        apply (simp_all add: nn_integral_cmult[symmetric] nn_integral_multc[symmetric] del: fact_Suc)
        apply (intro nn_integral_cong)
        apply (auto simp add: erlang_density_def mult_less_0_iff exp_minus field_simps exp_diff power_add *
                              ennreal_mult[symmetric]
                    simp del: fact_Suc split: split_indicator)
        done
      finally have "(\\<^sup>+y. ennreal (erlang_density k\<^sub>1 l (x - y) * erlang_density k\<^sub>2 l y) \lborel) =
        (\<lambda>x. ennreal ?C * ?I * erlang_density ?s l x) x"
        by (simp add: ennreal_mult) }
    note * = this

    assume [arith]: "0 < x"
    have 3: "1 = integral\<^sup>N lborel (\xa. ?LHS xa * indicator {0<..} xa)"
      by (subst 2[symmetric])
         (auto intro!: nn_integral_cong_AE AE_I[where N="{0}"]
               simp: erlang_density_def  nn_integral_multc[symmetric] indicator_def split: if_split_asm)
    also have "... = integral\<^sup>N lborel (\x. (ennreal (?C) * ?I) * ((erlang_density ?s l x) * indicator {0<..} x))"
      by (auto intro!: nn_integral_cong simp: ennreal_mult[symmetric] * split: split_indicator)
    also have "... = ennreal (?C) * ?I"
      using 1
      by (auto simp: nn_integral_cmult)
    finally have " ennreal (?C) * ?I = 1" by presburger

    then show ?thesis
      using * by (simp add: ennreal_mult)
  qed
qed

lemma (in prob_space) sum_indep_erlang:
  assumes indep: "indep_var borel X borel Y"
  assumes [simp, arith]: "0 < l"
  assumes erlX: "distributed M lborel X (erlang_density k\<^sub>1 l)"
  assumes erlY: "distributed M lborel Y (erlang_density k\<^sub>2 l)"
  shows "distributed M lborel (\x. X x + Y x) (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)"
  using assms
  apply (subst convolution_erlang_density[symmetric, OF \<open>0<l\<close>])
  apply (intro distributed_convolution)
  apply auto
  done

lemma (in prob_space) erlang_distributed_sum:
  assumes finI : "finite I"
  assumes A: "I \ {}"
  assumes [simp, arith]: "0 < l"
  assumes expX: "\i. i \ I \ distributed M lborel (X i) (erlang_density (k i) l)"
  assumes ind: "indep_vars (\i. borel) X I"
  shows "distributed M lborel (\x. \i\I. X i x) (erlang_density ((\i\I. Suc (k i)) - 1) l)"
using assms
proof (induct rule: finite_ne_induct)
  case (singleton i) then show ?case by auto
next
  case (insert i I)
    then have "distributed M lborel (\x. (X i x) + (\i\ I. X i x)) (erlang_density (Suc (k i) + Suc ((\i\I. Suc (k i)) - 1) - 1) l)"
      by(intro sum_indep_erlang indep_vars_sum) (auto intro!: indep_vars_subset)
    also have "(\x. (X i x) + (\i\ I. X i x)) = (\x. \i\insert i I. X i x)"
      using insert by auto
    also have "Suc(k i) + Suc ((\i\I. Suc (k i)) - 1) - 1 = (\i\insert i I. Suc (k i)) - 1"
      using insert by (auto intro!: Suc_pred simp: ac_simps)
    finally show ?case by fast
qed

lemma (in prob_space) exponential_distributed_sum:
  assumes finI: "finite I"
  assumes A: "I \ {}"
  assumes l: "0 < l"
  assumes expX: "\i. i \ I \ distributed M lborel (X i) (exponential_density l)"
  assumes ind: "indep_vars (\i. borel) X I"
  shows "distributed M lborel (\x. \i\I. X i x) (erlang_density ((card I) - 1) l)"
  using erlang_distributed_sum[OF assms] by simp

lemma (in information_space) entropy_exponential:
  assumes l[simp, arith]: "0 < l"
  assumes D: "distributed M lborel X (exponential_density l)"
  shows "entropy b lborel X = log b (exp 1 / l)"
proof -
  have [simp]: "integrable lborel (exponential_density l)"
    using distributed_integrable[OF D, of "\_. 1"] by simp

  have [simp]: "integral\<^sup>L lborel (exponential_density l) = 1"
    using distributed_integral[OF D, of "\_. 1"] by (simp add: prob_space)

  have [simp]: "integrable lborel (\x. exponential_density l x * x)"
    using erlang_ith_moment_integrable[OF l D, of 1] distributed_integrable[OF D, of "\x. x"] by simp

  have [simp]: "integral\<^sup>L lborel (\x. exponential_density l x * x) = 1 / l"
    using erlang_ith_moment[OF l D, of 1] distributed_integral[OF D, of "\x. x"] by simp

  have "entropy b lborel X = - (\ x. exponential_density l x * log b (exponential_density l x) \lborel)"
    using D by (rule entropy_distr) simp
  also have "(\ x. exponential_density l x * log b (exponential_density l x) \lborel) =
    (\<integral> x. (ln l * exponential_density l x - l * (exponential_density l x * x)) / ln b \<partial>lborel)"
    by (intro Bochner_Integration.integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps)
  also have "\ = (ln l - 1) / ln b"
    by simp
  finally show ?thesis
    by (simp add: log_def ln_div) (simp add: field_split_simps)
qed

subsection \<open>Uniform distribution\<close>

lemma uniform_distrI:
  assumes X: "X \ measurable M M'"
    and A: "A \ sets M'" "emeasure M' A \ \" "emeasure M' A \ 0"
  assumes distr: "\B. B \ sets M' \ emeasure M (X -` B \ space M) = emeasure M' (A \ B) / emeasure M' A"
  shows "distr M M' X = uniform_measure M' A"
  unfolding uniform_measure_def
proof (intro measure_eqI)
  let ?f = "\x. indicator A x / emeasure M' A"
  fix B assume B: "B \ sets (distr M M' X)"
  with X have "emeasure M (X -` B \ space M) = emeasure M' (A \ B) / emeasure M' A"
    by (simp add: distr[of B] measurable_sets)
  also have "\ = (1 / emeasure M' A) * emeasure M' (A \ B)"
     by (simp add: divide_ennreal_def ac_simps)
  also have "\ = (\\<^sup>+ x. (1 / emeasure M' A) * indicator (A \ B) x \M')"
    using A B
    by (intro nn_integral_cmult_indicator[symmetric]) (auto intro!: )
  also have "\ = (\\<^sup>+ x. ?f x * indicator B x \M')"
    by (rule nn_integral_cong) (auto split: split_indicator)
  finally show "emeasure (distr M M' X) B = emeasure (density M' ?f) B"
    using A B X by (auto simp add: emeasure_distr emeasure_density)
qed simp

lemma uniform_distrI_borel:
  fixes A :: "real set"
  assumes X[measurable]: "X \ borel_measurable M" and A: "emeasure lborel A = ennreal r" "0 < r"
    and [measurable]: "A \ sets borel"
  assumes distr: "\a. emeasure M {x\space M. X x \ a} = emeasure lborel (A \ {.. a}) / r"
  shows "distributed M lborel X (\x. indicator A x / measure lborel A)"
proof (rule distributedI_borel_atMost)
  let ?f = "\x. 1 / r * indicator A x"
  fix a
  have "emeasure lborel (A \ {..a}) \ emeasure lborel A"
    using A by (intro emeasure_mono) auto
  also have "\ < \"
    using A by simp
  finally have fin: "emeasure lborel (A \ {..a}) \ top"
    by simp
  from emeasure_eq_ennreal_measure[OF this]
  have fin_eq: "emeasure lborel (A \ {..a}) / r = ennreal (measure lborel (A \ {..a}) / r)"
    using A by (simp add: divide_ennreal measure_nonneg)
  then show "emeasure M {x\space M. X x \ a} = ennreal (measure lborel (A \ {..a}) / r)"
    using distr by simp

  have "(\\<^sup>+ x. ennreal (indicator A x / measure lborel A * indicator {..a} x) \lborel) =
    (\<integral>\<^sup>+ x. ennreal (1 / measure lborel A) * indicator (A \<inter> {..a}) x \<partial>lborel)"
    by (auto intro!: nn_integral_cong split: split_indicator)
  also have "\ = ennreal (1 / measure lborel A) * emeasure lborel (A \ {..a})"
    using \<open>A \<in> sets borel\<close>
    by (intro nn_integral_cmult_indicator) (auto simp: measure_nonneg)
  also have "\ = ennreal (measure lborel (A \ {..a}) / r)"
    unfolding emeasure_eq_ennreal_measure[OF fin] using A
    by (simp add: measure_def ennreal_mult'[symmetric])
  finally show "(\\<^sup>+ x. ennreal (indicator A x / measure lborel A * indicator {..a} x) \lborel) =
    ennreal (measure lborel (A \<inter> {..a}) / r)" .
qed (auto simp: measure_nonneg)

lemma (in prob_space) uniform_distrI_borel_atLeastAtMost:
  fixes a b :: real
  assumes X: "X \ borel_measurable M" and "a < b"
  assumes distr: "\t. a \ t \ t \ b \ \

(x in M. X x \ t) = (t - a) / (b - a)"
  shows "distributed M lborel X (\x. indicator {a..b} x / measure lborel {a..b})"
proof (rule uniform_distrI_borel)
  fix t
  have "t < a \ (a \ t \ t \ b) \ b < t"
    by auto
  then show "emeasure M {x\space M. X x \ t} = emeasure lborel ({a .. b} \ {..t}) / (b - a)"
  proof (elim disjE conjE)
    assume "t < a"
    then have "emeasure M {x\space M. X x \ t} \ emeasure M {x\space M. X x \ a}"
      using X by (auto intro!: emeasure_mono measurable_sets)
    also have "\ = 0"
      using distr[of a] \<open>a < b\<close> by (simp add: emeasure_eq_measure)
    finally have "emeasure M {x\space M. X x \ t} = 0"
      by (simp add: antisym measure_nonneg)
    with \<open>t < a\<close> show ?thesis by simp
  next
    assume bnds: "a \ t" "t \ b"
    have "{a..b} \ {..t} = {a..t}"
      using bnds by auto
    then show ?thesis using \<open>a \<le> t\<close> \<open>a < b\<close>
      using distr[OF bnds] by (simp add: emeasure_eq_measure divide_ennreal)
  next
    assume "b < t"
    have "1 = emeasure M {x\space M. X x \ b}"
      using distr[of b] \<open>a < b\<close> by (simp add: one_ennreal_def emeasure_eq_measure)
    also have "\ \ emeasure M {x\space M. X x \ t}"
      using X \<open>b < t\<close> by (auto intro!: emeasure_mono measurable_sets)
    finally have "emeasure M {x\space M. X x \ t} = 1"
       by (simp add: antisym emeasure_eq_measure)
    with \<open>b < t\<close> \<open>a < b\<close> show ?thesis by (simp add: measure_def divide_ennreal)
  qed
qed (insert X \<open>a < b\<close>, auto)

lemma (in prob_space) uniform_distributed_measure:
  fixes a b :: real
  assumes D: "distributed M lborel X (\x. indicator {a .. b} x / measure lborel {a .. b})"
  assumes t: "a \ t" "t \ b"
  shows "\

(x in M. X x \ t) = (t - a) / (b - a)"
proof -
  have "emeasure M {x \ space M. X x \ t} = emeasure (distr M lborel X) {.. t}"
    using distributed_measurable[OF D]
    by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure])
  also have "\ = (\\<^sup>+x. ennreal (1 / (b - a)) * indicator {a .. t} x \lborel)"
    using distributed_borel_measurable[OF D] \<open>a \<le> t\<close> \<open>t \<le> b\<close>
    unfolding distributed_distr_eq_density[OF D]
    by (subst emeasure_density)
       (auto intro!: nn_integral_cong simp: measure_def split: split_indicator)
  also have "\ = ennreal (1 / (b - a)) * (t - a)"
    using \<open>a \<le> t\<close> \<open>t \<le> b\<close>
    by (subst nn_integral_cmult_indicator) auto
  finally show ?thesis
    using t by (simp add: emeasure_eq_measure ennreal_mult''[symmetric] measure_nonneg)
qed

lemma (in prob_space) uniform_distributed_bounds:
  fixes a b :: real
  assumes D: "distributed M lborel X (\x. indicator {a .. b} x / measure lborel {a .. b})"
  shows "a < b"
proof (rule ccontr)
  assume "\ a < b"
  then have "{a .. b} = {} \ {a .. b} = {a .. a}" by simp
  with uniform_distributed_params[OF D] show False
    by (auto simp: measure_def)
qed

lemma (in prob_space) uniform_distributed_iff:
  fixes a b :: real
  shows "distributed M lborel X (\x. indicator {a..b} x / measure lborel {a..b}) \
    (X \<in> borel_measurable M \<and> a < b \<and> (\<forall>t\<in>{a .. b}. \<P>(x in M. X x \<le> t)= (t - a) / (b - a)))"
  using
    uniform_distributed_bounds[of X a b]
    uniform_distributed_measure[of X a b]
    distributed_measurable[of M lborel X]
  by (auto intro!: uniform_distrI_borel_atLeastAtMost simp del: content_real_if)

lemma (in prob_space) uniform_distributed_expectation:
  fixes a b :: real
  assumes D: "distributed M lborel X (\x. indicator {a .. b} x / measure lborel {a .. b})"
  shows "expectation X = (a + b) / 2"
proof (subst distributed_integral[OF D, of "\x. x", symmetric])
  have "a < b"
    using uniform_distributed_bounds[OF D] .

  have "(\ x. indicator {a .. b} x / measure lborel {a .. b} * x \lborel) =
    (\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel)"
    by (intro Bochner_Integration.integral_cong) auto
  also have "(\ x. (x / measure lborel {a .. b}) * indicator {a .. b} x \lborel) = (a + b) / 2"
  proof (subst integral_FTC_Icc_real)
    fix x
    show "DERIV (\x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}"
      using uniform_distributed_params[OF D]
      by (auto intro!: derivative_eq_intros simp del: content_real_if)
    show "isCont (\x. x / Sigma_Algebra.measure lborel {a..b}) x"
      using uniform_distributed_params[OF D]
      by (auto intro!: isCont_divide)
    have *: "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) =
      (b*b - a * a) / (2 * (b - a))"
      using \<open>a < b\<close>
      by (auto simp: measure_def power2_eq_square diff_divide_distrib[symmetric])
    show "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = (a + b) / 2"
      using \<open>a < b\<close>
      unfolding * square_diff_square_factored by (auto simp: field_simps)
  qed (insert \<open>a < b\<close>, simp)
  finally show "(\ x. indicator {a .. b} x / measure lborel {a .. b} * x \lborel) = (a + b) / 2" .
qed (auto simp: measure_nonneg)

lemma (in prob_space) uniform_distributed_variance:
  fixes a b :: real
  assumes D: "distributed M lborel X (\x. indicator {a .. b} x / measure lborel {a .. b})"
  shows "variance X = (b - a)\<^sup>2 / 12"
proof (subst distributed_variance)
  have [arith]: "a < b" using uniform_distributed_bounds[OF D] .
  let ?\<mu> = "expectation X" let ?D = "\<lambda>x. indicator {a..b} (x + ?\<mu>) / measure lborel {a..b}"
  have "(\x. x\<^sup>2 * (?D x) \lborel) = (\x. x\<^sup>2 * (indicator {a - ?\ .. b - ?\} x) / measure lborel {a .. b} \lborel)"
    by (intro Bochner_Integration.integral_cong) (auto split: split_indicator)
  also have "\ = (b - a)\<^sup>2 / 12"
    by (simp add: integral_power uniform_distributed_expectation[OF D])
       (simp add: eval_nat_numeral field_simps )
  finally show "(\x. x\<^sup>2 * ?D x \lborel) = (b - a)\<^sup>2 / 12" .
qed (auto intro: D simp del: content_real_if)

subsection \<open>Normal distribution\<close>


definition normal_density :: "real \ real \ real \ real" where
  "normal_density \ \ x = 1 / sqrt (2 * pi * \\<^sup>2) * exp (-(x - \)\<^sup>2/ (2 * \\<^sup>2))"

abbreviation std_normal_density :: "real \ real" where
  "std_normal_density \ normal_density 0 1"

lemma std_normal_density_def: "std_normal_density x = (1 / sqrt (2 * pi)) * exp (- x\<^sup>2 / 2)"
  unfolding normal_density_def by simp

lemma normal_density_nonneg[simp]: "0 \ normal_density \ \ x"
  by (auto simp: normal_density_def)

lemma normal_density_pos: "0 < \ \ 0 < normal_density \ \ x"
  by (auto simp: normal_density_def)

lemma borel_measurable_normal_density[measurable]: "normal_density \ \ \ borel_measurable borel"
  by (auto simp: normal_density_def[abs_def])

lemma gaussian_moment_0:
  "has_bochner_integral lborel (\x. indicator {0..} x *\<^sub>R exp (- x\<^sup>2)) (sqrt pi / 2)"
proof -
  let ?pI = "\f. (\\<^sup>+s. f (s::real) * indicator {0..} s \lborel)"
  let ?gauss = "\x. exp (- x\<^sup>2)"

  let ?I = "indicator {0<..} :: real \ real"
  let ?ff= "\x s. x * exp (- x\<^sup>2 * (1 + s\<^sup>2)) :: real"

  have *: "?pI ?gauss = (\\<^sup>+x. ?gauss x * ?I x \lborel)"
    by (intro nn_integral_cong_AE AE_I[where N="{0}"]) (auto split: split_indicator)

  have "?pI ?gauss * ?pI ?gauss = (\\<^sup>+x. \\<^sup>+s. ?gauss x * ?gauss s * ?I s * ?I x \lborel \lborel)"
    by (auto simp: nn_integral_cmult[symmetric] nn_integral_multc[symmetric] * ennreal_mult[symmetric]
             intro!: nn_integral_cong split: split_indicator)
  also have "\ = (\\<^sup>+x. \\<^sup>+s. ?ff x s * ?I s * ?I x \lborel \lborel)"
  proof (rule nn_integral_cong, cases)
    fix x :: real assume "x \ 0"
    then show "(\\<^sup>+s. ?gauss x * ?gauss s * ?I s * ?I x \lborel) = (\\<^sup>+s. ?ff x s * ?I s * ?I x \lborel)"
      by (subst nn_integral_real_affine[where t="0" and c="x"])
         (auto simp: mult_exp_exp nn_integral_cmult[symmetric] field_simps zero_less_mult_iff ennreal_mult[symmetric]
               intro!: nn_integral_cong split: split_indicator)
  qed simp
  also have "... = \\<^sup>+s. \\<^sup>+x. ?ff x s * ?I s * ?I x \lborel \lborel"
    by (rule lborel_pair.Fubini'[symmetric]) auto
  also have "... = ?pI (\s. ?pI (\x. ?ff x s))"
    by (rule nn_integral_cong_AE)
       (auto intro!: nn_integral_cong_AE AE_I[where N="{0}"] split: split_indicator_asm)
  also have "\ = ?pI (\s. ennreal (1 / (2 * (1 + s\<^sup>2))))"
  proof (intro nn_integral_cong ennreal_mult_right_cong)
    fix s :: real show "?pI (\x. ?ff x s) = ennreal (1 / (2 * (1 + s\<^sup>2)))"
    proof (subst nn_integral_FTC_atLeast)
      have "((\a. - (exp (- (a\<^sup>2 * (1 + s\<^sup>2))) / (2 + 2 * s\<^sup>2))) \ (- (0 / (2 + 2 * s\<^sup>2)))) at_top"
        apply (intro tendsto_intros filterlim_compose[OF exp_at_bot] filterlim_compose[OF filterlim_uminus_at_bot_at_top])
        apply (subst mult.commute)
        apply (auto intro!: filterlim_tendsto_pos_mult_at_top
                            filterlim_at_top_mult_at_top[OF filterlim_ident filterlim_ident]
                    simp: add_pos_nonneg  power2_eq_square add_nonneg_eq_0_iff)
        done
      then show "((\a. - (exp (- a\<^sup>2 - s\<^sup>2 * a\<^sup>2) / (2 + 2 * s\<^sup>2))) \ 0) at_top"
        by (simp add: field_simps)
    qed (auto intro!: derivative_eq_intros simp: field_simps add_nonneg_eq_0_iff)
  qed
  also have "... = ennreal (pi / 4)"
  proof (subst nn_integral_FTC_atLeast)
    show "((\a. arctan a / 2) \ (pi / 2) / 2 ) at_top"
      by (intro tendsto_intros) (simp_all add: tendsto_arctan_at_top)
  qed (auto intro!: derivative_eq_intros simp: add_nonneg_eq_0_iff field_simps power2_eq_square)
  finally have "?pI ?gauss^2 = pi / 4"
    by (simp add: power2_eq_square)
  then have "?pI ?gauss = sqrt (pi / 4)"
    using power_eq_iff_eq_base[of 2 "enn2real (?pI ?gauss)" "sqrt (pi / 4)"]
    by (cases "?pI ?gauss") (auto simp: power2_eq_square ennreal_mult[symmetric] ennreal_top_mult)
  also have "?pI ?gauss = (\\<^sup>+x. indicator {0..} x *\<^sub>R exp (- x\<^sup>2) \lborel)"
    by (intro nn_integral_cong) (simp split: split_indicator)
  also have "sqrt (pi / 4) = sqrt pi / 2"
    by (simp add: real_sqrt_divide)
  finally show ?thesis
    by (rule has_bochner_integral_nn_integral[rotated 3])
       auto
qed

lemma gaussian_moment_1:
  "has_bochner_integral lborel (\x::real. indicator {0..} x *\<^sub>R (exp (- x\<^sup>2) * x)) (1 / 2)"
proof -
  have "(\\<^sup>+x. indicator {0..} x *\<^sub>R (exp (- x\<^sup>2) * x) \lborel) =
    (\<integral>\<^sup>+x. ennreal (x * exp (- x\<^sup>2)) * indicator {0..} x \<partial>lborel)"
    by (intro nn_integral_cong)
       (auto simp: ac_simps split: split_indicator)
  also have "\ = ennreal (0 - (- exp (- 0\<^sup>2) / 2))"
  proof (rule nn_integral_FTC_atLeast)
    have "((\x::real. - exp (- x\<^sup>2) / 2) \ - 0 / 2) at_top"
      by (intro tendsto_divide tendsto_minus filterlim_compose[OF exp_at_bot]
                   filterlim_compose[OF filterlim_uminus_at_bot_at_top]
                   filterlim_pow_at_top filterlim_ident)
         auto
    then show "((\a::real. - exp (- a\<^sup>2) / 2) \ 0) at_top"
      by simp
  qed (auto intro!: derivative_eq_intros)
  also have "\ = ennreal (1 / 2)"
    by simp
  finally show ?thesis
    by (rule has_bochner_integral_nn_integral[rotated 3])
        (auto split: split_indicator)
qed

lemma
  fixes k :: nat
  shows gaussian_moment_even_pos:
    "has_bochner_integral lborel (\x::real. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k)))
       ((sqrt pi / 2) * (fact (2 * k) / (2 ^ (2 * k) * fact k)))"
       (is "?even")
    and gaussian_moment_odd_pos:
      "has_bochner_integral lborel (\x::real. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k + 1))) (fact k / 2)"
      (is "?odd")
proof -
  let ?M = "\k x. exp (- x\<^sup>2) * x^k :: real"

  { fix k I assume Mk: "has_bochner_integral lborel (\x. indicator {0..} x *\<^sub>R ?M k x) I"
    have "2 \ (0::real)"
      by linarith
    let ?f = "\b. \x. indicator {0..} x *\<^sub>R ?M (k + 2) x * indicator {..b} x \lborel"
    have "((\b. (k + 1) / 2 * (\x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x) \lborel) - ?M (k + 1) b / 2) \
        (k + 1) / 2 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>lborel) - 0 / 2) at_top" (is ?tendsto)
    proof (intro tendsto_intros \<open>2 \<noteq> 0\<close> tendsto_integral_at_top sets_lborel Mk[THEN integrable.intros])
      show "(?M (k + 1) \ 0) at_top"
      proof cases
        assume "even k"
        have "((\x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) \ 0 * 0) at_top"
          by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_compose[OF tendsto_power_div_exp_0]
                   filterlim_at_top_imp_at_infinity filterlim_ident filterlim_pow_at_top filterlim_ident)
             auto
        also have "(\x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) = ?M (k + 1)"
          using \<open>even k\<close> by (auto simp: fun_eq_iff exp_minus field_simps power2_eq_square power_mult elim: evenE)
        finally show ?thesis by simp
      next
        assume "odd k"
        have "((\x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) \ 0) at_top"
          by (intro filterlim_compose[OF tendsto_power_div_exp_0] filterlim_at_top_imp_at_infinity
                    filterlim_ident filterlim_pow_at_top)
             auto
        also have "(\x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) = ?M (k + 1)"
          using \<open>odd k\<close> by (auto simp: fun_eq_iff exp_minus field_simps power2_eq_square power_mult elim: oddE)
        finally show ?thesis by simp
      qed
    qed
    also have "?tendsto \ ((?f \ (k + 1) / 2 * (\x. indicator {0..} x *\<^sub>R ?M k x \lborel) - 0 / 2) at_top)"
    proof (intro filterlim_cong refl eventually_at_top_linorder[THEN iffD2] exI[of _ 0] allI impI)
      fix b :: real assume b: "0 \ b"
      have "Suc k * (\x. indicator {0..b} x *\<^sub>R ?M k x \lborel) = (\x. indicator {0..b} x *\<^sub>R (exp (- x\<^sup>2) * ((Suc k) * x ^ k)) \lborel)"
        unfolding integral_mult_right_zero[symmetric] by (intro Bochner_Integration.integral_cong) auto
      also have "\ = exp (- b\<^sup>2) * b ^ (Suc k) - exp (- 0\<^sup>2) * 0 ^ (Suc k) -
          (\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * x * exp (- x\<^sup>2) * x ^ (Suc k)) \<partial>lborel)"
        by (rule integral_by_parts')
           (auto intro!: derivative_eq_intros b
                 simp: diff_Suc of_nat_Suc field_simps split: nat.split)
      also have "... = exp (- b\<^sup>2) * b ^ (Suc k) - (\x. indicator {0..b} x *\<^sub>R (- 2 * (exp (- x\<^sup>2) * x ^ (k + 2))) \lborel)"
        by (auto simp: intro!: Bochner_Integration.integral_cong)
      also have "... = exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \lborel)"
        unfolding Bochner_Integration.integral_mult_right_zero [symmetric]
        by (simp del: real_scaleR_def)
      finally have "Suc k * (\x. indicator {0..b} x *\<^sub>R ?M k x \lborel) =
        exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\<integral>x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \<partial>lborel)" .
      then show "(k + 1) / 2 * (\x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x)\lborel) - exp (- b\<^sup>2) * b ^ (k + 1) / 2 = ?f b"
        by (simp add: field_simps atLeastAtMost_def indicator_inter_arith)
    qed
    finally have int_M_at_top: "((?f \ (k + 1) / 2 * (\x. indicator {0..} x *\<^sub>R ?M k x \lborel)) at_top)"
      by simp

    have "has_bochner_integral lborel (\x. indicator {0..} x *\<^sub>R ?M (k + 2) x) ((k + 1) / 2 * I)"
    proof (rule has_bochner_integral_monotone_convergence_at_top)
      fix y :: real
      have *: "(\x. indicator {0..} x *\<^sub>R ?M (k + 2) x * indicator {..y} x::real) =
            (\<lambda>x. indicator {0..y} x *\<^sub>R ?M (k + 2) x)"
        by rule (simp split: split_indicator)
      show "integrable lborel (\x. indicator {0..} x *\<^sub>R (?M (k + 2) x) * indicator {..y} x::real)"
        unfolding * by (rule borel_integrable_compact) (auto intro!: continuous_intros)
      show "((?f \ (k + 1) / 2 * I) at_top)"
        using int_M_at_top has_bochner_integral_integral_eq[OF Mk] by simp
    qed (auto split: split_indicator) }
  note step = this

  show ?even
  proof (induct k)
    case (Suc k)
    note step[OF this]
    also have "(real (2 * k + 1) / 2 * (sqrt pi / 2 * ((fact (2 * k)) / ((2::real)^(2*k) * fact k)))) =
      sqrt pi / 2 * ((fact (2 * Suc k)) / ((2::real)^(2 * Suc k) * fact (Suc k)))"
      apply (simp add: field_simps del: fact_Suc)
      apply (simp add: of_nat_mult field_simps)
      done
    finally show ?case
      by simp
  qed (insert gaussian_moment_0, simp)

  show ?odd
  proof (induct k)
    case (Suc k)
    note step[OF this]
    also have "(real (2 * k + 1 + 1) / (2::real) * ((fact k) / 2)) = (fact (Suc k)) / 2"
      by (simp add: field_simps of_nat_Suc field_split_simps del: fact_Suc) (simp add: field_simps)
    finally show ?case
      by simp
  qed (insert gaussian_moment_1, simp)
qed

context
  fixes k :: nat and \<mu> \<sigma> :: real assumes [arith]: "0 < \<sigma>"
begin

lemma normal_moment_even:
  "has_bochner_integral lborel (\x. normal_density \ \ x * (x - \) ^ (2 * k)) (fact (2 * k) / ((2 / \\<^sup>2)^k * fact k))"
proof -
  have eq: "\x::real. x\<^sup>2^k = (x^k)\<^sup>2"
    by (simp add: power_mult[symmetric] ac_simps)

  have "has_bochner_integral lborel (\x. exp (-x\<^sup>2)*x^(2 * k))
      (sqrt pi * (fact (2 * k) / (2 ^ (2 * k) * fact k)))"
    using has_bochner_integral_even_function[OF gaussian_moment_even_pos[where k=k]] by simp
  then have "has_bochner_integral lborel (\x. (exp (-x\<^sup>2)*x^(2 * k)) * ((2*\\<^sup>2)^k / sqrt (2 * pi * \\<^sup>2)))
      ((sqrt pi * (fact (2 * k) / (2 ^ (2 * k) * fact k))) * ((2*\<sigma>\<^sup>2)^k / sqrt (2 * pi * \<sigma>\<^sup>2)))"
    by (rule has_bochner_integral_mult_left)
  also have "(\x. (exp (-x\<^sup>2)*x^(2 * k)) * ((2*\\<^sup>2)^k / sqrt (2 * pi * \\<^sup>2))) =
    (\<lambda>x. exp (- ((sqrt 2 * \<sigma>) * x)\<^sup>2 / (2*\<sigma>\<^sup>2)) * ((sqrt 2 * \<sigma>) * x) ^ (2 * k) / sqrt (2 * pi * \<sigma>\<^sup>2))"
    by (auto simp: fun_eq_iff field_simps real_sqrt_power[symmetric] real_sqrt_mult
                   real_sqrt_divide power_mult eq)
  also have "((sqrt pi * (fact (2 * k) / (2 ^ (2 * k) * fact k))) * ((2*\\<^sup>2)^k / sqrt (2 * pi * \\<^sup>2))) =
    (inverse (sqrt 2 * \<sigma>) * ((fact (2 * k))) / ((2/\<sigma>\<^sup>2) ^ k * (fact k)))"
    by (auto simp: fun_eq_iff power_mult field_simps real_sqrt_power[symmetric] real_sqrt_mult
                   power2_eq_square)
  finally show ?thesis
    unfolding normal_density_def
    by (subst lborel_has_bochner_integral_real_affine_iff[where c="sqrt 2 * \" and t=\]) simp_all
qed

lemma normal_moment_abs_odd:
  "has_bochner_integral lborel (\x. normal_density \ \ x * \x - \\^(2 * k + 1)) (2^k * \^(2 * k + 1) * fact k * sqrt (2 / pi))"
proof -
  have "has_bochner_integral lborel (\x::real. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*\x\^(2 * k + 1))) (fact k / 2)"
    by (rule has_bochner_integral_cong[THEN iffD1, OF _ _ _ gaussian_moment_odd_pos[of k]]) auto
  from has_bochner_integral_even_function[OF this]
  have "has_bochner_integral lborel (\x::real. exp (-x\<^sup>2)*\x\^(2 * k + 1)) (fact k)"
    by simp
  then have "has_bochner_integral lborel (\x. (exp (-x\<^sup>2)*\x\^(2 * k + 1)) * (2^k * \^(2 * k + 1) / sqrt (pi * \\<^sup>2)))
      (fact k * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2)))"
    by (rule has_bochner_integral_mult_left)
  also have "(\x. (exp (-x\<^sup>2)*\x\^(2 * k + 1)) * (2^k * \^(2 * k + 1) / sqrt (pi * \\<^sup>2))) =
    (\<lambda>x. exp (- (((sqrt 2 * \<sigma>) * x)\<^sup>2 / (2 * \<sigma>\<^sup>2))) * \<bar>sqrt 2 * \<sigma> * x\<bar> ^ (2 * k + 1) / sqrt (2 * pi * \<sigma>\<^sup>2))"
    by (simp add: field_simps abs_mult real_sqrt_power[symmetric] power_mult real_sqrt_mult)
  also have "(fact k * (2^k * \^(2 * k + 1) / sqrt (pi * \\<^sup>2))) =
    (inverse (sqrt 2) * inverse \<sigma> * (2 ^ k * (\<sigma> * \<sigma> ^ (2 * k)) * (fact k) * sqrt (2 / pi)))"
    by (auto simp: fun_eq_iff power_mult field_simps real_sqrt_power[symmetric] real_sqrt_divide
                   real_sqrt_mult)
  finally show ?thesis
    unfolding normal_density_def
    by (subst lborel_has_bochner_integral_real_affine_iff[where c="sqrt 2 * \" and t=\])
       simp_all
qed

lemma normal_moment_odd:
  "has_bochner_integral lborel (\x. normal_density \ \ x * (x - \)^(2 * k + 1)) 0"
proof -
  have "has_bochner_integral lborel (\x. exp (- x\<^sup>2) * x^(2 * k + 1)::real) 0"
    using gaussian_moment_odd_pos by (rule has_bochner_integral_odd_function) simp
  then have "has_bochner_integral lborel (\x. (exp (-x\<^sup>2)*x^(2 * k + 1)) * (2^k*\^(2*k)/sqrt pi))
      (0 * (2^k*\<sigma>^(2*k)/sqrt pi))"
    by (rule has_bochner_integral_mult_left)
  also have "(\x. (exp (-x\<^sup>2)*x^(2 * k + 1)) * (2^k*\^(2*k)/sqrt pi)) =
    (\<lambda>x. exp (- ((sqrt 2 * \<sigma> * x)\<^sup>2 / (2 * \<sigma>\<^sup>2))) *
          (sqrt 2 * \<sigma> * x * (sqrt 2 * \<sigma> * x) ^ (2 * k)) /
          sqrt (2 * pi * \<sigma>\<^sup>2))"
    unfolding real_sqrt_mult
    by (simp add: field_simps abs_mult real_sqrt_power[symmetric] power_mult fun_eq_iff)
  finally show ?thesis
    unfolding normal_density_def
    by (subst lborel_has_bochner_integral_real_affine_iff[where c="sqrt 2 * \" and t=\]) simp_all
qed

lemma integral_normal_moment_even:
  "integral\<^sup>L lborel (\x. normal_density \ \ x * (x - \)^(2 * k)) = fact (2 * k) / ((2 / \\<^sup>2)^k * fact k)"
  using normal_moment_even by (rule has_bochner_integral_integral_eq)

lemma integral_normal_moment_abs_odd:
  "integral\<^sup>L lborel (\x. normal_density \ \ x * \x - \\^(2 * k + 1)) = 2 ^ k * \ ^ (2 * k + 1) * fact k * sqrt (2 / pi)"
  using normal_moment_abs_odd by (rule has_bochner_integral_integral_eq)

lemma integral_normal_moment_odd:
  "integral\<^sup>L lborel (\x. normal_density \ \ x * (x - \)^(2 * k + 1)) = 0"
  using normal_moment_odd by (rule has_bochner_integral_integral_eq)

end


context
  fixes \<sigma> :: real
  assumes \<sigma>_pos[arith]: "0 < \<sigma>"
begin

lemma normal_moment_nz_1: "has_bochner_integral lborel (\x. normal_density \ \ x * x) \"
proof -
  note normal_moment_even[OF \<sigma>_pos, of \<mu> 0]
  note normal_moment_odd[OF \<sigma>_pos, of \<mu> 0] has_bochner_integral_mult_left[of \<mu>, OF this]
  note has_bochner_integral_add[OF this]
  then show ?thesis
    by (simp add: power2_eq_square field_simps)
qed

lemma integral_normal_moment_nz_1:
  "integral\<^sup>L lborel (\x. normal_density \ \ x * x) = \"
  using normal_moment_nz_1 by (rule has_bochner_integral_integral_eq)

lemma integrable_normal_moment_nz_1: "integrable lborel (\x. normal_density \ \ x * x)"
  using normal_moment_nz_1 by rule

lemma integrable_normal_moment: "integrable lborel (\x. normal_density \ \ x * (x - \)^k)"
proof cases
  assume "even k" then show ?thesis
    using integrable.intros[OF normal_moment_even] by (auto elim: evenE)
next
  assume "odd k" then show ?thesis
    using integrable.intros[OF normal_moment_odd] by (auto elim: oddE)
qed

lemma integrable_normal_moment_abs: "integrable lborel (\x. normal_density \ \ x * \x - \\^k)"
proof cases
  assume "even k" then show ?thesis
    using integrable.intros[OF normal_moment_even] by (auto simp add: power_even_abs elim: evenE)
next
  assume "odd k" then show ?thesis
    using integrable.intros[OF normal_moment_abs_odd] by (auto elim: oddE)
qed

lemma integrable_normal_density[simp, intro]: "integrable lborel (normal_density \ \)"
  using integrable_normal_moment[of \<mu> 0] by simp

lemma integral_normal_density[simp]: "(\x. normal_density \ \ x \lborel) = 1"
  using integral_normal_moment_even[of \<sigma> \<mu> 0] by simp

lemma prob_space_normal_density:
  "prob_space (density lborel (normal_density \ \))"
  proof qed (simp add: emeasure_density nn_integral_eq_integral normal_density_nonneg)

end



context
  fixes k :: nat
begin

lemma std_normal_moment_even:
  "has_bochner_integral lborel (\x. std_normal_density x * x ^ (2 * k)) (fact (2 * k) / (2^k * fact k))"
  using normal_moment_even[of 1 0 k] by simp

lemma std_normal_moment_abs_odd:
  "has_bochner_integral lborel (\x. std_normal_density x * \x\^(2 * k + 1)) (sqrt (2/pi) * 2^k * fact k)"
  using normal_moment_abs_odd[of 1 0 k] by (simp add: ac_simps)

lemma std_normal_moment_odd:
  "has_bochner_integral lborel (\x. std_normal_density x * x^(2 * k + 1)) 0"
  using normal_moment_odd[of 1 0 k] by simp

lemma integral_std_normal_moment_even:
  "integral\<^sup>L lborel (\x. std_normal_density x * x^(2*k)) = fact (2 * k) / (2^k * fact k)"
  using std_normal_moment_even by (rule has_bochner_integral_integral_eq)

lemma integral_std_normal_moment_abs_odd:
  "integral\<^sup>L lborel (\x. std_normal_density x * \x\^(2 * k + 1)) = sqrt (2 / pi) * 2^k * fact k"
  using std_normal_moment_abs_odd by (rule has_bochner_integral_integral_eq)

lemma integral_std_normal_moment_odd:
  "integral\<^sup>L lborel (\x. std_normal_density x * x^(2 * k + 1)) = 0"
  using std_normal_moment_odd by (rule has_bochner_integral_integral_eq)

lemma integrable_std_normal_moment_abs: "integrable lborel (\x. std_normal_density x * \x\^k)"
  using integrable_normal_moment_abs[of 1 0 k] by simp

lemma integrable_std_normal_moment: "integrable lborel (\x. std_normal_density x * x^k)"
  using integrable_normal_moment[of 1 0 k] by simp

end

lemma (in prob_space) normal_density_affine:
  assumes X: "distributed M lborel X (normal_density \ \)"
  assumes [simp, arith]: "0 < \" "\ \ 0"
  shows "distributed M lborel (\x. \ + \ * X x) (normal_density (\ + \ * \) (\\\ * \))"
proof -
  have eq: "\x. \\\ * normal_density (\ + \ * \) (\\\ * \) (x * \ + \) =
    normal_density \<mu> \<sigma> x"
    by (simp add: normal_density_def real_sqrt_mult field_simps)
       (simp add: power2_eq_square field_simps)
  show ?thesis
    by (rule distributed_affineI[OF _ \<open>\<alpha> \<noteq> 0\<close>, where t=\<beta>])
       (simp_all add: eq X ennreal_mult'[symmetric])
qed

lemma (in prob_space) normal_standard_normal_convert:
  assumes pos_var[simp, arith]: "0 < \"
  shows "distributed M lborel X (normal_density \ \) = distributed M lborel (\x. (X x - \) / \) std_normal_density"
proof auto
  assume "distributed M lborel X (\x. ennreal (normal_density \ \ x))"
  then have "distributed M lborel (\x. -\ / \ + (1/\) * X x) (\x. ennreal (normal_density (-\ / \ + (1/\)* \) (\1/\\ * \) x))"
    by(rule normal_density_affine) auto

  then show "distributed M lborel (\x. (X x - \) / \) (\x. ennreal (std_normal_density x))"
    by (simp add: diff_divide_distrib[symmetric] field_simps)
next
  assume *: "distributed M lborel (\x. (X x - \) / \) (\x. ennreal (std_normal_density x))"
  have "distributed M lborel (\x. \ + \ * ((X x - \) / \)) (\x. ennreal (normal_density \ \\\ x))"
    using normal_density_affine[OF *, of \<sigma> \<mu>] by simp
  then show "distributed M lborel X (\x. ennreal (normal_density \ \ x))" by simp
qed

lemma conv_normal_density_zero_mean:
  assumes [simp, arith]: "0 < \" "0 < \"
  shows "(\x. \\<^sup>+y. ennreal (normal_density 0 \ (x - y) * normal_density 0 \ y) \lborel) =
    normal_density 0 (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2))"  (is "?LHS = ?RHS")
proof -
  define \<sigma>' \<tau>' where "\<sigma>' = \<sigma>\<^sup>2" and "\<tau>' = \<tau>\<^sup>2"
  then have [simp, arith]: "0 < \'" "0 < \'"
    by simp_all
  let ?\<sigma> = "sqrt ((\<sigma>' * \<tau>') / (\<sigma>' + \<tau>'))"
  have sqrt: "(sqrt (2 * pi * (\' + \')) * sqrt (2 * pi * (\' * \') / (\' + \'))) =
    (sqrt (2 * pi * \<sigma>') * sqrt (2 * pi * \<tau>'))"
    by (subst power_eq_iff_eq_base[symmetric, where n=2])
       (simp_all add: real_sqrt_mult[symmetric] power2_eq_square)
  have "?LHS =
--> --------------------

--> maximum size reached

--> --------------------

quality98%