Quelle Convolution.thy Sprache: Isabelle

(*  Title:      HOL/Probability/Convolution.thy
    Author:     Sudeep Kanav, TU München
    Author:     Johannes Hölzl, TU München *)

section \<open>Convolution Measure\<close>

theory Convolution
  imports Independent_Family
begin

lemma (in finite_measure) sigma_finite_measure: "sigma_finite_measure M"
  ..

definition convolution :: "('a :: ordered_euclidean_space) measure \ 'a measure \ 'a measure" (infix \\\ 50) where
  "convolution M N = distr (M \\<^sub>M N) borel (\(x, y). x + y)"

lemma
  shows space_convolution[simp]: "space (convolution M N) = space borel"
    and sets_convolution[simp]: "sets (convolution M N) = sets borel"
    and measurable_convolution1[simp]: "measurable A (convolution M N) = measurable A borel"
    and measurable_convolution2[simp]: "measurable (convolution M N) B = measurable borel B"
  by (simp_all add: convolution_def)

lemma nn_integral_convolution:
  assumes "finite_measure M" "finite_measure N"
  assumes [measurable_cong]: "sets N = sets borel" "sets M = sets borel"
  assumes [measurable]: "f \ borel_measurable borel"
  shows "(\\<^sup>+x. f x \convolution M N) = (\\<^sup>+x. \\<^sup>+y. f (x + y) \N \M)"
proof -
  interpret M: finite_measure M by fact
  interpret N: finite_measure N by fact
  interpret pair_sigma_finite M N ..
  show ?thesis
    unfolding convolution_def
    by (simp add: nn_integral_distr N.nn_integral_fst[symmetric])
qed

lemma convolution_emeasure:
  assumes "A \ sets borel" "finite_measure M" "finite_measure N"
  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
  assumes [simp]: "space M = space N" "space N = space borel"
  shows "emeasure (M \ N) A = \\<^sup>+x. (emeasure N {a. a + x \ A}) \M "
  using assms by (auto intro!: nn_integral_cong simp del: nn_integral_indicator simp: nn_integral_convolution
    nn_integral_indicator [symmetric] ac_simps split:split_indicator)

lemma convolution_emeasure':
  assumes [simp]:"A \ sets borel"
  assumes [simp]: "finite_measure M" "finite_measure N"
  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
  shows  "emeasure (M \ N) A = \\<^sup>+x. \\<^sup>+y. (indicator A (x + y)) \N \M"
  by (auto simp del: nn_integral_indicator simp: nn_integral_convolution
    nn_integral_indicator[symmetric] borel_measurable_indicator)

lemma convolution_finite:
  assumes [simp]: "finite_measure M" "finite_measure N"
  assumes [measurable_cong]: "sets N = sets borel" "sets M = sets borel"
  shows "finite_measure (M \ N)"
  unfolding convolution_def
  by (intro finite_measure_pair_measure finite_measure.finite_measure_distr) auto

