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