Theory Finite_Fields.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