lemma convolution_emeasure_3:
  assumes [simp, measurable]: "A \ sets borel"
  assumes [simp]: "finite_measure M" "finite_measure N" "finite_measure L"
  assumes [simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
  shows "emeasure (L \ (M \ N )) A = \\<^sup>+x. \\<^sup>+y. \\<^sup>+z. indicator A (x + y + z) \N \M \L"
  apply (subst nn_integral_indicator[symmetric], simp)
  apply (subst nn_integral_convolution,
        auto intro!: borel_measurable_indicator borel_measurable_indicator' convolution_finite)+
  by (rule nn_integral_cong)+ (auto simp: semigroup_add_class.add.assoc)

lemma convolution_emeasure_3':
  assumes [simp, measurable]:"A \ sets borel"
  assumes [simp]: "finite_measure M" "finite_measure N"  "finite_measure L"
  assumes [measurable_cong, simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
  shows "emeasure ((L \ M) \ N ) A = \\<^sup>+x. \\<^sup>+y. \\<^sup>+z. indicator A (x + y + z) \N \M \L"
  apply (subst nn_integral_indicator[symmetric], simp)+
  apply (subst nn_integral_convolution)
  apply (simp_all add: convolution_finite)
  apply (subst nn_integral_convolution)
  apply (simp_all add: finite_measure.sigma_finite_measure sigma_finite_measure.borel_measurable_nn_integral)
  done

lemma convolution_commutative:
  assumes [simp]: "finite_measure M" "finite_measure N"
  assumes [measurable_cong, simp]: "sets N = sets borel" "sets M = sets borel"
  shows "(M \ N) = (N \ M)"
proof (rule measure_eqI)
  interpret M: finite_measure M by fact
  interpret N: finite_measure N by fact
  interpret pair_sigma_finite M N ..

  show "sets (M \ N) = sets (N \ M)" by simp

  fix A assume "A \ sets (M \ N)"
  then have 1[measurable]:"A \ sets borel" by simp
  have "emeasure (M \ N) A = \\<^sup>+x. \\<^sup>+y. indicator A (x + y) \N \M" by (auto intro!: convolution_emeasure')
  also have "... = \\<^sup>+x. \\<^sup>+y. (\(x,y). indicator A (x + y)) (x, y) \N \M" by (auto intro!: nn_integral_cong)
  also have "... = \\<^sup>+y. \\<^sup>+x. (\(x,y). indicator A (x + y)) (x, y) \M \N" by (rule Fubini[symmetric]) simp
  also have "... = emeasure (N \ M) A" by (auto intro!: nn_integral_cong simp: add.commute convolution_emeasure')
  finally show "emeasure (M \ N) A = emeasure (N \ M) A" by simp
qed

lemma convolution_associative:
  assumes [simp]: "finite_measure M" "finite_measure N"  "finite_measure L"
  assumes [simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
  shows "(L \ (M \ N)) = ((L \ M) \ N)"
  by (auto intro!: measure_eqI simp: convolution_emeasure_3 convolution_emeasure_3')

lemma (in prob_space) sum_indep_random_variable:
  assumes ind: "indep_var borel X borel Y"
  assumes [simp, measurable]: "random_variable borel X"
  assumes [simp, measurable]: "random_variable borel Y"
  shows "distr M borel (\x. X x + Y x) = convolution (distr M borel X) (distr M borel Y)"
  using ind unfolding indep_var_distribution_eq convolution_def
  by (auto simp: distr_distr intro!:arg_cong[where f = "distr M borel"])

lemma (in prob_space) sum_indep_random_variable_lborel:
  assumes ind: "indep_var borel X borel Y"
  assumes [simp, measurable]: "random_variable lborel X"
  assumes [simp, measurable]:"random_variable lborel Y"
  shows "distr M lborel (\x. X x + Y x) = convolution (distr M lborel X) (distr M lborel Y)"
  using ind unfolding indep_var_distribution_eq convolution_def
  by (auto simp: distr_distr o_def intro!: arg_cong[where f = "distr M borel"] cong: distr_cong)

lemma convolution_density:
  fixes f g :: "real \ ennreal"
  assumes [measurable]: "f \ borel_measurable borel" "g \ borel_measurable borel"
  assumes [simp]:"finite_measure (density lborel f)" "finite_measure (density lborel g)"
  shows "density lborel f \ density lborel g = density lborel (\x. \\<^sup>+y. f (x - y) * g y \lborel)"
    (is "?l = ?r")
proof (intro measure_eqI)
  fix A assume "A \ sets ?l"
  then have [measurable]: "A \ sets borel"
    by simp

  have "(\\<^sup>+x. f x * (\\<^sup>+y. g y * indicator A (x + y) \lborel) \lborel) =
    (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. g y * (f x * indicator A (x + y)) \<partial>lborel) \<partial>lborel)"
  proof (intro nn_integral_cong_AE, eventually_elim)
    fix x
    have "f x * (\\<^sup>+ y. g y * indicator A (x + y) \lborel) =
      (\<integral>\<^sup>+ y. f x * (g y * indicator A (x + y)) \<partial>lborel)"
      by (intro nn_integral_cmult[symmetric]) auto
    then show "f x * (\\<^sup>+ y. g y * indicator A (x + y) \lborel) =
      (\<integral>\<^sup>+ y. g y * (f x * indicator A (x + y)) \<partial>lborel)"
      by (simp add: ac_simps)
  qed
  also have "\ = (\\<^sup>+y. (\\<^sup>+x. g y * (f x * indicator A (x + y)) \lborel) \lborel)"
    by (intro lborel_pair.Fubini') simp
  also have "\ = (\\<^sup>+y. (\\<^sup>+x. f (x - y) * g y * indicator A x \lborel) \lborel)"
  proof (intro nn_integral_cong_AE, eventually_elim)
    fix y
    have "(\\<^sup>+x. g y * (f x * indicator A (x + y)) \lborel) =
      g y * (\<integral>\<^sup>+x. f x * indicator A (x + y) \<partial>lborel)"
      by (intro nn_integral_cmult) auto
    also have "\ = g y * (\\<^sup>+x. f (x - y) * indicator A x \lborel)"
      by (subst nn_integral_real_affine[where c=1 and t="-y"])
         (auto simp add: one_ennreal_def[symmetric])
    also have "\ = (\\<^sup>+x. g y * (f (x - y) * indicator A x) \lborel)"
      by (intro nn_integral_cmult[symmetric]) auto
    finally show "(\\<^sup>+ x. g y * (f x * indicator A (x + y)) \lborel) =
      (\<integral>\<^sup>+ x. f (x - y) * g y * indicator A x \<partial>lborel)"
      by (simp add: ac_simps)
  qed
  also have "\ = (\\<^sup>+x. (\\<^sup>+y. f (x - y) * g y * indicator A x \lborel) \lborel)"
    by (intro lborel_pair.Fubini') simp
  finally show "emeasure ?l A = emeasure ?r A"
    by (auto simp: convolution_emeasure' nn_integral_density emeasure_density
      nn_integral_multc)
qed simp

lemma (in prob_space) distributed_finite_measure_density:
  "distributed M N X f \ finite_measure (density N f)"
  using finite_measure_distr[of X N] distributed_distr_eq_density[of M N X f] by simp

lemma (in prob_space) distributed_convolution:
  fixes f :: "real \ _"
  fixes g :: "real \ _"
  assumes indep: "indep_var borel X borel Y"
  assumes X: "distributed M lborel X f"
  assumes Y: "distributed M lborel Y g"
  shows "distributed M lborel (\x. X x + Y x) (\x. \\<^sup>+y. f (x - y) * g y \lborel)"
  unfolding distributed_def
proof safe
  have fg[measurable]: "f \ borel_measurable borel" "g \ borel_measurable borel"
    using distributed_borel_measurable[OF X] distributed_borel_measurable[OF Y] by simp_all

  show "(\x. \\<^sup>+ xa. f (x - xa) * g xa \lborel) \ borel_measurable lborel"
    by measurable

  have "distr M borel (\x. X x + Y x) = (distr M borel X \ distr M borel Y)"
    using distributed_measurable[OF X] distributed_measurable[OF Y]
    by (intro sum_indep_random_variable) (auto simp: indep)
  also have "\ = (density lborel f \ density lborel g)"
    using distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y]
    by (simp cong: distr_cong)
  also have "\ = density lborel (\x. \\<^sup>+ y. f (x - y) * g y \lborel)"
  proof (rule convolution_density)
    show "finite_measure (density lborel f)"
      using X by (rule distributed_finite_measure_density)
    show "finite_measure (density lborel g)"
      using Y by (rule distributed_finite_measure_density)
  qed fact+
  finally show "distr M lborel (\x. X x + Y x) = density lborel (\x. \\<^sup>+ y. f (x - y) * g y \lborel)"
    by (simp cong: distr_cong)
  show "random_variable lborel (\x. X x + Y x)"
    using distributed_measurable[OF X] distributed_measurable[OF Y] by simp
qed

lemma prob_space_convolution_density:
  fixes f:: "real \ _"
  fixes g:: "real \ _"
  assumes [measurable]: "f\ borel_measurable borel"
  assumes [measurable]: "g\ borel_measurable borel"
  assumes gt_0[simp]: "\x. 0 \ f x" "\x. 0 \ g x"
  assumes "prob_space (density lborel f)" (is "prob_space ?F")
  assumes "prob_space (density lborel g)" (is "prob_space ?G")
  shows "prob_space (density lborel (\x.\\<^sup>+y. f (x - y) * g y \lborel))" (is "prob_space ?D")
proof (subst convolution_density[symmetric])
  interpret F: prob_space ?F by fact
  show "finite_measure ?F" by unfold_locales
  interpret G: prob_space ?G by fact
  show "finite_measure ?G" by unfold_locales
  interpret FG: pair_prob_space ?F ?G ..

  show "prob_space (density lborel f \ density lborel g)"
    unfolding convolution_def by (rule FG.prob_space_distr) simp
qed simp_all

end

quality96%

¤ Dauer der Verarbeitung: 0.6 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.