Theory Density_Predicates
section ‹Density Predicates›
theory Density_Predicates
imports "HOL-Probability.Probability"
begin
subsection ‹Probability Densities›
definition is_subprob_density :: "'a measure ⇒ ('a ⇒ ennreal) ⇒ bool" where
"is_subprob_density M f ≡ (f ∈ borel_measurable M) ∧ space M ≠ {} ∧
(∀x∈space M. f x ≥ 0) ∧ (∫⇧+x. f x ∂M) ≤ 1"
lemma is_subprob_densityI[intro]:
"⟦f ∈ borel_measurable M; ⋀x. x ∈ space M ⟹ f x ≥ 0; space M ≠ {}; (∫⇧+x. f x ∂M) ≤ 1⟧
⟹ is_subprob_density M f"
unfolding is_subprob_density_def by simp
lemma is_subprob_densityD[dest]:
"is_subprob_density M f ⟹ f ∈ borel_measurable M"
"is_subprob_density M f ⟹ x ∈ space M ⟹ f x ≥ 0"
"is_subprob_density M f ⟹ space M ≠ {}"
"is_subprob_density M f ⟹ (∫⇧+x. f x ∂M) ≤ 1"
unfolding is_subprob_density_def by simp_all
subsection ‹Measure spaces with densities›
definition has_density :: "'a measure ⇒ 'a measure ⇒ ('a ⇒ ennreal) ⇒ bool" where
"has_density M N f ⟷ (f ∈ borel_measurable N) ∧ space N ≠ {} ∧ M = density N f"
lemma has_densityI[intro]:
"⟦f ∈ borel_measurable N; M = density N f; space N ≠ {}⟧ ⟹ has_density M N f"
unfolding has_density_def by blast
lemma has_densityD:
assumes "has_density M N f"
shows "f ∈ borel_measurable N" "M = density N f" "space N ≠ {}"
using assms unfolding has_density_def by simp_all
lemma has_density_sets: "has_density M N f ⟹ sets M = sets N"
unfolding has_density_def by simp
lemma has_density_space: "has_density M N f ⟹ space M = space N"
unfolding has_density_def by simp
lemma has_density_emeasure:
"has_density M N f ⟹ X ∈ sets M ⟹ emeasure M X = ∫⇧+x. f x * indicator X x ∂N"
unfolding has_density_def by (simp_all add: emeasure_density)
lemma nn_integral_cong': "(⋀x. x ∈ space N =simp=> f x = g x) ⟹ (∫⇧+x. f x ∂N) = (∫⇧+x. g x ∂N)"
by (simp add: simp_implies_def cong: nn_integral_cong)
lemma has_density_emeasure_space:
"has_density M N f ⟹ emeasure M (space M) = (∫⇧+x. f x ∂N)"
by (simp add: has_density_emeasure) (simp add: has_density_space cong: nn_integral_cong')
lemma has_density_emeasure_space':
"has_density M N f ⟹ emeasure (density N f) (space (density N f)) = ∫⇧+x. f x ∂N"
by (frule has_densityD(2)[symmetric]) (simp add: has_density_emeasure_space)
lemma has_density_imp_is_subprob_density:
"⟦has_density M N f; (∫⇧+x. f x ∂N) = 1⟧ ⟹ is_subprob_density N f"
by (auto dest: has_densityD)
lemma has_density_imp_is_subprob_density':
"⟦has_density M N f; prob_space M⟧ ⟹ is_subprob_density N f"
by (auto intro!: has_density_imp_is_subprob_density dest: prob_space.emeasure_space_1
simp: has_density_emeasure_space)
lemma has_density_equal_on_space:
assumes "has_density M N f" "⋀x. x ∈ space N ⟹ f x = g x"
shows "has_density M N g"
proof
from assms show "g ∈ borel_measurable N"
by (subst measurable_cong[of _ _ f]) (auto dest: has_densityD)
with assms show "M = density N g"
by (subst density_cong[of _ _ f]) (auto dest: has_densityD)
from assms(1) show "space N ≠ {}" by (rule has_densityD)
qed
lemma has_density_cong:
assumes "⋀x. x ∈ space N ⟹ f x = g x"
shows "has_density M N f = has_density M N g"
using assms by (intro iffI) (erule has_density_equal_on_space, simp)+
lemma has_density_dens_AE:
"⟦AE y in N. f y = f' y; f' ∈ borel_measurable N;
⋀x. x ∈ space M ⟹ f' x ≥ 0; has_density M N f⟧
⟹ has_density M N f'"
unfolding has_density_def by (simp cong: density_cong)
subsection ‹Probability spaces with densities›
lemma is_subprob_density_imp_has_density:
"⟦is_subprob_density N f; M = density N f⟧ ⟹ has_density M N f"
by (rule has_densityI) auto
lemma has_subprob_density_imp_subprob_space':
"⟦has_density M N f; is_subprob_density N f⟧ ⟹ subprob_space M"
proof (rule subprob_spaceI)
assume "has_density M N f"
hence "M = density N f" by (simp add: has_density_def)
also from ‹has_density M N f› have "space ... ≠ {}" by (simp add: has_density_def)
finally show "space M ≠ {}" .
qed (auto simp add: has_density_emeasure_space dest: has_densityD)
lemma has_subprob_density_imp_subprob_space[dest]:
"is_subprob_density M f ⟹ subprob_space (density M f)"
by (rule has_subprob_density_imp_subprob_space') auto
definition "has_subprob_density M N f ≡ has_density M N f ∧ subprob_space M"
lemma subprob_space_density_not_empty: "subprob_space (density M f) ⟹ space M ≠ {}"
by (subst space_density[symmetric], subst subprob_space.subprob_not_empty, assumption) simp
lemma has_subprob_densityI:
"⟦f ∈ borel_measurable N; M = density N f; subprob_space M⟧ ⟹ has_subprob_density M N f"
unfolding has_subprob_density_def by (auto simp: subprob_space_density_not_empty)
lemma has_subprob_densityI':
assumes "f ∈ borel_measurable N" "space N ≠ {}"
"M = density N f" "(∫⇧+x. f x ∂N) ≤ 1"
shows "has_subprob_density M N f"
proof-
from assms have D: "has_density M N f" by blast
moreover from D and assms have "subprob_space M"
by (auto intro!: subprob_spaceI simp: has_density_emeasure_space emeasure_density
cong: nn_integral_cong')
ultimately show ?thesis unfolding has_subprob_density_def by simp
qed
lemma has_subprob_densityD:
assumes "has_subprob_density M N f"
shows "f ∈ borel_measurable N" "⋀x. x ∈ space N ⟹ f x ≥ 0" "M = density N f" "subprob_space M"
using assms unfolding has_subprob_density_def by (auto dest: has_densityD)
lemma has_subprob_density_measurable[measurable_dest]:
"has_subprob_density M N f ⟹ f ∈ N →⇩M borel"
by (auto dest: has_subprob_densityD)
lemma has_subprob_density_imp_has_density:
"has_subprob_density M N f ⟹ has_density M N f" by (simp add: has_subprob_density_def)
lemma has_subprob_density_equal_on_space:
assumes "has_subprob_density M N f" "⋀x. x ∈ space N ⟹ f x = g x"
shows "has_subprob_density M N g"
using assms unfolding has_subprob_density_def by (auto dest: has_density_equal_on_space)
lemma has_subprob_density_cong:
assumes "⋀x. x ∈ space N ⟹ f x = g x"
shows "has_subprob_density M N f = has_subprob_density M N g"
using assms by (intro iffI) (erule has_subprob_density_equal_on_space, simp)+
lemma has_subprob_density_dens_AE:
"⟦AE y in N. f y = f' y; f' ∈ borel_measurable N;
⋀x. x ∈ space M ⟹ f' x ≥ 0; has_subprob_density M N f⟧
⟹ has_subprob_density M N f'"
unfolding has_subprob_density_def by (simp add: has_density_dens_AE)
subsection ‹Parametrized probability densities›
definition
"has_parametrized_subprob_density M N R f ≡
(∀x ∈ space M. has_subprob_density (N x) R (f x)) ∧ case_prod f ∈ borel_measurable (M ⨂⇩M R)"
lemma has_parametrized_subprob_densityI:
assumes "⋀x. x ∈ space M ⟹ N x = density R (f x)"
assumes "⋀x. x ∈ space M ⟹ subprob_space (N x)"
assumes "case_prod f ∈ borel_measurable (M ⨂⇩M R)"
shows "has_parametrized_subprob_density M N R f"
unfolding has_parametrized_subprob_density_def using assms
by (intro ballI conjI has_subprob_densityI) simp_all
lemma has_parametrized_subprob_densityD:
assumes "has_parametrized_subprob_density M N R f"
shows "⋀x. x ∈ space M ⟹ N x = density R (f x)"
and "⋀x. x ∈ space M ⟹ subprob_space (N x)"
and [measurable_dest]: "case_prod f ∈ borel_measurable (M ⨂⇩M R)"
using assms unfolding has_parametrized_subprob_density_def
by (auto dest: has_subprob_densityD)
lemma has_parametrized_subprob_density_integral:
assumes "has_parametrized_subprob_density M N R f" "x ∈ space M"
shows "(∫⇧+y. f x y ∂R) ≤ 1"
proof-
have "(∫⇧+y. f x y ∂R) = emeasure (density R (f x)) (space (density R (f x)))" using assms
by (auto simp: emeasure_density cong: nn_integral_cong' dest: has_parametrized_subprob_densityD)
also have "density R (f x) = (N x)" using assms by (auto dest: has_parametrized_subprob_densityD)
also have "emeasure ... (space ...) ≤ 1" using assms
by (subst subprob_space.emeasure_space_le_1) (auto dest: has_parametrized_subprob_densityD)
finally show ?thesis .
qed
lemma has_parametrized_subprob_density_cong:
assumes "⋀x. x ∈ space M ⟹ N x = N' x"
shows "has_parametrized_subprob_density M N R f = has_parametrized_subprob_density M N' R f"
using assms unfolding has_parametrized_subprob_density_def by auto
lemma has_parametrized_subprob_density_dens_AE:
assumes "⋀x. x ∈ space M ⟹ AE y in R. f x y = f' x y"
"case_prod f' ∈ borel_measurable (M ⨂⇩M R)"
"has_parametrized_subprob_density M N R f"
shows "has_parametrized_subprob_density M N R f'"
unfolding has_parametrized_subprob_density_def
proof (intro conjI ballI)
fix x assume x: "x ∈ space M"
with assms(3) have "space (N x) = space R"
by (auto dest!: has_parametrized_subprob_densityD(1))
with assms and x show "has_subprob_density (N x) R (f' x)"
by (rule_tac has_subprob_density_dens_AE[of "f x"])
(auto simp: has_parametrized_subprob_density_def)
qed fact
subsection ‹Density in the Giry monad›
lemma emeasure_bind_density:
assumes "space M ≠ {}" "⋀x. x ∈ space M ⟹ has_density (f x) N (g x)"
"f ∈ measurable M (subprob_algebra N)" "X ∈ sets N"
shows "emeasure (M ⤜ f) X = ∫⇧+x. ∫⇧+y. g x y * indicator X y ∂N ∂M"
proof-
from assms have "emeasure (M ⤜ f) X = ∫⇧+x. emeasure (f x) X ∂M"
by (intro emeasure_bind)
also have "... = ∫⇧+x. ∫⇧+y. g x y * indicator X y ∂N ∂M" using assms
by (intro nn_integral_cong) (simp add: has_density_emeasure sets_kernel)
finally show ?thesis .
qed
lemma bind_density:
assumes "sigma_finite_measure M" "sigma_finite_measure N"
"space M ≠ {}" "⋀x. x ∈ space M ⟹ has_density (f x) N (g x)"
and [measurable]: "case_prod g ∈ borel_measurable (M ⨂⇩M N)" "f ∈ measurable M (subprob_algebra N)"
shows "(M ⤜ f) = density N (λy. ∫⇧+x. g x y ∂M)"
proof (rule measure_eqI)
interpret sfN: sigma_finite_measure N by fact
interpret sfNM: pair_sigma_finite N M unfolding pair_sigma_finite_def using assms by simp
show eq: "sets (M ⤜ f) = sets (density N (λy. ∫⇧+x. g x y ∂M))"
using sets_bind[OF sets_kernel[OF assms(6)] assms(3)] by auto
fix X assume "X ∈ sets (M ⤜ f)"
with eq have [measurable]: "X ∈ sets N" by auto
with assms have "emeasure (M ⤜ f) X = ∫⇧+x. ∫⇧+y. g x y * indicator X y ∂N ∂M"
by (intro emeasure_bind_density) simp_all
also from ‹X ∈ sets N› have "... = ∫⇧+y. ∫⇧+x. g x y * indicator X y ∂M ∂N"
by (intro sfNM.Fubini') measurable
also {
fix y assume "y ∈ space N"
have "(λx. g x y) = case_prod g ∘ (λx. (x, y))" by (rule ext) simp
also from ‹y ∈ space N› have "... ∈ borel_measurable M"
by (intro measurable_comp[OF _ assms(5)] measurable_Pair2')
finally have "(λx. g x y) ∈ borel_measurable M" .
}
hence "... = ∫⇧+y. (∫⇧+x. g x y ∂M) * indicator X y ∂N"
by (intro nn_integral_cong nn_integral_multc) simp_all
also from ‹X ∈ sets N› and assms have "... = emeasure (density N (λy. ∫⇧+x. g x y ∂M)) X"
by (subst emeasure_density) (simp_all add: sfN.borel_measurable_nn_integral)
finally show "emeasure (M ⤜ f) X = emeasure (density N (λy. ∫⇧+x. g x y ∂M)) X" .
qed
lemma bind_has_density:
assumes "sigma_finite_measure M" "sigma_finite_measure N"
"space M ≠ {}" "⋀x. x ∈ space M ⟹ has_density (f x) N (g x)"
"case_prod g ∈ borel_measurable (M ⨂⇩M N)"
"f ∈ measurable M (subprob_algebra N)"
shows "has_density (M ⤜ f) N (λy. ∫⇧+x. g x y ∂M)"
proof
interpret sigma_finite_measure M by fact
show "(λy. ∫⇧+ x. g x y ∂M) ∈ borel_measurable N" using assms
by (intro borel_measurable_nn_integral, subst measurable_pair_swap_iff) simp
show "M ⤜ f = density N (λy. ∫⇧+ x. g x y ∂M)"
by (intro bind_density) (simp_all add: assms)
from ‹space M ≠ {}› obtain x where "x ∈ space M" by blast
with assms have "has_density (f x) N (g x)" by simp
thus "space N ≠ {}" by (rule has_densityD)
qed
lemma bind_has_density':
assumes sfM: "sigma_finite_measure M"
and sfR: "sigma_finite_measure R"
and not_empty: "space M ≠ {}" and dens_M: "has_density M N δM"
and dens_f: "⋀x. x ∈ space M ⟹ has_density (f x) R (δf x)"
and Mδf: "case_prod δf ∈ borel_measurable (N ⨂⇩M R)"
and Mf: "f ∈ measurable N (subprob_algebra R)"
shows "has_density (M ⤜ f) R (λy. ∫⇧+x. δM x * δf x y ∂N)"
proof-
from dens_M have M_M: "measurable M = measurable N"
by (intro ext measurable_cong_sets) (auto dest: has_densityD)
from dens_M have M_MR: "measurable (M ⨂⇩M R) = measurable (N ⨂⇩M R)"
by (intro ext measurable_cong_sets sets_pair_measure_cong) (auto dest: has_densityD)
have "has_density (M ⤜ f) R (λy. ∫⇧+x. δf x y ∂M)"
by (rule bind_has_density) (auto simp: assms M_MR M_M)
moreover {
fix y assume A: "y ∈ space R"
have "(λx. δf x y) = case_prod δf ∘ (λx. (x,y))" by (rule ext) (simp add: o_def)
also have "... ∈ borel_measurable N" by (intro measurable_comp[OF _ Mδf] measurable_Pair2' A)
finally have M_δf': "(λx. δf x y) ∈ borel_measurable N" .
from dens_M have "M = density N δM" by (auto dest: has_densityD)
also from dens_M have "(∫⇧+x. δf x y ∂...) = ∫⇧+x. δM x * δf x y ∂N"
by (subst nn_integral_density) (auto dest: has_densityD simp: M_δf')
finally have "(∫⇧+x. δf x y ∂M) = ∫⇧+x. δM x * δf x y ∂N" .
}
ultimately show "has_density (M ⤜ f) R (λy. ∫⇧+x. δM x * δf x y ∂N)"
by (rule has_density_equal_on_space) simp_all
qed
lemma bind_has_subprob_density:
assumes "subprob_space M" "sigma_finite_measure N"
"space M ≠ {}" "⋀x. x ∈ space M ⟹ has_density (f x) N (g x)"
"case_prod g ∈ borel_measurable (M ⨂⇩M N)"
"f ∈ measurable M (subprob_algebra N)"
shows "has_subprob_density (M ⤜ f) N (λy. ∫⇧+x. g x y ∂M)"
proof (unfold has_subprob_density_def, intro conjI)
from assms show "has_density (M ⤜ f) N (λy. ∫⇧+x. g x y ∂M)"
by (intro bind_has_density) (auto simp: subprob_space_imp_sigma_finite)
from assms show "subprob_space (M ⤜ f)" by (intro subprob_space_bind)
qed
lemma bind_has_subprob_density':
assumes "has_subprob_density M N δM" "space R ≠ {}" "sigma_finite_measure R"
"⋀x. x ∈ space M ⟹ has_subprob_density (f x) R (δf x)"
"case_prod δf ∈ borel_measurable (N ⨂⇩M R)" "f ∈ measurable N (subprob_algebra R)"
shows "has_subprob_density (M ⤜ f) R (λy. ∫⇧+x. δM x * δf x y ∂N)"
proof (unfold has_subprob_density_def, intro conjI)
from assms(1) have "space M ≠ {}" by (intro subprob_space.subprob_not_empty has_subprob_densityD)
with assms show "has_density (M ⤜ f) R (λy. ∫⇧+x. δM x * δf x y ∂N)"
by (intro bind_has_density' has_densityI)
(auto simp: subprob_space_imp_sigma_finite dest: has_subprob_densityD)
from assms show "subprob_space (M ⤜ f)"
by (intro subprob_space_bind) (auto dest: has_subprob_densityD)
qed
lemma null_measure_has_subprob_density:
"space M ≠ {} ⟹ has_subprob_density (null_measure M) M (λ_. 0)"
by (intro has_subprob_densityI)
(auto intro: null_measure_eq_density simp: subprob_space_null_measure_iff)
lemma emeasure_has_parametrized_subprob_density:
assumes "has_parametrized_subprob_density M N R f"
assumes "x ∈ space M" "X ∈ sets R"
shows "emeasure (N x) X = ∫⇧+y. f x y * indicator X y ∂R"
proof-
from has_parametrized_subprob_densityD(3)[OF assms(1)] and assms(2)
have Mf: "f x ∈ borel_measurable R" by simp
have "N x = density R (f x)"
by (rule has_parametrized_subprob_densityD(1)[OF assms(1,2)])
also from Mf and assms(3) have "emeasure ... X = ∫⇧+y. f x y * indicator X y ∂R"
by (rule emeasure_density)
finally show ?thesis .
qed
lemma emeasure_count_space_density_singleton:
assumes "x ∈ A" "has_density M (count_space A) f"
shows "emeasure M {x} = f x"
proof-
from has_densityD[OF assms(2)] have nonneg: "⋀x. x ∈ A ⟹ f x ≥ 0" by simp
from assms have M: "M = density (count_space A) f" by (intro has_densityD)
from assms have "emeasure M {x} = ∫⇧+y. f y * indicator {x} y ∂count_space A"
by (simp add: M emeasure_density)
also from assms and nonneg have "... = f x"
by (subst nn_integral_indicator_singleton) auto
finally show ?thesis .
qed
lemma subprob_count_space_density_le_1:
assumes "has_subprob_density M (count_space A) f" "x ∈ A"
shows "f x ≤ 1"
proof (cases "f x > 0")
assume "f x > 0"
from assms interpret subprob_space M by (intro has_subprob_densityD)
from assms have M: "M = density (count_space A) f" by (intro has_subprob_densityD)
from assms have "f x = emeasure M {x}"
by (intro emeasure_count_space_density_singleton[symmetric])
(auto simp: has_subprob_density_def)
also have "... ≤ 1" by (rule subprob_emeasure_le_1)
finally show ?thesis .
qed (auto simp: not_less intro: order.trans[of _ 0 1])
lemma has_density_embed_measure:
assumes inj: "inj f" and inv: "⋀x. x ∈ space N ⟹ f' (f x) = x"
shows "has_density (embed_measure M f) (embed_measure N f) (δ ∘ f') ⟷ has_density M N δ"
(is "has_density ?M' ?N' ?δ' ⟷ has_density M N δ")
proof
assume dens: "has_density ?M' ?N' ?δ'"
show "has_density M N δ"
proof
from dens show "space N ≠ {}" by (auto simp: space_embed_measure dest: has_densityD)
from dens have Mδf': "δ ∘ f' ∈ borel_measurable ?N'" by (rule has_densityD)
hence Mδf'f: "δ ∘ f' ∘ f ∈ borel_measurable N"
by (rule_tac measurable_comp, rule_tac measurable_embed_measure2[OF inj])
thus Mδ: "δ ∈ borel_measurable N" by (simp cong: measurable_cong add: inv)
from dens have "embed_measure M f = density (embed_measure N f) (δ ∘ f')" by (rule has_densityD)
also have "... = embed_measure (density N (δ ∘ f' ∘ f)) f"
by (simp only: density_embed_measure[OF inj Mδf'])
also have "density N (δ ∘ f' ∘ f) = density N δ"
by (intro density_cong[OF Mδf'f Mδ]) (simp_all add: inv)
finally show "M = density N δ" by (simp add: embed_measure_eq_iff[OF inj])
qed
next
assume dens: "has_density M N δ"
show "has_density ?M' ?N' ?δ'"
proof
from dens show "space ?N' ≠ {}" by (auto simp: space_embed_measure dest: has_densityD)
have Mf'f: "(λx. f' (f x)) ∈ measurable N N" by (subst measurable_cong[OF inv]) simp_all
from dens have Mδ: "δ ∈ borel_measurable N" by (auto dest: has_densityD)
from Mf'f and dens show Mδf': "δ ∘ f' ∈ borel_measurable (embed_measure N f)"
by (intro measurable_comp) (erule measurable_embed_measure1, rule has_densityD)
have "embed_measure M f = embed_measure (density N δ) f"
by (simp only: has_densityD[OF dens])
also from inv and dens and measurable_comp[OF Mf'f Mδ]
have "density N δ = density N (?δ' ∘ f)"
by (intro density_cong[OF Mδ]) (simp add: o_def, simp add: inv o_def)
also have "embed_measure (density N (?δ' ∘ f)) f = density (embed_measure N f) (δ ∘ f')"
by (simp only: density_embed_measure[OF inj Mδf', symmetric])
finally show "embed_measure M f = density (embed_measure N f) (δ ∘ f')" .
qed
qed
lemma has_density_embed_measure':
assumes inj: "inj f" and inv: "⋀x. x ∈ space N ⟹ f' (f x) = x" and
sets_M: "sets M = sets (embed_measure N f)"
shows "has_density (distr M N f') N (δ ∘ f) ⟷ has_density M (embed_measure N f) δ"
proof-
have sets': "sets (embed_measure (distr M N f') f) = sets (embed_measure N f)"
by (simp add: sets_embed_measure[OF inj])
have Mff': "(λx. f' (f x)) ∈ measurable N N" by (subst measurable_cong[OF inv]) simp_all
have inv': "⋀x. x ∈ space M ⟹ f (f' x) = x"
by (subst (asm) sets_eq_imp_space_eq[OF sets_M]) (auto simp: space_embed_measure inv)
have "M = distr M (embed_measure (distr M N f') f) (λx. f (f' x))"
by (subst distr_cong[OF refl _ inv', of _ M]) (simp_all add: sets_embed_measure inj sets_M)
also have "... = embed_measure (distr M N f') f"
apply (subst (2) embed_measure_eq_distr[OF inj], subst distr_distr)
apply (subst measurable_cong_sets[OF refl sets'], rule measurable_embed_measure2[OF inj])
apply (subst measurable_cong_sets[OF sets_M refl], rule measurable_embed_measure1, rule Mff')
apply (simp cong: distr_cong add: inv)
done
finally have M: "M = embed_measure (distr M N f') f" .
show ?thesis by (subst (2) M, subst has_density_embed_measure[OF inj inv, symmetric])
(auto simp: space_embed_measure inv intro!: has_density_cong)
qed
lemma has_density_embed_measure'':
assumes inj: "inj f" and inv: "⋀x. x ∈ space N ⟹ f' (f x) = x" and
"has_density M (embed_measure N f) δ"
shows "has_density (distr M N f') N (δ ∘ f)"
proof (subst has_density_embed_measure')
from assms(3) show "sets M = sets (embed_measure N f)" by (auto dest: has_densityD)
qed (insert assms)
lemma has_subprob_density_embed_measure'':
assumes inj: "inj f" and inv: "⋀x. x ∈ space N ⟹ f' (f x) = x" and
"has_subprob_density M (embed_measure N f) δ"
shows "has_subprob_density (distr M N f') N (δ ∘ f)"
proof (unfold has_subprob_density_def, intro conjI)
from assms show "has_density (distr M N f') N (δ ∘ f)"
by (intro has_density_embed_measure'' has_subprob_density_imp_has_density)
from assms(3) have "sets M = sets (embed_measure N f)" by (auto dest: has_subprob_densityD)
hence M: "measurable M = measurable (embed_measure N f)"
by (intro ext measurable_cong_sets) simp_all
have "(λx. f' (f x)) ∈ measurable N N" by (simp cong: measurable_cong add: inv)
moreover from assms have "space (embed_measure N f) ≠ {}"
unfolding has_subprob_density_def has_density_def by simp
ultimately show "subprob_space (distr M N f')" using assms
by (intro subprob_space.subprob_space_distr has_subprob_densityD)
(auto simp: M space_embed_measure intro!: measurable_embed_measure1 dest: has_subprob_densityD)
qed (insert assms)
end
Theory PDF_Transformations
section ‹Measure Space Transformations›
theory PDF_Transformations
imports Density_Predicates
begin
lemma not_top_le_1_ennreal[simp]: "¬ top ≤ (1::ennreal)"
by (simp add: top_unique)
lemma range_int: "range int = {n. n ≥ 0}"
proof (intro equalityI subsetI)
fix n :: int assume "n ∈ {n. n ≥ 0}"
hence "n = int (nat n)" by simp
thus "n ∈ range int" by blast
qed auto
lemma range_exp: "range (exp :: real ⇒ real) = {x. x > 0}"
proof (intro equalityI subsetI)
fix x :: real assume "x ∈ {x. x > 0}"
hence "x = exp (ln x)" by simp
thus "x ∈ range exp" by blast
qed auto
lemma Int_stable_Icc: "Int_stable (range (λ(a, b). {a .. b::real}))"
by (auto simp: Int_stable_def)
lemma distr_mult_real:
assumes "c ≠ 0" "has_density M lborel (f :: real ⇒ ennreal)"
shows "has_density (distr M borel ((*) c)) lborel (λx. f (x / c) * inverse (abs c))"
(is "has_density ?M' _ ?f'")
proof
from assms(2) have "M = density lborel f" by (rule has_densityD)
also from assms have Mf[measurable]: "f ∈ borel_measurable borel"
by (auto dest: has_densityD)
hence "distr (density lborel f) borel ((*) c) = density lborel ?f'" (is "?M1 = ?M2")
proof (intro measure_eqI)
fix X assume X[measurable]: "X ∈ sets (distr (density lborel f) borel ((*) c))"
with assms have "emeasure ?M1 X = ∫⇧+x. f x * indicator X (c * x) ∂lborel"
by (subst emeasure_distr, simp, simp, subst emeasure_density)
(auto dest: has_densityD intro!: measurable_sets_borel nn_integral_cong
split: split_indicator)
also from assms(1) and X have "... = ∫⇧+x. ?f' x * indicator X x ∂lborel"
apply (subst lborel_distr_mult'[of "inverse c"])
apply simp
apply (subst nn_integral_density)
apply (simp_all add: nn_integral_distr field_simps)
done
also from X have "... = emeasure ?M2 X"
by (subst emeasure_density) auto
finally show "emeasure ?M1 X = emeasure ?M2 X" .
qed simp
finally show "distr M borel ((*) c) = density lborel ?f'" .
qed (insert assms, auto dest: has_densityD)
lemma distr_uminus_real:
assumes "has_density M lborel (f :: real ⇒ ennreal)"
shows "has_density (distr M borel uminus) lborel (λx. f (- x))"
proof-
from assms have "has_density (distr M borel ((*) (- 1))) lborel
(λx. f (x / -1) * ennreal (inverse (abs (-1))))"
by (intro distr_mult_real) simp_all
also have "(*) (-1) = (uminus :: real ⇒ real)" by (intro ext) simp
also have "(λx. f (x / -1) * ennreal (inverse (abs (-1)))) = (λx. f (-x))"
by (intro ext) (simp add: one_ennreal_def[symmetric])
finally show ?thesis .
qed
lemma distr_plus_real:
assumes "has_density M lborel (f :: real ⇒ ennreal)"
shows "has_density (distr M borel ((+) c)) lborel (λx. f (x - c))"
proof
from assms have "M = density lborel f" by (rule has_densityD)
also from assms have Mf[measurable]: "f ∈ borel_measurable borel"
by (auto dest: has_densityD)
hence "distr (density lborel f) borel ((+) c) = density lborel (λx. f (x - c))" (is "?M1 = ?M2")
proof (intro measure_eqI)
fix X assume X: "X ∈ sets (distr (density lborel f) borel ((+) c))"
with assms have "emeasure ?M1 X = ∫⇧+x. f x * indicator X (c + x) ∂lborel"
by (subst emeasure_distr, simp, simp, subst emeasure_density)
(auto dest: has_densityD intro!: measurable_sets_borel nn_integral_cong
split: split_indicator)
also from X have "... = ∫⇧+x. f (x - c) * indicator X x ∂lborel"
by (subst lborel_distr_plus[where c = "-c", symmetric], subst nn_integral_distr) auto
also from X have "... = emeasure ?M2 X"
by (subst emeasure_density)
(auto simp: emeasure_density intro!: measurable_compose[OF borel_measurable_diff Mf])
finally show "emeasure ?M1 X = emeasure ?M2 X" .
qed simp
finally show "distr M borel ((+) c) = density lborel (λx. f (x - c))" .
qed (insert assms, auto dest: has_densityD)
lemma count_space_uminus:
"count_space UNIV = distr (count_space UNIV) (count_space UNIV) (uminus :: ('a :: ring ⇒ _))"
proof (rule distr_bij_count_space[symmetric])
show "bij (uminus :: 'a ⇒ 'a)"
by (auto intro!: o_bij[where g=uminus])
qed
lemma count_space_plus:
"count_space UNIV = distr (count_space UNIV) (count_space UNIV) ((+) (c :: ('a :: ring)))"
by (rule distr_bij_count_space [symmetric]) simp
lemma distr_uminus_ring_count_space:
assumes "has_density M (count_space UNIV) (f :: _ :: ring ⇒ ennreal)"
shows "has_density (distr M (count_space UNIV) uminus) (count_space UNIV) (λx. f (- x))"
proof
from assms have "M = density (count_space UNIV) f" by (rule has_densityD)
also have "distr (density (count_space UNIV) f) (count_space UNIV) uminus =
density (count_space UNIV)(λx. f (- x))" (is "?M1 = ?M2")
proof (intro measure_eqI)
fix X assume X: "X ∈ sets (distr (density (count_space UNIV) f) (count_space UNIV) uminus)"
with assms have "emeasure ?M1 X = ∫⇧+x. f x * indicator X (-x) ∂count_space UNIV"
by (subst emeasure_distr, simp, simp, subst emeasure_density)
(auto dest: has_densityD intro!: measurable_sets_borel nn_integral_cong
split: split_indicator)
also from X have "... = emeasure ?M2 X"
by (subst count_space_uminus) (simp_all add: nn_integral_distr emeasure_density)
finally show "emeasure ?M1 X = emeasure ?M2 X" .
qed simp
finally show "distr M (count_space UNIV) uminus = density (count_space UNIV) (λx. f (- x))" .
qed (insert assms, auto dest: has_densityD)
lemma distr_plus_ring_count_space:
assumes "has_density M (count_space UNIV) (f :: _ :: ring ⇒ ennreal)"
shows "has_density (distr M (count_space UNIV) ((+) c)) (count_space UNIV) (λx. f (x - c))"
proof
from assms have "M = density (count_space UNIV) f" by (rule has_densityD)
also have "distr (density (count_space UNIV) f) (count_space UNIV) ((+) c) =
density (count_space UNIV)(λx. f (x - c))" (is "?M1 = ?M2")
proof (intro measure_eqI)
fix X assume X: "X ∈ sets (distr (density (count_space UNIV) f) (count_space UNIV) ((+) c))"
with assms have "emeasure ?M1 X = ∫⇧+x. f x * indicator X (c + x) ∂count_space UNIV"
by (subst emeasure_distr, simp, simp, subst emeasure_density)
(auto dest: has_densityD intro!: measurable_sets_borel nn_integral_cong
split: split_indicator)
also from X have "... = emeasure ?M2 X"
by (subst count_space_plus[of "-c"]) (simp_all add: nn_integral_distr emeasure_density)
finally show "emeasure ?M1 X = emeasure ?M2 X" .
qed simp
finally show "distr M (count_space UNIV) ((+) c) = density (count_space UNIV) (λx. f (x - c))" .
qed (insert assms, auto dest: has_densityD)
lemma subprob_density_distr_real_eq:
assumes dens: "has_subprob_density M lborel f"
assumes Mh: "h ∈ borel_measurable borel"
assumes Mg: "g ∈ borel_measurable borel"
assumes measure_eq:
"⋀a b. a ≤ b ⟹ emeasure (distr (density lborel f) lborel h) {a..b} =
emeasure (density lborel g) {a..b}"
shows "has_subprob_density (distr M borel (h :: real ⇒ real)) lborel g"
proof (rule has_subprob_densityI)
from dens have sets_M: "sets M = sets borel" by (auto dest: has_subprob_densityD)
have meas_M[simp]: "measurable M = measurable borel"
by (intro ext, subst measurable_cong_sets[OF sets_M refl]) auto
from Mh and dens show subprob_space: "subprob_space (distr M borel h)"
by (intro subprob_space.subprob_space_distr) (auto dest: has_subprob_densityD)
show "distr M borel h = density lborel g"
proof (rule measure_eqI_generator_eq[OF Int_stable_Icc, of UNIV])
{
fix x :: real
obtain n :: nat where "n > abs x" using reals_Archimedean2 by auto
hence "∃n::nat. x ∈ {-real n..real n}" by (intro exI[of _ n]) auto
}
thus "(⋃i::nat. {-real i..real i}) = UNIV" by blast
next
fix i :: nat
from subprob_space have "emeasure (distr M borel h) {-real i..real i} ≤ 1"
by (intro subprob_space.subprob_emeasure_le_1) (auto dest: has_subprob_densityD)
thus "emeasure (distr M borel h) {- real i..real i} ≠ ∞" by auto
next
fix X :: "real set" assume "X ∈ range (λ(a,b). {a..b})"
then obtain a b where "X = {a..b}" by auto
with dens have "emeasure (distr M lborel h) X = emeasure (density lborel g) X"
by (cases "a ≤ b") (auto simp: measure_eq dest: has_subprob_densityD)
also have "distr M lborel h = distr M borel h"
by (rule distr_cong) auto
finally show "emeasure (distr M borel h) X = emeasure (density lborel g) X" .
qed (auto simp: borel_eq_atLeastAtMost)
qed (insert assms, auto)
lemma subprob_density_distr_real_exp:
assumes dens: "has_subprob_density M lborel f"
shows "has_subprob_density (distr M borel exp) lborel
(λx. if x > 0 then f (ln x) * ennreal (inverse x) else 0)"
(is "has_subprob_density _ _ ?g")
proof (rule subprob_density_distr_real_eq[OF dens])
from dens have [measurable]: "f ∈ borel_measurable borel"
by (auto dest: has_subprob_densityD)
have Mf: "(λx. f (ln x) * ennreal (inverse x)) ∈ borel_measurable borel" by simp
fix a b :: real assume "a ≤ b"
let ?A = "λi. {inverse (Suc i) :: real ..}"
let ?M1 = "distr (density lborel f) lborel exp" and ?M2 = "density lborel ?g"
{
fix x :: real assume "∀i. x < inverse (Suc i)"
hence "x ≤ 0" by (intro tendsto_lowerbound[OF LIMSEQ_inverse_real_of_nat])
(auto intro!: always_eventually less_imp_le)
}
hence decomp: "{a..b} = {x∈{a..b}. x ≤ 0} ∪ (⋃i. ?A i ∩ {a..b})" (is "_ = ?C ∪ ?D")
by (auto simp: not_le)
have inv_le: "⋀x i. x ≥ inverse (real (Suc i)) ⟹ ¬(x ≤ 0)"
by (subst not_le, erule dual_order.strict_trans1, simp)
hence "emeasure ?M1 {a..b} = emeasure ?M1 ?C + emeasure ?M1 ?D"
by (subst decomp, intro plus_emeasure[symmetric]) auto
also have "emeasure ?M1 ?C = 0" by (subst emeasure_distr) auto
also have "0 = emeasure ?M2 ?C"
by (subst emeasure_density, simp, simp, rule sym, subst nn_integral_0_iff) auto
also have "emeasure ?M1 (⋃i. ?A i ∩ {a..b}) = (SUP i. emeasure ?M1 (?A i ∩ {a..b}))"
by (rule SUP_emeasure_incseq[symmetric])
(auto simp: incseq_def max_def not_le dest: order.strict_trans1)
also have "⋀i. emeasure ?M1 (?A i ∩ {a..b}) = emeasure ?M2 (?A i ∩ {a..b})"
proof (case_tac "inverse (Suc i) ≤ b")
fix i assume True: "inverse (Suc i) ≤ b"
let ?a = "inverse (Suc i)"
from ‹a ≤ b› have A: "?A i ∩ {a..b} = {max ?a a..b}" (is "?E = ?F") by auto
hence "emeasure ?M1 ?E = emeasure ?M1 ?F" by simp
also have "strict_mono_on ln {max (inverse (real (Suc i))) a..b}"
by (rule strict_mono_onI, subst ln_less_cancel_iff)
(auto dest: inv_le simp del: of_nat_Suc)
with ‹a ≤ b› True dens
have "emeasure ?M1 ?F = emeasure (density lborel (λx. f (ln x) * inverse x)) ?F"
by (intro emeasure_density_distr_interval)
(auto simp: Mf not_less not_le range_exp dest: has_subprob_densityD dest!: inv_le
intro!: DERIV_ln continuous_on_inverse continuous_on_id simp del: of_nat_Suc)
also note A[symmetric]
also have "emeasure (density lborel (λx. f (ln x) * inverse x)) ?E = emeasure ?M2 ?E"
by (subst (1 2) emeasure_density)
(auto intro!: nn_integral_cong split: split_indicator dest!: inv_le simp del: of_nat_Suc)
finally show "emeasure ?M1 (?A i ∩ {a..b}) = emeasure ?M2 (?A i ∩ {a..b})" .
qed simp
hence "(SUP i. emeasure ?M1 (?A i ∩ {a..b})) = (SUP i. emeasure ?M2 (?A i ∩ {a..b}))" by simp
also have "... = emeasure ?M2 (⋃i. ?A i ∩ {a..b})"
by (rule SUP_emeasure_incseq)
(auto simp: incseq_def max_def not_le dest: order.strict_trans1)
also have "emeasure ?M2 ?C + emeasure ?M2 ?D = emeasure ?M2 (?C ∪ ?D)"
by (rule plus_emeasure) (auto dest: inv_le simp del: of_nat_Suc)
also note decomp[symmetric]
finally show "emeasure ?M1 {a..b} = emeasure ?M2 {a..b}" .
qed (insert dens, auto dest!: has_subprob_densityD(1))
lemma subprob_density_distr_real_inverse_aux:
assumes dens: "has_subprob_density M lborel f"
shows "has_subprob_density (distr M borel (λx. - inverse x)) lborel
(λx. f (-inverse x) * ennreal (inverse (x * x)))"
(is "has_subprob_density _ _ ?g")
proof (rule subprob_density_distr_real_eq[OF dens])
from dens have Mf[measurable]: "f ∈ borel_measurable borel" by (auto dest: has_subprob_densityD)
show Mg: "?g ∈ borel_measurable borel" by measurable
have surj[simp]: "surj (λx. - inverse x :: real)"
by (intro surjI[of _ "λx. - inverse x"]) (simp add: field_simps)
fix a b :: real assume "a ≤ b"
let ?A1 = "λi. {..-inverse (Suc i) :: real}" and ?A2 = "λi. {inverse (Suc i) :: real ..}"
let ?C = "if 0 ∈ {a..b} then {0} else {}"
let ?M1 = "distr (density lborel f) lborel (λx. - inverse x)" and ?M2 = "density lborel ?g"
have inv_le: "⋀x i. x ≥ inverse (real (Suc i)) ⟹ ¬(x ≤ 0)"
by (subst not_le, erule dual_order.strict_trans1, simp)
have "⋀x. x > 0 ⟹ ∃i. x ≥ inverse (Suc i)"
proof (rule ccontr)
fix x :: real assume "x > 0" "¬(∃i. x ≥ inverse (Suc i))"
hence "x ≤ 0" by (intro tendsto_lowerbound[OF LIMSEQ_inverse_real_of_nat])
(auto intro!: always_eventually less_imp_le simp: not_le)
with ‹x > 0› show False by simp
qed
hence A: "(⋃i. ?A2 i) = {0<..}" by (auto dest: inv_le simp del: of_nat_Suc)
moreover have "⋀x. x < 0 ⟹ ∃i. x ≤ -inverse (Suc i)"
proof (rule ccontr)
fix x :: real assume "x < 0" "¬(∃i. x ≤ -inverse (Suc i))"
hence "x ≥ 0"
by (intro tendsto_upperbound, simp)
(auto intro!: always_eventually less_imp_le LIMSEQ_inverse_real_of_nat_add_minus simp: not_le)
with ‹x < 0› show False by simp
qed
hence B: "(⋃i. ?A1 i) = {..<0}"
by (auto simp: le_minus_iff[of _ "inverse x" for x] dest!: inv_le simp del: of_nat_Suc)
ultimately have C: "UNIV = (⋃i. ?A1 i) ∪ (⋃i. ?A2 i) ∪ {0}" by (subst A, subst B) force
have UN_Int_distrib: "⋀f A. (⋃i. f i) ∩ A = (⋃i. f i ∩ A)" by blast
have decomp: "{a..b} = (⋃i. ?A1 i ∩ {a..b}) ∪ (⋃i. ?A2 i ∩ {a..b}) ∪ ?C" (is "_ = ?D ∪ ?E ∪ _")
by (subst Int_UNIV_left[symmetric], simp only: C Int_Un_distrib2 UN_Int_distrib)
(simp split: if_split)
have "emeasure ?M1 {a..b} = emeasure ?M1 ?D + emeasure ?M1 ?E + emeasure ?M1 ?C"
apply (subst decomp)
apply (subst plus_emeasure[symmetric], simp, simp, simp)
apply (subst plus_emeasure[symmetric])
apply (auto dest!: inv_le simp: not_le le_minus_iff[of _ "inverse x" for x] simp del: of_nat_Suc)
done
also have "(λx. - inverse x) -` {0 :: real} = {0}" by (auto simp: field_simps)
hence "emeasure ?M1 ?C = 0"
by (subst emeasure_distr) (auto split: if_split simp: emeasure_density Mf)
also have "emeasure ?M2 {0} = 0" by (simp add: emeasure_density)
hence "0 = emeasure ?M2 ?C"
by (rule_tac sym, rule_tac order.antisym, rule_tac order.trans, rule_tac emeasure_mono[of _ "{0}"]) simp_all
also have "emeasure ?M1 (⋃i. ?A1 i ∩ {a..b}) = (SUP i. emeasure ?M1 (?A1 i ∩ {a..b}))"
by (rule SUP_emeasure_incseq[symmetric])
(auto simp: incseq_def max_def not_le dest: order.strict_trans1)
also have "⋀i. emeasure ?M1 (?A1 i ∩ {a..b}) = emeasure ?M2 (?A1 i ∩ {a..b})"
proof (case_tac "-inverse (Suc i) ≥ a")
fix i assume True: "-inverse (Suc i) ≥ a"
let ?a = "-inverse (Suc i)"
from ‹a ≤ b› have A: "?A1 i ∩ {a..b} = {a..min ?a b}" (is "?F = ?G") by auto
hence "emeasure ?M1 ?F = emeasure ?M1 ?G" by simp
also have "strict_mono_on (λx. -inverse x) {a..min ?a b}"
by (rule strict_mono_onI)
(auto simp: le_minus_iff[of _ "inverse x" for x] dest!: inv_le simp del: of_nat_Suc)
with ‹a ≤ b› True dens
have "emeasure ?M1 ?G = emeasure ?M2 ?G"
by (intro emeasure_density_distr_interval)
(auto simp: Mf not_less dest: has_subprob_densityD inv_le
intro!: derivative_eq_intros continuous_on_mult continuous_on_inverse continuous_on_id)
also note A[symmetric]
finally show "emeasure ?M1 (?A1 i ∩ {a..b}) = emeasure ?M2 (?A1 i ∩ {a..b})" .
qed simp
hence "(SUP i. emeasure ?M1 (?A1 i ∩ {a..b})) = (SUP i. emeasure ?M2 (?A1 i ∩ {a..b}))" by simp
also have "... = emeasure ?M2 (⋃i. ?A1 i ∩ {a..b})"
by (rule SUP_emeasure_incseq)
(auto simp: incseq_def max_def not_le dest: order.strict_trans1)
also have "emeasure ?M1 (⋃i. ?A2 i ∩ {a..b}) = (SUP i. emeasure ?M1 (?A2 i ∩ {a..b}))"
by (rule SUP_emeasure_incseq[symmetric])
(auto simp: incseq_def max_def not_le dest: order.strict_trans1)
also have "⋀i. emeasure ?M1 (?A2 i ∩ {a..b}) = emeasure ?M2 (?A2 i ∩ {a..b})"
proof (case_tac "inverse (Suc i) ≤ b")
fix i assume True: "inverse (Suc i) ≤ b"
let ?a = "inverse (Suc i)"
from ‹a ≤ b› have A: "?A2 i ∩ {a..b} = {max ?a a..b}" (is "?F = ?G") by auto
hence "emeasure ?M1 ?F = emeasure ?M1 ?G" by simp
also have "strict_mono_on (λx. -inverse x) {max ?a a..b}"
by (rule strict_mono_onI) (auto dest!: inv_le simp: not_le simp del: of_nat_Suc)
with ‹a ≤ b› True dens
have "emeasure ?M1 ?G = emeasure ?M2 ?G"
by (intro emeasure_density_distr_interval)
(auto simp: Mf not_less dest: has_subprob_densityD inv_le
intro!: derivative_eq_intros continuous_on_mult continuous_on_inverse continuous_on_id)
also note A[symmetric]
finally show "emeasure ?M1 (?A2 i ∩ {a..b}) = emeasure ?M2 (?A2 i ∩ {a..b})" .
qed simp
hence "(SUP i. emeasure ?M1 (?A2 i ∩ {a..b})) = (SUP i. emeasure ?M2 (?A2 i ∩ {a..b}))" by simp
also have "... = emeasure ?M2 (⋃i. ?A2 i ∩ {a..b})"
by (rule SUP_emeasure_incseq)
(auto simp: incseq_def max_def not_le dest: order.strict_trans1)
also have "emeasure ?M2 ?D + emeasure ?M2 ?E + emeasure ?M2 ?C = emeasure ?M2 {a..b}"
apply (subst (4) decomp)
apply (subst plus_emeasure, simp, simp)
apply (auto dest!: inv_le simp: not_le le_minus_iff[of _ "inverse x" for x] simp del: of_nat_Suc)
apply (subst plus_emeasure)
apply (auto dest!: inv_le simp: not_le le_minus_iff[of _ "inverse x" for x])
done
finally show "emeasure ?M1 {a..b} = emeasure ?M2 {a..b}" .
qed simp
lemma subprob_density_distr_real_inverse:
assumes dens: "has_subprob_density M lborel f"
shows "has_subprob_density (distr M borel inverse) lborel (λx. f (inverse x) * ennreal (inverse (x * x)))"
proof (unfold has_subprob_density_def, intro conjI)
let ?g' = "(λx. f (-inverse x) * ennreal (inverse (x * x)))"
have prob: "has_subprob_density (distr M borel (λx. -inverse x)) lborel ?g'"
by (rule subprob_density_distr_real_inverse_aux[OF assms])
from assms have sets_M: "sets M = sets borel" by (auto dest: has_subprob_densityD)
have [simp]: "measurable M = measurable borel"
by (intro ext, subst measurable_cong_sets[OF sets_M refl]) auto
from prob have dens: "has_density (distr M lborel (λx. -inverse x)) lborel
(λx. f (-inverse x) * ennreal (inverse (x * x)))"
unfolding has_subprob_density_def by (simp cong: distr_cong)
from distr_uminus_real[OF this]
show "has_density (distr M borel inverse) lborel
(λx. f (inverse x) * ennreal (inverse (x * x)))"
by (simp add: distr_distr o_def cong: distr_cong)
show "subprob_space (distr M borel inverse)"
by (intro subprob_space.subprob_space_distr has_subprob_densityD[OF assms]) simp_all
qed
lemma distr_convolution_real:
assumes "has_density M lborel (f :: (real × real) ⇒ ennreal)"
shows "has_density (distr M borel (case_prod (+))) lborel (λz. ∫⇧+x. f (x, z - x) ∂lborel)"
(is "has_density ?M' _ ?f'")
proof
from has_densityD[OF assms] have Mf[measurable]: "f ∈ borel_measurable borel" by simp
show Mf': "(λz. ∫⇧+ x. f (x, z - x) ∂lborel) ∈ borel_measurable lborel" by measurable
from assms have sets_M: "sets M = sets borel" by (auto dest: has_densityD)
hence [simp]: "space M = UNIV" by (subst sets_eq_imp_space_eq[OF sets_M]) simp
from sets_M have [simp]: "measurable M = measurable borel"
by (intro ext measurable_cong_sets) simp_all
have M_add: "case_prod (+) ∈ borel_measurable (borel :: (real × real) measure)"
by (simp add: borel_prod[symmetric])
show "distr M borel (case_prod (+)) = density lborel ?f'"
proof (rule measure_eqI)
fix X :: "real set" assume X[measurable]: "X ∈ sets (distr M borel (case_prod (+)))"
hence "emeasure (distr M borel (case_prod (+))) X = emeasure M ((λ(x, y). x + y) -` X)"
by (simp_all add: M_add emeasure_distr)
also from X have "... = ∫⇧+z. f z * indicator ((λ(x, y). x + y) -` X) z ∂(lborel ⨂⇩M lborel)"
by (simp add: emeasure_density has_densityD[OF assms]
measurable_sets_borel[OF M_add] lborel_prod)
also have "... = ∫⇧+x. ∫⇧+y. f (x, y) * indicator ((λ(x, y). x + y) -` X) (x,y) ∂lborel ∂lborel"
apply (rule lborel.nn_integral_fst[symmetric])
apply measurable
apply (simp_all add: borel_prod)
done
also have "... = ∫⇧+x. ∫⇧+y. f (x, y) * indicator ((λ(x, y). x + y) -` X) (x,y)
∂distr lborel borel ((+) (-x)) ∂lborel"
by (rule nn_integral_cong, subst lborel_distr_plus) simp
also have "... = ∫⇧+x. ∫⇧+z. f (x, z-x) * indicator ((λ(x, y). x + y) -` X) (x, z-x)
∂lborel ∂lborel"
apply (rule nn_integral_cong)
apply (subst nn_integral_distr)
apply simp_all
apply measurable
apply (subst space_count_space)
apply auto
done
also have "... = ∫⇧+x. ∫⇧+z. f (x, z-x) * indicator X z ∂lborel ∂lborel"
by (intro nn_integral_cong) (simp split: split_indicator)
also have "... = ∫⇧+z. ∫⇧+x. f (x, z-x) * indicator X z ∂lborel ∂lborel" using X
by (subst lborel_pair.Fubini')
(simp_all add: pair_sigma_finite_def)
also have "... = ∫⇧+z. (∫⇧+x. f (x, z-x) ∂lborel) * indicator X z ∂lborel"
by (rule nn_integral_cong) (simp split: split_indicator)
also have "... = emeasure (density lborel ?f') X" using X
by (simp add: emeasure_density)
finally show "emeasure (distr M borel (case_prod (+))) X = emeasure (density lborel ?f') X" .
qed (insert assms, auto dest: has_densityD)
qed simp_all
lemma distr_convolution_ring_count_space:
assumes C: "countable (UNIV :: 'a set)"
assumes "has_density M (count_space UNIV) (f :: (('a :: ring) × 'a) ⇒ ennreal)"
shows "has_density (distr M (count_space UNIV) (case_prod (+))) (count_space UNIV)
(λz. ∫⇧+x. f (x, z - x) ∂count_space UNIV)"
(is "has_density ?M' _ ?f'")
proof
let ?CS = "count_space UNIV :: 'a measure" and ?CSP = "count_space UNIV :: ('a × 'a) measure"
show Mf': "(λz. ∫⇧+ x. f (x, z - x) ∂count_space UNIV) ∈ borel_measurable ?CS" by simp
from assms have sets_M: "sets M = UNIV" and [simp]: "space M = UNIV"
by (auto dest: has_densityD)
from assms have [simp]: "measurable M = measurable (count_space UNIV)"
by (intro ext measurable_cong_sets) (simp_all add: sets_M)
interpret sigma_finite_measure ?CS by (rule sigma_finite_measure_count_space_countable[OF C])
show "distr M ?CS (case_prod (+)) = density ?CS ?f'"
proof (rule measure_eqI)
fix X :: "'a set" assume X: "X ∈ sets (distr M ?CS (case_prod (+)))"
hence "emeasure (distr M ?CS (case_prod (+))) X = emeasure M ((λ(x, y). x + y) -` X)"
by (simp_all add: emeasure_distr)
also from X have "... = ∫⇧+z. f z * indicator ((λ(x, y). x + y) -` X) z ∂(?CS ⨂⇩M ?CS)"
by (simp add: emeasure_density has_densityD[OF assms(2)]
sets_M pair_measure_countable C)
also have "... = ∫⇧+x. ∫⇧+y. f (x, y) * indicator ((λ(x, y). x + y) -` X) (x,y) ∂?CS ∂?CS"
by (rule nn_integral_fst[symmetric]) (simp add: pair_measure_countable C)
also have "... = ∫⇧+x. ∫⇧+y. f (x, y) * indicator ((λ(x, y). x + y) -` X) (x,y)
∂distr ?CS ?CS ((+) (-x)) ∂?CS"
by (rule nn_integral_cong, subst count_space_plus) simp
also have "... = ∫⇧+x. ∫⇧+z. f (x, z-x) * indicator ((λ(x, y). x + y) -` X) (x, z-x) ∂?CS ∂?CS"
by (rule nn_integral_cong) (simp_all add: nn_integral_distr)
also have "... = ∫⇧+x. ∫⇧+z. f (x, z-x) * indicator X z ∂?CS ∂?CS"
by (intro nn_integral_cong) (simp split: split_indicator)
also have "... = ∫⇧+z. ∫⇧+x. f (x, z-x) * indicator X z ∂?CS ∂?CS" using X
by (subst pair_sigma_finite.Fubini')
(simp_all add: pair_sigma_finite_def sigma_finite_measure_count_space_countable
C pair_measure_countable)
also have "... = ∫⇧+z. (∫⇧+x. f (x, z-x) ∂?CS) * indicator X z ∂?CS"
by (rule nn_integral_cong) (simp split: split_indicator)
also have "... = emeasure (density ?CS ?f') X" using X by (simp add: emeasure_density)
finally show "emeasure (distr M ?CS (case_prod (+))) X = emeasure (density ?CS ?f') X" .
qed (insert assms, auto dest: has_densityD)
qed simp_all
end
Theory PDF_Values
section ‹Source Language Values›
theory PDF_Values
imports Density_Predicates
begin
subsection ‹Values and stock measures›
datatype pdf_type = UNIT | BOOL | INTEG | REAL | PRODUCT pdf_type pdf_type
datatype val = UnitVal
| BoolVal (extract_bool: bool)
| IntVal (extract_int: int)
| RealVal (extract_real: real)
| PairVal (extract_fst: val) (extract_snd: val) ("<|_, _|>" [0, 61] 1000)
where
"extract_bool UnitVal = False"
| "extract_bool (IntVal i) = False"
| "extract_bool (RealVal r) = False"
| "extract_bool (PairVal x y) = False"
| "extract_int UnitVal = 0"
| "extract_int (BoolVal b) = 0"
| "extract_int (RealVal r) = 0"
| "extract_int (PairVal x y) = 0"
| "extract_real UnitVal = 0"
| "extract_real (BoolVal b) = 0"
| "extract_real (IntVal i) = 0"
| "extract_real (PairVal x y) = 0"
primrec extract_pair' where
"extract_pair' f s <| x, y |> = (f x, s y)"
definition map_int_pair where
"map_int_pair f g x = (case x of <| IntVal a, IntVal b |> ⇒ f a b | _ ⇒ g x)"
definition map_real_pair where
"map_real_pair f g x = (case x of <| RealVal a, RealVal b |> ⇒ f a b | _ ⇒ g x)"
abbreviation "TRUE ≡ BoolVal True"
abbreviation "FALSE ≡ BoolVal False"
type_synonym vname = "nat"
type_synonym state = "vname ⇒ val"
lemma map_int_pair[simp]: "map_int_pair f g <| IntVal i, IntVal j |> = f i j"
by (simp add: map_int_pair_def)
lemma map_int_pair_REAL[simp]: "map_int_pair f g <| RealVal i, RealVal j |> = g <| RealVal i, RealVal j |>"
by (simp add: map_int_pair_def)
lemma map_real_pair[simp]: "map_real_pair f g <| RealVal i, RealVal j |> = f i j"
by (simp add: map_real_pair_def)
abbreviation "extract_pair ≡ extract_pair' id id"
abbreviation "extract_real_pair ≡ extract_pair' extract_real extract_real"
abbreviation "extract_int_pair ≡ extract_pair' extract_int extract_int"
definition "RealPairVal ≡ λ(x,y). <|RealVal x, RealVal y|>"
definition "IntPairVal ≡ λ(x,y). <|IntVal x, IntVal y|>"
lemma inj_RealPairVal: "inj RealPairVal" by (auto simp: RealPairVal_def intro!: injI)
lemma inj_IntPairVal: "inj IntPairVal" by (auto simp: IntPairVal_def intro!: injI)
fun val_type :: "val ⇒ pdf_type" where
"val_type (BoolVal b) = BOOL"
| "val_type (IntVal i) = INTEG"
| "val_type UnitVal = UNIT"
| "val_type (RealVal r) = REAL"
| "val_type (<|v1 , v2|>) = (PRODUCT (val_type v1) (val_type v2))"
lemma val_type_eq_REAL: "val_type x = REAL ⟷ x ∈ RealVal`UNIV"
by (cases x) auto
lemma val_type_eq_INTEG: "val_type x = INTEG ⟷ x ∈ IntVal`UNIV"
by (cases x) auto
definition "type_universe t = {v. val_type v = t}"
lemma type_universe_nonempty[simp]: "type_universe t ≠ {}"
by (induction t) (auto intro: val_type.simps simp: type_universe_def)
lemma val_in_type_universe[simp]:
"v ∈ type_universe (val_type v)"
by (simp add: type_universe_def)
lemma BoolVal_in_type_universe[simp]: "BoolVal v ∈ type_universe BOOL"
by (simp add: type_universe_def)
lemma IntVal_in_type_universe[simp]: "IntVal v ∈ type_universe INTEG"
by (simp add: type_universe_def)
lemma type_universe_type[simp]:
"w ∈ type_universe t ⟷ val_type w = t"
by (simp add: type_universe_def)
lemma type_universe_REAL: "type_universe REAL = RealVal ` UNIV"
apply (auto simp add: set_eq_iff image_iff)
apply (case_tac x)
apply auto
done
lemma type_universe_eq_imp_type_eq:
assumes "type_universe t1 = type_universe t2"
shows "t1 = t2"
proof-
from type_universe_nonempty obtain v where A: "v ∈ type_universe t1" by blast
hence "t1 = val_type v" by simp
also from A and assms have "v ∈ type_universe t2" by simp
hence "val_type v = t2" by simp
finally show ?thesis .
qed
lemma type_universe_eq_iff[simp]: "type_universe t1 = type_universe t2 ⟷ t1 = t2"
by (blast intro: type_universe_eq_imp_type_eq)
primrec stock_measure :: "pdf_type ⇒ val measure" where
"stock_measure UNIT = count_space {UnitVal}"
| "stock_measure INTEG = count_space (range IntVal)"
| "stock_measure BOOL = count_space (range BoolVal)"
| "stock_measure REAL = embed_measure lborel RealVal"
| "stock_measure (PRODUCT t1 t2) =
embed_measure (stock_measure t1 ⨂⇩M stock_measure t2) (λ(a, b). <|a, b|>)"
declare [[coercion stock_measure]]
lemma sigma_finite_stock_measure[simp]: "sigma_finite_measure (stock_measure t)"
by (induction t)
(auto intro!: sigma_finite_measure_count_space_countable sigma_finite_pair_measure
sigma_finite_embed_measure injI sigma_finite_lborel)
lemma val_case_stock_measurable:
assumes "t = UNIT ⟹ c ∈ space M"
assumes "⋀b. t = BOOL ⟹ g b ∈ space M"
assumes "⋀i. t = INTEG ⟹ h i ∈ space M"
assumes "t = REAL ⟹ j ∈ measurable borel M"
assumes *: "⋀t1 t2. t = PRODUCT t1 t2 ⟹ case_prod k ∈ measurable (stock_measure t1 ⨂⇩M stock_measure t2) M"
shows "(λx. case x of UnitVal ⇒ c | BoolVal b ⇒ g b | IntVal i ⇒ h i | RealVal r ⇒ j r
| PairVal y z ⇒ k y z) ∈ measurable t M"
proof (cases t)
case (PRODUCT t1 t2) with *[of t1 t2] show ?thesis
by (auto intro!: measurable_embed_measure1 simp: split_beta')
qed (auto intro!: measurable_embed_measure1 assms)
lemma space_stock_measure[simp]: "space (stock_measure t) = type_universe t"
by (induction t)
(auto simp add: type_universe_def space_pair_measure space_embed_measure
simp del: type_universe_type elim: val_type.elims)
lemma type_universe_stock_measure[measurable]: "type_universe t ∈ sets (stock_measure t)"
using sets.top[of "stock_measure t"] by simp
lemma inj_RealVal[simp]: "inj RealVal" by (auto intro!: inj_onI)
lemma inj_IntVal[simp]: "inj IntVal" by (auto intro!: inj_onI)
lemma inj_BoolVal[simp]: "inj BoolVal" by (auto intro!: inj_onI)
lemma inj_PairVal[simp]: "inj (λ(x, y). <| x , y |>)" by (auto intro: injI)
lemma measurable_PairVal[measurable]:
fixes t1 t2 :: pdf_type
shows "case_prod PairVal ∈ measurable (t1 ⨂⇩M t2) (PRODUCT t1 t2)"
using measurable_embed_measure2[measurable] by simp
lemma measurable_RealVal[measurable]: "RealVal ∈ measurable borel REAL"
using measurable_embed_measure2[measurable] by simp
lemma nn_integral_BoolVal:
assumes "⋀x. f (BoolVal x) ≥ 0"
shows "(∫⇧+x. f x ∂BOOL) = f (BoolVal True) + f (BoolVal False)"
proof-
have A: "range BoolVal = {BoolVal True, BoolVal False}" by auto
from assms show ?thesis
by (subst stock_measure.simps, subst A, subst nn_integral_count_space_finite)
(simp_all add: max_def A)
qed
lemma nn_integral_RealVal:
"f ∈ borel_measurable REAL ⟹ (∫⇧+x. f x ∂REAL) = (∫⇧+x. f (RealVal x) ∂lborel)"
unfolding stock_measure.simps using measurable_embed_measure2[measurable]
by (subst embed_measure_eq_distr, simp_all add: nn_integral_distr)
lemma nn_integral_IntVal: "(∫⇧+x. f x ∂INTEG) = (∫⇧+x. f (IntVal x) ∂count_space UNIV)"
using measurable_embed_measure1[measurable (raw)]
unfolding stock_measure.simps embed_measure_count_space[OF inj_IntVal, symmetric]
by (subst embed_measure_eq_distr[OF inj_IntVal], simp add: nn_integral_distr space_embed_measure)
lemma nn_integral_PairVal:
"f ∈ borel_measurable (PRODUCT t1 t2) ⟹
(∫⇧+x. f x ∂PRODUCT t1 t2) = (∫⇧+x. f (PairVal (fst x) (snd x)) ∂(t1 ⨂⇩M t2))"
unfolding stock_measure.simps
by (subst nn_integral_embed_measure) (simp_all add: split_beta' inj_on_def)
lemma BOOL_E: "⟦val_type v = BOOL; ⋀b. v = BoolVal b ⟹ P⟧ ⟹ P"
by (cases v) auto
lemma PROD_E: "⟦val_type v = PRODUCT t1 t2 ;
⋀a b. val_type a = t1 ⟹ val_type b = t2 ⟹ v = <| a, b |> ⟹ P⟧ ⟹ P"
by (cases v) auto
lemma REAL_E: "⟦val_type v = REAL; ⋀b. v = RealVal b ⟹ P⟧ ⟹ P"
by (cases v) auto
lemma INTEG_E: "⟦val_type v = INTEG; ⋀i. v = IntVal i ⟹ P⟧ ⟹ P"
by (cases v) auto
measurable_extract_pair'[measurable (raw)]:
fixes t1 t2 :: pdf_type
assumes [measurable]: "f ∈ measurable t1 M"
assumes [measurable]: "g ∈ measurable t2 N"
assumes h: "h ∈ measurable K (PRODUCT t1 t2)"
shows "(λx. extract_pair' f g (h x)) ∈ measurable K (M ⨂⇩M N)"
by (rule measurable_compose[OF h[unfolded stock_measure.simps] measurable_embed_measure1])
(simp add: split_beta')
measurable_extract_pair[measurable]: "extract_pair ∈ measurable (PRODUCT t1 t2) (t1 ⨂⇩M t2)"
by measurable
measurable_extract_real[measurable]: "extract_real ∈ measurable REAL borel"
apply simp
apply measurable
apply (rule measurable_embed_measure1)
apply simp
done
measurable_extract_int[measurable]: "extract_int ∈ measurable INTEG (count_space UNIV)"
by simp measurable
measurable_extract_int_pair[measurable]:
"extract_int_pair ∈ measurable (PRODUCT INTEG INTEG) (count_space UNIV ⨂⇩M count_space UNIV)"
by measurable
measurable_extract_real_pair[measurable]:
"extract_real_pair ∈ measurable (PRODUCT REAL REAL) (borel ⨂⇩M borel)"
by measurable
measurable_extract_real_pair'[measurable]:
"extract_real_pair ∈ measurable (PRODUCT REAL REAL) borel"
by (subst borel_prod[symmetric]) measurable
measurable_extract_bool[measurable]: "extract_bool ∈ measurable BOOL (count_space UNIV)"
by simp
lemma map_int_pair_measurable[measurable]:
assumes f: "case_prod f ∈ measurable (count_space UNIV ⨂⇩M count_space UNIV) M"
shows "map_int_pair f g ∈ measurable (PRODUCT INTEG INTEG) M"
proof (subst measurable_cong)
fix w assume "w ∈ space (PRODUCT INTEG INTEG)"
then show "map_int_pair f g w = (case_prod f o extract_int_pair) w"
by (auto simp: space_embed_measure space_pair_measure)
next
show "(λ(x, y). f x y) ∘ extract_int_pair ∈ measurable (stock_measure (PRODUCT INTEG INTEG)) M"
using measurable_extract_int_pair f by (rule measurable)
qed
lemma map_int_pair_measurable_REAL[measurable]:
assumes "g ∈ measurable (PRODUCT REAL REAL) M"
shows "map_int_pair f g ∈ measurable (PRODUCT REAL REAL) M"
proof (subst measurable_cong)
fix w assume "w ∈ space (PRODUCT REAL REAL)"
then show "map_int_pair f g w = g w"
by (auto simp: space_embed_measure space_pair_measure map_int_pair_def)
qed fact
lemma map_real_pair_measurable[measurable]:
assumes f: "case_prod f ∈ measurable (borel ⨂⇩M borel) M"
shows "map_real_pair f g ∈ measurable (PRODUCT REAL REAL) M"
proof (subst measurable_cong)
fix w assume "w ∈ space (PRODUCT REAL REAL)"
then show "map_real_pair f g w = (case_prod f o extract_real_pair) w"
by (auto simp: space_embed_measure space_pair_measure)
next
show "(λ(x, y). f x y) ∘ extract_real_pair ∈ measurable (stock_measure (PRODUCT REAL REAL)) M"
using measurable_extract_real_pair f by (rule measurable)
qed
lemma count_space_IntVal_prod[simp]: "INTEG ⨂⇩M INTEG = count_space (range IntVal × range IntVal)"
by (auto intro!: pair_measure_countable)
lemma count_space_BoolVal_prod[simp]: "BOOL ⨂⇩M BOOL = count_space (range BoolVal × range BoolVal)"
by (auto intro!: pair_measure_countable)
lemma measurable_stock_measure_val_type:
assumes "f ∈ measurable M (stock_measure t)" "x ∈ space M"
shows "val_type (f x) = t"
using assms by (auto dest!: measurable_space)
lemma singleton_in_stock_measure[simp]: "val_type v = t ⟹ {v} ∈ sets t"
proof (induction v arbitrary: t)
case (PairVal v1 v2)
have A: "{<|v1, v2|>} = (λ(v1,v2). <|v1,v2|>) ` ({v1}×{v2})" by simp
from pair_measureI[OF PairVal.IH, OF refl refl] PairVal.prems[symmetric] show ?case
by (simp only: val_type.simps stock_measure.simps A in_sets_embed_measure)
qed (auto simp: sets_embed_measure)
lemma emeasure_stock_measure_singleton_finite[simp]:
"emeasure (stock_measure (val_type v)) {v} ≠ ∞"
proof (induction v)
case (RealVal r)
have A: "{RealVal r} = RealVal ` {r}" by simp
have "RealVal ` {r} ∈ sets (embed_measure lborel RealVal)"
by (rule in_sets_embed_measure) simp
thus ?case by (simp only: A val_type.simps stock_measure.simps emeasure_embed_measure
inj_RealVal inj_vimage_image_eq) simp
next
case (PairVal v1 v2)
let ?M = "λx. stock_measure (val_type x)"
interpret sigma_finite_measure "stock_measure (val_type v2)"
by (rule sigma_finite_stock_measure)
have A: "{<|v1, v2|>} = (λ(v1,v2). <|v1,v2|>) ` ({v1}×{v2})" by simp
have B: "{v1}×{v2} ∈ ?M v1 ⨂⇩M ?M v2"
by (intro pair_measureI singleton_in_stock_measure) simp_all
hence "emeasure (?M (<|v1,v2|>)) {<|v1,v2|>} = emeasure (?M v1) {v1} * emeasure (?M v2) {v2}"
by (simp only: stock_measure.simps val_type.simps A emeasure_embed_measure_image inj_PairVal
inj_vimage_image_eq emeasure_pair_measure_Times singleton_in_stock_measure B)
with PairVal.IH show ?case by (simp add: ennreal_mult_eq_top_iff)
qed simp_all
subsection ‹Measures on states›
definition state_measure :: "vname set ⇒ (vname ⇒ pdf_type) ⇒ state measure" where
"state_measure V Γ ≡ Π⇩M y∈V. Γ y"
lemma state_measure_nonempty[simp]: "space (state_measure V Γ) ≠ {}"
by (simp add: state_measure_def space_PiM PiE_eq_empty_iff)
lemma space_state_measure: "space (state_measure V Γ) = (Π⇩E y∈V. type_universe (Γ y))"
by (simp add: state_measure_def space_PiM PiE_eq_empty_iff)
lemma state_measure_var_type:
"σ ∈ space (state_measure V Γ) ⟹ x ∈ V ⟹ val_type (σ x) = Γ x"
by (auto simp: state_measure_def space_PiM dest!: PiE_mem)
lemma merge_in_state_measure:
"x ∈ space (state_measure A Γ) ⟹ y ∈ space (state_measure B Γ) ⟹
merge A B (x, y) ∈ space (state_measure (A∪B) Γ)" unfolding state_measure_def
by (rule measurable_space, rule measurable_merge) (simp add: space_pair_measure)
lemma measurable_merge_stock[measurable (raw)]:
"f ∈ N →⇩M state_measure V Γ ⟹ g ∈ N →⇩M state_measure V' Γ ⟹
(λx. merge V V' (f x, g x)) ∈ N →⇩M state_measure (V ∪ V') Γ"
by (auto simp: state_measure_def)
lemma comp_in_state_measure:
assumes "σ ∈ space (state_measure V Γ)"
shows "σ ∘ f ∈ space (state_measure (f -` V) (Γ ∘ f))"
using assms by (auto simp: state_measure_def space_PiM)
lemma sigma_finite_state_measure[intro]:
"finite V ⟹ sigma_finite_measure (state_measure V Γ)" unfolding state_measure_def
by (auto intro!: product_sigma_finite.sigma_finite simp: product_sigma_finite_def)
subsection ‹Equalities of measure embeddings›
lemma embed_measure_RealPairVal:
"stock_measure (PRODUCT REAL REAL) = embed_measure lborel RealPairVal"
proof-
have [simp]: "(λ(x, y). <| x , y |>) ∘ (λ(x, y). (RealVal x, RealVal y)) = RealPairVal"
unfolding RealPairVal_def by auto
have "stock_measure (PRODUCT REAL REAL) =
embed_measure (embed_measure lborel (λ(x, y). (RealVal x, RealVal y))) (case_prod PairVal)"
by (auto simp: embed_measure_prod sigma_finite_lborel lborel_prod)
also have "... = embed_measure lborel RealPairVal"
by (subst embed_measure_comp) (auto intro!: injI)
finally show ?thesis .
qed
lemma embed_measure_IntPairVal:
"stock_measure (PRODUCT INTEG INTEG) = count_space (range IntPairVal)"
proof-
have [simp]: "(λ(x, y). <| x , y |>) ` (range IntVal × range IntVal) = range IntPairVal"
by (auto simp: IntPairVal_def)
show ?thesis
using count_space_IntVal_prod by (auto simp: embed_measure_prod embed_measure_count_space)
qed
subsection ‹Monadic operations on values›
definition "return_val x = return (stock_measure (val_type x)) x"
lemma sets_return_val[measurable_cong]: "sets (return_val x) = sets (stock_measure (val_type x))"
by (simp add: return_val_def)
lemma measurable_return_val[simp]:
"return_val ∈ measurable (stock_measure t) (subprob_algebra (stock_measure t))"
unfolding return_val_def[abs_def]
apply (subst measurable_cong)
apply (subst type_universe_type[THEN iffD1])
apply simp
apply (rule refl)
apply (rule return_measurable)
done
lemma bind_return_val:
assumes "space M ≠ {}" "f ∈ measurable M (stock_measure t')"
shows "M ⤜ (λx. return_val (f x)) = distr M (stock_measure t') f"
using assms
by (subst bind_return_distr[symmetric])
(auto simp: return_val_def intro!: bind_cong dest: measurable_stock_measure_val_type)
lemma bind_return_val':
assumes "val_type x = t" "f ∈ measurable (stock_measure t) (stock_measure t')"
shows "return_val x ⤜ (λx. return_val (f x)) = return_val (f x)"
proof-
have "return_val x ⤜ (λx. return_val (f x)) = return (stock_measure t') (f x)"
apply (subst bind_return_val, unfold return_val_def, simp)
apply (insert assms, simp cong: measurable_cong_sets) []
apply (subst distr_return, simp_all add: assms type_universe_def
del: type_universe_type)
done
also from assms(2) have "f x ∈ space (stock_measure t')"
by (rule measurable_space)
(simp add: assms(1) type_universe_def del: type_universe_type)
hence "return (stock_measure t') (f x) = return_val (f x)"
by (simp add: return_val_def)
finally show ?thesis .
qed
lemma bind_return_val'':
assumes "f ∈ measurable (stock_measure (val_type x)) (subprob_algebra M)"
shows "return_val x ⤜ f = f x"
unfolding return_val_def by (subst bind_return[OF assms]) simp_all
lemma bind_assoc_return_val:
assumes sets_M: "sets M = sets (stock_measure t)"
assumes Mf: "f ∈ measurable (stock_measure t) (stock_measure t')"
assumes Mg: "g ∈ measurable (stock_measure t') (stock_measure t'')"
shows "(M ⤜ (λx. return_val (f x))) ⤜ (λx. return_val (g x)) =
M ⤜ (λx. return_val (g (f x)))"
proof-
have "(M ⤜ (λx. return_val (f x))) ⤜ (λx. return_val (g x)) =
M ⤜ (λx. return_val (f x) ⤜ (λx. return_val (g x)))"
apply (subst bind_assoc)
apply (rule measurable_compose[OF _ measurable_return_val])
apply (subst measurable_cong_sets[OF sets_M refl], rule Mf)
apply (rule measurable_compose[OF Mg measurable_return_val], rule refl)
done
also have "... = M ⤜ (λx. return_val (g (f x)))"
apply (intro bind_cong refl)
apply (subst (asm) sets_eq_imp_space_eq[OF sets_M])
apply (drule measurable_space[OF Mf])
apply (subst bind_return_val'[where t = t' and t' = t''])
apply (simp_all add: Mg)
done
finally show ?thesis .
qed
lemma bind_return_val_distr:
assumes sets_M: "sets M = sets (stock_measure t)"
assumes Mf: "f ∈ measurable (stock_measure t) (stock_measure t')"
shows "M ⤜ return_val ∘ f = distr M (stock_measure t') f"
proof-
have "M ⤜ return_val ∘ f = M ⤜ return (stock_measure t') ∘ f"
apply (intro bind_cong refl)
apply (subst (asm) sets_eq_imp_space_eq[OF sets_M])
apply (drule measurable_space[OF Mf])
apply (simp add: return_val_def o_def)
done
also have "... = distr M (stock_measure t') f"
apply (rule bind_return_distr)
apply (simp add: sets_eq_imp_space_eq[OF sets_M])
apply (subst measurable_cong_sets[OF sets_M refl], rule Mf)
done
finally show ?thesis .
qed
subsection ‹Lifting of functions›
definition lift_RealVal where
"lift_RealVal f ≡ λ RealVal v ⇒ RealVal (f v) | _ ⇒ RealVal (f 0)"
definition lift_IntVal where
"lift_IntVal f ≡ λ IntVal v ⇒ IntVal (f v) | _ ⇒ IntVal (f 0)"
definition lift_RealIntVal where
"lift_RealIntVal f g ≡ λ IntVal v ⇒ IntVal (f v) | RealVal v ⇒ RealVal (g v)"
definition lift_RealIntVal2 where
"lift_RealIntVal2 f g ≡
map_int_pair (λa b. IntVal (f a b))
(map_real_pair (λa b. RealVal (g a b))
id)"
definition lift_Comp where
"lift_Comp f g ≡ map_int_pair (λa b. BoolVal (f a b))
(map_real_pair (λa b. BoolVal (g a b))
(λ_. FALSE))"
lemma lift_RealVal_eq: "lift_RealVal f (RealVal x) = RealVal (f x)"
by (simp add: lift_RealVal_def)
lemma lift_RealIntVal_Real:
"x ∈ space (stock_measure REAL) ⟹ lift_RealIntVal f g x = lift_RealVal g x"
by (auto simp: space_embed_measure lift_RealIntVal_def lift_RealVal_def)
lemma lift_RealIntVal_Int:
"x ∈ space (stock_measure INTEG) ⟹ lift_RealIntVal f g x = lift_IntVal f x"
by (auto simp: space_embed_measure lift_RealIntVal_def lift_IntVal_def)
declare stock_measure.simps[simp del]
lemma measurable_lift_RealVal[measurable]:
assumes [measurable]: "f ∈ borel_measurable borel"
shows "lift_RealVal f ∈ measurable REAL REAL"
unfolding lift_RealVal_def
by (auto intro!: val_case_stock_measurable)
lemma measurable_lift_IntVal[simp]: "lift_IntVal f ∈ range IntVal → range IntVal"
by (auto simp: lift_IntVal_def)
lemma measurable_lift_IntVal'[measurable]: "lift_IntVal f ∈ measurable INTEG INTEG"
unfolding lift_IntVal_def
by (auto intro!: val_case_stock_measurable)
lemma split_apply: "(case x of (a, b) ⇒ f a b) y = (case x of (a, b) ⇒ f a b y)"
by (cases x) simp
lemma measurable_lift_Comp_RealVal[measurable]:
assumes [measurable]: "Measurable.pred (borel ⨂⇩M borel) (case_prod g)"
shows "lift_Comp f g ∈ measurable (PRODUCT REAL REAL) BOOL"
unfolding lift_Comp_def by measurable
lemma measurable_lift_Comp_IntVal[simp]:
"lift_Comp f g ∈ measurable (PRODUCT INTEG INTEG) BOOL"
unfolding lift_Comp_def
by (auto intro!: val_case_stock_measurable)
lemma measurable_lift_RealIntVal_IntVal[simp]: "lift_RealIntVal f g ∈ range IntVal → range IntVal"
by (auto simp: embed_measure_count_space lift_RealIntVal_def)
lemma measurable_lift_RealIntVal_IntVal'[measurable]:
"lift_RealIntVal f g ∈ measurable INTEG INTEG"
by (auto simp: lift_RealIntVal_def intro!: val_case_stock_measurable)
lemma measurable_lift_RealIntVal_RealVal[measurable]:
assumes [measurable]: "g ∈ borel_measurable borel"
shows "lift_RealIntVal f g ∈ measurable REAL REAL"
unfolding lift_RealIntVal_def
by (auto intro!: val_case_stock_measurable)
lemma measurable_lift_RealIntVal2_IntVal[measurable]:
"lift_RealIntVal2 f g ∈ measurable (PRODUCT INTEG INTEG) INTEG"
unfolding lift_RealIntVal2_def
by (auto intro!: val_case_stock_measurable)
lemma measurable_lift_RealIntVal2_RealVal[measurable]:
assumes [measurable]: "case_prod g ∈ borel_measurable (borel ⨂⇩M borel)"
shows "lift_RealIntVal2 f g ∈ measurable (PRODUCT REAL REAL) REAL"
unfolding lift_RealIntVal2_def by measurable
lemma distr_lift_RealVal:
fixes f
assumes Mf[measurable]: "f ∈ borel_measurable borel"
assumes pdens: "has_subprob_density M (stock_measure REAL) δ"
assumes dens': "⋀M δ. has_subprob_density M lborel δ ⟹ has_density (distr M borel f) lborel (g δ)"
defines "N ≡ distr M (stock_measure REAL) (lift_RealVal f)"
shows "has_density N (stock_measure REAL) (g (λx. δ (RealVal x)) ∘ extract_real)"
proof (rule has_densityI)
from assms(2) have dens: "has_density M (stock_measure REAL) δ"
unfolding has_subprob_density_def by simp
from dens have sets_M[measurable_cong]: "sets M = sets REAL" by (auto dest: has_densityD)
note measurable_embed_measure1[measurable del]
have "N = distr M (stock_measure REAL) (lift_RealVal f)" by (simp add: N_def)
also have "… = distr M (stock_measure REAL) (RealVal ∘ f ∘ extract_real)"
using sets_eq_imp_space_eq[OF sets_M]
by (intro distr_cong) (auto simp: lift_RealVal_def stock_measure.simps space_embed_measure)
also have "... = distr (distr (distr M lborel extract_real) borel f) (stock_measure REAL) RealVal"
by (subst distr_distr)
(simp_all add: distr_distr[OF _ measurable_comp[OF _ Mf]] comp_assoc)
also have dens'': "has_density (distr (distr M lborel extract_real) borel f) lborel (g (δ ∘ RealVal))"
by (intro dens' has_subprob_density_embed_measure'') (insert pdens, simp_all add: extract_real_def stock_measure.simps)
hence "distr (distr M lborel extract_real) borel f = density lborel (g (δ ∘ RealVal))"
by (rule has_densityD)
also have "distr ... (stock_measure REAL) RealVal = embed_measure ... RealVal" (is "_ = ?M")
by (subst embed_measure_eq_distr[OF inj_RealVal], intro distr_cong)
(simp_all add: sets_embed_measure stock_measure.simps)
also have "... = density (embed_measure lborel RealVal) (g (λx. δ (RealVal x)) ∘ extract_real)"
using dens''[unfolded o_def]
apply (subst density_embed_measure', simp, simp add: extract_real_def)
apply (erule has_densityD, simp add: o_def)
done
finally show "N = density (stock_measure REAL) (g (λx. δ (RealVal x)) ∘ extract_real)"
by (simp add: stock_measure.simps)
from dens''[unfolded o_def, THEN has_densityD(1)] measurable_extract_real
show "g (λx. δ (RealVal x)) ∘ extract_real ∈ borel_measurable (stock_measure REAL)"
by (intro measurable_comp) auto
qed (subst space_stock_measure, simp)
lemma distr_lift_IntVal:
fixes f
assumes pdens: "has_density M (stock_measure INTEG) δ"
assumes dens': "⋀M δ. has_density M (count_space UNIV) δ ⟹
has_density (distr M (count_space UNIV) f) (count_space UNIV) (g δ)"
defines "N ≡ distr M (stock_measure INTEG) (lift_IntVal f)"
shows "has_density N (stock_measure INTEG) (g (λx. δ (IntVal x)) ∘ extract_int)"
proof (rule has_densityI)
let ?R = "count_space UNIV" and ?S = "count_space (range IntVal)"
have Mf: "f ∈ measurable ?R ?R" by simp
from assms(1) have dens: "has_density M (stock_measure INTEG) δ"
unfolding has_subprob_density_def by simp
from dens have sets_M[measurable_cong]: "sets M = sets INTEG" by (auto dest!: has_densityD(2))
have "N = distr M (stock_measure INTEG) (lift_IntVal f)" by (simp add: N_def)
also have "… = distr M (stock_measure INTEG) (IntVal ∘ f ∘ extract_int)"
using sets_eq_imp_space_eq[OF sets_M]
by (intro distr_cong) (auto simp: space_embed_measure lift_IntVal_def stock_measure.simps)
also have "… = distr (distr (distr M ?R extract_int) ?R f) (stock_measure INTEG) IntVal"
by (subst distr_distr) (simp_all add: distr_distr[OF _ measurable_comp[OF _ Mf]] comp_assoc)
also have dens'': "has_density (distr (distr M ?R extract_int) ?R f) ?R (g (δ ∘ IntVal))"
by (intro dens' has_density_embed_measure'')
(insert dens, simp_all add: extract_int_def embed_measure_count_space stock_measure.simps)
hence "distr (distr M ?R extract_int) ?R f = density ?R (g (δ ∘ IntVal))"
by (rule has_densityD)
also have "distr ... (stock_measure INTEG) IntVal = embed_measure ... IntVal" (is "_ = ?M")
by (subst embed_measure_eq_distr[OF inj_IntVal], intro distr_cong)
(auto simp: sets_embed_measure subset_image_iff stock_measure.simps)
also have "... = density (embed_measure ?R IntVal) (g (λx. δ (IntVal x)) ∘ extract_int)"
using dens''[unfolded o_def]
apply (subst density_embed_measure', simp, simp add: extract_int_def)
apply (erule has_densityD, simp add: o_def)
done
finally show "N = density (stock_measure INTEG) (g (λx. δ (IntVal x)) ∘ extract_int)"
by (simp add: embed_measure_count_space stock_measure.simps)
from dens''[unfolded o_def]
show "g (λx. δ (IntVal x)) ∘ extract_int ∈ borel_measurable (stock_measure INTEG)"
by (simp add: embed_measure_count_space stock_measure.simps)
qed (subst space_stock_measure, simp)
lemma distr_lift_RealPairVal:
fixes f f' g
assumes Mf[measurable]: "case_prod f ∈ borel_measurable borel"
assumes pdens: "has_subprob_density M (stock_measure (PRODUCT REAL REAL)) δ"
assumes dens': "⋀M δ. has_subprob_density M lborel δ ⟹ has_density (distr M borel (case_prod f)) lborel (g δ)"
defines "N ≡ distr M (stock_measure REAL) (lift_RealIntVal2 f' f)"
shows "has_density N (stock_measure REAL) (g (λx. δ (RealPairVal x)) ∘ extract_real)"
proof (rule has_densityI)
from assms(2) have dens: "has_density M (stock_measure (PRODUCT REAL REAL)) δ"
unfolding has_subprob_density_def by simp
have sets_M[measurable_cong]: "sets M = sets (stock_measure (PRODUCT REAL REAL))"
by (auto simp: has_subprob_densityD[OF pdens])
have "N = distr M (stock_measure REAL) (lift_RealIntVal2 f' f)" by (simp add: N_def)
also have "... = distr M (stock_measure REAL) (RealVal ∘ case_prod f ∘ extract_real_pair)"
using sets_eq_imp_space_eq[OF sets_M]
by (intro distr_cong) (auto simp: lift_RealIntVal2_def space_embed_measure space_pair_measure stock_measure.simps)
also have "... = distr (distr (distr M lborel extract_real_pair) borel (case_prod f)) REAL RealVal"
by (subst distr_distr) (simp_all add: distr_distr[OF _ measurable_comp[OF _ Mf]] comp_assoc)
also have dens'': "has_density (distr (distr M lborel extract_real_pair) borel (case_prod f)) lborel
(g (δ ∘ RealPairVal))" using inj_RealPairVal embed_measure_RealPairVal
by (intro dens' has_subprob_density_embed_measure'')
(insert pdens, simp_all add: RealPairVal_def split: prod.split)
hence "distr (distr M lborel extract_real_pair) borel (case_prod f) =
density lborel (g (δ ∘ RealPairVal))" by (rule has_densityD)
also have "distr ... (stock_measure REAL) RealVal = embed_measure ... RealVal" (is "_ = ?M")
by (subst embed_measure_eq_distr[OF inj_RealVal], intro distr_cong)
(simp_all add: sets_embed_measure stock_measure.simps)
also have "... = density (embed_measure lborel RealVal) (g (λx. δ (RealPairVal x)) ∘ extract_real)"
using dens''[unfolded o_def]
by (subst density_embed_measure', simp, simp add: extract_real_def)
(erule has_densityD, simp add: o_def)
finally show "N = density (stock_measure REAL) (g (λx. δ (RealPairVal x)) ∘ extract_real)"
by (simp add: stock_measure.simps)
from dens''[unfolded o_def]
show "g (λx. δ (RealPairVal x)) ∘ extract_real ∈ borel_measurable (stock_measure REAL)"
by (intro measurable_comp)
(rule measurable_extract_real, subst measurable_lborel2[symmetric], erule has_densityD)
qed (subst space_stock_measure, simp)
lemma distr_lift_IntPairVal:
fixes f f'
assumes pdens: "has_density M (stock_measure (PRODUCT INTEG INTEG)) δ"
assumes dens': "⋀M δ. has_density M (count_space UNIV) δ ⟹
has_density (distr M (count_space UNIV) (case_prod f))
(count_space UNIV) (g δ)"
defines "N ≡ distr M (stock_measure INTEG) (lift_RealIntVal2 f f')"
shows "has_density N (stock_measure INTEG) (g (λx. δ (IntPairVal x)) ∘ extract_int)"
proof (rule has_densityI)
let ?R = "count_space UNIV" and ?S = "count_space (range IntVal)"
and ?T = "count_space (range IntPairVal)" and ?tp = "PRODUCT INTEG INTEG"
have Mf: "f ∈ measurable ?R ?R" by simp
have MIV: "IntVal ∈ measurable ?R ?S" by simp
from assms(1) have dens: "has_density M (stock_measure ?tp) δ"
unfolding has_subprob_density_def by simp
from dens have "M = density (stock_measure ?tp) δ" by (rule has_densityD)
hence sets_M: "sets M = sets ?T" by (subst embed_measure_IntPairVal[symmetric]) auto
hence [simp]: "space M = space ?T" by (rule sets_eq_imp_space_eq)
from sets_M have [simp]: "measurable M = measurable (count_space (range IntPairVal))"
by (intro ext measurable_cong_sets) simp_all
have "N = distr M (stock_measure INTEG) (lift_RealIntVal2 f f')" by (simp add: N_def)
also have "... = distr M (stock_measure INTEG) (IntVal ∘ case_prod f ∘ extract_int_pair)"
by (intro distr_cong) (auto simp: lift_RealIntVal2_def space_embed_measure space_pair_measure IntPairVal_def)
also have "... = distr (distr (distr M (count_space UNIV) extract_int_pair)
(count_space UNIV) (case_prod f)) (stock_measure INTEG) IntVal"
apply (subst distr_distr[of _ ?R, symmetric], simp, simp)
apply (subst distr_distr[symmetric], subst stock_measure.simps, rule MIV,
simp_all add: assms(1) cong: distr_cong)
done
also have dens'': "has_density (distr (distr M (count_space UNIV) extract_int_pair) ?R (case_prod f)) ?R
(g (δ ∘ IntPairVal))" using inj_IntPairVal embed_measure_IntPairVal
by (intro dens' has_density_embed_measure'')
(insert dens, simp_all add: extract_int_def embed_measure_count_space IntPairVal_def split: prod.split)
hence "distr (distr M (count_space UNIV) extract_int_pair) ?R (case_prod f) =
density ?R (g (δ ∘ IntPairVal))" by (rule has_densityD)
also have "distr ... (stock_measure INTEG) IntVal = embed_measure ... IntVal" (is "_ = ?M")
by (subst embed_measure_eq_distr[OF inj_IntVal], intro distr_cong)
(auto simp: sets_embed_measure subset_image_iff stock_measure.simps)
also have "... = density (embed_measure ?R IntVal) (g (λx. δ (IntPairVal x)) ∘ extract_int)"
using dens''[unfolded o_def]
by (subst density_embed_measure', simp, simp add: extract_int_def)
(erule has_densityD, simp add: o_def)
finally show "N = density (stock_measure INTEG) (g (λx. δ (IntPairVal x)) ∘ extract_int)"
by (simp add: embed_measure_count_space stock_measure.simps)
from dens''[unfolded o_def]
show "g (λx. δ (IntPairVal x)) ∘ extract_int ∈ borel_measurable (stock_measure INTEG)"
by (simp add: embed_measure_count_space stock_measure.simps)
qed (subst space_stock_measure, simp)
end
Theory PDF_Semantics
theory PDF_Semantics
imports PDF_Values
begin
lemma measurable_subprob_algebra_density:
assumes "sigma_finite_measure N"
assumes "space N ≠ {}"
assumes [measurable]: "case_prod f ∈ borel_measurable (M ⨂⇩M N)"
assumes "⋀x. x ∈ space M ⟹ (∫⇧+y. f x y ∂N) ≤ 1"
shows "(λx. density N (f x)) ∈ measurable M (subprob_algebra N)"
proof (rule measurable_subprob_algebra)
fix x assume "x ∈ space M"
with assms show "subprob_space (density N (f x))"
by (intro subprob_spaceI) (auto simp: emeasure_density cong: nn_integral_cong')
next
interpret sigma_finite_measure N by fact
fix X assume X: "X ∈ sets N"
hence "(λx. (∫⇧+y. f x y * indicator X y ∂N)) ∈ borel_measurable M" by simp
moreover from X and assms have
"⋀x. x ∈ space M ⟹ emeasure (density N (f x)) X = (∫⇧+y. f x y * indicator X y ∂N)"
by (simp add: emeasure_density)
ultimately show "(λx. emeasure (density N (f x)) X) ∈ borel_measurable M"
by (simp only: cong: measurable_cong)
qed simp_all
section ‹Built-in Probability Distributions›
subsection ‹Bernoulli›
definition bernoulli_density :: "real ⇒ bool ⇒ ennreal" where
"bernoulli_density p b = (if p ∈ {0..1} then (if b then p else 1 - p) else 0)"
definition bernoulli :: "val ⇒ val measure" where
"bernoulli p = density BOOL (bernoulli_density (extract_real p) o extract_bool)"
lemma measurable_bernoulli_density[measurable]:
"case_prod bernoulli_density ∈ borel_measurable (borel ⨂⇩M count_space UNIV)"
unfolding bernoulli_density_def[abs_def] by measurable
lemma measurable_bernoulli[measurable]: "bernoulli ∈ measurable REAL (subprob_algebra BOOL)"
unfolding bernoulli_def[abs_def]
by (auto intro!: measurable_subprob_algebra_density
simp: measurable_split_conv nn_integral_BoolVal bernoulli_density_def
ennreal_plus[symmetric]
simp del: ennreal_plus)
subsection ‹Uniform›
definition uniform_real_density :: "real × real ⇒ real ⇒ ennreal" where
"uniform_real_density ≡ λ(a,b) x. ennreal (if a < b ∧ x ∈ {a..b} then inverse (b - a) else 0)"
definition uniform_int_density :: "int × int ⇒ int ⇒ ennreal" where
"uniform_int_density ≡ λ(a,b) x. (if x ∈ {a..b} then inverse (nat (b - a + 1)) else 0)"
lemma measurable_uniform_density_int[measurable]:
"(case_prod uniform_int_density)
∈ borel_measurable ((count_space UNIV ⨂⇩M count_space UNIV) ⨂⇩M count_space UNIV)"
by (simp add: pair_measure_countable)
lemma measurable_uniform_density_real[measurable]:
"(case_prod uniform_real_density) ∈ borel_measurable (borel ⨂⇩M borel)"
proof-
have "(case_prod uniform_real_density) =
(λx. uniform_real_density (fst (fst x), snd (fst x)) (snd x))"
by (rule ext) (simp split: prod.split)
also have "... ∈ borel_measurable (borel ⨂⇩M borel)"
unfolding uniform_real_density_def
by (simp only: prod.case) (simp add: borel_prod[symmetric])
finally show ?thesis .
qed
definition uniform_int :: "val ⇒ val measure" where
"uniform_int = map_int_pair (λl u. density INTEG (uniform_int_density (l,u) o extract_int)) (λ_. undefined)"
definition uniform_real :: "val ⇒ val measure" where
"uniform_real = map_real_pair (λl u. density REAL (uniform_real_density (l,u) o extract_real)) (λ_. undefined)"
lemma if_bounded: "(if a ≤ i ∧ i ≤ b then v else 0) = (v::real) * indicator {a .. b} i"
by auto
lemma measurable_uniform_int[measurable]:
"uniform_int ∈ measurable (PRODUCT INTEG INTEG) (subprob_algebra INTEG)"
unfolding uniform_int_def
proof (rule measurable measurable_subprob_algebra_density)+
fix x :: "int × int"
show "integral⇧N INTEG (uniform_int_density (fst x, snd x) ∘ extract_int) ≤ 1"
proof cases
assume "fst x ≤ snd x" then show ?thesis
by (cases x)
(simp add: uniform_int_density_def comp_def nn_integral_IntVal nn_integral_cmult
nn_integral_set_ennreal[symmetric] ennreal_of_nat_eq_real_of_nat
if_bounded[where 'a=int] ennreal_mult[symmetric]
del: ennreal_plus)
qed (simp add: uniform_int_density_def comp_def split_beta' if_bounded[where 'a=int])
qed (auto simp: comp_def)
lemma density_cong':
"(⋀x. x ∈ space M ⟹ f x = g x) ⟹ density M f = density M g"
unfolding density_def
by (auto dest: sets.sets_into_space intro!: nn_integral_cong measure_of_eq)
lemma measurable_uniform_real[measurable]:
"uniform_real ∈ measurable (PRODUCT REAL REAL) (subprob_algebra REAL)"
unfolding uniform_real_def
proof (rule measurable measurable_subprob_algebra_density)+
fix x :: "real × real"
obtain l u where [simp]: "x = (l, u)"
by (cases x) auto
show "(∫⇧+y. (uniform_real_density (fst x, snd x) o extract_real) y ∂REAL) ≤ 1"
proof cases
assume "l < u" then show ?thesis
by (simp add: nn_integral_RealVal uniform_real_density_def if_bounded nn_integral_cmult
nn_integral_set_ennreal[symmetric] ennreal_mult[symmetric])
qed (simp add: uniform_real_density_def comp_def)
qed (auto simp: comp_def borel_prod)
subsection ‹Gaussian›
definition gaussian_density :: "real × real ⇒ real ⇒ ennreal" where
"gaussian_density ≡
λ(m,s) x. (if s > 0 then exp (-(x - m)⇧2 / (2 * s⇧2)) / sqrt (2 * pi * s⇧2) else 0)"
lemma measurable_gaussian_density[measurable]:
"case_prod gaussian_density ∈ borel_measurable (borel ⨂⇩M borel)"
proof-
have "case_prod gaussian_density =
(λ(x,y). (if snd x > 0 then exp (-((y - fst x)^2) / (2 * snd x^2)) /
sqrt (2 * pi * snd x^2) else 0))"
unfolding gaussian_density_def by (intro ext) (simp split: prod.split)
also have "... ∈ borel_measurable (borel ⨂⇩M borel)"
by (simp add: borel_prod[symmetric])
finally show ?thesis .
qed
definition gaussian :: "val ⇒ val measure" where
"gaussian = map_real_pair (λm s. density REAL (gaussian_density (m,s) o extract_real)) undefined"
lemma measurable_gaussian[measurable]: "gaussian ∈ measurable (PRODUCT REAL REAL) (subprob_algebra REAL)"
unfolding gaussian_def
proof (rule measurable measurable_subprob_algebra_density)+
fix x :: "real × real"
show "integral⇧N (stock_measure REAL) (gaussian_density (fst x, snd x) ∘ extract_real) ≤ 1"
proof cases
assume "snd x > 0"
then have "integral⇧N lborel (gaussian_density x) = (∫⇧+y. normal_density (fst x) (snd x) y ∂lborel)"
by (auto simp add: gaussian_density_def normal_density_def split_beta' intro!: nn_integral_cong)
also have "… = 1"
using ‹snd x > 0›
by (subst nn_integral_eq_integral) (auto intro!: normal_density_nonneg)
finally show ?thesis
by (cases x) (simp add: nn_integral_RealVal comp_def)
next
assume "¬ snd x > 0" then show ?thesis
by (cases x)
(simp add: nn_integral_RealVal comp_def gaussian_density_def zero_ennreal_def[symmetric])
qed
qed (auto simp: comp_def borel_prod)
subsection ‹Poisson›
definition poisson_density' :: "real ⇒ int ⇒ ennreal" where
"poisson_density' rate k = pmf (poisson_pmf rate) (nat k) * indicator ({0 <..} × {0..}) (rate, k)"
lemma measurable_poisson_density'[measurable]:
"case_prod poisson_density' ∈ borel_measurable (borel ⨂⇩M count_space UNIV)"
proof -
have "case_prod poisson_density' =
(λ(rate, k). rate ^ nat k / real_of_nat (fact (nat k)) * exp (-rate) * indicator ({0 <..} × {0..}) (rate, k))"
by (auto split: split_indicator simp: fun_eq_iff poisson_density'_def)
then show ?thesis
by simp
qed
definition poisson :: "val ⇒ val measure" where
"poisson rate = density INTEG (poisson_density' (extract_real rate) o extract_int)"
lemma measurable_poisson[measurable]: "poisson ∈ measurable REAL (subprob_algebra INTEG)"
unfolding poisson_def[abs_def]
proof (rule measurable measurable_subprob_algebra_density)+
fix r :: real
have [simp]: "nat ` {0..} = UNIV"
by (auto simp: image_iff intro!: bexI[of _ "int x" for x])
{ assume "0 < r"
then have "(∫⇧+ x. ennreal (r ^ nat x * exp (- r) * indicator ({0<..} × {0..}) (r, x) / (fact (nat x))) ∂count_space UNIV)
= (∫⇧+ x. ennreal (pmf (poisson_pmf r) (nat x)) ∂count_space {0 ..})"
by (auto intro!: nn_integral_cong simp add: nn_integral_count_space_indicator split: split_indicator)
also have "… = 1"
using measure_pmf.emeasure_space_1[of "poisson_pmf r"]
by (subst nn_integral_pmf') (auto simp: inj_on_def)
finally have "(∫⇧+ x. ennreal (r ^ nat x * exp (- r) * indicator ({0<..} × {0..}) (r, x) / (fact (nat x))) ∂count_space UNIV) = 1"
. }
then show "integral⇧N INTEG (poisson_density' r ∘ extract_int) ≤ 1"
by (cases "0 < r")
(auto simp: nn_integral_IntVal poisson_density'_def zero_ennreal_def[symmetric])
qed (auto simp: comp_def)
section ‹Source Language Syntax and Semantics›
subsection ‹Expressions›
class expr = fixes free_vars :: "'a ⇒ vname set"
datatype pdf_dist = Bernoulli | UniformInt | UniformReal | Poisson | Gaussian
datatype pdf_operator = Fst | Snd | Add | Mult | Minus | Less | Equals | And | Not | Or | Pow |
Sqrt | Exp | Ln | Fact | Inverse | Pi | Cast pdf_type
datatype expr =
Var vname
| Val val
| LetVar expr expr ("LET _ IN _" [0, 60] 61)
| Operator pdf_operator expr (infixl "$$" 999)
| Pair expr expr ("<_ , _>" [0, 60] 1000)
| Random pdf_dist expr
| IfThenElse expr expr expr ("IF _ THEN _ ELSE _" [0, 0, 70] 71)
| Fail pdf_type
type_synonym tyenv = "vname ⇒ pdf_type"
instantiation expr :: expr
begin
primrec free_vars_expr :: "expr ⇒ vname set" where
"free_vars_expr (Var x) = {x}"
| "free_vars_expr (Val _) = {}"
| "free_vars_expr (LetVar e1 e2) = free_vars_expr e1 ∪ Suc -` free_vars_expr e2"
| "free_vars_expr (Operator _ e) = free_vars_expr e"
| "free_vars_expr (<e1, e2>) = free_vars_expr e1 ∪ free_vars_expr e2"
| "free_vars_expr (Random _ e) = free_vars_expr e"
| "free_vars_expr (IF b THEN e1 ELSE e2) =
free_vars_expr b ∪ free_vars_expr e1 ∪ free_vars_expr e2"
| "free_vars_expr (Fail _) = {}"
instance ..
end
primrec free_vars_expr_code :: "expr ⇒ vname set" where
"free_vars_expr_code (Var x) = {x}"
| "free_vars_expr_code (Val _) = {}"
| "free_vars_expr_code (LetVar e1 e2) =
free_vars_expr_code e1 ∪ (λx. x - 1) ` (free_vars_expr_code e2 - {0})"
| "free_vars_expr_code (Operator _ e) = free_vars_expr_code e"
| "free_vars_expr_code (<e1, e2>) = free_vars_expr_code e1 ∪ free_vars_expr_code e2"
| "free_vars_expr_code (Random _ e) = free_vars_expr_code e"
| "free_vars_expr_code (IF b THEN e1 ELSE e2) =
free_vars_expr_code b ∪ free_vars_expr_code e1 ∪ free_vars_expr_code e2"
| "free_vars_expr_code (Fail _) = {}"
lemma free_vars_expr_code[code]:
"free_vars (e::expr) = free_vars_expr_code e"
proof-
have "⋀A. Suc -` A = (λx. x - 1) ` (A - {0})" by force
thus ?thesis by (induction e) simp_all
qed
primrec dist_param_type where
"dist_param_type Bernoulli = REAL"
| "dist_param_type Poisson = REAL"
| "dist_param_type Gaussian = PRODUCT REAL REAL"
| "dist_param_type UniformInt = PRODUCT INTEG INTEG"
| "dist_param_type UniformReal = PRODUCT REAL REAL"
primrec dist_result_type where
"dist_result_type Bernoulli = BOOL"
| "dist_result_type UniformInt = INTEG"
| "dist_result_type UniformReal = REAL"
| "dist_result_type Poisson = INTEG"
| "dist_result_type Gaussian = REAL"
primrec dist_measure :: "pdf_dist ⇒ val ⇒ val measure" where
"dist_measure Bernoulli = bernoulli"
| "dist_measure UniformInt = uniform_int"
| "dist_measure UniformReal = uniform_real"
| "dist_measure Poisson = poisson"
| "dist_measure Gaussian = gaussian"
lemma measurable_dist_measure[measurable]:
"dist_measure d ∈ measurable (dist_param_type d) (subprob_algebra (dist_result_type d))"
by (cases d) simp_all
lemma sets_dist_measure[simp]:
"val_type x = dist_param_type dst ⟹
sets (dist_measure dst x) = sets (stock_measure (dist_result_type dst))"
by (rule sets_kernel[OF measurable_dist_measure]) simp
lemma space_dist_measure[simp]:
"val_type x = dist_param_type dst ⟹
space (dist_measure dst x) = type_universe (dist_result_type dst)"
by (subst space_stock_measure[symmetric]) (intro sets_eq_imp_space_eq sets_dist_measure)
primrec dist_dens :: "pdf_dist ⇒ val ⇒ val ⇒ ennreal" where
"dist_dens Bernoulli x y = bernoulli_density (extract_real x) (extract_bool y)"
| "dist_dens UniformInt x y = uniform_int_density (extract_int_pair x) (extract_int y)"
| "dist_dens UniformReal x y = uniform_real_density (extract_real_pair x) (extract_real y)"
| "dist_dens Gaussian x y = gaussian_density (extract_real_pair x) (extract_real y)"
| "dist_dens Poisson x y = poisson_density' (extract_real x) (extract_int y)"
lemma measurable_dist_dens[measurable]:
assumes "f ∈ measurable M (stock_measure (dist_param_type dst))" (is "_ ∈ measurable M ?N")
assumes "g ∈ measurable M (stock_measure (dist_result_type dst))" (is "_ ∈ measurable M ?R")
shows "(λx. dist_dens dst (f x) (g x)) ∈ borel_measurable M"
apply (rule measurable_Pair_compose_split[of "dist_dens dst", OF _ assms])
apply (subst dist_dens_def, cases dst, simp_all)
done
lemma dist_measure_has_density:
"v ∈ type_universe (dist_param_type dst) ⟹
has_density (dist_measure dst v) (stock_measure (dist_result_type dst)) (dist_dens dst v)"
proof (intro has_densityI)
fix v assume "v ∈ type_universe (dist_param_type dst)"
thus "dist_measure dst v = density (stock_measure (dist_result_type dst)) (dist_dens dst v)"
by (cases dst)
(auto simp: bernoulli_def uniform_int_def uniform_real_def poisson_def gaussian_def
intro!: density_cong' elim!: PROD_E REAL_E INTEG_E)
qed simp_all
lemma subprob_space_dist_measure:
"v ∈ type_universe (dist_param_type dst) ⟹ subprob_space (dist_measure dst v)"
using subprob_space_kernel[OF measurable_dist_measure, of v dst] by simp
lemma dist_measure_has_subprob_density:
"v ∈ type_universe (dist_param_type dst) ⟹
has_subprob_density (dist_measure dst v) (stock_measure (dist_result_type dst)) (dist_dens dst v)"
unfolding has_subprob_density_def
by (auto intro: subprob_space_dist_measure dist_measure_has_density)
lemma dist_dens_integral_space:
assumes "v ∈ type_universe (dist_param_type dst)"
shows "(∫⇧+u. dist_dens dst v u ∂stock_measure (dist_result_type dst)) ≤ 1"
proof-
let ?M = "density (stock_measure (dist_result_type dst)) (dist_dens dst v)"
from assms have "(∫⇧+u. dist_dens dst v u ∂stock_measure (dist_result_type dst)) =
emeasure ?M (space ?M)"
by (subst space_density, subst emeasure_density)
(auto intro!: measurable_dist_dens cong: nn_integral_cong')
also have "?M = dist_measure dst v" using dist_measure_has_density[OF assms]
by (auto dest: has_densityD)
also from assms have "emeasure ... (space ...) ≤ 1"
by (intro subprob_space.emeasure_space_le_1 subprob_space_dist_measure)
finally show ?thesis .
qed
subsection ‹Typing›
primrec op_type :: "pdf_operator ⇒ pdf_type ⇒ pdf_type option" where
"op_type Add x =
(case x of
PRODUCT INTEG INTEG ⇒ Some INTEG
| PRODUCT REAL REAL ⇒ Some REAL
| _ ⇒ None)"
| "op_type Mult x =
(case x of
PRODUCT INTEG INTEG ⇒ Some INTEG
| PRODUCT REAL REAL ⇒ Some REAL
| _ ⇒ None)"
| "op_type Minus x =
(case x of
INTEG ⇒ Some INTEG
| REAL ⇒ Some REAL
| _ ⇒ None)"
| "op_type Equals x =
(case x of
PRODUCT t1 t2 ⇒ if t1 = t2 then Some BOOL else None
| _ ⇒ None)"
| "op_type Less x =
(case x of
PRODUCT INTEG INTEG ⇒ Some BOOL
| PRODUCT REAL REAL ⇒ Some BOOL
| _ ⇒ None)"
| "op_type (Cast t) x =
(case (x, t) of
(BOOL, INTEG) ⇒ Some INTEG
| (BOOL, REAL) ⇒ Some REAL
| (INTEG, REAL) ⇒ Some REAL
| (REAL, INTEG) ⇒ Some INTEG
| _ ⇒ None)"
| "op_type Or x = (case x of PRODUCT BOOL BOOL ⇒ Some BOOL | _ ⇒ None)"
| "op_type And x = (case x of PRODUCT BOOL BOOL ⇒ Some BOOL | _ ⇒ None)"
| "op_type Not x = (case x of BOOL ⇒ Some BOOL | _ ⇒ None)"
| "op_type Inverse x = (case x of REAL ⇒ Some REAL | _ ⇒ None)"
| "op_type Fact x = (case x of INTEG ⇒ Some INTEG | _ ⇒ None)"
| "op_type Sqrt x = (case x of REAL ⇒ Some REAL | _ ⇒ None)"
| "op_type Exp x = (case x of REAL ⇒ Some REAL | _ ⇒ None)"
| "op_type Ln x = (case x of REAL ⇒ Some REAL | _ ⇒ None)"
| "op_type Pi x = (case x of UNIT ⇒ Some REAL | _ ⇒ None)"
| "op_type Pow x = (case x of
PRODUCT REAL INTEG ⇒ Some REAL
| PRODUCT INTEG INTEG ⇒ Some INTEG
| _ ⇒ None)"
| "op_type Fst x = (case x of PRODUCT t _ ⇒ Some t | _ ⇒ None)"
| "op_type Snd x = (case x of PRODUCT _ t ⇒ Some t | _ ⇒ None)"
subsection ‹Semantics›
abbreviation (input) de_bruijn_insert (infixr "⋅" 65) where
"de_bruijn_insert x f ≡ case_nat x f"
inductive expr_typing :: "tyenv ⇒ expr ⇒ pdf_type ⇒ bool" ("(1_/ ⊢/ (_ :/ _))" [50,0,50] 50) where
et_var: "Γ ⊢ Var x : Γ x"
| et_val: "Γ ⊢ Val v : val_type v"
| et_let: "Γ ⊢ e1 : t1 ⟹ t1 ⋅ Γ ⊢ e2 : t2 ⟹ Γ ⊢ LetVar e1 e2 : t2"
| et_op: "Γ ⊢ e : t ⟹ op_type oper t = Some t' ⟹ Γ ⊢ Operator oper e : t'"
| et_pair: "Γ ⊢ e1 : t1 ⟹ Γ ⊢ e2 : t2 ⟹ Γ ⊢ <e1, e2> : PRODUCT t1 t2"
| et_rand: "Γ ⊢ e : dist_param_type dst ⟹ Γ ⊢ Random dst e : dist_result_type dst"
| et_if: "Γ ⊢ b : BOOL ⟹ Γ ⊢ e1 : t ⟹ Γ ⊢ e2 : t ⟹ Γ ⊢ IF b THEN e1 ELSE e2 : t"
| et_fail: "Γ ⊢ Fail t : t"
lemma expr_typing_cong':
"Γ ⊢ e : t ⟹ (⋀x. x ∈ free_vars e ⟹ Γ x = Γ' x) ⟹ Γ' ⊢ e : t"
proof (induction arbitrary: Γ' rule: expr_typing.induct)
case (et_let Γ e1 t1 e2 t2 Γ')
have "Γ' ⊢ e1 : t1" using et_let.prems by (intro et_let.IH(1)) auto
moreover have "case_nat t1 Γ' ⊢ e2 : t2"
using et_let.prems by (intro et_let.IH(2)) (auto split: nat.split)
ultimately show ?case by (auto intro!: expr_typing.intros)
qed (auto intro!: expr_typing.intros)
lemma expr_typing_cong:
"(⋀x. x ∈ free_vars e ⟹ Γ x = Γ' x) ⟹ Γ ⊢ e : t ⟷ Γ' ⊢ e : t"
by (intro iffI) (simp_all add: expr_typing_cong')
inductive_cases expr_typing_valE[elim]: "Γ ⊢ Val v : t"
inductive_cases expr_typing_varE[elim]: "Γ ⊢ Var x : t"
inductive_cases expr_typing_letE[elim]: "Γ ⊢ LetVar e1 e2 : t"
inductive_cases expr_typing_ifE[elim]: "Γ ⊢ IfThenElse b e1 e2 : t"
inductive_cases expr_typing_opE[elim]: "Γ ⊢ Operator oper e : t"
inductive_cases expr_typing_pairE[elim]: "Γ ⊢ <e1, e2> : t"
inductive_cases expr_typing_randE[elim]: "Γ ⊢ Random dst e : t"
inductive_cases expr_typing_failE[elim]: "Γ ⊢ Fail t : t'"
lemma expr_typing_unique:
"Γ ⊢ e : t ⟹ Γ ⊢ e : t' ⟹ t = t'"
apply (induction arbitrary: t' rule: expr_typing.induct)
apply blast
apply blast
apply (erule expr_typing_letE, blast)
apply (erule expr_typing_opE, simp)
apply (erule expr_typing_pairE, blast)
apply (erule expr_typing_randE, blast)
apply (erule expr_typing_ifE, blast)
apply blast
done
fun expr_type :: "tyenv ⇒ expr ⇒ pdf_type option" where
"expr_type Γ (Var x) = Some (Γ x)"
| "expr_type Γ (Val v) = Some (val_type v)"
| "expr_type Γ (LetVar e1 e2) =
(case expr_type Γ e1 of
Some t ⇒ expr_type (case_nat t Γ) e2
| None ⇒ None)"
| "expr_type Γ (Operator oper e) =
(case expr_type Γ e of Some t ⇒ op_type oper t | None ⇒ None)"
| "expr_type Γ (<e1, e2>) =
(case (expr_type Γ e1, expr_type Γ e2) of
(Some t1, Some t2) ⇒ Some (PRODUCT t1 t2)
| _ ⇒ None)"
| "expr_type Γ (Random dst e) =
(if expr_type Γ e = Some (dist_param_type dst) then
Some (dist_result_type dst)
else None)"
| "expr_type Γ (IF b THEN e1 ELSE e2) =
(if expr_type Γ b = Some BOOL then
(case (expr_type Γ e1, expr_type Γ e2) of
(Some t, Some t') ⇒ if t = t' then Some t else None
| _ ⇒ None) else None)"
| "expr_type Γ (Fail t) = Some t"
lemma expr_type_Some_iff: "expr_type Γ e = Some t ⟷ Γ ⊢ e : t"
apply rule
apply (induction e arbitrary: Γ t,
auto intro!: expr_typing.intros split: option.split_asm if_split_asm) []
apply (induction rule: expr_typing.induct, auto simp del: fun_upd_apply)
done
lemmas expr_typing_code[code_unfold] = expr_type_Some_iff[symmetric]
subsubsection ‹Countable types›
primrec countable_type :: "pdf_type ⇒ bool" where
"countable_type UNIT = True"
| "countable_type BOOL = True"
| "countable_type INTEG = True"
| "countable_type REAL = False"
| "countable_type (PRODUCT t1 t2) = (countable_type t1 ∧ countable_type t2)"
lemma countable_type_countable[dest]:
"countable_type t ⟹ countable (space (stock_measure t))"
by (induction t)
(auto simp: pair_measure_countable space_embed_measure space_pair_measure stock_measure.simps)
lemma countable_type_imp_count_space:
"countable_type t ⟹ stock_measure t = count_space (type_universe t)"
proof (subst space_stock_measure[symmetric], induction t)
case (PRODUCT t1 t2)
hence countable: "countable_type t1" "countable_type t2" by simp_all
note A = PRODUCT.IH(1)[OF countable(1)] and B = PRODUCT.IH(2)[OF countable(2)]
show "stock_measure (PRODUCT t1 t2) = count_space (space (stock_measure (PRODUCT t1 t2)))"
apply (subst (1 2) stock_measure.simps)
apply (subst (1 2) A, subst (1 2) B)
apply (subst (1 2) pair_measure_countable)
apply (auto intro: countable_type_countable simp: countable simp del: space_stock_measure) [2]
apply (subst (1 2) embed_measure_count_space, force intro: injI)
apply simp
done
qed (simp_all add: stock_measure.simps)
lemma return_val_countable:
assumes "countable_type (val_type v)"
shows "return_val v = density (stock_measure (val_type v)) (indicator {v})" (is "?M1 = ?M2")
proof (rule measure_eqI)
let ?M3 = "count_space (type_universe (val_type v))"
fix X assume asm: "X ∈ ?M1"
with assms have "emeasure ?M2 X = ∫⇧+ x. indicator {v} x * indicator X x
∂count_space (type_universe (val_type v))"
by (simp add: return_val_def emeasure_density countable_type_imp_count_space)
also have "(λx. indicator {v} x * indicator X x :: ennreal) = (λx. indicator (X ∩ {v}) x)"
by (rule ext, subst Int_commute) (simp split: split_indicator)
also have "nn_integral ?M3 ... = emeasure ?M3 (X ∩ {v})"
by (subst nn_integral_indicator[symmetric]) auto
also from asm have "... = emeasure ?M1 X" by (auto simp: return_val_def split: split_indicator)
finally show "emeasure ?M1 X = emeasure ?M2 X" ..
qed (simp add: return_val_def)
subsection ‹Semantics›
definition bool_to_int :: "bool ⇒ int" where
"bool_to_int b = (if b then 1 else 0)"
lemma measurable_bool_to_int[measurable]:
"bool_to_int ∈ measurable (count_space UNIV) (count_space UNIV)"
by (rule measurable_count_space)
definition bool_to_real :: "bool ⇒ real" where
"bool_to_real b = (if b then 1 else 0)"
lemma measurable_bool_to_real[measurable]:
"bool_to_real ∈ borel_measurable (count_space UNIV)"
by (rule borel_measurable_count_space)
definition safe_ln :: "real ⇒ real" where
"safe_ln x = (if x > 0 then ln x else 0)"
lemma safe_ln_gt_0[simp]: "x > 0 ⟹ safe_ln x = ln x"
by (simp add: safe_ln_def)
lemma borel_measurable_safe_ln[measurable]: "safe_ln ∈ borel_measurable borel"
unfolding safe_ln_def[abs_def] by simp
definition safe_sqrt :: "real ⇒ real" where
"safe_sqrt x = (if x ≥ 0 then sqrt x else 0)"
lemma safe_sqrt_ge_0[simp]: "x ≥ 0 ⟹ safe_sqrt x = sqrt x"
by (simp add: safe_sqrt_def)
lemma borel_measurable_safe_sqrt[measurable]: "safe_sqrt ∈ borel_measurable borel"
unfolding safe_sqrt_def[abs_def] by simp
fun op_sem :: "pdf_operator ⇒ val ⇒ val" where
"op_sem Add = lift_RealIntVal2 (+) (+)"
| "op_sem Mult = lift_RealIntVal2 (*) (*)"
| "op_sem Minus = lift_RealIntVal uminus uminus"
| "op_sem Equals = (λ <|v1, v2|> ⇒ BoolVal (v1 = v2))"
| "op_sem Less = lift_Comp (<) (<)"
| "op_sem Or = (λ <|BoolVal a, BoolVal b|> ⇒ BoolVal (a ∨ b))"
| "op_sem And = (λ <|BoolVal a, BoolVal b|> ⇒ BoolVal (a ∧ b))"
| "op_sem Not = (λ BoolVal a ⇒ BoolVal (¬a))"
| "op_sem (Cast t) = (case t of
INTEG ⇒ (λ BoolVal b ⇒ IntVal (bool_to_int b)
| RealVal r ⇒ IntVal (floor r))
| REAL ⇒ (λ BoolVal b ⇒ RealVal (bool_to_real b)
| IntVal i ⇒ RealVal (real_of_int i)))"
| "op_sem Inverse = lift_RealVal inverse"
| "op_sem Fact = lift_IntVal (λi::int. fact (nat i))"
| "op_sem Sqrt = lift_RealVal safe_sqrt"
| "op_sem Exp = lift_RealVal exp"
| "op_sem Ln = lift_RealVal safe_ln"
| "op_sem Pi = (λ_. RealVal pi)"
| "op_sem Pow = (λ <|RealVal x, IntVal n|> ⇒ if n < 0 then RealVal 0 else RealVal (x ^ nat n)
| <|IntVal x, IntVal n|> ⇒ if n < 0 then IntVal 0 else IntVal (x ^ nat n))"
| "op_sem Fst = fst ∘ extract_pair"
| "op_sem Snd = snd ∘ extract_pair"
text ‹The semantics of expressions. Assumes that the expression given is well-typed.›
primrec expr_sem :: "state ⇒ expr ⇒ val measure" where
"expr_sem σ (Var x) = return_val (σ x)"
| "expr_sem σ (Val v) = return_val v"
| "expr_sem σ (LET e1 IN e2) =
do {
v ← expr_sem σ e1;
expr_sem (v ⋅ σ) e2
}"
| "expr_sem σ (oper $$ e) =
do {
x ← expr_sem σ e;
return_val (op_sem oper x)
}"
| "expr_sem σ <v, w> =
do {
x ← expr_sem σ v;
y ← expr_sem σ w;
return_val <|x, y|>
}"
| "expr_sem σ (IF b THEN e1 ELSE e2) =
do {
b' ← expr_sem σ b;
if b' = TRUE then expr_sem σ e1 else expr_sem σ e2
}"
| "expr_sem σ (Random dst e) =
do {
x ← expr_sem σ e;
dist_measure dst x
}"
| "expr_sem σ (Fail t) = null_measure (stock_measure t)"
lemma expr_sem_pair_vars: "expr_sem σ <Var x, Var y> = return_val <|σ x, σ y|>"
by (simp add: return_val_def bind_return[where N="PRODUCT (val_type (σ x)) (val_type (σ y))"]
cong: bind_cong_simp)
text ‹
Well-typed expressions produce a result in the measure space that corresponds to their type
›
lemma op_sem_val_type:
"op_type oper (val_type v) = Some t' ⟹ val_type (op_sem oper v) = t'"
by (cases oper) (auto split: val.split if_split_asm pdf_type.split_asm
simp: lift_RealIntVal_def lift_Comp_def
lift_IntVal_def lift_RealVal_def lift_RealIntVal2_def
elim!: PROD_E INTEG_E REAL_E)
lemma sets_expr_sem:
"Γ ⊢ w : t ⟹ (∀x ∈ free_vars w. val_type (σ x) = Γ x) ⟹
sets (expr_sem σ w) = sets (stock_measure t)"
proof (induction arbitrary: σ rule: expr_typing.induct)
case (et_var Γ x σ)
thus ?case by (simp add: return_val_def)
next
case (et_val Γ v σ)
thus ?case by (simp add: return_val_def)
next
case (et_let Γ e1 t1 e2 t2 σ)
hence "sets (expr_sem σ e1) = sets (stock_measure t1)" by simp
from sets_eq_imp_space_eq[OF this]
have A: "space (expr_sem σ e1) = type_universe t1" by (simp add:)
hence B: "(SOME x. x ∈ space (expr_sem σ e1)) ∈ space (expr_sem σ e1)" (is "?v ∈ _")
unfolding some_in_eq by simp
with A et_let have "sets (expr_sem (case_nat ?v σ) e2) = sets (stock_measure t2)"
by (intro et_let.IH(2)) (auto split: nat.split)
with B show "sets (expr_sem σ (LetVar e1 e2)) = sets (stock_measure t2)"
by (subst expr_sem.simps, subst bind_nonempty) auto
next
case (et_op Γ e t oper t' σ)
from et_op.IH[of σ] and et_op.prems
have [simp]: "sets (expr_sem σ e) = sets (stock_measure t)" by simp
from sets_eq_imp_space_eq[OF this]
have [simp]: "space (expr_sem σ e) = type_universe t" by (simp add:)
have "(SOME x. x ∈ space (expr_sem σ e)) ∈ space (expr_sem σ e)"
unfolding some_in_eq by simp
with et_op show ?case by (simp add: bind_nonempty return_val_def op_sem_val_type)
next
case (et_pair Γ e1 t1 e2 t2 σ)
hence [simp]: "space (expr_sem σ e1) = type_universe t1"
"space (expr_sem σ e2) = type_universe t2"
by (simp_all add: sets_eq_imp_space_eq)
have "(SOME x. x ∈ space (expr_sem σ e1)) ∈ space (expr_sem σ e1)"
"(SOME x. x ∈ space (expr_sem σ e2)) ∈ space (expr_sem σ e2)"
unfolding some_in_eq by simp_all
with et_pair.hyps show ?case by (simp add: bind_nonempty return_val_def)
next
case (et_rand Γ e dst σ)
from et_rand.IH[of σ] et_rand.prems
have "sets (expr_sem σ e) = sets (stock_measure (dist_param_type dst))" by simp
from this sets_eq_imp_space_eq[OF this]
show ?case
apply simp_all
apply (subst sets_bind)
apply auto
done
next
case (et_if Γ b e1 t e2 σ)
have "sets (expr_sem σ b) = sets (stock_measure BOOL)"
using et_if.prems by (intro et_if.IH) simp
from sets_eq_imp_space_eq[OF this]
have "space (expr_sem σ b) ≠ {}" by simp
moreover have "sets (expr_sem σ e1) = sets (stock_measure t)"
"sets (expr_sem σ e2) = sets (stock_measure t)"
using et_if.prems by (intro et_if.IH, simp)+
ultimately show ?case by (simp add: bind_nonempty)
qed simp_all
lemma space_expr_sem:
"Γ ⊢ w : t ⟹ (∀x ∈ free_vars w. val_type (σ x) = Γ x)
⟹ space (expr_sem σ w) = type_universe t"
by (subst space_stock_measure[symmetric]) (intro sets_expr_sem sets_eq_imp_space_eq)
lemma measurable_expr_sem_eq:
"Γ ⊢ e : t ⟹ σ ∈ space (state_measure V Γ) ⟹ free_vars e ⊆ V ⟹
measurable (expr_sem σ e) = measurable (stock_measure t)"
by (intro ext measurable_cong_sets sets_expr_sem)
(auto simp: state_measure_def space_PiM dest: PiE_mem)
lemma measurable_expr_semI:
"Γ ⊢ e : t ⟹ σ ∈ space (state_measure V Γ) ⟹ free_vars e ⊆ V ⟹
f ∈ measurable (stock_measure t) M ⟹ f ∈ measurable (expr_sem σ e) M"
by (subst measurable_expr_sem_eq)
lemma expr_sem_eq_on_vars:
"(⋀x. x∈free_vars e ⟹ σ⇩1 x = σ⇩2 x) ⟹ expr_sem σ⇩1 e = expr_sem σ⇩2 e"
proof (induction e arbitrary: σ⇩1 σ⇩2)
case (LetVar e1 e2 σ1 σ2)
from LetVar.prems have A: "expr_sem σ1 e1 = expr_sem σ2 e1" by (rule LetVar.IH(1)) simp_all
from LetVar.prems show ?case
by (subst (1 2) expr_sem.simps, subst A)
(auto intro!: bind_cong LetVar.IH(2) split: nat.split)
next
case (Operator oper e σ1 σ2)
from Operator.IH[OF Operator.prems] show ?case by simp
next
case (Pair e1 e2 σ1 σ2)
from Pair.prems have "expr_sem σ1 e1 = expr_sem σ2 e1" by (intro Pair.IH) auto
moreover from Pair.prems have "expr_sem σ1 e2 = expr_sem σ2 e2" by (intro Pair.IH) auto
ultimately show ?case by simp
next
case (Random dst e σ1 σ2)
from Random.prems have A: "expr_sem σ1 e = expr_sem σ2 e" by (rule Random.IH) simp_all
show ?case
by (subst (1 2) expr_sem.simps, subst A) (auto intro!: bind_cong)
next
case (IfThenElse b e1 e2 σ1 σ2)
have A: "expr_sem σ1 b = expr_sem σ2 b"
"expr_sem σ1 e1 = expr_sem σ2 e1"
"expr_sem σ1 e2 = expr_sem σ2 e2"
using IfThenElse.prems by (intro IfThenElse.IH, simp)+
thus ?case by (simp only: expr_sem.simps A)
qed simp_all
subsection ‹Measurability›
lemma borel_measurable_eq[measurable (raw)]:
assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
shows "Measurable.pred M (λx. f x = (g x::real))"
proof -
have *: "(λx. f x = g x) = (λx. f x - g x = 0)"
by simp
show ?thesis
unfolding * by measurable
qed
lemma measurable_equals:
"(λ(x,y). x = y) ∈ measurable (stock_measure t ⨂⇩M stock_measure t) (count_space UNIV)"
proof (induction t)
case REAL
let ?f = "λx. extract_real (fst x) = extract_real (snd x)"
show ?case
proof (subst measurable_cong)
fix x assume "x ∈ space (stock_measure REAL ⨂⇩M stock_measure REAL)"
thus "(λ(x,y). x = y) x = ?f x"
by (auto simp: space_pair_measure elim!: REAL_E)
next
show "?f ∈ measurable (stock_measure REAL ⨂⇩M stock_measure REAL) (count_space UNIV)"
by measurable
qed
next
case (PRODUCT t1 t2)
let ?g = "λ(x,y). x = y"
let ?f = "λx. ?g (fst (extract_pair (fst x)), fst (extract_pair (snd x))) ∧
?g (snd (extract_pair (fst x)), snd (extract_pair (snd x)))"
show ?case
proof (subst measurable_cong)
fix x assume "x ∈ space (stock_measure (PRODUCT t1 t2) ⨂⇩M stock_measure (PRODUCT t1 t2))"
thus "(λ(x,y). x = y) x = ?f x"
apply (auto simp: space_pair_measure)
apply (elim PROD_E)
apply simp
done
next
note PRODUCT[measurable]
show "Measurable.pred (stock_measure (PRODUCT t1 t2) ⨂⇩M stock_measure (PRODUCT t1 t2)) ?f"
by measurable
qed
qed (simp_all add: pair_measure_countable stock_measure.simps)
lemma measurable_equals_stock_measure[measurable (raw)]:
assumes "f ∈ measurable M (stock_measure t)" "g ∈ measurable M (stock_measure t)"
shows "Measurable.pred M (λx. f x = g x)"
using measurable_compose[OF measurable_Pair[OF assms] measurable_equals] by simp
lemma measurable_op_sem:
assumes "op_type oper t = Some t'"
shows "op_sem oper ∈ measurable (stock_measure t) (stock_measure t')"
proof (cases oper)
case Fst with assms show ?thesis by (simp split: pdf_type.split_asm)
next
case Snd with assms show ?thesis by (simp split: pdf_type.split_asm)
next
case Equals with assms show ?thesis
by (auto intro!: val_case_stock_measurable split: if_split_asm)
next
case Pow with assms show ?thesis
apply (auto intro!: val_case_stock_measurable split: pdf_type.splits)
apply (subst measurable_cong[where
g="λ(x, n). if extract_int n < 0 then RealVal 0 else RealVal (extract_real x ^ nat (extract_int n))"])
apply (auto simp: space_pair_measure elim!: REAL_E INTEG_E)
done
next
case Less with assms show ?thesis
by (auto split: pdf_type.splits)
qed (insert assms, auto split: pdf_type.split_asm intro!: val_case_stock_measurable)
definition shift_var_set :: "vname set ⇒ vname set" where
"shift_var_set V = insert 0 (Suc ` V)"
lemma shift_var_set_0[simp]: "0 ∈ shift_var_set V"
by (simp add: shift_var_set_def)
lemma shift_var_set_Suc[simp]: "Suc x ∈ shift_var_set V ⟷ x ∈ V"
by (auto simp add: shift_var_set_def)
lemma case_nat_update_0[simp]: "(case_nat x σ)(0 := y) = case_nat y σ"
by (intro ext) (simp split: nat.split)
lemma case_nat_delete_var_1[simp]:
"case_nat x (case_nat y σ) ∘ case_nat 0 (λx. Suc (Suc x)) = case_nat x σ"
by (intro ext) (simp split: nat.split)
lemma delete_var_1_vimage[simp]:
"case_nat 0 (λx. Suc (Suc x)) -` (shift_var_set (shift_var_set V)) = shift_var_set V"
by (auto simp: shift_var_set_def split: nat.split_asm)
lemma measurable_case_nat[measurable]:
assumes "g ∈ measurable R N" "h ∈ measurable R (Pi⇩M V M)"
shows "(λx. case_nat (g x) (h x)) ∈ measurable R (Pi⇩M (shift_var_set V) (case_nat N M))"
proof (rule measurable_Pair_compose_split[OF _ assms])
have "(λ(t,f). λx∈shift_var_set V. case_nat t f x)
∈ measurable (N ⨂⇩M PiM V M) (PiM (shift_var_set V) (case_nat N M))" (is ?P)
unfolding shift_var_set_def
by (subst measurable_split_conv, rule measurable_restrict) (auto split: nat.split_asm)
also have "⋀x f. f ∈ space (PiM V M) ⟹ x ∉ V ⟹ undefined = f x"
by (rule sym, subst (asm) space_PiM, erule PiE_arb)
hence "?P ⟷ (λ(t,f). case_nat t f)
∈ measurable (N ⨂⇩M PiM V M) (PiM (shift_var_set V) (case_nat N M))" (is "_ = ?P")
by (intro measurable_cong ext)
(auto split: nat.split simp: inj_image_mem_iff space_pair_measure shift_var_set_def)
finally show ?P .
qed
lemma measurable_case_nat'[measurable]:
assumes "g ∈ measurable R (stock_measure t)" "h ∈ measurable R (state_measure V Γ)"
shows "(λx. case_nat (g x) (h x)) ∈
measurable R (state_measure (shift_var_set V) (case_nat t Γ))"
proof-
have A: "(λx. stock_measure (case_nat t Γ x)) =
case_nat (stock_measure t) (λx. stock_measure (Γ x))"
by (intro ext) (simp split: nat.split)
show ?thesis using assms unfolding state_measure_def by (simp add: A)
qed
lemma case_nat_in_state_measure[intro]:
assumes "x ∈ type_universe t1" "σ ∈ space (state_measure V Γ)"
shows "case_nat x σ ∈ space (state_measure (shift_var_set V) (case_nat t1 Γ))"
apply (rule measurable_space[OF measurable_case_nat'])
apply (rule measurable_ident_sets[OF refl], rule measurable_const[OF assms(2)])
using assms
apply simp
done
lemma subset_shift_var_set:
"Suc -` A ⊆ V ⟹ A ⊆ shift_var_set V"
by (rule subsetI, rename_tac x, case_tac x) (auto simp: shift_var_set_def)
lemma measurable_expr_sem[measurable]:
assumes "Γ ⊢ e : t" and "free_vars e ⊆ V"
shows "(λσ. expr_sem σ e) ∈ measurable (state_measure V Γ)
(subprob_algebra (stock_measure t))"
using assms
proof (induction arbitrary: V rule: expr_typing.induct)
case (et_var Γ x)
have A: "(λσ. expr_sem σ (Var x)) = return_val ∘ (λσ. σ x)" by (simp add: o_def)
with et_var show ?case unfolding state_measure_def
by (subst A) (rule measurable_comp[OF measurable_component_singleton], simp_all)
next
case (et_val Γ v)
thus ?case by (auto intro!: measurable_const subprob_space_return
simp: space_subprob_algebra return_val_def)
next
case (et_let Γ e1 t1 e2 t2 V)
have A: "(λv. stock_measure (case_nat t1 Γ v)) =
case_nat (stock_measure t1) (λv. stock_measure (Γ v))"
by (rule ext) (simp split: nat.split)
from et_let.prems and et_let.hyps show ?case
apply (subst expr_sem.simps, intro measurable_bind)
apply (rule et_let.IH(1), simp)
apply (rule measurable_compose[OF _ et_let.IH(2)[of "shift_var_set V"]])
apply (simp_all add: subset_shift_var_set)
done
next
case (et_op Γ e t oper t')
thus ?case by (auto intro!: measurable_bind2 measurable_compose[OF _ measurable_return_val]
measurable_op_sem cong: measurable_cong)
next
case (et_pair t t1 t2 Γ e1 e2)
have "inj (λ(a,b). <|a, b|>)" by (auto intro: injI)
with et_pair show ?case
apply (subst expr_sem.simps)
apply (rule measurable_bind, (auto) [])
apply (rule measurable_bind[OF measurable_compose[OF measurable_fst]], (auto) [])
apply (rule measurable_compose[OF _ measurable_return_val], simp)
done
next
case (et_rand Γ e dst V)
from et_rand.prems and et_rand.hyps show ?case
by (auto intro!: et_rand.IH measurable_compose[OF measurable_snd]
measurable_bind measurable_dist_measure)
next
case (et_if Γ b e1 t e2 V)
let ?M = "λe t. (λσ. expr_sem σ e) ∈
measurable (state_measure V Γ) (subprob_algebra (stock_measure t))"
from et_if.prems have A[measurable]: "?M b BOOL" "?M e1 t" "?M e2 t" by (intro et_if.IH, simp)+
show ?case by (subst expr_sem.simps, rule measurable_bind[OF A(1)]) simp_all
next
case (et_fail Γ t V)
show ?case
by (auto intro!: measurable_subprob_algebra subprob_spaceI simp:)
qed
subsection ‹Randomfree expressions›
fun randomfree :: "expr ⇒ bool" where
"randomfree (Val _) = True"
| "randomfree (Var _) = True"
| "randomfree (Pair e1 e2) = (randomfree e1 ∧ randomfree e2)"
| "randomfree (Operator _ e) = randomfree e"
| "randomfree (LetVar e1 e2) = (randomfree e1 ∧ randomfree e2)"
| "randomfree (IfThenElse b e1 e2) = (randomfree b ∧ randomfree e1 ∧ randomfree e2)"
| "randomfree (Random _ _) = False"
| "randomfree (Fail _) = False"
primrec expr_sem_rf :: "state ⇒ expr ⇒ val" where
"expr_sem_rf _ (Val v) = v"
| "expr_sem_rf σ (Var x) = σ x"
| "expr_sem_rf σ (<e1, e2>) = <|expr_sem_rf σ e1, expr_sem_rf σ e2|>"
| "expr_sem_rf σ (Operator oper e) = op_sem oper (expr_sem_rf σ e)"
| "expr_sem_rf σ (LetVar e1 e2) = expr_sem_rf (expr_sem_rf σ e1 ⋅ σ) e2"
| "expr_sem_rf σ (IfThenElse b e1 e2) =
(if expr_sem_rf σ b = BoolVal True then expr_sem_rf σ e1 else expr_sem_rf σ e2)"
| "expr_sem_rf _ (Random _ _) = undefined"
| "expr_sem_rf _ (Fail _) = undefined"
lemma measurable_expr_sem_rf[measurable]:
"Γ ⊢ e : t ⟹ randomfree e ⟹ free_vars e ⊆ V ⟹
(λσ. expr_sem_rf σ e) ∈ measurable (state_measure V Γ) (stock_measure t)"
proof (induction arbitrary: V rule: expr_typing.induct)
case (et_val Γ v V)
thus ?case by (auto intro!: measurable_const simp:)
next
case (et_var Γ x V)
thus ?case by (auto simp: state_measure_def intro!: measurable_component_singleton)
next
case (et_pair Γ e1 t1 e2 t2 V)
have "inj (λ(x,y). <|x, y|>)" by (auto intro: injI)
with et_pair show ?case by simp
next
case (et_op Γ e t oper t' V)
thus ?case by (auto intro!: measurable_compose[OF _ measurable_op_sem])
next
case (et_let Γ e1 t1 e2 t2 V)
hence M1: "(λσ. expr_sem_rf σ e1) ∈ measurable (state_measure V Γ) (stock_measure t1)"
and M2: "(λσ. expr_sem_rf σ e2) ∈ measurable (state_measure (shift_var_set V) (case_nat t1 Γ))
(stock_measure t2)"
using subset_shift_var_set
by (auto intro!: et_let.IH(1)[of V] et_let.IH(2)[of "shift_var_set V"])
have "(λσ. expr_sem_rf σ (LetVar e1 e2)) =
(λσ. expr_sem_rf σ e2) ∘ (λ(σ,y). case_nat y σ) ∘ (λσ. (σ, expr_sem_rf σ e1))" (is "_ = ?f")
by (intro ext) simp
also have "?f ∈ measurable (state_measure V Γ) (stock_measure t2)"
apply (intro measurable_comp, rule measurable_Pair, rule measurable_ident_sets[OF refl])
apply (rule M1, subst measurable_split_conv, rule measurable_case_nat')
apply (rule measurable_snd, rule measurable_fst, rule M2)
done
finally show ?case .
qed (simp_all add: expr_sem_rf_def)
lemma expr_sem_rf_sound:
"Γ ⊢ e : t ⟹ randomfree e ⟹ free_vars e ⊆ V ⟹ σ ∈ space (state_measure V Γ) ⟹
return_val (expr_sem_rf σ e) = expr_sem σ e"
proof (induction arbitrary: V σ rule: expr_typing.induct)
case (et_val Γ v)
thus ?case by simp
next
case (et_var Γ x)
thus ?case by simp
next
case (et_pair Γ e1 t1 e2 t2 V σ)
let ?M = "state_measure V Γ"
from et_pair.hyps and et_pair.prems
have e1: "return_val (expr_sem_rf σ e1) = expr_sem σ e1" and
e2: "return_val (expr_sem_rf σ e2) = expr_sem σ e2"
by (auto intro!: et_pair.IH[of V])
from e1 and et_pair.prems have "space (return_val (expr_sem_rf σ e1)) = type_universe t1"
by (subst e1, subst space_expr_sem[OF et_pair.hyps(1)])
(auto dest: state_measure_var_type)
hence A: "val_type (expr_sem_rf σ e1) = t1" "expr_sem_rf σ e1 ∈ type_universe t1"
by (auto simp add: return_val_def)
from e2 and et_pair.prems have "space (return_val (expr_sem_rf σ e2)) = type_universe t2"
by (subst e2, subst space_expr_sem[OF et_pair.hyps(2)])
(auto dest: state_measure_var_type)
hence B: "val_type (expr_sem_rf σ e2) = t2" "expr_sem_rf σ e2 ∈ type_universe t2"
by (auto simp add: return_val_def)
have "expr_sem σ (<e1, e2>) = expr_sem σ e1 ⤜
(λv. expr_sem σ e2 ⤜ (λw. return_val (<|v,w|>)))" by simp
also have "expr_sem σ e1 = return (stock_measure t1) (expr_sem_rf σ e1)"
using e1 by (simp add: et_pair.prems return_val_def A)
also have "... ⤜ (λv. expr_sem σ e2 ⤜ (λw. return_val (<|v,w|>))) =
... ⤜ (λv. return_val (<|v, expr_sem_rf σ e2|>))"
proof (intro bind_cong refl)
fix v assume "v ∈ space (return (stock_measure t1) (expr_sem_rf σ e1))"
hence v: "val_type v = t1" "v ∈ type_universe t1" by (simp_all add:)
have "expr_sem σ e2 ⤜ (λw. return_val (<|v,w|>)) =
return (stock_measure t2) (expr_sem_rf σ e2) ⤜ (λw. return_val (<|v,w|>))"
using e2 by (simp add: et_pair.prems return_val_def B)
also have "... = return (stock_measure t2) (expr_sem_rf σ e2) ⤜
(λw. return (stock_measure (PRODUCT t1 t2)) (<|v,w|>))"
proof (intro bind_cong refl)
fix w assume "w ∈ space (return (stock_measure t2) (expr_sem_rf σ e2))"
hence w: "val_type w = t2" by (simp add:)
thus "return_val (<|v,w|>) = return (stock_measure (PRODUCT t1 t2)) (<|v,w|>)"
by (auto simp: return_val_def v w)
qed
also have "... = return_val (<|v, expr_sem_rf σ e2|>)"
using v B
by (subst bind_return[where N="PRODUCT t1 t2"]) (auto simp: return_val_def)
finally show "expr_sem σ e2 ⤜ (λw. return_val (<|v,w|>)) = return_val (<|v, expr_sem_rf σ e2|>)" .
qed
also have "(λv. <|v, expr_sem_rf σ e2|>) ∈ measurable (stock_measure t1) (stock_measure (PRODUCT t1 t2))"
using B by (auto intro!: injI)
hence "return (stock_measure t1) (expr_sem_rf σ e1) ⤜ (λv. return_val (<|v, expr_sem_rf σ e2|>)) =
return_val (<|expr_sem_rf σ e1, expr_sem_rf σ e2|>)"
by (subst bind_return, rule measurable_compose[OF _ measurable_return_val])
(auto simp: A)
finally show "return_val (expr_sem_rf σ (<e1,e2>)) = expr_sem σ (<e1, e2>)" by simp
next
case (et_if Γ b e1 t e2 V σ)
let ?P = "λe. expr_sem σ e = return_val (expr_sem_rf σ e)"
from et_if.prems have A: "?P b" "?P e1" "?P e2" by ((intro et_if.IH[symmetric], simp_all) [])+
from et_if.prems and et_if.hyps have "space (expr_sem σ b) = type_universe BOOL"
by (intro space_expr_sem) (auto simp: state_measure_var_type)
hence [simp]: "val_type (expr_sem_rf σ b) = BOOL" by (simp add: A return_val_def)
have B: "return_val (expr_sem_rf σ e1) ∈ space (subprob_algebra (stock_measure t))"
"return_val (expr_sem_rf σ e2) ∈ space (subprob_algebra (stock_measure t))"
using et_if.hyps and et_if.prems
by ((subst A[symmetric], intro measurable_space[OF measurable_expr_sem], auto) [])+
thus ?case
by (auto simp: A bind_return_val''[where M=t])
next
case (et_op Γ e t oper t' V)
let ?M = "PiM V (λx. stock_measure (Γ x))"
from et_op.prems have e: "return_val (expr_sem_rf σ e) = expr_sem σ e"
by (intro et_op.IH[of V]) auto
with et_op.prems have "space (return_val (expr_sem_rf σ e)) = type_universe t"
by (subst e, subst space_expr_sem[OF et_op.hyps(1)])
(auto dest: state_measure_var_type)
hence A: "val_type (expr_sem_rf σ e) = t" "expr_sem_rf σ e ∈ type_universe t"
by (auto simp add: return_val_def)
from et_op.prems e
have "expr_sem σ (Operator oper e) =
return_val (expr_sem_rf σ e) ⤜ (λv. return_val (op_sem oper v))" by simp
also have "... = return_val (op_sem oper (expr_sem_rf σ e))"
by (subst return_val_def, rule bind_return,
rule measurable_compose[OF measurable_op_sem measurable_return_val])
(auto simp: A et_op.hyps)
finally show "return_val (expr_sem_rf σ (Operator oper e)) = expr_sem σ (Operator oper e)" by simp
next
case (et_let Γ e1 t1 e2 t2 V)
let ?M = "state_measure V Γ" and ?N = "state_measure (shift_var_set V) (case_nat t1 Γ)"
let ?σ' = "case_nat (expr_sem_rf σ e1) σ"
from et_let.prems have e1: "return_val (expr_sem_rf σ e1) = expr_sem σ e1"
by (auto intro!: et_let.IH(1)[of V])
from et_let.prems have S: "space (return_val (expr_sem_rf σ e1)) = type_universe t1"
by (subst e1, subst space_expr_sem[OF et_let.hyps(1)])
(auto dest: state_measure_var_type)
hence A: "val_type (expr_sem_rf σ e1) = t1" "expr_sem_rf σ e1 ∈ type_universe t1"
by (auto simp add: return_val_def)
with et_let.prems have e2: "⋀σ. σ ∈ space ?N ⟹ return_val (expr_sem_rf σ e2) = expr_sem σ e2"
using subset_shift_var_set
by (intro et_let.IH(2)[of "shift_var_set V"]) (auto simp del: fun_upd_apply)
from et_let.prems have "expr_sem σ (LetVar e1 e2) =
return_val (expr_sem_rf σ e1) ⤜ (λv. expr_sem (case_nat v σ) e2)"
by (simp add: e1)
also from et_let.prems
have "... = return_val (expr_sem_rf σ e1) ⤜ (λv. return_val (expr_sem_rf (case_nat v σ) e2))"
by (intro bind_cong refl, subst e2) (auto simp: S)
also from et_let have Me2[measurable]: "(λσ. expr_sem_rf σ e2) ∈ measurable ?N (stock_measure t2)"
using subset_shift_var_set by (intro measurable_expr_sem_rf) auto
have "(λ(σ,y). case_nat y σ) ∘ (λy. (σ, y)) ∈ measurable (stock_measure t1) ?N"
using ‹σ ∈ space ?M› by simp
have "return_val (expr_sem_rf σ e1) ⤜ (λv. return_val (expr_sem_rf (case_nat v σ) e2)) =
return_val (expr_sem_rf ?σ' e2)" using ‹σ ∈ space ?M›
by (subst return_val_def, intro bind_return, subst A)
(rule measurable_compose[OF _ measurable_return_val[of t2]], simp_all)
finally show ?case by simp
qed simp_all
lemma val_type_expr_sem_rf:
assumes "Γ ⊢ e : t" "randomfree e" "free_vars e ⊆ V" "σ ∈ space (state_measure V Γ)"
shows "val_type (expr_sem_rf σ e) = t"
proof-
have "type_universe (val_type (expr_sem_rf σ e)) = space (return_val (expr_sem_rf σ e))"
by (simp add: return_val_def)
also from assms have "return_val (expr_sem_rf σ e) = expr_sem σ e"
by (intro expr_sem_rf_sound) auto
also from assms have "space ... = type_universe t"
by (intro space_expr_sem[of Γ])
(auto simp: state_measure_def space_PiM dest: PiE_mem)
finally show ?thesis by simp
qed
lemma expr_sem_rf_eq_on_vars:
"(⋀x. x∈free_vars e ⟹ σ1 x = σ2 x) ⟹ expr_sem_rf σ1 e = expr_sem_rf σ2 e"
proof (induction e arbitrary: σ1 σ2)
case (Operator oper e σ1 σ2)
hence "expr_sem_rf σ1 e = expr_sem_rf σ2 e" by (intro Operator.IH) auto
thus ?case by simp
next
case (LetVar e1 e2 σ1 σ2)
hence A: "expr_sem_rf σ1 e1 = expr_sem_rf σ2 e1" by (intro LetVar.IH) auto
{
fix y assume "y ∈ free_vars e2"
hence "case_nat (expr_sem_rf σ1 e1) σ1 y = case_nat (expr_sem_rf σ2 e1) σ2 y"
using LetVar(3) by (auto simp add: A split: nat.split)
}
hence "expr_sem_rf (case_nat (expr_sem_rf σ1 e1) σ1) e2 =
expr_sem_rf (case_nat (expr_sem_rf σ2 e1) σ2) e2" by (intro LetVar.IH) simp
thus ?case by simp
next
case (Pair e1 e2 σ1 σ2)
have "expr_sem_rf σ1 e1 = expr_sem_rf σ2 e1" "expr_sem_rf σ1 e2 = expr_sem_rf σ2 e2"
by (intro Pair.IH, simp add: Pair)+
thus ?case by simp
next
case (IfThenElse b e1 e2 σ1 σ2)
have "expr_sem_rf σ1 b = expr_sem_rf σ2 b" "expr_sem_rf σ1 e1 = expr_sem_rf σ2 e1"
"expr_sem_rf σ1 e2 = expr_sem_rf σ2 e2" by (intro IfThenElse.IH, simp add: IfThenElse)+
thus ?case by simp
next
case (Random dst e σ1 σ2)
have "expr_sem_rf σ1 e = expr_sem_rf σ2 e" by (intro Random.IH) (simp add: Random)
thus ?case by simp
qed auto
end
Theory PDF_Density_Contexts
section ‹Density Contexts›
theory PDF_Density_Contexts
imports PDF_Semantics
begin
lemma measurable_proj_state_measure[measurable (raw)]:
"i ∈ V ⟹ (λx. x i) ∈ measurable (state_measure V Γ) (Γ i)"
unfolding state_measure_def by measurable
lemma measurable_dens_ctxt_fun_upd[measurable (raw)]:
"f ∈ N →⇩M state_measure V' Γ ⟹ V = V' ∪ {x} ⟹
g ∈ N →⇩M stock_measure (Γ x) ⟹
(λω. (f ω)(x := g ω)) ∈ N →⇩M state_measure V Γ"
unfolding state_measure_def
by (rule measurable_fun_upd[where J=V']) auto
lemma measurable_case_nat_Suc_PiM:
"(λσ. σ ∘ Suc) ∈ measurable (PiM (Suc ` A) (case_nat M N)) (PiM A N)"
proof-
have "(λσ. λx∈A. σ (Suc x)) ∈ measurable
(PiM (Suc ` A) (case_nat M N)) (PiM A (λx. case_nat M N (Suc x)))" (is "?A")
by measurable
also have "?A ⟷ ?thesis"
by (force intro!: measurable_cong ext simp: state_measure_def space_PiM dest: PiE_mem)
finally show ?thesis .
qed
lemma measurable_case_nat_Suc:
"(λσ. σ ∘ Suc) ∈ measurable (state_measure (Suc ` A) (case_nat t Γ)) (state_measure A Γ)"
proof-
have "(λσ. λx∈A. σ (Suc x)) ∈ measurable
(state_measure (Suc ` A) (case_nat t Γ)) (state_measure A (λi. case_nat t Γ (Suc i)))" (is "?A")
unfolding state_measure_def by measurable
also have "?A ⟷ ?thesis"
by (force intro!: measurable_cong ext simp: state_measure_def space_PiM dest: PiE_mem)
finally show ?thesis .
qed
text ‹A density context holds a set of variables @{term V}, their types (using @{term Γ}), and a
common density function @{term δ} of the finite product space of all the variables in @{term V}.
@{term δ} takes a state @{term "σ ∈ (Π⇩E x∈V. type_universe (Γ x))"} and returns the common density
of these variables.›
type_synonym dens_ctxt = "vname set × vname set × (vname ⇒ pdf_type) × (state ⇒ ennreal)"
type_synonym expr_density = "state ⇒ val ⇒ ennreal"
definition empty_dens_ctxt :: dens_ctxt where
"empty_dens_ctxt = ({}, {}, λ_. undefined, λ_. 1)"
definition state_measure'
:: "vname set ⇒ vname set ⇒ (vname ⇒ pdf_type) ⇒ state ⇒ state measure" where
"state_measure' V V' Γ ρ =
distr (state_measure V Γ) (state_measure (V∪V') Γ) (λσ. merge V V' (σ, ρ))"
text ‹The marginal density of a variable @{term x} is obtained by integrating the common density
@{term δ} over all the remaining variables.›
definition marg_dens :: "dens_ctxt ⇒ vname ⇒ expr_density" where
"marg_dens = (λ(V,V',Γ,δ) x ρ v. ∫⇧+σ. δ (merge V V' (σ(x := v), ρ)) ∂state_measure (V-{x}) Γ)"
definition marg_dens2 :: "dens_ctxt ⇒ vname ⇒ vname ⇒ expr_density" where
"marg_dens2 ≡ (λ(V,V',Γ,δ) x y ρ v.
∫⇧+σ. δ (merge V V' (σ(x := fst (extract_pair v), y := snd (extract_pair v)), ρ))
∂state_measure (V-{x,y}) Γ)"
definition dens_ctxt_measure :: "dens_ctxt ⇒ state ⇒ state measure" where
"dens_ctxt_measure ≡ λ(V,V',Γ,δ) ρ. density (state_measure' V V' Γ ρ) δ"
definition branch_prob :: "dens_ctxt ⇒ state ⇒ ennreal" where
"branch_prob 𝒴 ρ = emeasure (dens_ctxt_measure 𝒴 ρ) (space (dens_ctxt_measure 𝒴 ρ))"
lemma dens_ctxt_measure_nonempty[simp]:
"space (dens_ctxt_measure 𝒴 ρ) ≠ {}"
unfolding dens_ctxt_measure_def state_measure'_def by (cases 𝒴) simp
lemma sets_dens_ctxt_measure_eq[measurable_cong]:
"sets (dens_ctxt_measure (V,V',Γ,δ) ρ) = sets (state_measure (V∪V') Γ)"
by (simp_all add: dens_ctxt_measure_def state_measure'_def)
lemma measurable_dens_ctxt_measure_eq:
"measurable (dens_ctxt_measure (V,V',Γ,δ) ρ) = measurable (state_measure (V∪V') Γ)"
by (intro ext measurable_cong_sets)
(simp_all add: dens_ctxt_measure_def state_measure'_def)
lemma space_dens_ctxt_measure:
"space (dens_ctxt_measure (V,V',Γ,δ) ρ) = space (state_measure (V∪V') Γ)"
unfolding dens_ctxt_measure_def state_measure'_def by simp
definition apply_dist_to_dens :: "pdf_dist ⇒ (state ⇒ val ⇒ ennreal) ⇒ (state ⇒ val ⇒ ennreal)" where
"apply_dist_to_dens dst f = (λρ y. ∫⇧+x. f ρ x * dist_dens dst x y ∂stock_measure (dist_param_type dst))"
definition remove_var :: "state ⇒ state" where
"remove_var σ = (λx. σ (Suc x))"
lemma measurable_remove_var[measurable]:
"remove_var ∈ measurable (state_measure (shift_var_set V) (case_nat t Γ)) (state_measure V Γ)"
proof-
have "(λσ. λx∈V. σ (Suc x)) ∈ measurable
(state_measure (shift_var_set V) (case_nat t Γ)) (state_measure V (λx. case_nat t Γ (Suc x)))"
(is "?f ∈ ?M")
unfolding state_measure_def shift_var_set_def by measurable
also have "⋀x f. x ∉ V ⟹ f ∈ space (state_measure (shift_var_set V) (case_nat t Γ)) ⟹
f (Suc x) = undefined" unfolding state_measure_def
by (subst (asm) space_PiM, drule PiE_arb[of _ _ _ "Suc x" for x])
(simp_all add: space_PiM shift_var_set_def inj_image_mem_iff)
hence "?f ∈ ?M ⟷ remove_var ∈ ?M" unfolding remove_var_def[abs_def] state_measure_def
by (intro measurable_cong ext) (auto simp: space_PiM intro!: sym[of _ undefined])
finally show ?thesis by simp
qed
lemma measurable_case_nat_undefined[measurable]:
"case_nat undefined ∈ measurable (state_measure A Γ) (state_measure (Suc`A) (case_nat t Γ))" (is "_ ∈ ?M")
proof-
have "(λσ. λx∈Suc`A. case_nat undefined σ x) ∈ ?M" (is "?f ∈ _")
unfolding state_measure_def by (rule measurable_restrict) auto
also have "?f ∈ ?M ⟷ ?thesis"
by (intro measurable_cong ext)
(auto simp: state_measure_def space_PiM dest: PiE_mem split: nat.split)
finally show ?thesis .
qed
definition insert_dens
:: "vname set ⇒ vname set ⇒ expr_density ⇒ (state ⇒ ennreal) ⇒ state ⇒ ennreal" where
"insert_dens V V' f δ ≡ λσ. δ (remove_var σ) * f (remove_var σ) (σ 0)"
definition if_dens :: "(state ⇒ ennreal) ⇒ (state ⇒ val ⇒ ennreal) ⇒ bool ⇒ (state ⇒ ennreal)" where
"if_dens δ f b ≡ λσ. δ σ * f σ (BoolVal b)"
definition if_dens_det :: "(state ⇒ ennreal) ⇒ expr ⇒ bool ⇒ (state ⇒ ennreal)" where
"if_dens_det δ e b ≡ λσ. δ σ * (if expr_sem_rf σ e = BoolVal b then 1 else 0)"
lemma measurable_if_dens:
assumes [measurable]: "δ ∈ borel_measurable M"
assumes [measurable]: "case_prod f ∈ borel_measurable (M ⨂⇩M count_space (range BoolVal))"
shows "if_dens δ f b ∈ borel_measurable M"
unfolding if_dens_def by measurable
lemma measurable_if_dens_det:
assumes e: "Γ ⊢ e : BOOL" "randomfree e" "free_vars e ⊆ V"
assumes [measurable]: "δ ∈ borel_measurable (state_measure V Γ)"
shows "if_dens_det δ e b ∈ borel_measurable (state_measure V Γ)"
unfolding if_dens_det_def
proof (intro borel_measurable_times_ennreal assms measurable_If)
have "{x ∈ space (state_measure V Γ). expr_sem_rf x e = BoolVal b} =
(λσ. expr_sem_rf σ e) -` {BoolVal b} ∩ space (state_measure V Γ)" by auto
also have "... ∈ sets (state_measure V Γ)"
by (rule measurable_sets, rule measurable_expr_sem_rf[OF e]) simp_all
finally show "{x ∈ space (state_measure V Γ). expr_sem_rf x e = BoolVal b}
∈ sets (state_measure V Γ)" .
qed simp_all
locale density_context =
fixes V V' Γ δ
assumes subprob_space_dens:
"⋀ρ. ρ ∈ space (state_measure V' Γ) ⟹ subprob_space (dens_ctxt_measure (V,V',Γ,δ) ρ)"
and finite_vars[simp]: "finite V" "finite V'"
and measurable_dens[measurable]:
"δ ∈ borel_measurable (state_measure (V ∪ V') Γ)"
and disjoint: "V ∩ V' = {}"
begin
abbreviation "𝒴 ≡ (V,V',Γ,δ)"
lemma branch_prob_altdef:
assumes ρ: "ρ ∈ space (state_measure V' Γ)"
shows "branch_prob 𝒴 ρ = ∫⇧+ x. δ (merge V V' (x, ρ)) ∂state_measure V Γ"
proof-
have "branch_prob 𝒴 ρ =
∫⇧+ x. δ (merge V V' (x, ρ)) * indicator (space (state_measure (V ∪ V') Γ))
(merge V V' (x, ρ)) ∂state_measure V Γ"
using ρ unfolding branch_prob_def[abs_def] dens_ctxt_measure_def state_measure'_def
by (simp add: emeasure_density ennreal_mult'' ennreal_indicator nn_integral_distr)
also from ρ have "... = ∫⇧+ x. δ (merge V V' (x, ρ)) ∂state_measure V Γ"
by (intro nn_integral_cong) (simp split: split_indicator add: merge_in_state_measure)
finally show ?thesis .
qed
lemma measurable_branch_prob[measurable]:
"branch_prob 𝒴 ∈ borel_measurable (state_measure V' Γ)"
proof-
interpret sigma_finite_measure "state_measure V Γ" by auto
show ?thesis
by (simp add: branch_prob_altdef cong: measurable_cong)
qed
lemma measurable_marg_dens':
assumes [simp]: "x ∈ V"
shows "case_prod (marg_dens 𝒴 x) ∈ borel_measurable (state_measure V' Γ ⨂⇩M stock_measure (Γ x))"
proof-
interpret sigma_finite_measure "state_measure (V - {x}) Γ"
unfolding state_measure_def
by (rule product_sigma_finite.sigma_finite, simp_all add: product_sigma_finite_def)
from assms have "V = insert x (V - {x})" by blast
hence A: "PiM V = PiM ..." by simp
show ?thesis unfolding marg_dens_def
by (simp add: insert_absorb)
qed
lemma insert_Diff: "insert x (A - B) = insert x A - (B - {x})"
by auto
lemma measurable_marg_dens2':
assumes "x ∈ V" "y ∈ V"
shows "case_prod (marg_dens2 𝒴 x y) ∈
borel_measurable (state_measure V' Γ ⨂⇩M stock_measure (PRODUCT (Γ x) (Γ y)))"
proof-
interpret sigma_finite_measure "state_measure (V - {x, y}) Γ"
unfolding state_measure_def
by (rule product_sigma_finite.sigma_finite, simp_all add: product_sigma_finite_def)
have [measurable]: "V = insert x (V - {x, y}) ∪ {y}"
using assms by blast
show ?thesis unfolding marg_dens2_def
by simp
qed
lemma measurable_marg_dens:
assumes "x ∈ V" "ρ ∈ space (state_measure V' Γ)"
shows "marg_dens 𝒴 x ρ ∈ borel_measurable (stock_measure (Γ x))"
using assms by (intro measurable_Pair_compose_split[OF measurable_marg_dens']) simp_all
lemma measurable_marg_dens2:
assumes "x ∈ V" "y ∈ V" "x ≠ y" "ρ ∈ space (state_measure V' Γ)"
shows "marg_dens2 𝒴 x y ρ ∈ borel_measurable (stock_measure (PRODUCT (Γ x) (Γ y)))"
using assms by (intro measurable_Pair_compose_split[OF measurable_marg_dens2']) simp_all
lemma measurable_state_measure_component:
"x ∈ V ⟹ (λσ. σ x) ∈ measurable (state_measure V Γ) (stock_measure (Γ x))"
unfolding state_measure_def
by (auto intro!: measurable_component_singleton)
lemma measurable_dens_ctxt_measure_component:
"x ∈ V ⟹ (λσ. σ x) ∈ measurable (dens_ctxt_measure (V,V',Γ,δ) ρ) (stock_measure (Γ x))"
unfolding dens_ctxt_measure_def state_measure'_def state_measure_def
by (auto intro!: measurable_component_singleton)
lemma space_dens_ctxt_measure_dens_ctxt_measure':
assumes "x ∈ V"
shows "space (state_measure V Γ) =
{σ(x := y) |σ y. σ ∈ space (state_measure (V-{x}) Γ) ∧ y ∈ type_universe (Γ x)}"
proof-
from assms have "insert x (V-{x}) = V" by auto
hence "state_measure V Γ = Pi⇩M (insert x (V-{x})) (λy. stock_measure (Γ y))"
unfolding state_measure_def by simp
also have "space ... = {σ(x := y) |σ y. σ ∈ space (state_measure (V-{x}) Γ) ∧ y ∈ type_universe (Γ x)}"
unfolding state_measure_def space_PiM PiE_insert_eq
by (simp add: image_def Bex_def) blast
finally show ?thesis .
qed
lemma state_measure_integral_split:
assumes "x ∈ A" "finite A"
assumes "f ∈ borel_measurable (state_measure A Γ)"
shows "(∫⇧+σ. f σ ∂state_measure A Γ) =
(∫⇧+y. ∫⇧+σ. f (σ(x := y)) ∂state_measure (A-{x}) Γ ∂stock_measure (Γ x))"
proof-
interpret product_sigma_finite "λy. stock_measure (Γ y)"
unfolding product_sigma_finite_def by auto
from assms have [simp]: "insert x A = A" by auto
have "(∫⇧+σ. f σ ∂state_measure A Γ) = (∫⇧+σ. f σ ∂Π⇩M v∈insert x (A-{x}). stock_measure (Γ v))"
unfolding state_measure_def by simp
also have "... = ∫⇧+y. ∫⇧+σ. f (σ(x := y)) ∂state_measure (A-{x}) Γ ∂stock_measure (Γ x)"
using assms unfolding state_measure_def
by (subst product_nn_integral_insert_rev) simp_all
finally show ?thesis .
qed
lemma fun_upd_in_state_measure:
"⟦σ ∈ space (state_measure A Γ); y ∈ space (stock_measure (Γ x))⟧
⟹ σ(x := y) ∈ space (state_measure (insert x A) Γ)"
unfolding state_measure_def by (auto simp: space_PiM split: if_split_asm)
lemma marg_dens_integral:
fixes X :: "val set" assumes "x ∈ V" and [measurable]: "X ∈ sets (stock_measure (Γ x))"
assumes "ρ