Theory Finite_Product_Measure
section ‹Finite Product Measure›
theory Finite_Product_Measure
imports Binary_Product_Measure Function_Topology
begin
lemma Pi_choice: "(∀i∈I. ∃x∈F i. P i x) ⟷ (∃f∈Pi I F. ∀i∈I. P i (f i))"
by (metis Pi_iff)
lemma PiE_choice: "(∀i∈I. ∃x∈F i. P i x) ⟷(∃f∈Pi⇩E I F. ∀i∈I. P i (f i))"
unfolding Pi_choice by (metis Int_iff PiE_def restrict_PiE restrict_apply)
lemma case_prod_const: "(λ(i, j). c) = (λ_. c)"
by auto
subsection ‹More about Function restricted by \<^const>‹extensional››
definition
"merge I J = (λ(x, y) i. if i ∈ I then x i else if i ∈ J then y i else undefined)"
lemma merge_apply[simp]:
"I ∩ J = {} ⟹ i ∈ I ⟹ merge I J (x, y) i = x i"
"I ∩ J = {} ⟹ i ∈ J ⟹ merge I J (x, y) i = y i"
"J ∩ I = {} ⟹ i ∈ I ⟹ merge I J (x, y) i = x i"
"J ∩ I = {} ⟹ i ∈ J ⟹ merge I J (x, y) i = y i"
"i ∉ I ⟹ i ∉ J ⟹ merge I J (x, y) i = undefined"
unfolding merge_def by auto
lemma merge_commute:
"I ∩ J = {} ⟹ merge I J (x, y) = merge J I (y, x)"
by (force simp: merge_def)
lemma Pi_cancel_merge_range[simp]:
"I ∩ J = {} ⟹ x ∈ Pi I (merge I J (A, B)) ⟷ x ∈ Pi I A"
"I ∩ J = {} ⟹ x ∈ Pi I (merge J I (B, A)) ⟷ x ∈ Pi I A"
"J ∩ I = {} ⟹ x ∈ Pi I (merge I J (A, B)) ⟷ x ∈ Pi I A"
"J ∩ I = {} ⟹ x ∈ Pi I (merge J I (B, A)) ⟷ x ∈ Pi I A"
by (auto simp: Pi_def)
lemma Pi_cancel_merge[simp]:
"I ∩ J = {} ⟹ merge I J (x, y) ∈ Pi I B ⟷ x ∈ Pi I B"
"J ∩ I = {} ⟹ merge I J (x, y) ∈ Pi I B ⟷ x ∈ Pi I B"
"I ∩ J = {} ⟹ merge I J (x, y) ∈ Pi J B ⟷ y ∈ Pi J B"
"J ∩ I = {} ⟹ merge I J (x, y) ∈ Pi J B ⟷ y ∈ Pi J B"
by (auto simp: Pi_def)
lemma extensional_merge[simp]: "merge I J (x, y) ∈ extensional (I ∪ J)"
by (auto simp: extensional_def)
lemma restrict_merge[simp]:
"I ∩ J = {} ⟹ restrict (merge I J (x, y)) I = restrict x I"
"I ∩ J = {} ⟹ restrict (merge I J (x, y)) J = restrict y J"
"J ∩ I = {} ⟹ restrict (merge I J (x, y)) I = restrict x I"
"J ∩ I = {} ⟹ restrict (merge I J (x, y)) J = restrict y J"
by (auto simp: restrict_def)
lemma split_merge: "P (merge I J (x,y) i) ⟷ (i ∈ I ⟶ P (x i)) ∧ (i ∈ J - I ⟶ P (y i)) ∧ (i ∉ I ∪ J ⟶ P undefined)"
unfolding merge_def by auto
lemma PiE_cancel_merge[simp]:
"I ∩ J = {} ⟹
merge I J (x, y) ∈ Pi⇩E (I ∪ J) B ⟷ x ∈ Pi I B ∧ y ∈ Pi J B"
by (auto simp: PiE_def restrict_Pi_cancel)
lemma merge_singleton[simp]: "i ∉ I ⟹ merge I {i} (x,y) = restrict (x(i := y i)) (insert i I)"
unfolding merge_def by (auto simp: fun_eq_iff)
lemma extensional_merge_sub: "I ∪ J ⊆ K ⟹ merge I J (x, y) ∈ extensional K"
unfolding merge_def extensional_def by auto
lemma merge_restrict[simp]:
"merge I J (restrict x I, y) = merge I J (x, y)"
"merge I J (x, restrict y J) = merge I J (x, y)"
unfolding merge_def by auto
lemma merge_x_x_eq_restrict[simp]:
"merge I J (x, x) = restrict x (I ∪ J)"
unfolding merge_def by auto
lemma injective_vimage_restrict:
assumes J: "J ⊆ I"
and sets: "A ⊆ (Π⇩E i∈J. S i)" "B ⊆ (Π⇩E i∈J. S i)" and ne: "(Π⇩E i∈I. S i) ≠ {}"
and eq: "(λx. restrict x J) -` A ∩ (Π⇩E i∈I. S i) = (λx. restrict x J) -` B ∩ (Π⇩E i∈I. S i)"
shows "A = B"
proof (intro set_eqI)
fix x
from ne obtain y where y: "⋀i. i ∈ I ⟹ y i ∈ S i" by auto
have "J ∩ (I - J) = {}" by auto
show "x ∈ A ⟷ x ∈ B"
proof cases
assume x: "x ∈ (Π⇩E i∈J. S i)"
have "x ∈ A ⟷ merge J (I - J) (x,y) ∈ (λx. restrict x J) -` A ∩ (Π⇩E i∈I. S i)"
using y x ‹J ⊆ I› PiE_cancel_merge[of "J" "I - J" x y S]
by (auto simp del: PiE_cancel_merge simp add: Un_absorb1)
then show "x ∈ A ⟷ x ∈ B"
using y x ‹J ⊆ I› PiE_cancel_merge[of "J" "I - J" x y S]
by (auto simp del: PiE_cancel_merge simp add: Un_absorb1 eq)
qed (use sets in auto)
qed
lemma restrict_vimage:
"I ∩ J = {} ⟹
(λx. (restrict x I, restrict x J)) -` (Pi⇩E I E × Pi⇩E J F) = Pi (I ∪ J) (merge I J (E, F))"
by (auto simp: restrict_Pi_cancel PiE_def)
lemma merge_vimage:
"I ∩ J = {} ⟹ merge I J -` Pi⇩E (I ∪ J) E = Pi I E × Pi J E"
by (auto simp: restrict_Pi_cancel PiE_def)
subsection ‹Finite product spaces›
definition prod_emb where
"prod_emb I M K X = (λx. restrict x K) -` X ∩ (Π⇩E i∈I. space (M i))"
lemma prod_emb_iff:
"f ∈ prod_emb I M K X ⟷ f ∈ extensional I ∧ (restrict f K ∈ X) ∧ (∀i∈I. f i ∈ space (M i))"
unfolding prod_emb_def PiE_def by auto
lemma
shows prod_emb_empty[simp]: "prod_emb M L K {} = {}"
and prod_emb_Un[simp]: "prod_emb M L K (A ∪ B) = prod_emb M L K A ∪ prod_emb M L K B"
and prod_emb_Int: "prod_emb M L K (A ∩ B) = prod_emb M L K A ∩ prod_emb M L K B"
and prod_emb_UN[simp]: "prod_emb M L K (⋃i∈I. F i) = (⋃i∈I. prod_emb M L K (F i))"
and prod_emb_INT[simp]: "I ≠ {} ⟹ prod_emb M L K (⋂i∈I. F i) = (⋂i∈I. prod_emb M L K (F i))"
and prod_emb_Diff[simp]: "prod_emb M L K (A - B) = prod_emb M L K A - prod_emb M L K B"
by (auto simp: prod_emb_def)
lemma prod_emb_PiE: "J ⊆ I ⟹ (⋀i. i ∈ J ⟹ E i ⊆ space (M i)) ⟹
prod_emb I M J (Π⇩E i∈J. E i) = (Π⇩E i∈I. if i ∈ J then E i else space (M i))"
by (force simp: prod_emb_def PiE_iff if_split_mem2)
lemma prod_emb_PiE_same_index[simp]:
"(⋀i. i ∈ I ⟹ E i ⊆ space (M i)) ⟹ prod_emb I M I (Pi⇩E I E) = Pi⇩E I E"
by (auto simp: prod_emb_def PiE_iff)
lemma prod_emb_trans[simp]:
"J ⊆ K ⟹ K ⊆ L ⟹ prod_emb L M K (prod_emb K M J X) = prod_emb L M J X"
by (auto simp add: Int_absorb1 prod_emb_def PiE_def)
lemma prod_emb_Pi:
assumes "X ∈ (Π j∈J. sets (M j))" "J ⊆ K"
shows "prod_emb K M J (Pi⇩E J X) = (Π⇩E i∈K. if i ∈ J then X i else space (M i))"
using assms sets.space_closed
by (auto simp: prod_emb_def PiE_iff split: if_split_asm) blast+
lemma prod_emb_id:
"B ⊆ (Π⇩E i∈L. space (M i)) ⟹ prod_emb L M L B = B"
by (auto simp: prod_emb_def subset_eq extensional_restrict)
lemma prod_emb_mono:
"F ⊆ G ⟹ prod_emb A M B F ⊆ prod_emb A M B G"
by (auto simp: prod_emb_def)
definition PiM :: "'i set ⇒ ('i ⇒ 'a measure) ⇒ ('i ⇒ 'a) measure" where
"PiM I M = extend_measure (Π⇩E i∈I. space (M i))
{(J, X). (J ≠ {} ∨ I = {}) ∧ finite J ∧ J ⊆ I ∧ X ∈ (Π j∈J. sets (M j))}
(λ(J, X). prod_emb I M J (Π⇩E j∈J. X j))
(λ(J, X). ∏j∈J ∪ {i∈I. emeasure (M i) (space (M i)) ≠ 1}. if j ∈ J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))"
definition prod_algebra :: "'i set ⇒ ('i ⇒ 'a measure) ⇒ ('i ⇒ 'a) set set" where
"prod_algebra I M = (λ(J, X). prod_emb I M J (Π⇩E j∈J. X j)) `
{(J, X). (J ≠ {} ∨ I = {}) ∧ finite J ∧ J ⊆ I ∧ X ∈ (Π j∈J. sets (M j))}"
abbreviation
"Pi⇩M I M ≡ PiM I M"
syntax
"_PiM" :: "pttrn ⇒ 'i set ⇒ 'a measure ⇒ ('i => 'a) measure"
(‹(‹indent=3 notation=‹binder Π⇩M››Π⇩M _∈_./ _)› 10)
syntax_consts
"_PiM" == PiM
translations
"Π⇩M x∈I. M" == "CONST PiM I (%x. M)"
lemma extend_measure_cong:
assumes "Ω = Ω'" "I = I'" "G = G'" "⋀i. i ∈ I' ⟹ μ i = μ' i"
shows "extend_measure Ω I G μ = extend_measure Ω' I' G' μ'"
unfolding extend_measure_def by (auto simp add: assms)
lemma Pi_cong_sets:
"⟦I = J; ⋀x. x ∈ I ⟹ M x = N x⟧ ⟹ Pi I M = Pi J N"
by auto
lemma PiM_cong:
assumes "I = J" "⋀x. x ∈ I ⟹ M x = N x"
shows "PiM I M = PiM J N"
unfolding PiM_def
proof (rule extend_measure_cong, goal_cases)
case 1
show ?case using assms
by (subst assms(1), intro PiE_cong[of J "λi. space (M i)" "λi. space (N i)"]) simp_all
next
case 2
have "⋀K. K ⊆ J ⟹ (Π j∈K. sets (M j)) = (Π j∈K. sets (N j))"
using assms by (intro Pi_cong_sets) auto
thus ?case by (auto simp: assms)
next
case 3
show ?case using assms
by (intro ext) (auto simp: prod_emb_def dest: PiE_mem)
next
case (4 x)
thus ?case using assms
by (auto intro!: prod.cong split: if_split_asm)
qed
lemma prod_algebra_sets_into_space:
"prod_algebra I M ⊆ Pow (Π⇩E i∈I. space (M i))"
by (auto simp: prod_emb_def prod_algebra_def)
lemma prod_algebra_eq_finite:
assumes I: "finite I"
shows "prod_algebra I M = {(Π⇩E i∈I. X i) |X. X ∈ (Π j∈I. sets (M j))}" (is "?L = ?R")
proof (intro iffI set_eqI)
fix A assume "A ∈ ?L"
then obtain J E where J: "J ≠ {} ∨ I = {}" "finite J" "J ⊆ I" "∀i∈J. E i ∈ sets (M i)"
and A: "A = prod_emb I M J (Π⇩E j∈J. E j)"
by (auto simp: prod_algebra_def)
let ?A = "Π⇩E i∈I. if i ∈ J then E i else space (M i)"
have A: "A = ?A"
unfolding A using J by (intro prod_emb_PiE sets.sets_into_space) auto
show "A ∈ ?R" unfolding A using J sets.top
by (intro CollectI exI[of _ "λi. if i ∈ J then E i else space (M i)"]) simp
next
fix A assume "A ∈ ?R"
then obtain X where A: "A = (Π⇩E i∈I. X i)" and X: "X ∈ (Π j∈I. sets (M j))" by auto
then have A: "A = prod_emb I M I (Π⇩E i∈I. X i)"
by (simp add: prod_emb_PiE_same_index[OF sets.sets_into_space] Pi_iff)
from X I show "A ∈ ?L" unfolding A
by (auto simp: prod_algebra_def)
qed
lemma prod_algebraI:
"finite J ⟹ (J ≠ {} ∨ I = {}) ⟹ J ⊆ I ⟹ (⋀i. i ∈ J ⟹ E i ∈ sets (M i))
⟹ prod_emb I M J (Π⇩E j∈J. E j) ∈ prod_algebra I M"
by (auto simp: prod_algebra_def)
lemma prod_algebraI_finite:
"finite I ⟹ (∀i∈I. E i ∈ sets (M i)) ⟹ (Pi⇩E I E) ∈ prod_algebra I M"
using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets.sets_into_space] by simp
lemma Int_stable_PiE: "Int_stable {Pi⇩E J E | E. ∀i∈I. E i ∈ sets (M i)}"
proof (safe intro!: Int_stableI)
fix E F assume "∀i∈I. E i ∈ sets (M i)" "∀i∈I. F i ∈ sets (M i)"
then show "∃G. Pi⇩E J E ∩ Pi⇩E J F = Pi⇩E J G ∧ (∀i∈I. G i ∈ sets (M i))"
by (auto intro!: exI[of _ "λi. E i ∩ F i"] simp: PiE_Int)
qed
lemma prod_algebraE:
assumes A: "A ∈ prod_algebra I M"
obtains J E where "A = prod_emb I M J (Π⇩E j∈J. E j)"
"finite J" "J ≠ {} ∨ I = {}" "J ⊆ I" "⋀i. i ∈ J ⟹ E i ∈ sets (M i)"
using A by (auto simp: prod_algebra_def)
lemma prod_algebraE_all:
assumes A: "A ∈ prod_algebra I M"
obtains E where "A = Pi⇩E I E" "E ∈ (Π i∈I. sets (M i))"
proof -
from A obtain E J where A: "A = prod_emb I M J (Pi⇩E J E)"
and J: "J ⊆ I" and E: "E ∈ (Π i∈J. sets (M i))"
by (auto simp: prod_algebra_def)
from E have "⋀i. i ∈ J ⟹ E i ⊆ space (M i)"
using sets.sets_into_space by auto
then have "A = (Π⇩E i∈I. if i∈J then E i else space (M i))"
using A J by (auto simp: prod_emb_PiE)
moreover have "(λi. if i∈J then E i else space (M i)) ∈ (Π i∈I. sets (M i))"
using sets.top E by auto
ultimately show ?thesis using that by auto
qed
lemma Int_stable_prod_algebra: "Int_stable (prod_algebra I M)"
unfolding Int_stable_def
proof safe
fix A assume "A ∈ prod_algebra I M"
from prod_algebraE[OF this] obtain J E where A:
"A = prod_emb I M J (Pi⇩E J E)"
"finite J"
"J ≠ {} ∨ I = {}"
"J ⊆ I"
"⋀i. i ∈ J ⟹ E i ∈ sets (M i)"
by auto
fix B assume "B ∈ prod_algebra I M"
from prod_algebraE[OF this] obtain K F where B:
"B = prod_emb I M K (Pi⇩E K F)"
"finite K"
"K ≠ {} ∨ I = {}"
"K ⊆ I"
"⋀i. i ∈ K ⟹ F i ∈ sets (M i)"
by auto
have "A ∩ B = prod_emb I M (J ∪ K) (Π⇩E i∈J ∪ K. (if i ∈ J then E i else space (M i)) ∩
(if i ∈ K then F i else space (M i)))"
unfolding A B using A(2,3,4) A(5)[THEN sets.sets_into_space] B(2,3,4)
B(5)[THEN sets.sets_into_space]
apply (subst (1 2 3) prod_emb_PiE)
apply (simp_all add: subset_eq PiE_Int)
apply blast
apply (intro PiE_cong)
apply auto
done
also have "… ∈ prod_algebra I M"
using A B by (auto intro!: prod_algebraI)
finally show "A ∩ B ∈ prod_algebra I M" .
qed
proposition prod_algebra_mono:
assumes space: "⋀i. i ∈ I ⟹ space (E i) = space (F i)"
assumes sets: "⋀i. i ∈ I ⟹ sets (E i) ⊆ sets (F i)"
shows "prod_algebra I E ⊆ prod_algebra I F"
proof
fix A assume "A ∈ prod_algebra I E"
then obtain J G where J: "J ≠ {} ∨ I = {}" "finite J" "J ⊆ I"
and A: "A = prod_emb I E J (Π⇩E i∈J. G i)"
and G: "⋀i. i ∈ J ⟹ G i ∈ sets (E i)"
by (auto simp: prod_algebra_def)
moreover
from space have "(Π⇩E i∈I. space (E i)) = (Π⇩E i∈I. space (F i))"
by (rule PiE_cong)
with A have "A = prod_emb I F J (Π⇩E i∈J. G i)"
by (simp add: prod_emb_def)
moreover
from sets G J have "⋀i. i ∈ J ⟹ G i ∈ sets (F i)"
by auto
ultimately show "A ∈ prod_algebra I F"
apply (simp add: prod_algebra_def image_iff)
apply (intro exI[of _ J] exI[of _ G] conjI)
apply auto
done
qed
proposition prod_algebra_cong:
assumes "I = J" and "(⋀i. i ∈ I ⟹ sets (M i) = sets (N i))"
shows "prod_algebra I M = prod_algebra J N"
by (metis assms prod_algebra_mono sets_eq_imp_space_eq subsetI subset_antisym)
lemma space_in_prod_algebra: "(Π⇩E i∈I. space (M i)) ∈ prod_algebra I M"
proof cases
assume "I = {}" then show ?thesis
by (auto simp add: prod_algebra_def image_iff prod_emb_def)
next
assume "I ≠ {}"
then obtain i where "i ∈ I" by auto
then have "(Π⇩E i∈I. space (M i)) = prod_emb I M {i} (Π⇩E i∈{i}. space (M i))"
by (auto simp: prod_emb_def)
then show ?thesis
by (simp add: ‹i ∈ I› prod_algebraI)
qed
lemma space_PiM: "space (Π⇩M i∈I. M i) = (Π⇩E i∈I. space (M i))"
using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro space_extend_measure) simp
lemma prod_emb_subset_PiM[simp]: "prod_emb I M K X ⊆ space (PiM I M)"
by (auto simp: prod_emb_def space_PiM)
lemma space_PiM_empty_iff[simp]: "space (PiM I M) = {} ⟷ (∃i∈I. space (M i) = {})"
by (auto simp: space_PiM PiE_eq_empty_iff)
lemma undefined_in_PiM_empty[simp]: "(λx. undefined) ∈ space (PiM {} M)"
by (auto simp: space_PiM)
lemma sets_PiM: "sets (Π⇩M i∈I. M i) = sigma_sets (Π⇩E i∈I. space (M i)) (prod_algebra I M)"
using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro sets_extend_measure) simp
proposition sets_PiM_single: "sets (PiM I M) =
sigma_sets (Π⇩E i∈I. space (M i)) {{f∈Π⇩E i∈I. space (M i). f i ∈ A} | i A. i ∈ I ∧ A ∈ sets (M i)}"
(is "_ = sigma_sets ?Ω ?R")
unfolding sets_PiM
proof (rule sigma_sets_eqI)
interpret R: sigma_algebra ?Ω "sigma_sets ?Ω ?R" by (rule sigma_algebra_sigma_sets) auto
fix A assume "A ∈ prod_algebra I M"
from prod_algebraE[OF this] obtain J X where X:
"A = prod_emb I M J (Pi⇩E J X)"
"finite J"
"J ≠ {} ∨ I = {}"
"J ⊆ I"
"⋀i. i ∈ J ⟹ X i ∈ sets (M i)"
by auto
show "A ∈ sigma_sets ?Ω ?R"
proof cases
assume "I = {}"
with X show ?thesis
by (metis (no_types, lifting) PiE_cong R.top empty_iff prod_emb_PiE subset_eq)
next
assume "I ≠ {}"
with X have "A = (⋂j∈J. {f∈(Π⇩E i∈I. space (M i)). f j ∈ X j})"
by (auto simp: prod_emb_def)
also have "… ∈ sigma_sets ?Ω ?R"
using X ‹I ≠ {}› by (intro R.finite_INT sigma_sets.Basic) auto
finally show "A ∈ sigma_sets ?Ω ?R" .
qed
next
fix A assume "A ∈ ?R"
then obtain i B where A: "A = {f∈Π⇩E i∈I. space (M i). f i ∈ B}" "i ∈ I" "B ∈ sets (M i)"
by auto
then have "A = prod_emb I M {i} (Π⇩E i∈{i}. B)"
by (auto simp: prod_emb_def)
also have "… ∈ sigma_sets ?Ω (prod_algebra I M)"
using A by (intro sigma_sets.Basic prod_algebraI) auto
finally show "A ∈ sigma_sets ?Ω (prod_algebra I M)" .
qed
lemma sets_PiM_eq_proj:
assumes "I ≠ {}"
shows "sets (PiM I M) = sets (SUP i∈I. vimage_algebra (Π⇩E i∈I. space (M i)) (λx. x i) (M i))"
(is "?lhs = ?rhs")
proof -
have "?lhs =
sigma_sets (Π⇩E i∈I. space (M i)) {{f ∈ Π⇩E i∈I. space (M i). f i ∈ A} |i A. i ∈ I ∧ A ∈ sets (M i)}"
by (simp add: sets_PiM_single)
also have "… = sigma_sets (Π⇩E i∈I. space (M i))
(⋃x∈I. sets (vimage_algebra (Π⇩E i∈I. space (M i)) (λxa. xa x) (M x)))"
apply (subst arg_cong [of _ _ Sup, OF image_cong, OF refl])
apply (rule sets_vimage_algebra2)
by (auto intro!: arg_cong2[where f=sigma_sets])
also have "... = sigma_sets (Π⇩E i∈I. space (M i))
(⋃ (sets ` (λi. vimage_algebra (Π⇩E i∈I. space (M i)) (λx. x i) (M i)) ` I))"
by simp
also have "... = ?rhs"
by (subst sets_Sup_eq[where X="Π⇩E i∈I. space (M i)"]) (use assms in auto)
finally show ?thesis .
qed
lemma
shows space_PiM_empty: "space (Pi⇩M {} M) = {λk. undefined}"
and sets_PiM_empty: "sets (Pi⇩M {} M) = { {}, {λk. undefined} }"
by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)
proposition sets_PiM_sigma:
assumes Ω_cover: "⋀i. i ∈ I ⟹ ∃S⊆E i. countable S ∧ Ω i = ⋃S"
assumes E: "⋀i. i ∈ I ⟹ E i ⊆ Pow (Ω i)"
assumes J: "⋀j. j ∈ J ⟹ finite j" "⋃J = I"
defines "P ≡ {{f∈(Π⇩E i∈I. Ω i). ∀i∈j. f i ∈ A i} | A j. j ∈ J ∧ A ∈ Pi j E}"
shows "sets (Π⇩M i∈I. sigma (Ω i) (E i)) = sets (sigma (Π⇩E i∈I. Ω i) P)"
proof cases
assume "I = {}"
with ‹⋃J = I› have "P = {{λ_. undefined}} ∨ P = {}"
by (auto simp: P_def)
with ‹I = {}› show ?thesis
by (auto simp add: sets_PiM_empty sigma_sets_empty_eq)
next
let ?F = "λi. {(λx. x i) -` A ∩ Pi⇩E I Ω |A. A ∈ E i}"
assume "I ≠ {}"
then have "sets (Pi⇩M I (λi. sigma (Ω i) (E i))) =
sets (SUP i∈I. vimage_algebra (Π⇩E i∈I. Ω i) (λx. x i) (sigma (Ω i) (E i)))"
by (subst sets_PiM_eq_proj) (auto simp: space_measure_of_conv)
also have "… = sets (SUP i∈I. sigma (Pi⇩E I Ω) (?F i))"
using E by (intro sets_SUP_cong arg_cong[where f=sets] vimage_algebra_sigma) auto
also have "… = sets (sigma (Pi⇩E I Ω) (⋃i∈I. ?F i))"
using ‹I ≠ {}› by (intro arg_cong[where f=sets] SUP_sigma_sigma) auto
also have "… = sets (sigma (Pi⇩E I Ω) P)"
proof (intro arg_cong[where f=sets] sigma_eqI sigma_sets_eqI)
show "(⋃i∈I. ?F i) ⊆ Pow (Pi⇩E I Ω)" "P ⊆ Pow (Pi⇩E I Ω)"
by (auto simp: P_def)
next
interpret P: sigma_algebra "Π⇩E i∈I. Ω i" "sigma_sets (Π⇩E i∈I. Ω i) P"
by (auto intro!: sigma_algebra_sigma_sets simp: P_def)
fix Z assume "Z ∈ (⋃i∈I. ?F i)"
then obtain i A where i: "i ∈ I" "A ∈ E i" and Z_def: "Z = (λx. x i) -` A ∩ Pi⇩E I Ω"
by auto
from ‹i ∈ I› J obtain j where j: "i ∈ j" "j ∈ J" "j ⊆ I" "finite j"
by auto
obtain S where S: "⋀i. i ∈ j ⟹ S i ⊆ E i" "⋀i. i ∈ j ⟹ countable (S i)"
"⋀i. i ∈ j ⟹ Ω i = ⋃(S i)"
by (metis subset_eq Ω_cover ‹j ⊆ I›)
define A' where "A' n = n(i := A)" for n
then have A'_i: "⋀n. A' n i = A"
by simp
{ fix n assume "n ∈ Pi⇩E (j - {i}) S"
then have "A' n ∈ Pi j E"
unfolding PiE_def Pi_def using S(1) by (auto simp: A'_def ‹A ∈ E i› )
with ‹j ∈ J› have "{f ∈ Pi⇩E I Ω. ∀i∈j. f i ∈ A' n i} ∈ P"
by (auto simp: P_def) }
note A'_in_P = this
{ fix x assume "x i ∈ A" "x ∈ Pi⇩E I Ω"
with S(3) ‹j ⊆ I› have "∀i∈j. ∃s∈S i. x i ∈ s"
by (auto simp: PiE_def Pi_def)
then obtain s where s: "⋀i. i ∈ j ⟹ s i ∈ S i" "⋀i. i ∈ j ⟹ x i ∈ s i"
by metis
with ‹x i ∈ A› have "∃n∈Pi⇩E (j-{i}) S. ∀i∈j. x i ∈ A' n i"
by (intro bexI[of _ "restrict (s(i := A)) (j-{i})"]) (auto simp: A'_def split: if_splits) }
then have "Z = (⋃n∈Pi⇩E (j-{i}) S. {f∈(Π⇩E i∈I. Ω i). ∀i∈j. f i ∈ A' n i})"
unfolding Z_def
by (auto simp add: set_eq_iff ball_conj_distrib ‹i∈j› A'_i dest: bspec[OF _ ‹i∈j›]
cong: conj_cong)
also have "… ∈ sigma_sets (Π⇩E i∈I. Ω i) P"
using ‹finite j› S(2)
by (intro P.countable_UN' countable_PiE) (simp_all add: image_subset_iff A'_in_P)
finally show "Z ∈ sigma_sets (Π⇩E i∈I. Ω i) P" .
next
interpret F: sigma_algebra "Π⇩E i∈I. Ω i" "sigma_sets (Π⇩E i∈I. Ω i) (⋃i∈I. ?F i)"
by (auto intro!: sigma_algebra_sigma_sets)
fix b assume "b ∈ P"
then obtain A j where b: "b = {f∈(Π⇩E i∈I. Ω i). ∀i∈j. f i ∈ A i}" "j ∈ J" "A ∈ Pi j E"
by (auto simp: P_def)
show "b ∈ sigma_sets (Pi⇩E I Ω) (⋃i∈I. ?F i)"
proof cases
assume "j = {}"
with b have "b = (Π⇩E i∈I. Ω i)"
by auto
then show ?thesis
by blast
next
assume "j ≠ {}"
with J b(2,3) have eq: "b = (⋂i∈j. ((λx. x i) -` A i ∩ Pi⇩E I Ω))"
unfolding b(1)
by (auto simp: PiE_def Pi_def)
show ?thesis
unfolding eq using ‹A ∈ Pi j E› ‹j ∈ J› J(2)
by (intro F.finite_INT J ‹j ∈ J› ‹j ≠ {}› sigma_sets.Basic) blast
qed
qed
finally show "?thesis" .
qed
lemma sets_PiM_in_sets:
assumes space: "space N = (Π⇩E i∈I. space (M i))"
assumes sets: "⋀i A. i ∈ I ⟹ A ∈ sets (M i) ⟹ {x∈space N. x i ∈ A} ∈ sets N"
shows "sets (Π⇩M i ∈ I. M i) ⊆ sets N"
unfolding sets_PiM_single space[symmetric]
by (intro sets.sigma_sets_subset subsetI) (auto intro: sets)
lemma sets_PiM_cong[measurable_cong]:
assumes "I = J" "⋀i. i ∈ J ⟹ sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)"
using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong)
lemma sets_PiM_I:
assumes "finite J" "J ⊆ I" "∀i∈J. E i ∈ sets (M i)"
shows "prod_emb I M J (Π⇩E j∈J. E j) ∈ sets (Π⇩M i∈I. M i)"
proof cases
assume "J = {}"
then have "prod_emb I M J (Π⇩E j∈J. E j) = (Π⇩E j∈I. space (M j))"
by (auto simp: prod_emb_def)
then show ?thesis
by (auto simp add: sets_PiM intro!: sigma_sets_top)
next
assume "J ≠ {}" with assms show ?thesis
by (force simp add: sets_PiM prod_algebra_def)
qed
proposition measurable_PiM:
assumes space: "f ∈ space N → (Π⇩E i∈I. space (M i))"
assumes sets: "⋀X J. J ≠ {} ∨ I = {} ⟹ finite J ⟹ J ⊆ I ⟹ (⋀i. i ∈ J ⟹ X i ∈ sets (M i)) ⟹
f -` prod_emb I M J (Pi⇩E J X) ∩ space N ∈ sets N"
shows "f ∈ measurable N (PiM I M)"
using sets_PiM prod_algebra_sets_into_space space
proof (rule measurable_sigma_sets)
fix A assume "A ∈ prod_algebra I M"
from prod_algebraE[OF this] obtain J X where
"A = prod_emb I M J (Pi⇩E J X)"
"finite J"
"J ≠ {} ∨ I = {}"
"J ⊆ I"
"⋀i. i ∈ J ⟹ X i ∈ sets (M i)"
by auto
with sets[of J X] show "f -` A ∩ space N ∈ sets N" by auto
qed
lemma measurable_PiM_Collect:
assumes space: "f ∈ space N → (Π⇩E i∈I. space (M i))"
assumes sets: "⋀X J. J ≠ {} ∨ I = {} ⟹ finite J ⟹ J ⊆ I ⟹ (⋀i. i ∈ J ⟹ X i ∈ sets (M i)) ⟹
{ω∈space N. ∀i∈J. f ω i ∈ X i} ∈ sets N"
shows "f ∈ measurable N (PiM I M)"
using sets_PiM prod_algebra_sets_into_space space
proof (rule measurable_sigma_sets)
fix A assume "A ∈ prod_algebra I M"
from prod_algebraE[OF this] obtain J X
where X:
"A = prod_emb I M J (Pi⇩E J X)"
"finite J"
"J ≠ {} ∨ I = {}"
"J ⊆ I"
"⋀i. i ∈ J ⟹ X i ∈ sets (M i)"
by auto
then have "f -` A ∩ space N = {ω ∈ space N. ∀i∈J. f ω i ∈ X i}"
using space by (auto simp: prod_emb_def del: PiE_I)
also have "… ∈ sets N" using X(3,2,4,5) by (rule sets)
finally show "f -` A ∩ space N ∈ sets N" .
qed
lemma measurable_PiM_single:
assumes space: "f ∈ space N → (Π⇩E i∈I. space (M i))"
assumes sets: "⋀A i. i ∈ I ⟹ A ∈ sets (M i) ⟹ {ω ∈ space N. f ω i ∈ A} ∈ sets N"
shows "f ∈ measurable N (PiM I M)"
using sets_PiM_single
proof (rule measurable_sigma_sets)
fix A assume "A ∈ {{f ∈ Π⇩E i∈I. space (M i). f i ∈ A} |i A. i ∈ I ∧ A ∈ sets (M i)}"
then obtain B i where "A = {f ∈ Π⇩E i∈I. space (M i). f i ∈ B}" and B: "i ∈ I" "B ∈ sets (M i)"
by auto
with space have "f -` A ∩ space N = {ω ∈ space N. f ω i ∈ B}" by auto
also have "… ∈ sets N" using B by (rule sets)
finally show "f -` A ∩ space N ∈ sets N" .
qed (auto simp: space)
lemma measurable_PiM_single':
assumes f: "⋀i. i ∈ I ⟹ f i ∈ measurable N (M i)"
and "(λω i. f i ω) ∈ space N → (Π⇩E i∈I. space (M i))"
shows "(λω i. f i ω) ∈ measurable N (Pi⇩M I M)"
proof (rule measurable_PiM_single)
fix A i assume A: "i ∈ I" "A ∈ sets (M i)"
then have "{ω ∈ space N. f i ω ∈ A} = f i -` A ∩ space N"
by auto
then show "{ω ∈ space N. f i ω ∈ A} ∈ sets N"
using A f by (auto intro!: measurable_sets)
qed fact
lemma sets_PiM_I_finite[measurable]:
assumes "finite I" and sets: "(⋀i. i ∈ I ⟹ E i ∈ sets (M i))"
shows "(Π⇩E j∈I. E j) ∈ sets (Π⇩M i∈I. M i)"
using sets_PiM_I[of I I E M] sets.sets_into_space[OF sets] ‹finite I› sets by auto
lemma measurable_component_singleton[measurable (raw)]:
assumes "i ∈ I" shows "(λx. x i) ∈ measurable (Pi⇩M I M) (M i)"
proof (unfold measurable_def, intro CollectI conjI ballI)
fix A assume "A ∈ sets (M i)"
then have "(λx. x i) -` A ∩ space (Pi⇩M I M) = prod_emb I M {i} (Π⇩E j∈{i}. A)"
using sets.sets_into_space ‹i ∈ I›
by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: if_split_asm)
then show "(λx. x i) -` A ∩ space (Pi⇩M I M) ∈ sets (Pi⇩M I M)"
using ‹A ∈ sets (M i)› ‹i ∈ I› by (auto intro!: sets_PiM_I)
qed (use ‹i ∈ I› in ‹auto simp: space_PiM›)
lemma measurable_component_singleton'[measurable_dest]:
assumes f: "f ∈ measurable N (Pi⇩M I M)"
assumes g: "g ∈ measurable L N"
assumes i: "i ∈ I"
shows "(λx. (f (g x)) i) ∈ measurable L (M i)"
using measurable_compose[OF measurable_compose[OF g f] measurable_component_singleton, OF i] .
lemma measurable_PiM_component_rev:
"i ∈ I ⟹ f ∈ measurable (M i) N ⟹ (λx. f (x i)) ∈ measurable (PiM I M) N"
by simp
lemma measurable_case_nat[measurable (raw)]:
assumes [measurable (raw)]: "i = 0 ⟹ f ∈ measurable M N"
"⋀j. i = Suc j ⟹ (λx. g x j) ∈ measurable M N"
shows "(λx. case_nat (f x) (g x) i) ∈ measurable M N"
by (cases i) simp_all
lemma measurable_case_nat'[measurable (raw)]:
assumes fg[measurable]: "f ∈ measurable N M" "g ∈ measurable N (Π⇩M i∈UNIV. M)"
shows "(λx. case_nat (f x) (g x)) ∈ measurable N (Π⇩M i∈UNIV. M)"
using fg[THEN measurable_space]
by (auto intro!: measurable_PiM_single' simp add: space_PiM PiE_iff split: nat.split)
lemma measurable_add_dim[measurable]:
"(λ(f, y). f(i := y)) ∈ measurable (Pi⇩M I M ⨂⇩M M i) (Pi⇩M (insert i I) M)"
(is "?f ∈ measurable ?P ?I")
proof (rule measurable_PiM_single)
fix j A assume j: "j ∈ insert i I" and A: "A ∈ sets (M j)"
have "{ω ∈ space ?P. (λ(f, x). fun_upd f i x) ω j ∈ A} =
(if j = i then space (Pi⇩M I M) × A else ((λx. x j) ∘ fst) -` A ∩ space ?P)"
using sets.sets_into_space[OF A] by (auto simp add: space_pair_measure space_PiM)
also have "… ∈ sets ?P"
using A j
by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
finally show "{ω ∈ space ?P. case_prod (λf. fun_upd f i) ω j ∈ A} ∈ sets ?P" .
qed (auto simp: space_pair_measure space_PiM PiE_def)
proposition measurable_fun_upd:
assumes I: "I = J ∪ {i}"
assumes f[measurable]: "f ∈ measurable N (PiM J M)"
assumes h[measurable]: "h ∈ measurable N (M i)"
shows "(λx. (f x) (i := h x)) ∈ measurable N (PiM I M)"
proof (intro measurable_PiM_single')
fix j assume "j ∈ I" then show "(λω. ((f ω)(i := h ω)) j) ∈ measurable N (M j)"
unfolding I by (cases "j = i") auto
next
show "(λx. (f x)(i := h x)) ∈ space N → (Π⇩E i∈I. space (M i))"
using I f[THEN measurable_space] h[THEN measurable_space]
by (auto simp: space_PiM PiE_iff extensional_def)
qed
lemma measurable_component_update:
"x ∈ space (Pi⇩M I M) ⟹ i ∉ I ⟹ (λv. x(i := v)) ∈ measurable (M i) (Pi⇩M (insert i I) M)"
by simp
lemma measurable_merge[measurable]:
"merge I J ∈ measurable (Pi⇩M I M ⨂⇩M Pi⇩M J M) (Pi⇩M (I ∪ J) M)"
(is "?f ∈ measurable ?P ?U")
proof (rule measurable_PiM_single)
fix i A assume A: "A ∈ sets (M i)" "i ∈ I ∪ J"
then have "{ω ∈ space ?P. merge I J ω i ∈ A} =
(if i ∈ I then ((λx. x i) ∘ fst) -` A ∩ space ?P else ((λx. x i) ∘ snd) -` A ∩ space ?P)"
by (auto simp: merge_def)
also have "… ∈ sets ?P"
using A
by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
finally show "{ω ∈ space ?P. merge I J ω i ∈ A} ∈ sets ?P" .
qed (auto simp: space_pair_measure space_PiM PiE_iff merge_def extensional_def)
lemma measurable_restrict[measurable (raw)]:
assumes X: "⋀i. i ∈ I ⟹ X i ∈ measurable N (M i)"
shows "(λx. λi∈I. X i x) ∈ measurable N (Pi⇩M I M)"
proof (rule measurable_PiM_single)
fix A i assume A: "i ∈ I" "A ∈ sets (M i)"
then have "{ω ∈ space N. (λi∈I. X i ω) i ∈ A} = X i -` A ∩ space N"
by auto
then show "{ω ∈ space N. (λi∈I. X i ω) i ∈ A} ∈ sets N"
using A X by (auto intro!: measurable_sets)
next
show "(λx. λi∈I. X i x) ∈ space N → (Π⇩E i∈I. space (M i))"
using X by (auto simp add: PiE_def dest: measurable_space)
qed
lemma measurable_abs_UNIV:
"(⋀n. (λω. f n ω) ∈ measurable M (N n)) ⟹ (λω n. f n ω) ∈ measurable M (PiM UNIV N)"
by (intro measurable_PiM_single) (auto dest: measurable_space)
lemma measurable_restrict_subset: "J ⊆ L ⟹ (λf. restrict f J) ∈ measurable (Pi⇩M L M) (Pi⇩M J M)"
by (intro measurable_restrict measurable_component_singleton) auto
lemma measurable_restrict_subset':
assumes "J ⊆ L" "⋀x. x ∈ J ⟹ sets (M x) = sets (N x)"
shows "(λf. restrict f J) ∈ measurable (Pi⇩M L M) (Pi⇩M J N)"
by (metis (no_types) assms measurable_cong_sets measurable_restrict_subset sets_PiM_cong)
lemma measurable_prod_emb[intro, simp]:
"J ⊆ L ⟹ X ∈ sets (Pi⇩M J M) ⟹ prod_emb L M J X ∈ sets (Pi⇩M L M)"
unfolding prod_emb_def space_PiM[symmetric]
by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton)
lemma merge_in_prod_emb:
assumes "y ∈ space (PiM I M)" "x ∈ X" and X: "X ∈ sets (Pi⇩M J M)" and "J ⊆ I"
shows "merge J I (x, y) ∈ prod_emb I M J X"
using assms sets.sets_into_space[OF X]
by (simp add: merge_def prod_emb_def subset_eq space_PiM PiE_def extensional_restrict Pi_iff
cong: if_cong restrict_cong)
(simp add: extensional_def)
lemma prod_emb_eq_emptyD:
assumes J: "J ⊆ I" and ne: "space (PiM I M) ≠ {}" and X: "X ∈ sets (Pi⇩M J M)"
and *: "prod_emb I M J X = {}"
shows "X = {}"
proof safe
fix x assume "x ∈ X"
obtain ω where "ω ∈ space (PiM I M)"
using ne by blast
from merge_in_prod_emb[OF this ‹x∈X› X J] * show "x ∈ {}" by auto
qed
lemma sets_in_Pi_aux:
"finite I ⟹ (⋀j. j ∈ I ⟹ {x∈space (M j). x ∈ F j} ∈ sets (M j)) ⟹
{x∈space (PiM I M). x ∈ Pi I F} ∈ sets (PiM I M)"
by (simp add: subset_eq Pi_iff)
lemma sets_in_Pi[measurable (raw)]:
"finite I ⟹ f ∈ measurable N (PiM I M) ⟹
(⋀j. j ∈ I ⟹ {x∈space (M j). x ∈ F j} ∈ sets (M j)) ⟹
Measurable.pred N (λx. f x ∈ Pi I F)"
unfolding pred_def
by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto
lemma sets_in_extensional_aux:
"{x∈space (PiM I M). x ∈ extensional I} ∈ sets (PiM I M)"
by (smt (verit) PiE_iff mem_Collect_eq sets.top space_PiM subsetI subset_antisym)
lemma sets_in_extensional[measurable (raw)]:
"f ∈ measurable N (PiM I M) ⟹ Measurable.pred N (λx. f x ∈ extensional I)"
unfolding pred_def
by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto
lemma sets_PiM_I_countable:
assumes I: "countable I" and E: "⋀i. i ∈ I ⟹ E i ∈ sets (M i)" shows "Pi⇩E I E ∈ sets (Pi⇩M I M)"
proof cases
assume "I ≠ {}"
then have "Pi⇩E I E = (⋂i∈I. prod_emb I M {i} (Pi⇩E {i} E))"
using E[THEN sets.sets_into_space] by (auto simp: PiE_iff prod_emb_def fun_eq_iff)
also have "… ∈ sets (PiM I M)"
using I ‹I ≠ {}› by (simp add: E sets.countable_INT' sets_PiM_I subset_eq)
finally show ?thesis .
qed (simp add: sets_PiM_empty)
lemma sets_PiM_D_countable:
assumes A: "A ∈ PiM I M"
shows "∃J⊆I. ∃X∈PiM J M. countable J ∧ A = prod_emb I M J X"
using A[unfolded sets_PiM_single]
proof induction
case (Basic A)
then obtain i X where *: "i ∈ I" "X ∈ sets (M i)" and "A = {f ∈ Π⇩E i∈I. space (M i). f i ∈ X}"
by auto
then have A: "A = prod_emb I M {i} (Π⇩E _∈{i}. X)"
by (auto simp: prod_emb_def)
then show ?case
by (intro exI[of _ "{i}"] conjI bexI[of _ "Π⇩E _∈{i}. X"])
(auto intro: countable_finite * sets_PiM_I_finite)
next
case Empty then show ?case
by (intro exI[of _ "{}"] conjI bexI[of _ "{}"]) auto
next
case (Compl A)
then obtain J X where "J ⊆ I" "X ∈ sets (Pi⇩M J M)" "countable J" "A = prod_emb I M J X"
by auto
then show ?case
by (intro exI[of _ J] bexI[of _ "space (PiM J M) - X"] conjI)
(auto simp add: space_PiM prod_emb_PiE intro!: sets_PiM_I_countable)
next
case (Union K)
obtain J X where J: "⋀i. J i ⊆ I" "⋀i. countable (J i)" and X: "⋀i. X i ∈ sets (Pi⇩M (J i) M)"
and K: "⋀i. K i = prod_emb I M (J i) (X i)"
by (metis Union.IH)
show ?case
proof (intro exI bexI conjI)
show "(⋃i. J i) ⊆ I" "countable (⋃i. J i)"
using J by auto
with J show "⋃(K ` UNIV) = prod_emb I M (⋃i. J i) (⋃i. prod_emb (⋃i. J i) M (J i) (X i))"
by (simp add: K[abs_def] SUP_upper)
qed(auto intro: X)
qed
proposition measure_eqI_PiM_finite:
assumes [simp]: "finite I" "sets P = PiM I M" "sets Q = PiM I M"
assumes eq: "⋀A. (⋀i. i ∈ I ⟹ A i ∈ sets (M i)) ⟹ P (Pi⇩E I A) = Q (Pi⇩E I A)"
assumes A: "range A ⊆ prod_algebra I M" "(⋃i. A i) = space (PiM I M)" "⋀i::nat. P (A i) ≠ ∞"
shows "P = Q"
proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space])
show "range A ⊆ prod_algebra I M" "(⋃i. A i) = (Π⇩E i∈I. space (M i))" "⋀i. P (A i) ≠ ∞"
unfolding space_PiM[symmetric] by fact+
fix X assume "X ∈ prod_algebra I M"
then obtain J E where X: "X = prod_emb I M J (Π⇩E j∈J. E j)"
and J: "finite J" "J ⊆ I" "⋀j. j ∈ J ⟹ E j ∈ sets (M j)"
by (force elim!: prod_algebraE)
then show "emeasure P X = emeasure Q X"
unfolding X by (subst (1 2) prod_emb_Pi) (auto simp: eq)
qed (simp_all add: sets_PiM)
proposition measure_eqI_PiM_infinite:
assumes [simp]: "sets P = PiM I M" "sets Q = PiM I M"
assumes eq: "⋀A J. finite J ⟹ J ⊆ I ⟹ (⋀i. i ∈ J ⟹ A i ∈ sets (M i)) ⟹
P (prod_emb I M J (Pi⇩E J A)) = Q (prod_emb I M J (Pi⇩E J A))"
assumes A: "finite_measure P"
shows "P = Q"
proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space])
interpret finite_measure P by fact
define i where "i = (SOME i. i ∈ I)"
have i: "I ≠ {} ⟹ i ∈ I"
unfolding i_def by (rule someI_ex) auto
define A where "A n =
(if I = {} then prod_emb I M {} (Π⇩E i∈{}. {}) else prod_emb I M {i} (Π⇩E i∈{i}. space (M i)))"
for n :: nat
then show "range A ⊆ prod_algebra I M"
using prod_algebraI[of "{}" I "λi. space (M i)" M] by (auto intro!: prod_algebraI i)
have "⋀i. A i = space (PiM I M)"
by (auto simp: prod_emb_def space_PiM PiE_iff A_def i ex_in_conv[symmetric] exI)
then show "(⋃i. A i) = (Π⇩E i∈I. space (M i))" "⋀i. emeasure P (A i) ≠ ∞"
by (auto simp: space_PiM)
next
fix X assume X: "X ∈ prod_algebra I M"
then obtain J E where X: "X = prod_emb I M J (Π⇩E j∈J. E j)"
and J: "finite J" "J ⊆ I" "⋀j. j ∈ J ⟹ E j ∈ sets (M j)"
by (force elim!: prod_algebraE)
then show "emeasure P X = emeasure Q X"
by (auto intro!: eq)
qed (auto simp: sets_PiM)
locale product_sigma_finite =
fixes M :: "'i ⇒ 'a measure"
assumes sigma_finite_measures: "⋀i. sigma_finite_measure (M i)"
sublocale product_sigma_finite ⊆ M?: sigma_finite_measure "M i" for i
by (rule sigma_finite_measures)
locale finite_product_sigma_finite = product_sigma_finite M for M :: "'i ⇒ 'a measure" +
fixes I :: "'i set"
assumes finite_index: "finite I"
proposition (in finite_product_sigma_finite) sigma_finite_pairs:
"∃F::'i ⇒ nat ⇒ 'a set.
(∀i∈I. range (F i) ⊆ sets (M i)) ∧
(∀k. ∀i∈I. emeasure (M i) (F i k) ≠ ∞) ∧ incseq (λk. Π⇩E i∈I. F i k) ∧
(⋃k. Π⇩E i∈I. F i k) = space (PiM I M)"
proof -
have "∀i::'i. ∃F::nat ⇒ 'a set. range F ⊆ sets (M i) ∧ incseq F ∧ (⋃i. F i) = space (M i) ∧ (∀k. emeasure (M i) (F k) ≠ ∞)"
using M.sigma_finite_incseq by metis
then obtain F :: "'i ⇒ nat ⇒ 'a set"
where "∀x. range (F x) ⊆ sets (M x) ∧ incseq (F x) ∧ ⋃ (range (F x)) = space (M x) ∧ (∀k. emeasure (M x) (F x k) ≠ ∞)"
by metis
then have F: "⋀i. range (F i) ⊆ sets (M i)" "⋀i. incseq (F i)" "⋀i. (⋃j. F i j) = space (M i)" "⋀i k. emeasure (M i) (F i k) ≠ ∞"
by auto
let ?F = "λk. Π⇩E i∈I. F i k"
note space_PiM[simp]
show ?thesis
proof (intro exI[of _ F] conjI allI incseq_SucI set_eqI iffI ballI)
fix i show "range (F i) ⊆ sets (M i)" by fact
next
fix i k show "emeasure (M i) (F i k) ≠ ∞" by fact
next
fix x assume "x ∈ (⋃i. ?F i)" with F(1) show "x ∈ space (PiM I M)"
by (auto simp: PiE_def dest!: sets.sets_into_space)
next
fix f assume "f ∈ space (PiM I M)"
with Pi_UN[OF finite_index, of "λk i. F i k"] F
show "f ∈ (⋃i. ?F i)" by (auto simp: incseq_def PiE_def)
next
fix i show "?F i ⊆ ?F (Suc i)"
using ‹⋀i. incseq (F i)›[THEN incseq_SucD] by auto
qed
qed
lemma emeasure_PiM_empty[simp]: "emeasure (PiM {} M) {λ_. undefined} = 1"
proof -
let ?μ = "λA. if A = {} then 0 else (1::ennreal)"
have "emeasure (Pi⇩M {} M) (prod_emb {} M {} (Π⇩E i∈{}. {})) = 1"
proof (subst emeasure_extend_measure_Pair[OF PiM_def])
show "positive (PiM {} M) ?μ"
by (auto simp: positive_def)
show "countably_additive (PiM {} M) ?μ"
by (rule sets.countably_additiveI_finite)
(auto simp: additive_def positive_def sets_PiM_empty space_PiM_empty intro!: )
qed (auto simp: prod_emb_def)
also have "(prod_emb {} M {} (Π⇩E i∈{}. {})) = {λ_. undefined}"
by (auto simp: prod_emb_def)
finally show ?thesis
by simp
qed
lemma PiM_empty: "PiM {} M = count_space {λ_. undefined}"
by (rule measure_eqI) (auto simp add: sets_PiM_empty)
lemma (in product_sigma_finite) emeasure_PiM:
"finite I ⟹ (⋀i. i∈I ⟹ A i ∈ sets (M i)) ⟹ emeasure (PiM I M) (Pi⇩E I A) = (∏i∈I. emeasure (M i) (A i))"
proof (induct I arbitrary: A rule: finite_induct)
case (insert i I)
interpret finite_product_sigma_finite M I by standard fact
have "finite (insert i I)" using ‹finite I› by auto
interpret I': finite_product_sigma_finite M "insert i I" by standard fact
let ?h = "(λ(f, y). f(i := y))"
let ?P = "distr (Pi⇩M I M ⨂⇩M M i) (Pi⇩M (insert i I) M) ?h"
let ?μ = "emeasure ?P"
let ?I = "{j ∈ insert i I. emeasure (M j) (space (M j)) ≠ 1}"
let ?f = "λJ E j. if j ∈ J then emeasure (M j) (E j) else emeasure (M j) (space (M j))"
have "emeasure (Pi⇩M (insert i I) M) (prod_emb (insert i I) M (insert i I) (Pi⇩E (insert i I) A)) =
(∏i∈insert i I. emeasure (M i) (A i))"
proof (subst emeasure_extend_measure_Pair[OF PiM_def])
fix J E assume "(J ≠ {} ∨ insert i I = {}) ∧ finite J ∧ J ⊆ insert i I ∧ E ∈ (Π j∈J. sets (M j))"
then have J: "J ≠ {}" "finite J" "J ⊆ insert i I" and E: "∀j∈J. E j ∈ sets (M j)" by auto
let ?p = "prod_emb (insert i I) M J (Pi⇩E J E)"
let ?p' = "prod_emb I M (J - {i}) (Π⇩E j∈J-{i}. E j)"
have "?μ ?p =
emeasure (Pi⇩M I M ⨂⇩M (M i)) (?h -` ?p ∩ space (Pi⇩M I M ⨂⇩M M i))"
by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
also have "?h -` ?p ∩ space (Pi⇩M I M ⨂⇩M M i) = ?p' × (if i ∈ J then E i else space (M i))"
using J E[rule_format, THEN sets.sets_into_space]
by (force simp: space_pair_measure space_PiM prod_emb_iff PiE_def Pi_iff split: if_split_asm)
also have "emeasure (Pi⇩M I M ⨂⇩M (M i)) (?p' × (if i ∈ J then E i else space (M i))) =
emeasure (Pi⇩M I M) ?p' * emeasure (M i) (if i ∈ J then (E i) else space (M i))"
using J E by (intro M.emeasure_pair_measure_Times sets_PiM_I) auto
also have "?p' = (Π⇩E j∈I. if j ∈ J-{i} then E j else space (M j))"
using J E[rule_format, THEN sets.sets_into_space]
by (auto simp: prod_emb_iff PiE_def Pi_iff split: if_split_asm) blast+
also have "emeasure (Pi⇩M I M) (Π⇩E j∈I. if j ∈ J-{i} then E j else space (M j)) =
(∏ j∈I. if j ∈ J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
using E by (subst insert) (auto intro!: prod.cong)
also have "(∏j∈I. if j ∈ J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) *
emeasure (M i) (if i ∈ J then E i else space (M i)) = (∏j∈insert i I. ?f J E j)"
using insert by (auto simp: mult.commute intro!: arg_cong2[where f="(*)"] prod.cong)
also have "… = (∏j∈J ∪ ?I. ?f J E j)"
using insert(1,2) J E by (intro prod.mono_neutral_right) auto
finally show "?μ ?p = …" .
show "prod_emb (insert i I) M J (Pi⇩E J E) ∈ Pow (Π⇩E i∈insert i I. space (M i))"
using J E[rule_format, THEN sets.sets_into_space] by (auto simp: prod_emb_iff PiE_def)
next
show "positive (sets (Pi⇩M (insert i I) M)) ?μ" "countably_additive (sets (Pi⇩M (insert i I) M)) ?μ"
using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all
next
show "(insert i I ≠ {} ∨ insert i I = {}) ∧ finite (insert i I) ∧
insert i I ⊆ insert i I ∧ A ∈ (Π j∈insert i I. sets (M j))"
using insert by auto
qed (auto intro!: prod.cong)
with insert show ?case
by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space)
qed simp
lemma (in product_sigma_finite) PiM_eqI:
assumes I[simp]: "finite I" and P: "sets P = PiM I M"
assumes eq: "⋀A. (⋀i. i ∈ I ⟹ A i ∈ sets (M i)) ⟹ P (Pi⇩E I A) = (∏i∈I. emeasure (M i) (A i))"
shows "P = PiM I M"
proof -
interpret finite_product_sigma_finite M I
by standard fact
from sigma_finite_pairs obtain C where C:
"∀i∈I. range (C i) ⊆ sets (M i)" "∀k. ∀i∈I. emeasure (M i) (C i k) ≠ ∞"
"incseq (λk. Π⇩E i∈I. C i k)" "(⋃k. Π⇩E i∈I. C i k) = space (Pi⇩M I M)"
by auto
show ?thesis
proof (rule measure_eqI_PiM_finite[OF I refl P, symmetric])
show "(⋀i. i ∈ I ⟹ A i ∈ sets (M i)) ⟹ (Pi⇩M I M) (Pi⇩E I A) = P (Pi⇩E I A)" for A
by (simp add: eq emeasure_PiM)
define A where "A n = (Π⇩E i∈I. C i n)" for n
with C show "range A ⊆ prod_algebra I M" "⋀i. emeasure (Pi⇩M I M) (A i) ≠ ∞" "(⋃i. A i) = space (PiM I M)"
by (auto intro!: prod_algebraI_finite simp: emeasure_PiM subset_eq ennreal_prod_eq_top)
qed
qed
lemma (in product_sigma_finite) sigma_finite:
assumes "finite I"
shows "sigma_finite_measure (PiM I M)"
proof
interpret finite_product_sigma_finite M I by standard fact
obtain F where F: "⋀j. countable (F j)" "⋀j f. f ∈ F j ⟹ f ∈ sets (M j)"
"⋀j f. f ∈ F j ⟹ emeasure (M j) f ≠ ∞" and
in_space: "⋀j. space (M j) = ⋃(F j)"
using sigma_finite_countable by (metis subset_eq)
moreover have "(⋃(Pi⇩E I ` Pi⇩E I F)) = space (Pi⇩M I M)"
using in_space by (auto simp: space_PiM PiE_iff intro!: PiE_choice[THEN iffD1])
ultimately show "∃A. countable A ∧ A ⊆ sets (Pi⇩M I M) ∧ ⋃A = space (Pi⇩M I M) ∧ (∀a∈A. emeasure (Pi⇩M I M) a ≠ ∞)"
by (intro exI[of _ "Pi⇩E I ` Pi⇩E I F"])
(auto intro!: countable_PiE sets_PiM_I_finite
simp: PiE_iff emeasure_PiM finite_index ennreal_prod_eq_top)
qed
sublocale finite_product_sigma_finite ⊆ sigma_finite_measure "Pi⇩M I M"
using sigma_finite[OF finite_index] .
lemma (in finite_product_sigma_finite) measure_times:
"(⋀i. i ∈ I ⟹ A i ∈ sets (M i)) ⟹ emeasure (Pi⇩M I M) (Pi⇩E I A) = (∏i∈I. emeasure (M i) (A i))"
using emeasure_PiM[OF finite_index] by auto
lemma (in product_sigma_finite) nn_integral_empty:
"0 ≤ f (λk. undefined) ⟹ integral⇧N (Pi⇩M {} M) f = f (λk. undefined)"
by (simp add: PiM_empty nn_integral_count_space_finite max.absorb2)
lemma (in product_sigma_finite) distr_merge:
assumes IJ[simp]: "I ∩ J = {}" and fin: "finite I" "finite J"
shows "distr (Pi⇩M I M ⨂⇩M Pi⇩M J M) (Pi⇩M (I ∪ J) M) (merge I J) = Pi⇩M (I ∪ J) M"
(is "?D = ?P")
proof (rule PiM_eqI)
interpret I: finite_product_sigma_finite M I by standard fact
interpret J: finite_product_sigma_finite M J by standard fact
fix A assume A: "⋀i. i ∈ I ∪ J ⟹ A i ∈ sets (M i)"
have *: "(merge I J -` Pi⇩E (I ∪ J) A ∩ space (Pi⇩M I M ⨂⇩M Pi⇩M J M)) = Pi⇩E I A × Pi⇩E J A"
using A[THEN sets.sets_into_space] by (auto simp: space_PiM space_pair_measure)
from A fin show "emeasure (distr (Pi⇩M I M ⨂⇩M Pi⇩M J M) (Pi⇩M (I ∪ J) M) (merge I J)) (Pi⇩E (I ∪ J) A) =
(∏i∈I ∪ J. emeasure (M i) (A i))"
by (subst emeasure_distr)
(auto simp: * J.emeasure_pair_measure_Times I.measure_times J.measure_times prod.union_disjoint)
qed (use fin in simp_all)
proposition (in product_sigma_finite) product_nn_integral_fold:
assumes IJ: "I ∩ J = {}" "finite I" "finite J"
and f[measurable]: "f ∈ borel_measurable (Pi⇩M (I ∪ J) M)"
shows "integral⇧N (Pi⇩M (I ∪ J) M) f = (∫⇧+ x. (∫⇧+ y. f (merge I J (x, y)) ∂(Pi⇩M J M)) ∂(Pi⇩M I M))"
(is "?lhs = ?rhs")
proof -
interpret I: finite_product_sigma_finite M I by standard fact
interpret J: finite_product_sigma_finite M J by standard fact
interpret P: pair_sigma_finite "Pi⇩M I M" "Pi⇩M J M" by standard
have P_borel: "(λx. f (merge I J x)) ∈ borel_measurable (Pi⇩M I M ⨂⇩M Pi⇩M J M)"
using measurable_comp[OF measurable_merge f] by (simp add: comp_def)
have "?lhs = integral⇧N (distr (Pi⇩M I M ⨂⇩M Pi⇩M J M) (Pi⇩M (I ∪ J) M) (merge I J)) f"
by (simp add: I.finite_index J.finite_index assms(1) distr_merge)
also have "... = ∫⇧+ x. f (merge I J x) ∂(Pi⇩M I M ⨂⇩M Pi⇩M J M)"
by (simp add: nn_integral_distr)
also have "... = ?rhs"
using P.Fubini P.nn_integral_snd by force
finally show ?thesis .
qed
lemma (in product_sigma_finite) distr_singleton:
"distr (Pi⇩M {i} M) (M i) (λx. x i) = M i" (is "?D = _")
proof (intro measure_eqI[symmetric])
interpret I: finite_product_sigma_finite M "{i}" by standard simp
fix A assume A: "A ∈ sets (M i)"
then have "(λx. x i) -` A ∩ space (Pi⇩M {i} M) = (Π⇩E i∈{i}. A)"
using sets.sets_into_space by (auto simp: space_PiM)
then show "emeasure (M i) A = emeasure ?D A"
using A I.measure_times[of "λ_. A"]
by (simp add: emeasure_distr measurable_component_singleton)
qed simp
lemma (in product_sigma_finite) product_nn_integral_singleton:
assumes f: "f ∈ borel_measurable (M i)"
shows "integral⇧N (Pi⇩M {i} M) (λx. f (x i)) = integral⇧N (M i) f"
proof -
interpret I: finite_product_sigma_finite M "{i}" by standard simp
from f show ?thesis
by (metis distr_singleton insert_iff measurable_component_singleton nn_integral_distr)
qed
proposition (in product_sigma_finite) product_nn_integral_insert:
assumes I[simp]: "finite I" "i ∉ I"
and f: "f ∈ borel_measurable (Pi⇩M (insert i I) M)"
shows "integral⇧N (Pi⇩M (insert i I) M) f = (∫⇧+ x. (∫⇧+ y. f (x(i := y)) ∂(M i)) ∂(Pi⇩M I M))"
proof -
interpret I: finite_product_sigma_finite M I by standard auto
interpret i: finite_product_sigma_finite M "{i}" by standard auto
have IJ: "I ∩ {i} = {}" and insert: "I ∪ {i} = insert i I"
using f by auto
show ?thesis
unfolding product_nn_integral_fold[OF IJ, unfolded insert, OF I(1) i.finite_index f]
proof (rule nn_integral_cong, subst product_nn_integral_singleton[symmetric])
fix x assume x: "x ∈ space (Pi⇩M I M)"
let ?f = "λy. f (x(i := y))"
show "?f ∈ borel_measurable (M i)"
using measurable_comp[OF measurable_component_update f, OF x ‹i ∉ I›]
unfolding comp_def .
show "(∫⇧+ y. f (merge I {i} (x, y)) ∂Pi⇩M {i} M) = (∫⇧+ y. f (x(i := y i)) ∂Pi⇩M {i} M)"
using x
by (auto intro!: nn_integral_cong arg_cong[where f=f]
simp add: space_PiM extensional_def PiE_def)
qed
qed
lemma (in product_sigma_finite) product_nn_integral_insert_rev:
assumes I[simp]: "finite I" "i ∉ I"
and [measurable]: "f ∈ borel_measurable (Pi⇩M (insert i I) M)"
shows "integral⇧N (Pi⇩M (insert i I) M) f = (∫⇧+ y. (∫⇧+ x. f (x(i := y)) ∂(Pi⇩M I M)) ∂(M i))"
apply (subst product_nn_integral_insert[OF assms])
apply (rule pair_sigma_finite.Fubini')
apply (simp add: local.sigma_finite pair_sigma_finite.intro sigma_finite_measures)
apply measurable
done
lemma (in product_sigma_finite) product_nn_integral_prod:
assumes "finite I" "⋀i. i ∈ I ⟹ f i ∈ borel_measurable (M i)"
shows "(∫⇧+ x. (∏i∈I. f i (x i)) ∂Pi⇩M I M) = (∏i∈I. integral⇧N (M i) (f i))"
using assms proof (induction I)
case (insert i I)
note insert.prems[measurable]
note ‹finite I›[intro, simp]
interpret I: finite_product_sigma_finite M I by standard auto
have *: "⋀x y. (∏j∈I. f j (if j = i then y else x j)) = (∏j∈I. f j (x j))"
using insert by (auto intro!: prod.cong)
have prod: "⋀J. J ⊆ insert i I ⟹ (λx. (∏i∈J. f i (x i))) ∈ borel_measurable (Pi⇩M J M)"
using sets.sets_into_space insert
by (intro borel_measurable_prod_ennreal
measurable_comp[OF measurable_component_singleton, unfolded comp_def])
auto
then show ?case
using product_nn_integral_insert[OF insert(1,2)]
by (simp add: insert(2-) * nn_integral_multc nn_integral_cmult)
qed (simp add: space_PiM)
proposition (in product_sigma_finite) product_nn_integral_pair:
assumes [measurable]: "case_prod f ∈ borel_measurable (M x ⨂⇩M M y)"
assumes xy: "x ≠ y"
shows "(∫⇧+σ. f (σ x) (σ y) ∂PiM {x, y} M) = (∫⇧+z. f (fst z) (snd z) ∂(M x ⨂⇩M M y))"
proof -
interpret psm: pair_sigma_finite "M x" "M y"
unfolding pair_sigma_finite_def using sigma_finite_measures by simp_all
have "{x, y} = {y, x}" by auto
also have "(∫⇧+σ. f (σ x) (σ y) ∂PiM {y, x} M) = (∫⇧+y. ∫⇧+σ. f (σ x) y ∂PiM {x} M ∂M y)"
using xy by (subst product_nn_integral_insert_rev) simp_all
also have "... = (∫⇧+y. ∫⇧+x. f x y ∂M x ∂M y)"
by (intro nn_integral_cong, subst product_nn_integral_singleton) simp_all
also have "... = (∫⇧+z. f (fst z) (snd z) ∂(M x ⨂⇩M M y))"
by (subst psm.nn_integral_snd[symmetric]) simp_all
finally show ?thesis .
qed
lemma (in product_sigma_finite) distr_component:
"distr (M i) (Pi⇩M {i} M) (λx. λi∈{i}. x) = Pi⇩M {i} M" (is "?D = ?P")
proof (intro PiM_eqI)
fix A assume A: "⋀ia. ia ∈ {i} ⟹ A ia ∈ sets (M ia)"
then have "(λx. λi∈{i}. x) -` Pi⇩E {i} A ∩ space (M i) = A i"
by (fastforce dest: sets.sets_into_space)
with A show "emeasure (distr (M i) (Pi⇩M {i} M) (λx. λi∈{i}. x)) (Pi⇩E {i} A) = (∏i∈{i}. emeasure (M i) (A i))"
by (subst emeasure_distr) (auto intro!: sets_PiM_I_finite measurable_restrict)
qed simp_all
lemma (in product_sigma_finite)
assumes IJ: "I ∩ J = {}" "finite I" "finite J" and A: "A ∈ sets (Pi⇩M (I ∪ J) M)"
shows emeasure_fold_integral:
"emeasure (Pi⇩M (I ∪ J) M) A = (∫⇧+x. emeasure (Pi⇩M J M) ((λy. merge I J (x, y)) -` A ∩ space (Pi⇩M J M)) ∂Pi⇩M I M)"
(is "?lhs = ?rhs")
and emeasure_fold_measurable:
"(λx. emeasure (Pi⇩M J M) ((λy. merge I J (x, y)) -` A ∩ space (Pi⇩M J M))) ∈ borel_measurable (Pi⇩M I M)" (is ?B)
proof -
interpret I: finite_product_sigma_finite M I by standard fact
interpret J: finite_product_sigma_finite M J by standard fact
interpret IJ: pair_sigma_finite "Pi⇩M I M" "Pi⇩M J M" ..
have merge: "merge I J -` A ∩ space (Pi⇩M I M ⨂⇩M Pi⇩M J M) ∈ sets (Pi⇩M I M ⨂⇩M Pi⇩M J M)"
by (intro measurable_sets[OF _ A] measurable_merge assms)
have "?lhs = emeasure (distr (Pi⇩M I M ⨂⇩M Pi⇩M J M) (Pi⇩M (I ∪ J) M) (merge I J)) A"
by (simp add: I.finite_index J.finite_index assms(1) distr_merge)
also have "... = emeasure (Pi⇩M I M ⨂⇩M Pi⇩M J M) (merge I J -` A ∩ space (Pi⇩M I M ⨂⇩M Pi⇩M J M))"
by (meson A emeasure_distr measurable_merge)
also have "... = ?rhs"
apply (subst J.emeasure_pair_measure_alt[OF merge])
by (auto intro!: nn_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
finally show "?lhs = ?rhs" .
show ?B
using IJ.measurable_emeasure_Pair1[OF merge]
by (simp add: vimage_comp comp_def space_pair_measure cong: measurable_cong)
qed
lemma sets_Collect_single:
"i ∈ I ⟹ A ∈ sets (M i) ⟹ { x ∈ space (Pi⇩M I M). x i ∈ A } ∈ sets (Pi⇩M I M)"
by simp
lemma pair_measure_eq_distr_PiM:
fixes M1 :: "'a measure" and M2 :: "'a measure"
assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
shows "(M1 ⨂⇩M M2) = distr (Pi⇩M UNIV (case_bool M1 M2)) (M1 ⨂⇩M M2) (λx. (x True, x False))"
(is "?P = ?D")
proof (rule pair_measure_eqI[OF assms])
interpret B: product_sigma_finite "case_bool M1 M2"
unfolding product_sigma_finite_def using assms by (auto split: bool.split)
let ?B = "Pi⇩M UNIV (case_bool M1 M2)"
have [simp]: "fst ∘ (λx. (x True, x False)) = (λx. x True)" "snd ∘ (λx. (x True, x False)) = (λx. x False)"
by auto
fix A B assume A: "A ∈ sets M1" and B: "B ∈ sets M2"
have "emeasure M1 A * emeasure M2 B = (∏ i∈UNIV. emeasure (case_bool M1 M2 i) (case_bool A B i))"
by (simp add: UNIV_bool ac_simps)
also have "… = emeasure ?B (Pi⇩E UNIV (case_bool A B))"
using A B by (subst B.emeasure_PiM) (auto split: bool.split)
also have "Pi⇩E UNIV (case_bool A B) = (λx. (x True, x False)) -` (A × B) ∩ space ?B"
using A[THEN sets.sets_into_space] B[THEN sets.sets_into_space]
by (auto simp: PiE_iff all_bool_eq space_PiM split: bool.split)
finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A × B)"
using A B
measurable_component_singleton[of True UNIV "case_bool M1 M2"]
measurable_component_singleton[of False UNIV "case_bool M1 M2"]
by (subst emeasure_distr) (auto simp: measurable_pair_iff)
qed simp
lemma infprod_in_sets[intro]:
fixes E :: "nat ⇒ 'a set" assumes E: "⋀i. E i ∈ sets (M i)"
shows "Pi UNIV E ∈ sets (Π⇩M i∈UNIV::nat set. M i)"
proof -
have "Pi UNIV E = (⋂i. prod_emb UNIV M {..i} (Π⇩E j∈{..i}. E j))"
using E E[THEN sets.sets_into_space]
by (auto simp: prod_emb_def Pi_iff extensional_def)
with E show ?thesis by auto
qed
subsection ‹Measurability›
text ‹There are two natural sigma-algebras on a product space: the borel sigma algebra,
generated by open sets in the product, and the product sigma algebra, countably generated by
products of measurable sets along finitely many coordinates. The second one is defined and studied
in 🗏‹Finite_Product_Measure.thy›.
These sigma-algebra share a lot of natural properties (measurability of coordinates, for instance),
but there is a fundamental difference: open sets are generated by arbitrary unions, not only
countable ones, so typically many open sets will not be measurable with respect to the product sigma
algebra (while all sets in the product sigma algebra are borel). The two sigma algebras coincide
only when everything is countable (i.e., the product is countable, and the borel sigma algebra in
the factor is countably generated).
In this paragraph, we develop basic measurability properties for the borel sigma algebra, and
compare it with the product sigma algebra as explained above.
›
lemma measurable_product_coordinates [measurable (raw)]:
"(λx. x i) ∈ measurable borel borel"
by (rule borel_measurable_continuous_onI[OF continuous_on_product_coordinates])
lemma measurable_product_then_coordinatewise:
fixes f::"'a ⇒ 'b ⇒ ('c::topological_space)"
assumes [measurable]: "f ∈ borel_measurable M"
shows "(λx. f x i) ∈ borel_measurable M"
proof -
have "(λx. f x i) = (λy. y i) o f"
unfolding comp_def by auto
then show ?thesis by simp
qed
text ‹To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
of the product sigma algebra that is more similar to the one we used above for the product
topology.›
lemma sets_PiM_finite:
"sets (Pi⇩M I M) = sigma_sets (Π⇩E i∈I. space (M i))
{(Π⇩E i∈I. X i) |X. (∀i. X i ∈ sets (M i)) ∧ finite {i. X i ≠ space (M i)}}"
proof
have "{(Π⇩E i∈I. X i) |X. (∀i. X i ∈ sets (M i)) ∧ finite {i. X i ≠ space (M i)}} ⊆ sets (Pi⇩M I M)"
proof clarify
fix X assume H: "∀i. X i ∈ sets (M i)" "finite {i. X i ≠ space (M i)}"
then have *: "X i ∈ sets (M i)" for i by simp
define J where "J = {i ∈ I. X i ≠ space (M i)}"
have "finite J" "J ⊆ I" unfolding J_def using H by auto
define Y where "Y = (Π⇩E j∈J. X j)"
have "prod_emb I M J Y ∈ sets (Pi⇩M I M)"
unfolding Y_def apply (rule sets_PiM_I) using ‹finite J› ‹J ⊆ I› * by auto
moreover have "prod_emb I M J Y = (Π⇩E i∈I. X i)"
unfolding prod_emb_def Y_def J_def using H sets.sets_into_space[OF *]
by (auto simp add: PiE_iff, blast)
ultimately show "Pi⇩E I X ∈ sets (Pi⇩M I M)" by simp
qed
then show "sigma_sets (Π⇩E i∈I. space (M i)) {(Π⇩E i∈I. X i) |X. (∀i. X i ∈ sets (M i)) ∧ finite {i. X i ≠ space (M i)}}
⊆ sets (Pi⇩M I M)"
by (metis (mono_tags, lifting) sets.sigma_sets_subset' sets.top space_PiM)
have *: "∃X. {f. (∀i∈I. f i ∈ space (M i)) ∧ f ∈ extensional I ∧ f i ∈ A} = Pi⇩E I X ∧
(∀i. X i ∈ sets (M i)) ∧ finite {i. X i ≠ space (M i)}"
if "i ∈ I" "A ∈ sets (M i)" for i A
proof -
define X where "X = (λj. if j = i then A else space (M j))"
have "{f. (∀i∈I. f i ∈ space (M i)) ∧ f ∈ extensional I ∧ f i ∈ A} = Pi⇩E I X"
unfolding X_def using sets.sets_into_space[OF ‹A ∈ sets (M i)›] ‹i ∈ I›
by (auto simp add: PiE_iff extensional_def, metis subsetCE, metis)
moreover have "X j ∈ sets (M j)" for j
unfolding X_def using ‹A ∈ sets (M i)› by auto
moreover have "finite {j. X j ≠ space (M j)}"
unfolding X_def by simp
ultimately show ?thesis by auto
qed
show "sets (Pi⇩M I M) ⊆ sigma_sets (Π⇩E i∈I. space (M i)) {(Π⇩E i∈I. X i) |X. (∀i. X i ∈ sets (M i)) ∧ finite {i. X i ≠ space (M i)}}"
unfolding sets_PiM_single
by (intro sigma_sets_mono') (auto simp add: PiE_iff *)
qed
lemma sets_PiM_subset_borel:
"sets (Pi⇩M UNIV (λ_. borel)) ⊆ sets borel"
proof -
have *: "Pi⇩E UNIV X ∈ sets borel" if [measurable]: "⋀i. X i ∈ sets borel" "finite {i. X i ≠ UNIV}" for X::"'a ⇒ 'b set"
proof -
define I where "I = {i. X i ≠ UNIV}"
have "finite I" unfolding I_def using that by simp
have "Pi⇩E UNIV X = (⋂i∈I. (λx. x i)-`(X i) ∩ space borel) ∩ space borel"
unfolding I_def by auto
also have "... ∈ sets borel"
using that ‹finite I› by measurable
finally show ?thesis by simp
qed
then have "{(Π⇩E i∈UNIV. X i) |X::('a ⇒ 'b set). (∀i. X i ∈ sets borel) ∧ finite {i. X i ≠ space borel}} ⊆ sets borel"
by auto
then show ?thesis unfolding sets_PiM_finite space_borel
by (simp add: * sets.sigma_sets_subset')
qed
proposition sets_PiM_equal_borel:
"sets (Pi⇩M UNIV (λi::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
proof
obtain K::"('a ⇒ 'b) set set" where K: "topological_basis K" "countable K"
"⋀k. k ∈ K ⟹ ∃X. (k = Pi⇩E UNIV X) ∧ (∀i. open (X i)) ∧ finite {i. X i ≠ UNIV}"
using product_topology_countable_basis by fast
have *: "k ∈ sets (Pi⇩M UNIV (λ_. borel))" if "k ∈ K" for k
proof -
obtain X where H: "k = Pi⇩E UNIV X" "⋀i. open (X i)" "finite {i. X i ≠ UNIV}"
using K(3)[OF ‹k ∈ K›] by blast
show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
qed
have **: "U ∈ sets (Pi⇩M UNIV (λ_. borel))" if "open U" for U::"('a ⇒ 'b) set"
proof -
obtain B where "B ⊆ K" "U = (⋃B)"
using ‹open U› ‹topological_basis K› by (metis topological_basis_def)
have "countable B" using ‹B ⊆ K› ‹countable K› countable_subset by blast
moreover have "k ∈ sets (Pi⇩M UNIV (λ_. borel))" if "k ∈ B" for k
using ‹B ⊆ K› * that by auto
ultimately show ?thesis unfolding ‹U = (⋃B)› by auto
qed
have "sigma_sets UNIV (Collect open) ⊆ sets (Pi⇩M UNIV (λi::'a. (borel::('b measure))))"
by (metis "**" mem_Collect_eq open_UNIV sets.sigma_sets_subset' subsetI)
then show "sets (borel::('a ⇒ 'b) measure) ⊆ sets (Pi⇩M UNIV (λ_. borel))"
unfolding borel_def by auto
qed (simp add: sets_PiM_subset_borel)
lemma measurable_coordinatewise_then_product:
fixes f::"'a ⇒ ('b::countable) ⇒ ('c::second_countable_topology)"
assumes [measurable]: "⋀i. (λx. f x i) ∈ borel_measurable M"
shows "f ∈ borel_measurable M"
proof -
have "f ∈ measurable M (Pi⇩M UNIV (λ_. borel))"
by (rule measurable_PiM_single', auto simp add: assms)
then show ?thesis using sets_PiM_equal_borel measurable_cong_sets by blast
qed
end