Theory Measure_as_QuasiBorel_Measure

(*  Title:   Measure_as_QuasiBorel_Measure.thy
    Author:  Michikazu Hirata, Tokyo Institute of Technology

subsection ‹ Measure as QBS Measure›
theory Measure_as_QuasiBorel_Measure
  imports "Pair_QuasiBorel_Measure"


lemma distr_id':
  assumes "sets N = sets M"
          "f  N M N"
      and "x. x  space N  f x = x"
    shows "distr N M f = N"
proof(rule measure_eqI)
  fix A
  assume 0:"A  sets (distr N M f)"
  then have 1:"A  space N"
    by (auto simp: assms(1) sets.sets_into_space)

  have 2:"A  sets M"
    using 0 by simp
  have 3:"f  N M M"
    using assms(2) by(simp add: measurable_cong_sets[OF _ assms(1)])
  have "f -` A  space N = A"
  proof -
    have "f -` A = A  {x. x  space N  f x  A}"
      fix x
      assume h:"x  f -` A"
      consider "x  A" | "x  A"
        by auto
      thus "x  A  {x. x  space N  f x  A}"
      proof cases
        case 1
        then show ?thesis
          by simp
        case 2
        have "x  space N"
        proof(rule ccontr)
          assume "¬ x  space N"
          then have "x  space N"
            by simp
          hence "f x = x"
            by(simp add: assms(3))
          hence "f x  A"
            by(simp add: 2)
          thus False
            using h by simp
        thus ?thesis
          using h by simp
      fix x
      show "x  A  {x. x  space N  f x  A}  x  f -` A"
        using 1 assms by auto
    thus ?thesis
      using "1" by blast
  thus "emeasure (distr N M f) A = emeasure N A"
    by(simp add: emeasure_distr[OF 3 2])
qed (simp add: assms(1))

text ‹ Every probability measure on a standard Borel space can be represented as a measure on
       a quasi-Borel space~cite"Heunen_2017", Proposition 23.›
locale standard_borel_prob_space = standard_borel P + p:prob_space P
  for P :: "'a measure"

sublocale qbs_prob "measure_to_qbs P" g "distr P real_borel f"
  by(auto intro!: qbs_probI p.prob_space_distr)

lift_definition as_qbs_measure :: "'a qbs_prob_space" is
"(measure_to_qbs P, g, distr P real_borel f)"
  by simp

lemma as_qbs_measure_retract:
  assumes [measurable]:"a  P M real_borel"
      and [measurable]:"b  real_borel M P"
      and [simp]:"x. x  space P  (b  a) x = x"
    shows "qbs_prob (measure_to_qbs P) b (distr P real_borel a)"
          "as_qbs_measure = qbs_prob_space (measure_to_qbs P, b, distr P real_borel a)"
proof -
  interpret pqp: pair_qbs_prob "measure_to_qbs P" g "distr P real_borel f" "measure_to_qbs P" b "distr P real_borel a"
    by(auto intro!: qbs_probI p.prob_space_distr simp: pair_qbs_prob_def)
  show "qbs_prob (measure_to_qbs P) b (distr P real_borel a)"
       "as_qbs_measure = qbs_prob_space (measure_to_qbs P, b, distr P real_borel a)"
    by(auto intro!: pqp.qbs_prob_space_eq
          simp: distr_distr distr_id'[OF standard_borel_lr_sets_ident[symmetric]] distr_id'[OF standard_borel_lr_sets_ident[symmetric] _ assms(3)] pqp.qp2.qbs_prob_axioms as_qbs_measure.abs_eq)

lemma measure_as_qbs_measure_qbs:
 "qbs_prob_space_qbs as_qbs_measure = measure_to_qbs P"
  by transfer auto

lemma measure_as_qbs_measure_image:
 "as_qbs_measure  monadP_qbs_Px (measure_to_qbs P)"
  by(auto simp: measure_as_qbs_measure_qbs monadP_qbs_Px_def)

lemma as_qbs_measure_as_measure[simp]:
 "distr (distr P real_borel f) (qbs_to_measure (measure_to_qbs P)) g = P"
  by(auto intro!: distr_id'[OF standard_borel_lr_sets_ident[symmetric]] simp : qbs_prob_t_measure_def distr_distr )

lemma measure_as_qbs_measure_recover:
 "qbs_prob_measure as_qbs_measure = P"
  by transfer (simp add: qbs_prob_t_measure_def)


lemma(in standard_borel) qbs_prob_measure_recover:
  assumes "q  monadP_qbs_Px (measure_to_qbs M)"
  shows "standard_borel_prob_space.as_qbs_measure (qbs_prob_measure q) = q"
proof -
  obtain α μ where hq:
  "q = qbs_prob_space (measure_to_qbs M, α, μ)" "qbs_prob (measure_to_qbs M) α μ"
    using rep_monadP_qbs_Px[OF assms] by auto
  then interpret qp: qbs_prob "measure_to_qbs M" α μ by simp
  interpret sp: standard_borel_prob_space "distr μ (qbs_to_measure (measure_to_qbs M)) α"
    using qp.in_Mx
    by(auto intro!: prob_space.prob_space_distr
           simp: standard_borel_prob_space_def standard_borel_sets[OF sets_distr[of μ "qbs_to_measure (measure_to_qbs M)" α,simplified standard_borel_lr_sets_ident,symmetric]])
  interpret st: standard_borel "distr μ M α"
    by(auto intro!: standard_borel_sets)
  have [measurable]:"st.g  real_borel M M"
    using measurable_distr_eq2 st.g_meas by blast
  show ?thesis
    by(auto intro!: pair_qbs_prob.qbs_prob_space_eq
          simp add: hq(1) sp.as_qbs_measure.abs_eq pair_qbs_prob_def qp.qbs_prob_axioms sp.qbs_prob_axioms)
     (simp_all add: measure_to_qbs_cong_sets[OF sets_distr[of μ "qbs_to_measure (measure_to_qbs M)" α,simplified standard_borel_lr_sets_ident]])

lemma(in standard_borel_prob_space) ennintegral_as_qbs_ennintegral:
  assumes "k  borel_measurable P"
  shows "(+Q x. k x as_qbs_measure) = (+ x. k x P)"
proof -
  have 1:"k  measure_to_qbs P Q Q0"
    using assms by auto
  thus ?thesis
    by(simp add: as_qbs_measure.abs_eq qbs_prob_ennintegral_def2[OF 1])

lemma(in standard_borel_prob_space) integral_as_qbs_integral:
 "(Q x. k x as_qbs_measure) = ( x. k x P)"
  by(simp add: as_qbs_measure.abs_eq qbs_prob_integral_def2)

lemma(in standard_borel) measure_with_args_morphism:
  assumes [measurable]:"μ  X M prob_algebra M"
  shows "standard_borel_prob_space.as_qbs_measure  μ  measure_to_qbs X Q monadP_qbs (measure_to_qbs M)"
proof(auto intro!: qbs_morphismI)
  fix α
  assume h[measurable]:"α  real_borel M X"
  have "r. (standard_borel_prob_space.as_qbs_measure  μ  α) r = qbs_prob_space (measure_to_qbs M, g, ((λl. distr (μ l) real_borel f)  α) r)"
  proof auto
    fix r
    interpret sp: standard_borel_prob_space "μ (α r)"
      using measurable_space[OF assms measurable_space[OF h]]
      by(simp add: standard_borel_prob_space_def space_prob_algebra)
    have 1[measurable_cong]: "sets (μ (α r)) = sets M"
      using measurable_space[OF assms measurable_space[OF h]] by(simp add: space_prob_algebra)
    have 2:"f  μ (α r) M real_borel" "g  real_borel M μ (α r)" "x. x  space (μ (α r))  (g  f) x = x"
      using measurable_space[OF assms measurable_space[OF h]]
      by(simp_all add: standard_borel_prob_space_def sets_eq_imp_space_eq[OF 1])
    show "standard_borel_prob_space.as_qbs_measure (μ (α r)) = qbs_prob_space (measure_to_qbs M, g, distr (μ (α r)) real_borel f)"
      by(simp add: sp.as_qbs_measure_retract[OF 2] measure_to_qbs_cong_sets[OF  subprob_measurableD(2)[OF measurable_prob_algebraD[OF assms] measurable_space[OF h]]])
  thus "standard_borel_prob_space.as_qbs_measure  μ  α  monadP_qbs_MPx (measure_to_qbs M)"
    by(auto intro!: bexI[where x=g] bexI[where x="(λl. distr (μ l) real_borel f)  α"] simp: monadP_qbs_MPx_def in_MPx_def)

lemma(in standard_borel) measure_with_args_recover:
  assumes "μ  space X  space (prob_algebra M)"
      and "x  space X"
    shows "qbs_prob_measure (standard_borel_prob_space.as_qbs_measure (μ x)) = μ x"
    using standard_borel_sets[of "μ x"] funcset_mem[OF assms]
    by(simp add: standard_borel_prob_space_def space_prob_algebra standard_borel_prob_space.measure_as_qbs_measure_recover)

subsection ‹Example of Probability Measures›
text ‹Probability measures on $\mathbb{R}$ can be represented as probability measures on the quasi-Borel space $\mathbb{R}$.›
subsubsection ‹ Normal Distribution ›
definition normal_distribution :: "real × real  real measure" where
"normal_distribution μσ = (if 0 < (snd μσ) then density lborel (λx. ennreal (normal_density (fst μσ) (snd μσ) x))
                                      else return lborel 0)"

lemma normal_distribution_measurable:
 "normal_distribution  real_borel M real_borel M prob_algebra real_borel"
proof(rule measurable_prob_algebra_generated[where Ω=UNIV and G=borel])
  fix A :: "real set"
  assume h:"A  sets borel"
  have "(λx. emeasure (normal_distribution x) A) = (λx. if 0 < (snd x) then emeasure (density lborel (λr. ennreal (normal_density (fst x) (snd x) r))) A
                                                                                     else emeasure (return lborel 0) A)"
    by(auto simp add: normal_distribution_def)
  also have "...  borel_measurable (borel M borel)"
  proof(rule measurable_If)
    have [simp]:"(λx. indicat_real A (snd x))  borel_measurable ((borel M borel) M borel)"
    proof -
      have "(λx. indicat_real A (snd x)) = indicat_real A  snd"
        by auto
      also have "...  borel_measurable ((borel M borel) M borel)"
        by (meson borel_measurable_indicator h measurable_comp measurable_snd)
      finally show ?thesis .
    have "(λx. emeasure (density lborel (λr. ennreal (normal_density (fst x) (snd x) r))) A) = (λx. set_nn_integral lborel A (λr. ennreal (normal_density (fst x) (snd x) r)))"
      using h by(auto intro!: emeasure_density)
    also have "... = (λx. +r. ennreal (normal_density (fst x) (snd x) r * indicat_real A r)lborel)"
      by(simp add: nn_integral_set_ennreal)
    also have "...  borel_measurable (borel M borel)"
      apply(auto intro!: lborel.borel_measurable_nn_integral
                   simp: split_beta' measurable_cong_sets[OF sets_pair_measure_cong[OF refl sets_lborel]] )
      unfolding normal_density_def
      by(rule borel_measurable_times) simp_all
    finally show "(λx. emeasure (density lborel (λr. ennreal (normal_density (fst x) (snd x) r))) A)  borel_measurable (borel M borel)" .
  qed simp_all
  finally show "(λx. emeasure (normal_distribution x) A)  borel_measurable (borel M borel)" .
qed (auto simp add: sets.sigma_sets_eq[of borel,simplified] sets.Int_stable prob_space_normal_density normal_distribution_def prob_space_return)

definition qbs_normal_distribution :: "real  real  real qbs_prob_space" where
"qbs_normal_distribution  curry (standard_borel_prob_space.as_qbs_measure  normal_distribution)"

lemma qbs_normal_distribution_morphism:
 "qbs_normal_distribution  Q Q exp_qbs Q (monadP_qbs Q)"
  unfolding qbs_normal_distribution_def
  by(rule curry_preserves_morphisms[OF real.measure_with_args_morphism[OF normal_distribution_measurable,simplified r_preserves_product]])

  fixes μ σ :: real
  assumes sigma:"σ > 0"

interpretation n_dist:standard_borel_prob_space "normal_distribution (μ,σ)"
  by(simp add: standard_borel_prob_space_def sigma prob_space_normal_density normal_distribution_def) 

lemma qbs_normal_distribution_def2:
 "qbs_normal_distribution μ σ = n_dist.as_qbs_measure"
  by(simp add: qbs_normal_distribution_def)

lemma qbs_normal_distribution_integral:
 "(Q x. f x  (qbs_normal_distribution μ σ)) = ( x. f x  (density lborel (λx. ennreal (normal_density μ σ x))))"
  by(simp add: qbs_normal_distribution_def2 n_dist.integral_as_qbs_integral)
    (simp add: normal_distribution_def sigma)

lemma qbs_normal_distribution_expectation:
  assumes "f  real_borel M real_borel"
    shows "(Q x. f x  (qbs_normal_distribution μ σ)) = ( x. normal_density μ σ x * f x  lborel)"
  by(simp add: qbs_normal_distribution_integral assms integral_real_density integral_density)


subsubsection ‹ Uniform Distribution ›
definition interval_uniform_distribution :: "real  real  real measure" where
"interval_uniform_distribution a b  (if a < b then uniform_measure lborel {a<..<b}
                                               else return lborel 0)"

