Theory PDF_Target_Density_Contexts
section ‹Concrete Density Contexts›
theory PDF_Target_Density_Contexts
imports PDF_Density_Contexts PDF_Target_Semantics
begin
subsection ‹Definition›
type_synonym cdens_ctxt = "vname list × vname list × tyenv × cexpr"
definition dens_ctxt_α :: "cdens_ctxt ⇒ dens_ctxt" where
"dens_ctxt_α ≡ λ(vs,vs',Γ,δ). (set vs, set vs', Γ, λσ. extract_real (cexpr_sem σ δ))"
definition shift_vars :: "nat list ⇒ nat list" where
"shift_vars vs = 0 # map Suc vs"
lemma set_shift_vars[simp]: "set (shift_vars vs) = shift_var_set (set vs)"
unfolding shift_vars_def shift_var_set_def by simp
definition is_density_expr :: "cdens_ctxt ⇒ pdf_type ⇒ cexpr ⇒ bool" where
"is_density_expr ≡ λ(vs,vs',Γ,δ) t e.
case_nat t Γ ⊢⇩c e : REAL ∧
free_vars e ⊆ shift_var_set (set vs') ∧
nonneg_cexpr (shift_var_set (set vs')) (case_nat t Γ) e"
lemma is_density_exprI:
"case_nat t Γ ⊢⇩c e : REAL ⟹
free_vars e ⊆ shift_var_set (set vs') ⟹
nonneg_cexpr (shift_var_set (set vs')) (case_nat t Γ) e ⟹
is_density_expr (vs, vs', Γ, δ) t e"
unfolding is_density_expr_def by simp
lemma is_density_exprD:
assumes "is_density_expr (vs, vs', Γ, δ) t e"
shows "case_nat t Γ ⊢⇩c e : REAL" "free_vars e ⊆ shift_var_set (set vs')"
and is_density_exprD_nonneg: "nonneg_cexpr (shift_var_set (set vs')) (case_nat t Γ) e"
using assms unfolding is_density_expr_def by simp_all
lemma density_context_α:
assumes "cdens_ctxt_invar vs vs' Γ δ"
shows "density_context (set vs) (set vs') Γ (λσ. extract_real (cexpr_sem σ δ))"
proof (unfold density_context_def, intro allI ballI conjI impI subprob_spaceI)
show "(λx. ennreal (extract_real (cexpr_sem x δ)))
∈ borel_measurable (state_measure (set vs ∪ set vs') Γ)"
apply (intro measurable_compose[OF _ measurable_ennreal] measurable_compose[OF _ measurable_extract_real])
apply (insert cdens_ctxt_invarD[OF assms], auto)
done
note [measurable] = this
fix ρ assume ρ: "ρ ∈ space (state_measure (set vs') Γ)"
let ?M = "dens_ctxt_measure (set vs, set vs', Γ, λx. ennreal (extract_real (cexpr_sem x δ))) ρ"
from ρ have "(λσ. merge (set vs) (set vs') (σ, ρ))
∈ measurable (state_measure (set vs) Γ) (state_measure (set vs ∪ set vs') Γ)"
unfolding state_measure_def by simp
hence "emeasure ?M (space ?M) =
∫⇧+x. ennreal (extract_real (cexpr_sem (merge (set vs) (set vs') (x, ρ)) δ))
∂state_measure (set vs) Γ" (is "_ = ?I")
using ρ unfolding dens_ctxt_measure_def state_measure'_def
by (simp add: emeasure_density nn_integral_distr, intro nn_integral_cong)
(simp_all split: split_indicator add: merge_in_state_measure)
also from cdens_ctxt_invarD[OF assms] have "subprob_cexpr (set vs) (set vs') Γ δ" by simp
with ρ have "?I ≤ 1" unfolding subprob_cexpr_def by blast
finally show "emeasure ?M (space ?M) ≤ 1" .
qed (insert cdens_ctxt_invarD[OF assms], simp_all add: nonneg_cexpr_def)
subsection ‹Expressions for density context operations›
definition marg_dens_cexpr :: "tyenv ⇒ vname list ⇒ vname ⇒ cexpr ⇒ cexpr" where
"marg_dens_cexpr Γ vs x e =
map_vars (λy. if y = x then 0 else Suc y) (integrate_vars Γ (filter (λy. y ≠ x) vs) e)"
lemma free_vars_marg_dens_cexpr:
assumes "cdens_ctxt_invar vs vs' Γ δ"
shows "free_vars (marg_dens_cexpr Γ vs x δ) ⊆ shift_var_set (set vs')"
proof-
have "free_vars (marg_dens_cexpr Γ vs x δ) ⊆ shift_var_set (free_vars δ - set vs)"
unfolding marg_dens_cexpr_def shift_var_set_def by auto
also from cdens_ctxt_invarD[OF assms] have "... ⊆ shift_var_set (set vs')"
unfolding shift_var_set_def by auto
finally show ?thesis .
qed
lemma cexpr_typing_marg_dens_cexpr[intro]:
"Γ ⊢⇩c δ : REAL ⟹ case_nat (Γ x) Γ ⊢⇩c marg_dens_cexpr Γ vs x δ : REAL"
unfolding marg_dens_cexpr_def
by (rule cexpr_typing_map_vars, rule cexpr_typing_cong', erule cexpr_typing_integrate_vars) simp
lemma cexpr_sem_marg_dens:
assumes "cdens_ctxt_invar vs vs' Γ δ"
assumes x: "x ∈ set vs" and ρ: "ρ ∈ space (state_measure (set vs') Γ)"
shows "AE v in stock_measure (Γ x).
ennreal (extract_real (cexpr_sem (case_nat v ρ) (marg_dens_cexpr Γ vs x δ))) =
marg_dens (dens_ctxt_α (vs,vs',Γ,δ)) x ρ v"
proof-
note invar = cdens_ctxt_invarD[OF assms(1)]
let ?vs = "filter (λy. y ≠ x) vs"
note cdens_ctxt_invar_imp_integrable[OF assms(1) ρ]
moreover from x have insert_eq: "insert x {xa ∈ set vs. xa ≠ x} = set vs" by auto
ultimately have integrable:
"AE v in stock_measure (Γ x).
integrable (state_measure (set ?vs) Γ)
(λσ. extract_real (cexpr_sem (merge (set ?vs) (insert x (set vs')) (σ, ρ(x := v))) δ))"
using invar x ρ by (intro integrable_cexpr_projection) auto
show ?thesis
proof (rule AE_mp[OF integrable], rule AE_I2, intro impI)
fix v assume v: "v ∈ space (stock_measure (Γ x))"
assume integrable:
"integrable (state_measure (set ?vs) Γ)
(λσ. extract_real (cexpr_sem (merge (set ?vs) (insert x (set vs')) (σ, ρ(x := v))) δ))"
from v and ρ have ρ': "(ρ(x := v)) ∈ space (state_measure (set (x#vs')) Γ)"
by (auto simp: state_measure_def space_PiM split: if_split_asm)
have "cexpr_sem (case_nat v ρ) (marg_dens_cexpr Γ vs x δ) =
cexpr_sem (case_nat v ρ ∘ (λy. if y = x then 0 else Suc y))
(integrate_vars Γ [y←vs . y ≠ x] δ)" (is "_ = ?A")
unfolding marg_dens_cexpr_def by (simp add: cexpr_sem_map_vars)
also have "⋀y. y ∈ free_vars (integrate_vars Γ [y←vs . y ≠ x] δ)
⟹ (case_nat v ρ ∘ (λy. if y = x then 0 else Suc y)) y = (ρ(x := v)) y"
unfolding o_def by simp
hence "?A = cexpr_sem (ρ(x := v)) (integrate_vars Γ [y←vs . y ≠ x] δ)" by (rule cexpr_sem_eq_on_vars)
also from x have "insert x {xa ∈ set vs. xa ≠ x} ∪ set vs' = set vs ∪ set vs'" by auto
hence "extract_real (cexpr_sem (ρ(x := v)) (integrate_vars Γ [y←vs . y ≠ x] δ)) =
∫⇧+σ. extract_real (cexpr_sem (merge (set ?vs) (insert x (set vs')) (σ, ρ(x := v))) δ)
∂state_measure (set ?vs) Γ"
using ρ' invar integrable by (subst cexpr_sem_integrate_vars') (auto )
also from x have "(λσ. merge (set ?vs) (insert x (set vs')) (σ, ρ(x := v))) =
(λσ. merge (set vs) (set vs') (σ(x := v), ρ))"
by (intro ext) (auto simp: merge_def)
also from x have "set ?vs = set vs - {x}" by auto
also have "(∫⇧+σ. extract_real (cexpr_sem (merge (set vs) (set vs') (σ(x := v), ρ)) δ)
∂state_measure (set vs - {x}) Γ) =
marg_dens (dens_ctxt_α (vs,vs',Γ,δ)) x ρ v"
unfolding marg_dens_def dens_ctxt_α_def by simp
finally show "ennreal (extract_real (cexpr_sem (λa. case a of 0 ⇒ v | Suc a ⇒ ρ a)
(marg_dens_cexpr Γ vs x δ))) =
marg_dens (dens_ctxt_α (vs, vs', Γ, δ)) x ρ v" .
qed
qed
lemma nonneg_cexpr_sem_marg_dens:
assumes "cdens_ctxt_invar vs vs' Γ δ"
assumes x: "x ∈ set vs" and ρ: "ρ ∈ space (state_measure (set vs') Γ)"
assumes v: "v ∈ type_universe (Γ x)"
shows "extract_real (cexpr_sem (case_nat v ρ) (marg_dens_cexpr Γ vs x δ)) ≥ 0"
proof-
note invar = cdens_ctxt_invarD[OF assms(1)]
from assms have ρ: "case_nat v ρ ∘ (λy. if y = x then 0 else Suc y)
∈ space (state_measure (set (x#vs')) Γ)"
by (force simp: state_measure_def space_PiM o_def split: if_split_asm)
moreover from x have "insert x {xa ∈ set vs. xa ≠ x} ∪ set vs' = set vs ∪ set vs'" by auto
ultimately show ?thesis using assms invar unfolding marg_dens_cexpr_def
by (subst cexpr_sem_map_vars, intro nonneg_cexpr_sem_integrate_vars[of _ "set (x#vs')"]) auto
qed
definition marg_dens2_cexpr :: "tyenv ⇒ vname list ⇒ vname ⇒ vname ⇒ cexpr ⇒ cexpr" where
"marg_dens2_cexpr Γ vs x y e =
(cexpr_comp_aux (Suc x) (fst⇩c (CVar 0))
(cexpr_comp_aux (Suc y) (snd⇩c (CVar 0))
(map_vars Suc (integrate_vars Γ (filter (λz. z ≠ x ∧ z ≠ y) vs) e))))"
lemma free_vars_marg_dens2_cexpr:
assumes "cdens_ctxt_invar vs vs' Γ δ"
shows "free_vars (marg_dens2_cexpr Γ vs x y δ) ⊆ shift_var_set (set vs')"
proof-
have "free_vars (marg_dens2_cexpr Γ vs x y δ) ⊆
shift_var_set (free_vars δ - set vs)"
unfolding marg_dens2_cexpr_def using cdens_ctxt_invarD[OF assms(1)]
apply (intro order.trans[OF free_vars_cexpr_comp_aux] Un_least)
apply (subst Diff_subset_conv, intro order.trans[OF free_vars_cexpr_comp_aux])
apply (auto simp: shift_var_set_def)
done
also from cdens_ctxt_invarD[OF assms(1)] have "... ⊆ shift_var_set (set vs')"
unfolding shift_var_set_def by auto
finally show ?thesis .
qed
lemma cexpr_typing_marg_dens2_cexpr[intro]:
assumes "Γ ⊢⇩c δ : REAL"
shows "case_nat (PRODUCT (Γ x) (Γ y)) Γ ⊢⇩c marg_dens2_cexpr Γ vs x y δ : REAL"
proof-
have A: "(case_nat (PRODUCT (Γ x) (Γ y)) Γ) (Suc x := Γ x, Suc y := Γ y) ∘ Suc = Γ"
by (intro ext) (auto split: nat.split)
show ?thesis unfolding marg_dens2_cexpr_def
apply (rule cexpr_typing_cexpr_comp_aux[of _ _ "Γ x"])
apply (rule cexpr_typing_cexpr_comp_aux[of _ _ "Γ y"])
apply (rule cexpr_typing_map_vars, subst A, rule cexpr_typing_integrate_vars[OF assms])
apply (rule cet_op, rule cet_var, simp, rule cet_op, rule cet_var, simp)
done
qed
lemma cexpr_sem_marg_dens2:
assumes "cdens_ctxt_invar vs vs' Γ δ"
assumes x: "x ∈ set vs" and y: "y ∈ set vs" and "x ≠ y"
assumes ρ: "ρ ∈ space (state_measure (set vs') Γ)"
shows "AE z in stock_measure (PRODUCT (Γ x) (Γ y)).
ennreal (extract_real (cexpr_sem (case_nat z ρ) (marg_dens2_cexpr Γ vs x y δ))) =
marg_dens2 (dens_ctxt_α (vs,vs',Γ,δ)) x y ρ z"
proof-
note invar = cdens_ctxt_invarD[OF assms(1)]
let ?f = "λx. ennreal (extract_real (cexpr_sem x δ))"
let ?vs = "filter (λz. z ≠ x ∧ z ≠ y) vs"
interpret product_sigma_finite "λx. stock_measure (Γ x)"
unfolding product_sigma_finite_def by simp
interpret sf_PiM: sigma_finite_measure "PiM (set ?vs) (λx. stock_measure (Γ x))"
by (intro sigma_finite) simp
have meas: "(λσ. extract_real (cexpr_sem (merge (set vs) (set vs') (σ, ρ)) δ))
∈ borel_measurable (state_measure (set vs) Γ)" using assms invar
by (intro measurable_cexpr_sem') simp_all
from x y have insert_eq: "insert x (insert y (set ?vs)) = set vs" by auto
from x y have insert_eq': "insert y (insert x (set ?vs)) = set vs" by auto
have meas_upd1: "(λ(σ,v). σ(y := v)) ∈
measurable (PiM (insert x (set vs)) (λx. stock_measure (Γ x)) ⨂⇩M stock_measure (Γ y))
(PiM (insert y (insert x (set vs))) (λx. stock_measure (Γ x)))"
using measurable_add_dim[of y "insert x (set ?vs)" "λx. stock_measure (Γ x)"]
by (simp only: insert_eq', simp)
hence meas_upd2: "(λxa. (snd xa) (x := fst (fst xa), y := snd (fst xa)))
∈ measurable ((stock_measure (Γ x) ⨂⇩M stock_measure (Γ y)) ⨂⇩M
Pi⇩M (set ?vs) (λy. stock_measure (Γ y)))
(Pi⇩M (set vs) (λy. stock_measure (Γ y)))"
by (subst insert_eq'[symmetric], intro measurable_Pair_compose_split[OF measurable_add_dim])
(simp_all del: fun_upd_apply)
from x y have A: "set vs = {x, y} ∪ set ?vs" by auto
have "(∫⇧+σ. ?f (merge (set vs) (set vs') (σ, ρ)) ∂state_measure (set vs) Γ) =
(∫⇧+σ'. ∫⇧+σ. ?f (merge (set vs) (set vs') (merge {x, y} (set ?vs) (σ', σ), ρ))
∂state_measure (set ?vs) Γ ∂state_measure {x,y} Γ)" (is "_ = ?I")
using meas insert_eq unfolding state_measure_def
by (subst A, subst product_nn_integral_fold) (simp_all add: measurable_compose[OF _ measurable_ennreal])
also have "⋀σ' σ. merge (set vs) (set vs') (merge {x, y} (set ?vs) (σ', σ), ρ) =
merge (set vs) (set vs') (σ(x := σ' x, y := σ' y), ρ)"
by (intro ext) (auto simp: merge_def)
hence "?I = (∫⇧+σ'. ∫⇧+σ. ?f (merge (set vs) (set vs') (σ(x := σ' x, y := σ' y), ρ))
∂state_measure (set ?vs) Γ ∂state_measure {x,y} Γ)" by simp
also have "... = ∫⇧+z. ∫⇧+σ. ?f (merge (set vs) (set vs') (σ(x := fst z, y := snd z), ρ))
∂state_measure (set ?vs) Γ ∂(stock_measure (Γ x) ⨂⇩M stock_measure (Γ y))"
(is "_ = ?I") using ‹x ≠ y› meas_upd2 ρ invar unfolding state_measure_def
by (subst product_nn_integral_pair, subst measurable_split_conv,
intro sf_PiM.borel_measurable_nn_integral)
(auto simp: measurable_split_conv state_measure_def intro!: measurable_compose[OF _ measurable_ennreal]
measurable_compose[OF _ measurable_cexpr_sem'] measurable_Pair )
finally have "(∫⇧+σ. ?f (merge (set vs) (set vs') (σ, ρ)) ∂state_measure (set vs) Γ) = ?I" .
moreover have "(∫⇧+σ. ?f (merge (set vs) (set vs') (σ, ρ)) ∂state_measure (set vs) Γ) ≠ ∞"
using cdens_ctxt_invar_imp_integrable[OF assms(1) ρ] unfolding real_integrable_def by simp
ultimately have "?I ≠ ∞" by simp
hence "AE z in stock_measure (Γ x) ⨂⇩M stock_measure (Γ y).
(∫⇧+σ. ?f (merge (set vs) (set vs') (σ(x := fst z, y := snd z), ρ))
∂state_measure (set ?vs) Γ) ≠ ∞" (is "AE z in _. ?P z")
using meas_upd2 ρ invar unfolding state_measure_def
by (intro nn_integral_PInf_AE sf_PiM.borel_measurable_nn_integral)
(auto intro!: measurable_compose[OF _ measurable_ennreal] measurable_compose[OF _ measurable_cexpr_sem']
measurable_Pair simp: measurable_split_conv state_measure_def)
hence "AE z in stock_measure (Γ x) ⨂⇩M stock_measure (Γ y).
ennreal (extract_real (cexpr_sem (case_nat (case_prod PairVal z) ρ) (marg_dens2_cexpr Γ vs x y δ))) =
marg_dens2 (dens_ctxt_α (vs,vs',Γ,δ)) x y ρ (case_prod PairVal z)"
proof (rule AE_mp[OF _ AE_I2[OF impI]])
fix z assume z: "z ∈ space (stock_measure (Γ x) ⨂⇩M stock_measure (Γ y))"
assume fin: "?P z"
have "⋀σ. merge (set vs) (set vs') (σ(x := fst z, y := snd z), ρ) =
merge (set ?vs) ({x,y} ∪ set vs') (σ, ρ(x := fst z, y := snd z))" using x y
by (intro ext) (simp add: merge_def)
hence A: "(∫⇧+σ. ?f (merge (set vs) (set vs') (σ(x := fst z, y := snd z), ρ))
∂state_measure (set ?vs) Γ) =
(∫⇧+σ. ?f (merge (set ?vs) ({x,y} ∪ set vs') (σ, ρ(x := fst z, y := snd z)))
∂state_measure (set ?vs) Γ)" (is "_ = ∫⇧+σ. ennreal (?g σ) ∂?M")
by (intro nn_integral_cong) simp
have ρ': "ρ(x := fst z, y := snd z) ∈ space (state_measure ({x, y} ∪ set vs') Γ)"
using z ρ unfolding state_measure_def
by (auto simp: space_PiM space_pair_measure split: if_split_asm)
have integrable: "integrable ?M ?g"
proof (intro integrableI_nonneg[OF _ AE_I2])
show "?g ∈ borel_measurable ?M" using invar ρ' by (intro measurable_cexpr_sem') auto
show "(∫⇧+σ. ennreal (?g σ) ∂?M) < ∞" using fin A by (simp add: top_unique less_top)
fix σ assume σ: "σ ∈ space ?M"
from x y have "set ?vs ∪ ({x,y} ∪ set vs') = set vs ∪ set vs'" by auto
thus "?g σ ≥ 0" using merge_in_state_measure[OF σ ρ']
by (intro nonneg_cexprD[OF invar(4)]) simp_all
qed
from x y have B: "(set ?vs ∪ ({x, y} ∪ set vs')) = set vs ∪ set vs'" by auto
have nonneg: "nonneg_cexpr (set [z←vs . z ≠ x ∧ z ≠ y] ∪ ({x, y} ∪ set vs')) Γ δ"
using invar by (subst B) simp
have "ennreal (extract_real (cexpr_sem (case_nat (case_prod PairVal z) ρ) (marg_dens2_cexpr Γ vs x y δ))) =
extract_real (cexpr_sem ((case_nat <|fst z, snd z|> ρ) (Suc x := fst z, Suc y := snd z) ∘ Suc)
(integrate_vars Γ ?vs δ))"
unfolding marg_dens2_cexpr_def
by (simp add: cexpr_sem_cexpr_comp_aux cexpr_sem_map_vars split: prod.split)
also have "((case_nat <|fst z, snd z|> ρ) (Suc x := fst z, Suc y := snd z)) ∘ Suc =
ρ(x := fst z, y := snd z)" (is "?ρ1 = ?ρ2") by (intro ext) (simp split: nat.split)
also have "ennreal (extract_real (cexpr_sem (ρ(x := fst z, y := snd z))
(integrate_vars Γ [z←vs . z ≠ x ∧ z ≠ y] δ))) =
∫⇧+xa. ?f (merge (set ?vs) ({x, y} ∪ set vs') (xa, ρ(x := fst z, y := snd z))) ∂?M"
using invar assms by (intro cexpr_sem_integrate_vars'[OF ρ' _ _ nonneg integrable]) auto
also have C: "set ?vs = set vs - {x, y}" by auto
have "(∫⇧+xa. ?f (merge (set ?vs) ({x, y} ∪ set vs') (xa, ρ(x := fst z, y := snd z))) ∂?M) =
marg_dens2 (dens_ctxt_α (vs,vs',Γ,δ)) x y ρ (case_prod PairVal z)"
unfolding marg_dens2_def
by (subst A[symmetric], subst C, simp only: dens_ctxt_α_def prod.case)
(auto intro!: nn_integral_cong split: prod.split)
finally show "ennreal (extract_real (cexpr_sem (case_nat (case_prod PairVal z) ρ)
(marg_dens2_cexpr Γ vs x y δ))) =
marg_dens2 (dens_ctxt_α (vs, vs', Γ, δ)) x y ρ (case_prod PairVal z)" .
qed
thus ?thesis by (subst stock_measure.simps, subst AE_embed_measure[OF inj_PairVal]) simp
qed
lemma nonneg_cexpr_sem_marg_dens2:
assumes "cdens_ctxt_invar vs vs' Γ δ"
assumes x: "x ∈ set vs" and y: "y ∈ set vs" and ρ: "ρ ∈ space (state_measure (set vs') Γ)"
assumes v: "v ∈ type_universe (PRODUCT (Γ x) (Γ y))"
shows "extract_real (cexpr_sem (case_nat v ρ) (marg_dens2_cexpr Γ vs x y δ)) ≥ 0"
proof-
from v obtain a b where v': "v = <|a, b|>" "a ∈ type_universe (Γ x)" "b ∈ type_universe (Γ y)"
by (auto simp: val_type_eq_PRODUCT)
let ?vs = "filter (λz. z ≠ x ∧ z ≠ y) vs"
note invar = cdens_ctxt_invarD[OF assms(1)]
have A: "((case_nat v ρ) (Suc x := fst (extract_pair v), Suc y := snd (extract_pair v))) ∘ Suc =
ρ(x := fst (extract_pair v), y := snd (extract_pair v))" by (intro ext) auto
have B: "ρ(x := fst (extract_pair v), y := snd (extract_pair v))
∈ space (state_measure (set vs' ∪ {x,y}) Γ)" using x y v' ρ
by (auto simp: space_state_measure split: if_split_asm)
from x y have "set ?vs ∪ (set vs' ∪ {x, y}) = set vs ∪ set vs'" by auto
with invar have "nonneg_cexpr (set ?vs ∪ (set vs' ∪ {x, y})) Γ δ" by simp
thus ?thesis using assms invar(1-3) A unfolding marg_dens2_cexpr_def
by (auto simp: cexpr_sem_cexpr_comp_aux cexpr_sem_map_vars intro!: nonneg_cexpr_sem_integrate_vars[OF B])
qed
definition branch_prob_cexpr :: "cdens_ctxt ⇒ cexpr" where
"branch_prob_cexpr ≡ λ(vs, vs', Γ, δ). integrate_vars Γ vs δ"
lemma free_vars_branch_prob_cexpr[simp]:
"free_vars (branch_prob_cexpr (vs, vs', Γ, δ)) = free_vars δ - set vs"
unfolding branch_prob_cexpr_def by simp
lemma cexpr_typing_branch_prob_cexpr[intro]:
"Γ ⊢⇩c δ : REAL ⟹ Γ ⊢⇩c branch_prob_cexpr (vs,vs',Γ,δ) : REAL"
unfolding branch_prob_cexpr_def
by (simp only: prod.case, rule cexpr_typing_integrate_vars)
lemma cexpr_sem_branch_prob:
assumes "cdens_ctxt_invar vs vs' Γ δ"
assumes ρ: "ρ ∈ space (state_measure (set vs') Γ)"
shows "ennreal (extract_real (cexpr_sem ρ (branch_prob_cexpr (vs, vs', Γ, δ)))) =
branch_prob (dens_ctxt_α (vs, vs', Γ, δ)) ρ"
proof-
note invar = cdens_ctxt_invarD[OF assms(1)]
interpret density_context "set vs" "set vs'" Γ "λσ. extract_real (cexpr_sem σ δ)"
by (rule density_context_α) fact
have "ennreal (extract_real (cexpr_sem ρ (branch_prob_cexpr (vs, vs', Γ, δ)))) =
∫⇧+σ. extract_real (cexpr_sem (merge (set vs) (set vs') (σ, ρ)) δ)
∂state_measure (set vs) Γ" (is "_ = ?I")
using assms(2) invar unfolding branch_prob_cexpr_def
by (simp only: prod.case, subst cexpr_sem_integrate_vars')
(auto intro!: cdens_ctxt_invar_imp_integrable assms)
also have "... = branch_prob (dens_ctxt_α (vs, vs', Γ, δ)) ρ"
using ρ unfolding dens_ctxt_α_def by (simp only: prod.case branch_prob_altdef[of ρ])
finally show ?thesis .
qed
lemma subprob_imp_subprob_cexpr:
assumes "density_context V V' Γ (λσ. extract_real (cexpr_sem σ δ))"
shows "subprob_cexpr V V' Γ δ"
proof (intro subprob_cexprI)
interpret density_context V V' Γ "λσ. extract_real (cexpr_sem σ δ)" by fact
fix ρ assume ρ: "ρ ∈ space (state_measure V' Γ)"
let ?M = "dens_ctxt_measure (V, V', Γ, λσ. extract_real (cexpr_sem σ δ)) ρ"
from ρ have "(∫⇧+ x. ennreal (extract_real (cexpr_sem (merge V V' (x, ρ)) δ)) ∂state_measure V Γ) =
branch_prob (V, V', Γ, λσ. extract_real (cexpr_sem σ δ)) ρ" (is "?I = _")
by (subst branch_prob_altdef[symmetric]) simp_all
also have "... = emeasure ?M (space ?M)" unfolding branch_prob_def by simp
also have "... ≤ 1" by (rule subprob_space.emeasure_space_le_1) (simp add: subprob_space_dens ρ)
finally show "?I ≤ 1" .
qed
end