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 PiE_choice: "(∃f∈Pi⇩E I F. ∀i∈I. P i (f i)) ⟷ (∀i∈I. ∃x∈F i. P i x)"
  by (auto simp: Bex_def PiE_iff Ball_def dest!: choice_iff'[THEN iffD1])
     (force intro: exI[of _ "restrict f I" for f])

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 (insert sets, 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"
  unfolding Pi_def 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 sets: "(⋀i. i ∈ I ⟹ sets (M i) = sets (N i))"
  shows "prod_algebra I M = prod_algebra J N"
proof -
  have space: "⋀i. i ∈ I ⟹ space (M i) = space (N i)"
    using sets_eq_imp_space_eq[OF sets] by auto
  with sets show ?thesis unfolding ‹I = J›
    by (intro antisym prod_algebra_mono) auto
qed

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)
  also have "… ∈ prod_algebra I M"
    using ‹i ∈ I› by (intro prod_algebraI) auto
  finally show ?thesis .
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 have "A = {λx. undefined}" by (auto simp: prod_emb_def)
    with ‹I = {}› show ?thesis by (auto intro!: sigma_sets_top)
  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:
  "I ≠ {} ⟹ sets (PiM I M) = sets (SUP i∈I. vimage_algebra (Π⇩E i∈I. space (M i)) (λx. x i) (M i))"
  apply (simp add: sets_PiM_single)
  apply (subst sets_Sup_eq[where X="Π⇩E i∈I. space (M i)"])
  apply auto []
  apply auto []
  apply simp
  apply (subst arg_cong [of _ _ Sup, OF image_cong, OF refl])
  apply (rule sets_vimage_algebra2)
  apply (auto intro!: arg_cong2[where f=sigma_sets])
  done

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 (insert ‹i ∈ I›, 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)
qed (insert X, auto simp add: PiE_def dest: measurable_space)

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)"
proof-
  from assms(1) have "(λf. restrict f J) ∈ measurable (Pi⇩M L M) (Pi⇩M J M)"
    by (rule measurable_restrict_subset)
  also from assms(2) have "measurable (Pi⇩M L M) (Pi⇩M J M) = measurable (Pi⇩M L M) (Pi⇩M J N)"
    by (intro sets_PiM_cong measurable_cong_sets) simp_all
  finally show ?thesis .
qed

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)"
proof -
  have "{x∈space (PiM I M). x ∈ extensional I} = space (PiM I M)"
    by (auto simp add: extensional_def space_PiM)
  then show ?thesis by simp
qed

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 (safe intro!: sets.countable_INT' measurable_prod_emb sets_PiM_I_finite E)
  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[of _ "⋃i. J i"] bexI[of _ "⋃i. prod_emb (⋃i. J i) M (J i) (X i)"] 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✐‹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) ?μ"
      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 iffD2])
  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 (insert fin, 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))"
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)
  show ?thesis
    apply (subst distr_merge[OF IJ, symmetric])
    apply (subst nn_integral_distr[OF measurable_merge])
    apply measurable []
    apply (subst J.nn_integral_fst[symmetric, OF P_borel])
    apply simp
    done
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
    apply (subst distr_singleton[symmetric])
    apply (subst nn_integral_distr[OF measurable_component_singleton])
    apply simp_all
    done
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.