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: "(iI. xF i. P i x)  (fPi I F. iI. P i (f i))"
  by (metis Pi_iff)

lemma PiE_choice: "(iI. xF i. P i x) (fPiE I F. iI. 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

subsectiontag unimportant› ‹More about Function restricted by constextensional

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)  PiE (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 iJ. S i)" "B  (ΠE iJ. S i)" and ne: "(ΠE iI. S i)  {}"
  and eq: "(λx. restrict x J) -` A  (ΠE iI. S i) = (λx. restrict x J) -` B  (ΠE iI. 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 iJ. S i)"
    have "x  A  merge J (I - J) (x,y)  (λx. restrict x J) -` A  (ΠE iI. 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)) -` (PiE I E × PiE 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 -` PiE (I  J) E = Pi I E × Pi J E"
  by (auto simp: restrict_Pi_cancel PiE_def)

subsection ‹Finite product spaces›

definitiontag important› prod_emb where
  "prod_emb I M K X = (λx. restrict x K) -` X  (ΠE iI. space (M i))"

lemma prod_emb_iff:
  "f  prod_emb I M K X  f  extensional I  (restrict f K  X)  (iI. 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 (iI. F i) = (iI. prod_emb M L K (F i))"
    and prod_emb_INT[simp]: "I  {}  prod_emb M L K (iI. F i) = (iI. 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 iJ. E i) = (ΠE iI. 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 (PiE I E) = PiE 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  (Π jJ. sets (M j))" "J  K"
  shows "prod_emb K M J (PiE J X) = (ΠE iK. 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 iL. 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)

definitiontag important› PiM :: "'i set  ('i  'a measure)  ('i  'a) measure" where
  "PiM I M = extend_measure (ΠE iI. space (M i))
    {(J, X). (J  {}  I = {})  finite J  J  I  X  (Π jJ. sets (M j))}
    (λ(J, X). prod_emb I M J (ΠE jJ. X j))
    (λ(J, X). jJ  {iI. emeasure (M i) (space (M i))  1}. if j  J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))"