lemma sets_interval_uniform_distribution[measurable_cong]:
 "sets (interval_uniform_distribution a b) = borel"
  by(simp add: interval_uniform_distribution_def)

lemma interval_uniform_distribution_meaurable:
 "(λr. interval_uniform_distribution (fst r) (snd r))  real_borel M real_borel M prob_algebra real_borel"
proof(rule measurable_prob_algebra_generated[where Ω=UNIV and G="range (λ(a, b). {a<..<b})"])
  show "sets real_borel = sigma_sets UNIV (range (λ(a, b). {a<..<b}))"
    by(simp add: borel_eq_box)
  show "Int_stable (range (λ(a, b). {a<..<b::real}))"
    by(fastforce intro!: Int_stableI simp: split_beta' image_iff)
  show "range (λ(a, b). {a<..<b})  Pow UNIV"
    by simp
  fix a
  show "prob_space (interval_uniform_distribution (fst a) (snd a))"
    by(simp add: interval_uniform_distribution_def prob_space_return prob_space_uniform_measure)
  fix a
  show " sets (interval_uniform_distribution (fst a) (snd a)) = sets real_borel"
    by(simp add: interval_uniform_distribution_def)
  fix A
  assume "A  range (λ(a, b). {a<..<b::real})"
  then obtain a b where ha:"A = {a<..<b}" by auto
  consider  "b  a" | "a < b" by fastforce
  then show "(λx. emeasure (interval_uniform_distribution (fst x) (snd x)) A)  real_borel M real_borel M ennreal_borel"
             (is "?f  ?meas")
  proof cases
    case 1
    then show ?thesis
      by(simp add: ha)
    case h2:2
    have "?f = (λx. if fst x < snd x then ennreal (min (snd x) b - max (fst x) a) / ennreal (snd x - fst x) else indicator A 0)"
    proof(standard; auto simp: interval_uniform_distribution_def ha)
      fix x y :: real
      assume hxy:"x < y"
      consider "b  x" | "a  x  x < b" | "x < a  a < y" | "y  a"
        using h2 by fastforce
      thus "emeasure lborel ({max x a<..<min y b}) / ennreal (y - x) = ennreal (min y b - max x a) / ennreal (y - x)"
        by cases (use hxy ennreal_neg h2 in auto)
    also have "...  ?meas"
      by simp
    finally show ?thesis .

definition qbs_interval_uniform_distribution :: "real  real  real qbs_prob_space" where
"qbs_interval_uniform_distribution  curry (standard_borel_prob_space.as_qbs_measure  (λr. interval_uniform_distribution (fst r) (snd r)))"

lemma qbs_interval_uniform_distribution_morphism:
 "qbs_interval_uniform_distribution  Q Q exp_qbs Q (monadP_qbs Q)"
  unfolding qbs_interval_uniform_distribution_def
  using curry_preserves_morphisms[OF real.measure_with_args_morphism[OF interval_uniform_distribution_meaurable,simplified r_preserves_product]] .

  fixes a b :: real
  assumes a_less_than_b:"a < b"

definition "ab_qbs_uniform_distribution  qbs_interval_uniform_distribution a b"

interpretation ab_u_dist: standard_borel_prob_space "interval_uniform_distribution a b"
  by(auto intro!: prob_space_uniform_measure simp: interval_uniform_distribution_def standard_borel_prob_space_def prob_space_return)

lemma qbs_interval_uniform_distribution_def2:
 "ab_qbs_uniform_distribution = ab_u_dist.as_qbs_measure"
  by(simp add: qbs_interval_uniform_distribution_def ab_qbs_uniform_distribution_def)

lemma qbs_uniform_distribution_expectation:
  assumes "f  Q Q Q0"
  shows "(+Q x. f x ab_qbs_uniform_distribution) = (+x  {a<..<b}. f x lborel) / (b - a)"
        (is "?lhs = ?rhs")
proof -
  have "?lhs = (+x. f x (interval_uniform_distribution a b))"
    using assms by(auto simp: qbs_interval_uniform_distribution_def2 intro!:ab_u_dist.ennintegral_as_qbs_ennintegral dest:ab_u_dist.qbs_morphism_dest[simplified measure_to_qbs_cong_sets[OF sets_interval_uniform_distribution]])
  also have "... = ?rhs"
    using assms
    by(auto simp: interval_uniform_distribution_def a_less_than_b intro!:nn_integral_uniform_measure[where M=lborel and S="{a<..<b}",simplified emeasure_lborel_Ioo[OF order.strict_implies_order[OF a_less_than_b]]])
  finally show ?thesis .


subsubsection ‹ Bernoulli Distribution ›
definition qbs_bernoulli :: "real  bool qbs_prob_space" where
"qbs_bernoulli  standard_borel_prob_space.as_qbs_measure  (λx. measure_pmf (bernoulli_pmf x))"

lemma bernoulli_measurable:
 "(λx. measure_pmf (bernoulli_pmf x))  real_borel M prob_algebra bool_borel"
proof(rule measurable_prob_algebra_generated[where Ω=UNIV and G=UNIV],simp_all)
  fix A :: "bool set"
  have "A  {True,False}"
    by auto
  then consider "A = {}" | "A = {True}" | "A = {False}" | "A = {False,True}"
    by auto
  thus "(λa. emeasure (measure_pmf (bernoulli_pmf a)) A)  borel_measurable borel"
    by(cases,simp_all add: emeasure_measure_pmf_finite bernoulli_pmf.rep_eq UNIV_bool[symmetric])
qed (auto simp add: sets_borel_eq_count_space Int_stable_def measure_pmf.prob_space_axioms)

lemma qbs_bernoulli_morphism:
 "qbs_bernoulli  Q Q monadP_qbs 𝔹Q"
  using bool.measure_with_args_morphism[OF bernoulli_measurable]
  by (simp add: qbs_bernoulli_def)

lemma qbs_bernoulli_measure:
 "qbs_prob_measure (qbs_bernoulli p) = measure_pmf (bernoulli_pmf p)"
  using bool.measure_with_args_recover[of "λx. measure_pmf (bernoulli_pmf x)" real_borel p] bernoulli_measurable
  by(simp add: measurable_def qbs_bernoulli_def)

  fixes p :: real
  assumes pgeq_0[simp]:"0  p" and pleq_1[simp]:"p  1"

lemma qbs_bernoulli_expectation:
  "(Q x. f x qbs_bernoulli p) = f True * p + f False * (1 - p)"
  by(simp add: qbs_prob_integral_def2 qbs_bernoulli_measure)