Theory Finite_Fields_More_PMF

section ‹Additional results about PMFs›

theory Finite_Fields_More_PMF
  imports "HOL-Probability.Probability_Mass_Function"
begin

lemma powr_mono_rev:
  fixes x :: real
  assumes "a  b" and  "x > 0" "x  1"
  shows "x powr b  x powr a"
proof -
  have "x powr b = (1/x) powr (-b)" using assms by (simp add: powr_divide powr_minus_divide)
  also have "...  (1/x) powr (-a)" using assms by (intro powr_mono) auto
  also have "... = x powr a" using assms by (simp add: powr_divide powr_minus_divide)
  finally show ?thesis by simp
qed

lemma integral_bind_pmf:
  fixes f :: "_  real"
  assumes "bounded (f ` set_pmf (bind_pmf p q))"
  shows "(x. f x bind_pmf p q) = (x. y. f y q x p)" (is "?L = ?R")
proof -
  obtain M where a:"¦f x¦  M" if "x  set_pmf (bind_pmf p q)" for x
    using assms(1) unfolding bounded_iff by auto
  define clamp where "clamp x = (if ¦x¦ > M then 0 else x) " for x

  obtain x where "x  set_pmf (bind_pmf p q)" using set_pmf_not_empty by fast
  hence M_ge_0: "M  0" using a by fastforce

  have a:"x y. x  set_pmf p  y  set_pmf (q x)  ¬¦f y¦ > M"
    using a by fastforce
  hence "(x. f x bind_pmf p q) = (x. clamp (f x) bind_pmf p q)"
    unfolding clamp_def by (intro integral_cong_AE AE_pmfI) auto
  also have "... =  (x. y. clamp (f y) q x p)" unfolding measure_pmf_bind 
    by (subst integral_bind[where K="count_space UNIV" and B'="1" and B="M"])
      (simp_all add:measure_subprob clamp_def M_ge_0)
  also have "... = ?R" unfolding clamp_def using a by (intro integral_cong_AE AE_pmfI) simp_all
  finally show ?thesis by simp
qed

lemma measure_bind_pmf:
  "measure (bind_pmf m f) s = (x. measure (f x) s m)" (is "?L = ?R")
proof -
  have "?L = (x. indicator s x bind_pmf m f)" by simp
  also have "... = (x. (y. indicator s y f x) m)"
    by (intro integral_bind_pmf) (auto intro!:boundedI)
  also have "... = ?R" by simp
  finally show ?thesis by simp
qed

end