# Theory Finite_Product_Measure

```(*  Title:      HOL/Analysis/Finite_Product_Measure.thy
Author:     Johannes Hölzl, TU München
*)

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✐‹tag unimportant› ‹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✐‹tag important› 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✐‹tag important› 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✐‹tag important› 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"  ("(3Π⇩M _∈_./ _)"  10)
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 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)"
moreover
from sets G J have "⋀i. i ∈ J ⟹ G i ∈ sets (F i)"
by auto
ultimately show "A ∈ prod_algebra I F"
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)}"
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)

"(λ(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)

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)"

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 .

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))"
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)

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✐‹tag unimportant› product_sigma_finite =
fixes M :: "'i ⇒ 'a measure"
assumes sigma_finite_measures: "⋀i. sigma_finite_measure (M i)"

sublocale✐‹tag unimportant› product_sigma_finite ⊆ M?: sigma_finite_measure "M i" for i
by (rule sigma_finite_measures)

locale✐‹tag unimportant› 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) ?μ"
(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
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✐‹tag important› (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)"
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"]
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]