definitiontag 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 jJ. X j)) `
    {(J, X). (J  {}  I = {})  finite J  J  I  X  (Π jJ. sets (M j))}"

abbreviation
  "PiM I M  PiM I M"

syntax
  "_PiM" :: "pttrn  'i set  'a measure  ('i => 'a) measure"  ("(3ΠM __./ _)"  10)
translations
  "ΠM xI. 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  (Π jK. sets (M j)) = (Π jK. 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 iI. 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 iI. X i) |X. X  (Π jI. 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" "iJ. E i  sets (M i)"
    and A: "A = prod_emb I M J (ΠE jJ. E j)"
    by (auto simp: prod_algebra_def)
  let ?A = "ΠE iI. 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 iI. X i)" and X: "X  (Π jI. sets (M j))" by auto
  then have A: "A = prod_emb I M I (ΠE iI. 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 jJ. E j)  prod_algebra I M"
  by (auto simp: prod_algebra_def)

lemma prod_algebraI_finite:
  "finite I  (iI. E i  sets (M i))  (PiE 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 {PiE J E | E. iI. E i  sets (M i)}"
proof (safe intro!: Int_stableI)
  fix E F assume "iI. E i  sets (M i)" "iI. F i  sets (M i)"
  then show "G. PiE J E  PiE J F = PiE J G  (iI. 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 jJ. 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 = PiE I E" "E  (Π iI. sets (M i))"
proof -
  from A obtain E J where A: "A = prod_emb I M J (PiE J E)"
    and J: "J  I" and E: "E  (Π iJ. 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 iI. if iJ then E i else space (M i))"
    using A J by (auto simp: prod_emb_PiE)
  moreover have "(λi. if iJ then E i else space (M i))  (Π iI. 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 (PiE 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 (PiE 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 iJ  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 iJ. G i)"
    and G: "i. i  J  G i  sets (E i)"
    by (auto simp: prod_algebra_def)
  moreover
  from space have "(ΠE iI. space (E i)) = (ΠE iI. space (F i))"
    by (rule PiE_cong)
  with A have "A = prod_emb I F J (ΠE iJ. 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 iI. 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 iI. 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 iI. M i) = (ΠE iI. 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) = {}   (iI. 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 iI. M i) = sigma_sets (ΠE iI. 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 iI. space (M i)) {{fΠE iI. 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 (PiE 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 = (jJ. {f(ΠE iI. 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 iI. 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 iI. vimage_algebra (ΠE iI. space (M i)) (λx. x i) (M i))"
        (is "?lhs = ?rhs")
proof -
  have "?lhs = 
        sigma_sets (ΠE iI. space (M i)) {{f  ΠE iI. 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 iI. space (M i))
                (xI. sets (vimage_algebra (ΠE iI. 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 iI. space (M i))
     ( (sets ` (λi. vimage_algebra (ΠE iI. space (M i)) (λx. x i) (M i)) ` I))"
    by simp
  also have "... = ?rhs"
    by (subst sets_Sup_eq[where X="ΠE iI. space (M i)"]) (use assms in auto)
  finally show ?thesis .
qed

lemma
  shows space_PiM_empty: "space (PiM {} M) = {λk. undefined}"
    and sets_PiM_empty: "sets (PiM {} 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  SE 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 iI. Ω i). ij. f i  A i} | A j. j  J  A  Pi j E}"
  shows "sets (ΠM iI. sigma (Ω i) (E i)) = sets (sigma (ΠE iI. Ω 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  PiE I Ω |A. A  E i}"
  assume "I  {}"
  then have "sets (PiM I (λi. sigma (Ω i) (E i))) =
      sets (SUP iI. vimage_algebra (ΠE iI. Ω i) (λx. x i) (sigma (Ω i) (E i)))"
    by (subst sets_PiM_eq_proj) (auto simp: space_measure_of_conv)
  also have " = sets (SUP iI. sigma (PiE I Ω) (?F i))"
    using E by (intro sets_SUP_cong arg_cong[where f=sets] vimage_algebra_sigma) auto
  also have " = sets (sigma (PiE I Ω) (iI. ?F i))"
    using I  {} by (intro arg_cong[where f=sets] SUP_sigma_sigma) auto
  also have " = sets (sigma (PiE I Ω) P)"
  proof (intro arg_cong[where f=sets] sigma_eqI sigma_sets_eqI)
    show "(iI. ?F i)  Pow (PiE I Ω)" "P  Pow (PiE I Ω)"
      by (auto simp: P_def)
  next
    interpret P: sigma_algebra "ΠE iI. Ω i" "sigma_sets (ΠE iI. Ω i) P"
      by (auto intro!: sigma_algebra_sigma_sets simp: P_def)

    fix Z assume "Z  (iI. ?F i)"
    then obtain i A where i: "i  I" "A  E i" and Z_def: "Z = (λx. x i) -` A  PiE 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  PiE (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  PiE I Ω. ij. f i  A' n i}  P"
        by (auto simp: P_def) }
    note A'_in_P = this

    { fix x assume "x i  A" "x  PiE I Ω"
      with S(3) j  I have "ij. sS 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 "nPiE (j-{i}) S. ij. 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 = (nPiE (j-{i}) S. {f(ΠE iI. Ω i). ij. f i  A' n i})"
      unfolding Z_def
      by (auto simp add: set_eq_iff ball_conj_distrib ij A'_i dest: bspec[OF _ ij]
               cong: conj_cong)
    also have "  sigma_sets (ΠE iI. Ω 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 iI. Ω i) P" .
  next
    interpret F: sigma_algebra "ΠE iI. Ω i" "sigma_sets (ΠE iI. Ω i) (iI. ?F i)"
      by (auto intro!: sigma_algebra_sigma_sets)

    fix b assume "b  P"
    then obtain A j where b: "b = {f(ΠE iI. Ω i). ij. f i  A i}" "j  J" "A  Pi j E"
      by (auto simp: P_def)
    show "b  sigma_sets (PiE I Ω) (iI. ?F i)"
    proof cases
      assume "j = {}"
      with b have "b = (ΠE iI. Ω i)"
        by auto
      then show ?thesis
        by blast
    next
      assume "j  {}"
      with J b(2,3) have eq: "b = (ij. ((λx. x i) -` A i  PiE 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 iI. space (M i))"
  assumes sets: "i A. i  I  A  sets (M i)  {xspace 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" "iJ. E i  sets (M i)"
  shows "prod_emb I M J (ΠE jJ. E j)  sets (ΠM iI. M i)"
proof cases
  assume "J = {}"
  then have "prod_emb I M J (ΠE jJ. E j) = (ΠE jI. 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 iI. 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 (PiE 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 (PiE 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 iI. space (M i))"
  assumes sets: "X J. J  {}  I = {}  finite J  J  I  (i. i  J  X i  sets (M i)) 
    {ωspace N. iJ. 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 (PiE 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. iJ. 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 iI. 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 iI. space (M i). f i  A} |i A. i  I  A  sets (M i)}"
  then obtain B i where "A = {f  ΠE iI. 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 iI. space (M i))"
  shows "(λω i. f i ω)  measurable N (PiM 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 jI. E j)  sets (ΠM iI. 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 (PiM 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 (PiM 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 (PiM I M)  sets (PiM 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 (PiM 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 iUNIV. M)"
  shows "(λx. case_nat (f x) (g x))  measurable N (ΠM iUNIV. 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 (PiM I M M M i) (PiM (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 (PiM 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 iI. 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 (PiM I M)  i  I  (λv. x(i := v))  measurable (M i) (PiM (insert i I) M)"
  by simp

lemma measurable_merge[measurable]:
  "merge I J  measurable (PiM I M M PiM J M) (PiM (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. λiI. X i x)  measurable N (PiM I M)"
proof (rule measurable_PiM_single)
  fix A i assume A: "i  I" "A  sets (M i)"
  then have "{ω  space N. (λiI. X i ω) i  A} = X i -` A  space N"
    by auto
  then show "{ω  space N. (λiI. X i ω) i  A}  sets N"
    using A X by (auto intro!: measurable_sets)
next
  show "(λx. λiI. X i x)  space N  (ΠE iI. 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 (PiM L M) (PiM 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 (PiM L M) (PiM 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 (PiM J M)  prod_emb L M J X  sets (PiM 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 (PiM 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 (PiM 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 xX X J] * show "x  {}" by auto
qed

lemma sets_in_Pi_aux:
  "finite I  (j. j  I  {xspace (M j). x  F j}  sets (M j)) 
  {xspace (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  {xspace (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:
  "{xspace (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 "PiE I E  sets (PiM I M)"
proof cases
  assume "I  {}"
  then have "PiE I E = (iI. prod_emb I M {i} (PiE {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 "JI. XPiM 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 iI. 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 (PiM 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 (PiM (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 (PiE I A) = Q (PiE 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 iI. 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 jJ. 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 (PiE J A)) = Q (prod_emb I M J (PiE 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 iI. 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 jJ. 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)

localetag unimportant› product_sigma_finite =
  fixes M :: "'i  'a measure"
  assumes sigma_finite_measures: "i. sigma_finite_measure (M i)"

sublocaletag unimportant› product_sigma_finite  M?: sigma_finite_measure "M i" for i
  by (rule sigma_finite_measures)

localetag 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.
    (iI. range (F i)  sets (M i)) 
    (k. iI. emeasure (M i) (F i k)  )  incseq (λk. ΠE iI. F i k) 
    (k. ΠE iI. 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 iI. 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 (PiM {} 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. iI  A i  sets (M i))  emeasure (PiM I M) (PiE I A) = (iI. 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 (PiM I M M M i) (PiM (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 (PiM (insert i I) M) (prod_emb (insert i I) M (insert i I) (PiE (insert i I) A)) =
    (iinsert 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  (Π jJ. sets (M j))"
    then have J: "J  {}" "finite J" "J  insert i I" and E: "jJ. E j  sets (M j)" by auto
    let ?p = "prod_emb (insert i I) M J (PiE J E)"
    let ?p' = "prod_emb I M (J - {i}) (ΠE jJ-{i}. E j)"
    have " ?p =
      emeasure (PiM I M M (M i)) (?h -` ?p  space (PiM I M M M i))"
      by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
    also have "?h -` ?p  space (PiM 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 (PiM I M M (M i)) (?p' × (if i  J then E i else space (M i))) =
      emeasure (PiM 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 jI. 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 (PiM I M) (ΠE jI. if j  J-{i} then E j else space (M j)) =
      ( jI. 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 "(jI. 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)) = (jinsert i I. ?f J E j)"
      using insert by (auto simp: mult.commute intro!: arg_cong2[where f="(*)"] prod.cong)
    also have " = (jJ  ?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 (PiE J E)  Pow (ΠE iinsert 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 (PiM (insert i I) M)) " "countably_additive (sets (PiM (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  (Π jinsert 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 (PiE I A) = (iI. 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:
    "iI. range (C i)  sets (M i)" "k. iI. emeasure (M i) (C i k)  "
    "incseq (λk. ΠE iI. C i k)" "(k. ΠE iI. C i k) = space (PiM 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))  (PiM I M) (PiE I A) = P (PiE I A)" for A
      by (simp add: eq emeasure_PiM)
    define A where "A n = (ΠE iI. C i n)" for n
    with C show "range A  prod_algebra I M" "i. emeasure (PiM 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 "((PiE I ` PiE I F)) = space (PiM I M)"
    using in_space by (auto simp: space_PiM PiE_iff intro!: PiE_choice[THEN iffD1])
  ultimately show "A. countable A  A  sets (PiM I M)  A = space (PiM I M)  (aA. emeasure (PiM I M) a  )"
    by (intro exI[of _ "PiE I ` PiE 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 "PiM 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 (PiM I M) (PiE I A) = (iI. 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)  integralN (PiM {} M) f = f (λk. undefined)"
  by (simp add: PiM_empty nn_integral_count_space_finite max.absorb2)

lemmatag important› (in product_sigma_finite) distr_merge:
  assumes IJ[simp]: "I  J = {}" and fin: "finite I" "finite J"
  shows "distr (PiM I M M PiM J M) (PiM (I  J) M) (merge I J) = PiM (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 -` PiE (I  J) A  space (PiM I M M PiM J M)) = PiE I A × PiE J A"
    using A[THEN sets.sets_into_space] by (auto simp: space_PiM space_pair_measure)
  from A fin show "emeasure (distr (PiM I M M PiM J M) (PiM (I  J) M) (merge I J)) (PiE (I  J) A) =
      (iI  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 (PiM (I  J) M)"
shows "integralN (PiM (I  J) M) f = (+ x. (+ y. f (merge I J (x, y)) (PiM J M)) (PiM 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 "PiM I M" "PiM J M" by standard
  have P_borel: "(λx. f (merge I J x))  borel_measurable (PiM I M M PiM J M)"
    using measurable_comp[OF measurable_merge f] by (simp add: comp_def)
  have "?lhs = integralN (distr (PiM I M M PiM J M) (PiM (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) (PiM I M M PiM 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 (PiM {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 (PiM {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 "integralN (PiM {i} M) (λx. f (x i)) = integralN (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 (PiM (insert i I) M)"
  shows "integralN (PiM (insert i I) M) f = (+ x. (+ y. f (x(i := y)) (M i)) (PiM 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 (PiM 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)) PiM {i} M) = (+ y. f (x(i := y i)) PiM {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]: