src/HOL/Analysis/Finite_Product_Measure.thy
changeset 68833 fde093888c16
parent 67399 eab6ce8368fa
child 69064 5840724b1d71
     1.1 --- a/src/HOL/Analysis/Finite_Product_Measure.thy	Mon Aug 27 22:58:36 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Tue Aug 28 13:28:39 2018 +0100
     1.3 @@ -2,20 +2,20 @@
     1.4      Author:     Johannes Hölzl, TU München
     1.5  *)
     1.6  
     1.7 -section \<open>Finite product measures\<close>
     1.8 +section%important \<open>Finite product measures\<close>
     1.9  
    1.10  theory Finite_Product_Measure
    1.11  imports Binary_Product_Measure
    1.12  begin
    1.13  
    1.14 -lemma PiE_choice: "(\<exists>f\<in>Pi\<^sub>E I F. \<forall>i\<in>I. P i (f i)) \<longleftrightarrow> (\<forall>i\<in>I. \<exists>x\<in>F i. P i x)"
    1.15 +lemma%unimportant PiE_choice: "(\<exists>f\<in>Pi\<^sub>E I F. \<forall>i\<in>I. P i (f i)) \<longleftrightarrow> (\<forall>i\<in>I. \<exists>x\<in>F i. P i x)"
    1.16    by (auto simp: Bex_def PiE_iff Ball_def dest!: choice_iff'[THEN iffD1])
    1.17       (force intro: exI[of _ "restrict f I" for f])
    1.18  
    1.19 -lemma case_prod_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
    1.20 +lemma%unimportant case_prod_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
    1.21    by auto
    1.22  
    1.23 -subsubsection \<open>More about Function restricted by @{const extensional}\<close>
    1.24 +subsubsection%unimportant \<open>More about Function restricted by @{const extensional}\<close>
    1.25  
    1.26  definition
    1.27    "merge I J = (\<lambda>(x, y) i. if i \<in> I then x i else if i \<in> J then y i else undefined)"
    1.28 @@ -109,59 +109,59 @@
    1.29    "I \<inter> J = {} \<Longrightarrow> merge I J -` Pi\<^sub>E (I \<union> J) E = Pi I E \<times> Pi J E"
    1.30    by (auto simp: restrict_Pi_cancel PiE_def)
    1.31  
    1.32 -subsection \<open>Finite product spaces\<close>
    1.33 +subsection%important \<open>Finite product spaces\<close>
    1.34  
    1.35 -subsubsection \<open>Products\<close>
    1.36 +subsubsection%important \<open>Products\<close>
    1.37  
    1.38 -definition prod_emb where
    1.39 +definition%important prod_emb where
    1.40    "prod_emb I M K X = (\<lambda>x. restrict x K) -` X \<inter> (\<Pi>\<^sub>E i\<in>I. space (M i))"
    1.41  
    1.42 -lemma prod_emb_iff:
    1.43 +lemma%important prod_emb_iff:
    1.44    "f \<in> prod_emb I M K X \<longleftrightarrow> f \<in> extensional I \<and> (restrict f K \<in> X) \<and> (\<forall>i\<in>I. f i \<in> space (M i))"
    1.45 -  unfolding prod_emb_def PiE_def by auto
    1.46 +  unfolding%unimportant prod_emb_def PiE_def by auto
    1.47  
    1.48 -lemma
    1.49 +lemma%unimportant (*FIX ME needs a name *)
    1.50    shows prod_emb_empty[simp]: "prod_emb M L K {} = {}"
    1.51      and prod_emb_Un[simp]: "prod_emb M L K (A \<union> B) = prod_emb M L K A \<union> prod_emb M L K B"
    1.52      and prod_emb_Int: "prod_emb M L K (A \<inter> B) = prod_emb M L K A \<inter> prod_emb M L K B"
    1.53      and prod_emb_UN[simp]: "prod_emb M L K (\<Union>i\<in>I. F i) = (\<Union>i\<in>I. prod_emb M L K (F i))"
    1.54      and prod_emb_INT[simp]: "I \<noteq> {} \<Longrightarrow> prod_emb M L K (\<Inter>i\<in>I. F i) = (\<Inter>i\<in>I. prod_emb M L K (F i))"
    1.55      and prod_emb_Diff[simp]: "prod_emb M L K (A - B) = prod_emb M L K A - prod_emb M L K B"
    1.56 -  by (auto simp: prod_emb_def)
    1.57 +  by%unimportant (auto simp: prod_emb_def)
    1.58  
    1.59 -lemma prod_emb_PiE: "J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow>
    1.60 +lemma%unimportant prod_emb_PiE: "J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow>
    1.61      prod_emb I M J (\<Pi>\<^sub>E i\<in>J. E i) = (\<Pi>\<^sub>E i\<in>I. if i \<in> J then E i else space (M i))"
    1.62    by (force simp: prod_emb_def PiE_iff if_split_mem2)
    1.63  
    1.64 -lemma prod_emb_PiE_same_index[simp]:
    1.65 +lemma%unimportant prod_emb_PiE_same_index[simp]:
    1.66      "(\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow> prod_emb I M I (Pi\<^sub>E I E) = Pi\<^sub>E I E"
    1.67    by (auto simp: prod_emb_def PiE_iff)
    1.68  
    1.69 -lemma prod_emb_trans[simp]:
    1.70 +lemma%unimportant prod_emb_trans[simp]:
    1.71    "J \<subseteq> K \<Longrightarrow> K \<subseteq> L \<Longrightarrow> prod_emb L M K (prod_emb K M J X) = prod_emb L M J X"
    1.72    by (auto simp add: Int_absorb1 prod_emb_def PiE_def)
    1.73  
    1.74 -lemma prod_emb_Pi:
    1.75 +lemma%unimportant prod_emb_Pi:
    1.76    assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
    1.77    shows "prod_emb K M J (Pi\<^sub>E J X) = (\<Pi>\<^sub>E i\<in>K. if i \<in> J then X i else space (M i))"
    1.78    using assms sets.space_closed
    1.79    by (auto simp: prod_emb_def PiE_iff split: if_split_asm) blast+
    1.80  
    1.81 -lemma prod_emb_id:
    1.82 +lemma%unimportant prod_emb_id:
    1.83    "B \<subseteq> (\<Pi>\<^sub>E i\<in>L. space (M i)) \<Longrightarrow> prod_emb L M L B = B"
    1.84    by (auto simp: prod_emb_def subset_eq extensional_restrict)
    1.85  
    1.86 -lemma prod_emb_mono:
    1.87 +lemma%unimportant prod_emb_mono:
    1.88    "F \<subseteq> G \<Longrightarrow> prod_emb A M B F \<subseteq> prod_emb A M B G"
    1.89    by (auto simp: prod_emb_def)
    1.90  
    1.91 -definition PiM :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
    1.92 +definition%important PiM :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
    1.93    "PiM I M = extend_measure (\<Pi>\<^sub>E i\<in>I. space (M i))
    1.94      {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}
    1.95      (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^sub>E j\<in>J. X j))
    1.96      (\<lambda>(J, X). \<Prod>j\<in>J \<union> {i\<in>I. emeasure (M i) (space (M i)) \<noteq> 1}. if j \<in> J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))"
    1.97  
    1.98 -definition prod_algebra :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) set set" where
    1.99 +definition%important prod_algebra :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) set set" where
   1.100    "prod_algebra I M = (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^sub>E j\<in>J. X j)) `
   1.101      {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}"
   1.102  
   1.103 @@ -173,20 +173,20 @@
   1.104  translations
   1.105    "\<Pi>\<^sub>M x\<in>I. M" == "CONST PiM I (%x. M)"
   1.106  
   1.107 -lemma extend_measure_cong:
   1.108 +lemma%important extend_measure_cong:
   1.109    assumes "\<Omega> = \<Omega>'" "I = I'" "G = G'" "\<And>i. i \<in> I' \<Longrightarrow> \<mu> i = \<mu>' i"
   1.110    shows "extend_measure \<Omega> I G \<mu> = extend_measure \<Omega>' I' G' \<mu>'"
   1.111 -  unfolding extend_measure_def by (auto simp add: assms)
   1.112 +  unfolding%unimportant extend_measure_def by (auto simp add: assms)
   1.113  
   1.114 -lemma Pi_cong_sets:
   1.115 +lemma%unimportant Pi_cong_sets:
   1.116      "\<lbrakk>I = J; \<And>x. x \<in> I \<Longrightarrow> M x = N x\<rbrakk> \<Longrightarrow> Pi I M = Pi J N"
   1.117    unfolding Pi_def by auto
   1.118  
   1.119 -lemma PiM_cong:
   1.120 +lemma%important PiM_cong:
   1.121    assumes "I = J" "\<And>x. x \<in> I \<Longrightarrow> M x = N x"
   1.122    shows "PiM I M = PiM J N"
   1.123    unfolding PiM_def
   1.124 -proof (rule extend_measure_cong, goal_cases)
   1.125 +proof%unimportant (rule extend_measure_cong, goal_cases)
   1.126    case 1
   1.127    show ?case using assms
   1.128      by (subst assms(1), intro PiE_cong[of J "\<lambda>i. space (M i)" "\<lambda>i. space (N i)"]) simp_all
   1.129 @@ -206,14 +206,14 @@
   1.130  qed
   1.131  
   1.132  
   1.133 -lemma prod_algebra_sets_into_space:
   1.134 +lemma%unimportant prod_algebra_sets_into_space:
   1.135    "prod_algebra I M \<subseteq> Pow (\<Pi>\<^sub>E i\<in>I. space (M i))"
   1.136    by (auto simp: prod_emb_def prod_algebra_def)
   1.137  
   1.138 -lemma prod_algebra_eq_finite:
   1.139 +lemma%important prod_algebra_eq_finite:
   1.140    assumes I: "finite I"
   1.141    shows "prod_algebra I M = {(\<Pi>\<^sub>E i\<in>I. X i) |X. X \<in> (\<Pi> j\<in>I. sets (M j))}" (is "?L = ?R")
   1.142 -proof (intro iffI set_eqI)
   1.143 +proof%unimportant (intro iffI set_eqI)
   1.144    fix A assume "A \<in> ?L"
   1.145    then obtain J E where J: "J \<noteq> {} \<or> I = {}" "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)"
   1.146      and A: "A = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)"
   1.147 @@ -232,32 +232,32 @@
   1.148      by (auto simp: prod_algebra_def)
   1.149  qed
   1.150  
   1.151 -lemma prod_algebraI:
   1.152 +lemma%unimportant prod_algebraI:
   1.153    "finite J \<Longrightarrow> (J \<noteq> {} \<or> I = {}) \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i))
   1.154      \<Longrightarrow> prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) \<in> prod_algebra I M"
   1.155    by (auto simp: prod_algebra_def)
   1.156  
   1.157 -lemma prod_algebraI_finite:
   1.158 +lemma%unimportant prod_algebraI_finite:
   1.159    "finite I \<Longrightarrow> (\<forall>i\<in>I. E i \<in> sets (M i)) \<Longrightarrow> (Pi\<^sub>E I E) \<in> prod_algebra I M"
   1.160    using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets.sets_into_space] by simp
   1.161  
   1.162 -lemma Int_stable_PiE: "Int_stable {Pi\<^sub>E J E | E. \<forall>i\<in>I. E i \<in> sets (M i)}"
   1.163 +lemma%unimportant Int_stable_PiE: "Int_stable {Pi\<^sub>E J E | E. \<forall>i\<in>I. E i \<in> sets (M i)}"
   1.164  proof (safe intro!: Int_stableI)
   1.165    fix E F assume "\<forall>i\<in>I. E i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
   1.166    then show "\<exists>G. Pi\<^sub>E J E \<inter> Pi\<^sub>E J F = Pi\<^sub>E J G \<and> (\<forall>i\<in>I. G i \<in> sets (M i))"
   1.167      by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"] simp: PiE_Int)
   1.168  qed
   1.169  
   1.170 -lemma prod_algebraE:
   1.171 +lemma%unimportant prod_algebraE:
   1.172    assumes A: "A \<in> prod_algebra I M"
   1.173    obtains J E where "A = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)"
   1.174      "finite J" "J \<noteq> {} \<or> I = {}" "J \<subseteq> I" "\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i)"
   1.175    using A by (auto simp: prod_algebra_def)
   1.176  
   1.177 -lemma prod_algebraE_all:
   1.178 +lemma%important prod_algebraE_all:
   1.179    assumes A: "A \<in> prod_algebra I M"
   1.180    obtains E where "A = Pi\<^sub>E I E" "E \<in> (\<Pi> i\<in>I. sets (M i))"
   1.181 -proof -
   1.182 +proof%unimportant -
   1.183    from A obtain E J where A: "A = prod_emb I M J (Pi\<^sub>E J E)"
   1.184      and J: "J \<subseteq> I" and E: "E \<in> (\<Pi> i\<in>J. sets (M i))"
   1.185      by (auto simp: prod_algebra_def)
   1.186 @@ -270,7 +270,7 @@
   1.187    ultimately show ?thesis using that by auto
   1.188  qed
   1.189  
   1.190 -lemma Int_stable_prod_algebra: "Int_stable (prod_algebra I M)"
   1.191 +lemma%unimportant Int_stable_prod_algebra: "Int_stable (prod_algebra I M)"
   1.192  proof (unfold Int_stable_def, safe)
   1.193    fix A assume "A \<in> prod_algebra I M"
   1.194    from prod_algebraE[OF this] guess J E . note A = this
   1.195 @@ -291,11 +291,11 @@
   1.196    finally show "A \<inter> B \<in> prod_algebra I M" .
   1.197  qed
   1.198  
   1.199 -lemma prod_algebra_mono:
   1.200 +lemma%unimportant prod_algebra_mono:
   1.201    assumes space: "\<And>i. i \<in> I \<Longrightarrow> space (E i) = space (F i)"
   1.202    assumes sets: "\<And>i. i \<in> I \<Longrightarrow> sets (E i) \<subseteq> sets (F i)"
   1.203    shows "prod_algebra I E \<subseteq> prod_algebra I F"
   1.204 -proof
   1.205 +proof%unimportant
   1.206    fix A assume "A \<in> prod_algebra I E"
   1.207    then obtain J G where J: "J \<noteq> {} \<or> I = {}" "finite J" "J \<subseteq> I"
   1.208      and A: "A = prod_emb I E J (\<Pi>\<^sub>E i\<in>J. G i)"
   1.209 @@ -316,17 +316,17 @@
   1.210      done
   1.211  qed
   1.212  
   1.213 -lemma prod_algebra_cong:
   1.214 +lemma%unimportant prod_algebra_cong:
   1.215    assumes "I = J" and sets: "(\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i))"
   1.216    shows "prod_algebra I M = prod_algebra J N"
   1.217 -proof -
   1.218 +proof%unimportant -
   1.219    have space: "\<And>i. i \<in> I \<Longrightarrow> space (M i) = space (N i)"
   1.220      using sets_eq_imp_space_eq[OF sets] by auto
   1.221    with sets show ?thesis unfolding \<open>I = J\<close>
   1.222      by (intro antisym prod_algebra_mono) auto
   1.223  qed
   1.224  
   1.225 -lemma space_in_prod_algebra:
   1.226 +lemma%unimportant space_in_prod_algebra:
   1.227    "(\<Pi>\<^sub>E i\<in>I. space (M i)) \<in> prod_algebra I M"
   1.228  proof cases
   1.229    assume "I = {}" then show ?thesis
   1.230 @@ -341,26 +341,26 @@
   1.231    finally show ?thesis .
   1.232  qed
   1.233  
   1.234 -lemma space_PiM: "space (\<Pi>\<^sub>M i\<in>I. M i) = (\<Pi>\<^sub>E i\<in>I. space (M i))"
   1.235 +lemma%unimportant space_PiM: "space (\<Pi>\<^sub>M i\<in>I. M i) = (\<Pi>\<^sub>E i\<in>I. space (M i))"
   1.236    using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro space_extend_measure) simp
   1.237  
   1.238 -lemma prod_emb_subset_PiM[simp]: "prod_emb I M K X \<subseteq> space (PiM I M)"
   1.239 +lemma%unimportant prod_emb_subset_PiM[simp]: "prod_emb I M K X \<subseteq> space (PiM I M)"
   1.240    by (auto simp: prod_emb_def space_PiM)
   1.241  
   1.242 -lemma space_PiM_empty_iff[simp]: "space (PiM I M) = {} \<longleftrightarrow>  (\<exists>i\<in>I. space (M i) = {})"
   1.243 +lemma%unimportant space_PiM_empty_iff[simp]: "space (PiM I M) = {} \<longleftrightarrow>  (\<exists>i\<in>I. space (M i) = {})"
   1.244    by (auto simp: space_PiM PiE_eq_empty_iff)
   1.245  
   1.246 -lemma undefined_in_PiM_empty[simp]: "(\<lambda>x. undefined) \<in> space (PiM {} M)"
   1.247 +lemma%unimportant undefined_in_PiM_empty[simp]: "(\<lambda>x. undefined) \<in> space (PiM {} M)"
   1.248    by (auto simp: space_PiM)
   1.249  
   1.250 -lemma sets_PiM: "sets (\<Pi>\<^sub>M i\<in>I. M i) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) (prod_algebra I M)"
   1.251 +lemma%unimportant sets_PiM: "sets (\<Pi>\<^sub>M i\<in>I. M i) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) (prod_algebra I M)"
   1.252    using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro sets_extend_measure) simp
   1.253  
   1.254 -lemma sets_PiM_single: "sets (PiM I M) =
   1.255 +lemma%important sets_PiM_single: "sets (PiM I M) =
   1.256      sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {{f\<in>\<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A} | i A. i \<in> I \<and> A \<in> sets (M i)}"
   1.257      (is "_ = sigma_sets ?\<Omega> ?R")
   1.258    unfolding sets_PiM
   1.259 -proof (rule sigma_sets_eqI)
   1.260 +proof%unimportant (rule sigma_sets_eqI)
   1.261    interpret R: sigma_algebra ?\<Omega> "sigma_sets ?\<Omega> ?R" by (rule sigma_algebra_sigma_sets) auto
   1.262    fix A assume "A \<in> prod_algebra I M"
   1.263    from prod_algebraE[OF this] guess J X . note X = this
   1.264 @@ -388,7 +388,7 @@
   1.265    finally show "A \<in> sigma_sets ?\<Omega> (prod_algebra I M)" .
   1.266  qed
   1.267  
   1.268 -lemma sets_PiM_eq_proj:
   1.269 +lemma%unimportant sets_PiM_eq_proj:
   1.270    "I \<noteq> {} \<Longrightarrow> sets (PiM I M) = sets (SUP i:I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>x. x i) (M i))"
   1.271    apply (simp add: sets_PiM_single)
   1.272    apply (subst sets_Sup_eq[where X="\<Pi>\<^sub>E i\<in>I. space (M i)"])
   1.273 @@ -401,18 +401,18 @@
   1.274    apply (auto intro!: arg_cong2[where f=sigma_sets])
   1.275    done
   1.276  
   1.277 -lemma
   1.278 +lemma%unimportant (*FIX ME needs name *)
   1.279    shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\<lambda>k. undefined}"
   1.280      and sets_PiM_empty: "sets (Pi\<^sub>M {} M) = { {}, {\<lambda>k. undefined} }"
   1.281    by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)
   1.282  
   1.283 -lemma sets_PiM_sigma:
   1.284 +lemma%important sets_PiM_sigma:
   1.285    assumes \<Omega>_cover: "\<And>i. i \<in> I \<Longrightarrow> \<exists>S\<subseteq>E i. countable S \<and> \<Omega> i = \<Union>S"
   1.286    assumes E: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (\<Omega> i)"
   1.287    assumes J: "\<And>j. j \<in> J \<Longrightarrow> finite j" "\<Union>J = I"
   1.288    defines "P \<equiv> {{f\<in>(\<Pi>\<^sub>E i\<in>I. \<Omega> i). \<forall>i\<in>j. f i \<in> A i} | A j. j \<in> J \<and> A \<in> Pi j E}"
   1.289    shows "sets (\<Pi>\<^sub>M i\<in>I. sigma (\<Omega> i) (E i)) = sets (sigma (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P)"
   1.290 -proof cases
   1.291 +proof%unimportant cases
   1.292    assume "I = {}"
   1.293    with \<open>\<Union>J = I\<close> have "P = {{\<lambda>_. undefined}} \<or> P = {}"
   1.294      by (auto simp: P_def)
   1.295 @@ -496,21 +496,21 @@
   1.296    finally show "?thesis" .
   1.297  qed
   1.298  
   1.299 -lemma sets_PiM_in_sets:
   1.300 +lemma%unimportant sets_PiM_in_sets:
   1.301    assumes space: "space N = (\<Pi>\<^sub>E i\<in>I. space (M i))"
   1.302    assumes sets: "\<And>i A. i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> {x\<in>space N. x i \<in> A} \<in> sets N"
   1.303    shows "sets (\<Pi>\<^sub>M i \<in> I. M i) \<subseteq> sets N"
   1.304    unfolding sets_PiM_single space[symmetric]
   1.305    by (intro sets.sigma_sets_subset subsetI) (auto intro: sets)
   1.306  
   1.307 -lemma sets_PiM_cong[measurable_cong]:
   1.308 +lemma%unimportant sets_PiM_cong[measurable_cong]:
   1.309    assumes "I = J" "\<And>i. i \<in> J \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)"
   1.310    using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong)
   1.311  
   1.312 -lemma sets_PiM_I:
   1.313 +lemma%important sets_PiM_I:
   1.314    assumes "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)"
   1.315    shows "prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) \<in> sets (\<Pi>\<^sub>M i\<in>I. M i)"
   1.316 -proof cases
   1.317 +proof%unimportant cases
   1.318    assume "J = {}"
   1.319    then have "prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) = (\<Pi>\<^sub>E j\<in>I. space (M j))"
   1.320      by (auto simp: prod_emb_def)
   1.321 @@ -521,7 +521,7 @@
   1.322      by (force simp add: sets_PiM prod_algebra_def)
   1.323  qed
   1.324  
   1.325 -lemma measurable_PiM:
   1.326 +lemma%unimportant measurable_PiM:
   1.327    assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
   1.328    assumes sets: "\<And>X J. J \<noteq> {} \<or> I = {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)) \<Longrightarrow>
   1.329      f -` prod_emb I M J (Pi\<^sub>E J X) \<inter> space N \<in> sets N"
   1.330 @@ -533,13 +533,13 @@
   1.331    with sets[of J X] show "f -` A \<inter> space N \<in> sets N" by auto
   1.332  qed
   1.333  
   1.334 -lemma measurable_PiM_Collect:
   1.335 +lemma%important measurable_PiM_Collect:
   1.336    assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
   1.337    assumes sets: "\<And>X J. J \<noteq> {} \<or> I = {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)) \<Longrightarrow>
   1.338      {\<omega>\<in>space N. \<forall>i\<in>J. f \<omega> i \<in> X i} \<in> sets N"
   1.339    shows "f \<in> measurable N (PiM I M)"
   1.340    using sets_PiM prod_algebra_sets_into_space space
   1.341 -proof (rule measurable_sigma_sets)
   1.342 +proof%unimportant (rule measurable_sigma_sets)
   1.343    fix A assume "A \<in> prod_algebra I M"
   1.344    from prod_algebraE[OF this] guess J X . note X = this
   1.345    then have "f -` A \<inter> space N = {\<omega> \<in> space N. \<forall>i\<in>J. f \<omega> i \<in> X i}"
   1.346 @@ -548,7 +548,7 @@
   1.347    finally show "f -` A \<inter> space N \<in> sets N" .
   1.348  qed
   1.349  
   1.350 -lemma measurable_PiM_single:
   1.351 +lemma%unimportant measurable_PiM_single:
   1.352    assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
   1.353    assumes sets: "\<And>A i. i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> {\<omega> \<in> space N. f \<omega> i \<in> A} \<in> sets N"
   1.354    shows "f \<in> measurable N (PiM I M)"
   1.355 @@ -562,11 +562,11 @@
   1.356    finally show "f -` A \<inter> space N \<in> sets N" .
   1.357  qed (auto simp: space)
   1.358  
   1.359 -lemma measurable_PiM_single':
   1.360 +lemma%important measurable_PiM_single':
   1.361    assumes f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> measurable N (M i)"
   1.362      and "(\<lambda>\<omega> i. f i \<omega>) \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
   1.363    shows "(\<lambda>\<omega> i. f i \<omega>) \<in> measurable N (Pi\<^sub>M I M)"
   1.364 -proof (rule measurable_PiM_single)
   1.365 +proof%unimportant (rule measurable_PiM_single)
   1.366    fix A i assume A: "i \<in> I" "A \<in> sets (M i)"
   1.367    then have "{\<omega> \<in> space N. f i \<omega> \<in> A} = f i -` A \<inter> space N"
   1.368      by auto
   1.369 @@ -574,12 +574,12 @@
   1.370      using A f by (auto intro!: measurable_sets)
   1.371  qed fact
   1.372  
   1.373 -lemma sets_PiM_I_finite[measurable]:
   1.374 +lemma%unimportant sets_PiM_I_finite[measurable]:
   1.375    assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))"
   1.376    shows "(\<Pi>\<^sub>E j\<in>I. E j) \<in> sets (\<Pi>\<^sub>M i\<in>I. M i)"
   1.377    using sets_PiM_I[of I I E M] sets.sets_into_space[OF sets] \<open>finite I\<close> sets by auto
   1.378  
   1.379 -lemma measurable_component_singleton[measurable (raw)]:
   1.380 +lemma%unimportant measurable_component_singleton[measurable (raw)]:
   1.381    assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^sub>M I M) (M i)"
   1.382  proof (unfold measurable_def, intro CollectI conjI ballI)
   1.383    fix A assume "A \<in> sets (M i)"
   1.384 @@ -590,30 +590,30 @@
   1.385      using \<open>A \<in> sets (M i)\<close> \<open>i \<in> I\<close> by (auto intro!: sets_PiM_I)
   1.386  qed (insert \<open>i \<in> I\<close>, auto simp: space_PiM)
   1.387  
   1.388 -lemma measurable_component_singleton'[measurable_dest]:
   1.389 +lemma%unimportant measurable_component_singleton'[measurable_dest]:
   1.390    assumes f: "f \<in> measurable N (Pi\<^sub>M I M)"
   1.391    assumes g: "g \<in> measurable L N"
   1.392    assumes i: "i \<in> I"
   1.393    shows "(\<lambda>x. (f (g x)) i) \<in> measurable L (M i)"
   1.394    using measurable_compose[OF measurable_compose[OF g f] measurable_component_singleton, OF i] .
   1.395  
   1.396 -lemma measurable_PiM_component_rev:
   1.397 +lemma%unimportant measurable_PiM_component_rev:
   1.398    "i \<in> I \<Longrightarrow> f \<in> measurable (M i) N \<Longrightarrow> (\<lambda>x. f (x i)) \<in> measurable (PiM I M) N"
   1.399    by simp
   1.400  
   1.401 -lemma measurable_case_nat[measurable (raw)]:
   1.402 +lemma%unimportant measurable_case_nat[measurable (raw)]:
   1.403    assumes [measurable (raw)]: "i = 0 \<Longrightarrow> f \<in> measurable M N"
   1.404      "\<And>j. i = Suc j \<Longrightarrow> (\<lambda>x. g x j) \<in> measurable M N"
   1.405    shows "(\<lambda>x. case_nat (f x) (g x) i) \<in> measurable M N"
   1.406    by (cases i) simp_all
   1.407  
   1.408 -lemma measurable_case_nat'[measurable (raw)]:
   1.409 +lemma%unimportant measurable_case_nat'[measurable (raw)]:
   1.410    assumes fg[measurable]: "f \<in> measurable N M" "g \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)"
   1.411    shows "(\<lambda>x. case_nat (f x) (g x)) \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)"
   1.412    using fg[THEN measurable_space]
   1.413    by (auto intro!: measurable_PiM_single' simp add: space_PiM PiE_iff split: nat.split)
   1.414  
   1.415 -lemma measurable_add_dim[measurable]:
   1.416 +lemma%unimportant measurable_add_dim[measurable]:
   1.417    "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^sub>M I M \<Otimes>\<^sub>M M i) (Pi\<^sub>M (insert i I) M)"
   1.418      (is "?f \<in> measurable ?P ?I")
   1.419  proof (rule measurable_PiM_single)
   1.420 @@ -627,12 +627,12 @@
   1.421    finally show "{\<omega> \<in> space ?P. case_prod (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" .
   1.422  qed (auto simp: space_pair_measure space_PiM PiE_def)
   1.423  
   1.424 -lemma measurable_fun_upd:
   1.425 +lemma%important measurable_fun_upd:
   1.426    assumes I: "I = J \<union> {i}"
   1.427    assumes f[measurable]: "f \<in> measurable N (PiM J M)"
   1.428    assumes h[measurable]: "h \<in> measurable N (M i)"
   1.429    shows "(\<lambda>x. (f x) (i := h x)) \<in> measurable N (PiM I M)"
   1.430 -proof (intro measurable_PiM_single')
   1.431 +proof%unimportant (intro measurable_PiM_single')
   1.432    fix j assume "j \<in> I" then show "(\<lambda>\<omega>. ((f \<omega>)(i := h \<omega>)) j) \<in> measurable N (M j)"
   1.433      unfolding I by (cases "j = i") auto
   1.434  next
   1.435 @@ -641,14 +641,14 @@
   1.436      by (auto simp: space_PiM PiE_iff extensional_def)
   1.437  qed
   1.438  
   1.439 -lemma measurable_component_update:
   1.440 +lemma%unimportant measurable_component_update:
   1.441    "x \<in> space (Pi\<^sub>M I M) \<Longrightarrow> i \<notin> I \<Longrightarrow> (\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^sub>M (insert i I) M)"
   1.442    by simp
   1.443  
   1.444 -lemma measurable_merge[measurable]:
   1.445 +lemma%important measurable_merge[measurable]:
   1.446    "merge I J \<in> measurable (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M)"
   1.447      (is "?f \<in> measurable ?P ?U")
   1.448 -proof (rule measurable_PiM_single)
   1.449 +proof%unimportant (rule measurable_PiM_single)
   1.450    fix i A assume A: "A \<in> sets (M i)" "i \<in> I \<union> J"
   1.451    then have "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} =
   1.452      (if i \<in> I then ((\<lambda>x. x i) \<circ> fst) -` A \<inter> space ?P else ((\<lambda>x. x i) \<circ> snd) -` A \<inter> space ?P)"
   1.453 @@ -659,7 +659,7 @@
   1.454    finally show "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} \<in> sets ?P" .
   1.455  qed (auto simp: space_pair_measure space_PiM PiE_iff merge_def extensional_def)
   1.456  
   1.457 -lemma measurable_restrict[measurable (raw)]:
   1.458 +lemma%unimportant measurable_restrict[measurable (raw)]:
   1.459    assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)"
   1.460    shows "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable N (Pi\<^sub>M I M)"
   1.461  proof (rule measurable_PiM_single)
   1.462 @@ -670,14 +670,14 @@
   1.463      using A X by (auto intro!: measurable_sets)
   1.464  qed (insert X, auto simp add: PiE_def dest: measurable_space)
   1.465  
   1.466 -lemma measurable_abs_UNIV:
   1.467 +lemma%unimportant measurable_abs_UNIV:
   1.468    "(\<And>n. (\<lambda>\<omega>. f n \<omega>) \<in> measurable M (N n)) \<Longrightarrow> (\<lambda>\<omega> n. f n \<omega>) \<in> measurable M (PiM UNIV N)"
   1.469    by (intro measurable_PiM_single) (auto dest: measurable_space)
   1.470  
   1.471 -lemma measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)"
   1.472 +lemma%unimportant measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)"
   1.473    by (intro measurable_restrict measurable_component_singleton) auto
   1.474  
   1.475 -lemma measurable_restrict_subset':
   1.476 +lemma%unimportant measurable_restrict_subset':
   1.477    assumes "J \<subseteq> L" "\<And>x. x \<in> J \<Longrightarrow> sets (M x) = sets (N x)"
   1.478    shows "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)"
   1.479  proof-
   1.480 @@ -688,12 +688,12 @@
   1.481    finally show ?thesis .
   1.482  qed
   1.483  
   1.484 -lemma measurable_prod_emb[intro, simp]:
   1.485 +lemma%unimportant measurable_prod_emb[intro, simp]:
   1.486    "J \<subseteq> L \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> prod_emb L M J X \<in> sets (Pi\<^sub>M L M)"
   1.487    unfolding prod_emb_def space_PiM[symmetric]
   1.488    by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton)
   1.489  
   1.490 -lemma merge_in_prod_emb:
   1.491 +lemma%unimportant merge_in_prod_emb:
   1.492    assumes "y \<in> space (PiM I M)" "x \<in> X" and X: "X \<in> sets (Pi\<^sub>M J M)" and "J \<subseteq> I"
   1.493    shows "merge J I (x, y) \<in> prod_emb I M J X"
   1.494    using assms sets.sets_into_space[OF X]
   1.495 @@ -701,7 +701,7 @@
   1.496             cong: if_cong restrict_cong)
   1.497       (simp add: extensional_def)
   1.498  
   1.499 -lemma prod_emb_eq_emptyD:
   1.500 +lemma%unimportant prod_emb_eq_emptyD:
   1.501    assumes J: "J \<subseteq> I" and ne: "space (PiM I M) \<noteq> {}" and X: "X \<in> sets (Pi\<^sub>M J M)"
   1.502      and *: "prod_emb I M J X = {}"
   1.503    shows "X = {}"
   1.504 @@ -712,19 +712,19 @@
   1.505    from merge_in_prod_emb[OF this \<open>x\<in>X\<close> X J] * show "x \<in> {}" by auto
   1.506  qed
   1.507  
   1.508 -lemma sets_in_Pi_aux:
   1.509 +lemma%unimportant sets_in_Pi_aux:
   1.510    "finite I \<Longrightarrow> (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
   1.511    {x\<in>space (PiM I M). x \<in> Pi I F} \<in> sets (PiM I M)"
   1.512    by (simp add: subset_eq Pi_iff)
   1.513  
   1.514 -lemma sets_in_Pi[measurable (raw)]:
   1.515 +lemma%unimportant sets_in_Pi[measurable (raw)]:
   1.516    "finite I \<Longrightarrow> f \<in> measurable N (PiM I M) \<Longrightarrow>
   1.517    (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
   1.518    Measurable.pred N (\<lambda>x. f x \<in> Pi I F)"
   1.519    unfolding pred_def
   1.520    by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto
   1.521  
   1.522 -lemma sets_in_extensional_aux:
   1.523 +lemma%unimportant sets_in_extensional_aux:
   1.524    "{x\<in>space (PiM I M). x \<in> extensional I} \<in> sets (PiM I M)"
   1.525  proof -
   1.526    have "{x\<in>space (PiM I M). x \<in> extensional I} = space (PiM I M)"
   1.527 @@ -732,12 +732,12 @@
   1.528    then show ?thesis by simp
   1.529  qed
   1.530  
   1.531 -lemma sets_in_extensional[measurable (raw)]:
   1.532 +lemma%unimportant sets_in_extensional[measurable (raw)]:
   1.533    "f \<in> measurable N (PiM I M) \<Longrightarrow> Measurable.pred N (\<lambda>x. f x \<in> extensional I)"
   1.534    unfolding pred_def
   1.535    by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto
   1.536  
   1.537 -lemma sets_PiM_I_countable:
   1.538 +lemma%unimportant sets_PiM_I_countable:
   1.539    assumes I: "countable I" and E: "\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i)" shows "Pi\<^sub>E I E \<in> sets (Pi\<^sub>M I M)"
   1.540  proof cases
   1.541    assume "I \<noteq> {}"
   1.542 @@ -748,11 +748,11 @@
   1.543    finally show ?thesis .
   1.544  qed (simp add: sets_PiM_empty)
   1.545  
   1.546 -lemma sets_PiM_D_countable:
   1.547 +lemma%important sets_PiM_D_countable:
   1.548    assumes A: "A \<in> PiM I M"
   1.549    shows "\<exists>J\<subseteq>I. \<exists>X\<in>PiM J M. countable J \<and> A = prod_emb I M J X"
   1.550    using A[unfolded sets_PiM_single]
   1.551 -proof induction
   1.552 +proof%unimportant induction
   1.553    case (Basic A)
   1.554    then obtain i X where *: "i \<in> I" "X \<in> sets (M i)" and "A = {f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> X}"
   1.555      by auto
   1.556 @@ -784,12 +784,12 @@
   1.557    qed(auto intro: X)
   1.558  qed
   1.559  
   1.560 -lemma measure_eqI_PiM_finite:
   1.561 +lemma%important measure_eqI_PiM_finite:
   1.562    assumes [simp]: "finite I" "sets P = PiM I M" "sets Q = PiM I M"
   1.563    assumes eq: "\<And>A. (\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> P (Pi\<^sub>E I A) = Q (Pi\<^sub>E I A)"
   1.564    assumes A: "range A \<subseteq> prod_algebra I M" "(\<Union>i. A i) = space (PiM I M)" "\<And>i::nat. P (A i) \<noteq> \<infinity>"
   1.565    shows "P = Q"
   1.566 -proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space])
   1.567 +proof%unimportant (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space])
   1.568    show "range A \<subseteq> prod_algebra I M" "(\<Union>i. A i) = (\<Pi>\<^sub>E i\<in>I. space (M i))" "\<And>i. P (A i) \<noteq> \<infinity>"
   1.569      unfolding space_PiM[symmetric] by fact+
   1.570    fix X assume "X \<in> prod_algebra I M"
   1.571 @@ -800,13 +800,13 @@
   1.572      unfolding X by (subst (1 2) prod_emb_Pi) (auto simp: eq)
   1.573  qed (simp_all add: sets_PiM)
   1.574  
   1.575 -lemma measure_eqI_PiM_infinite:
   1.576 +lemma%important measure_eqI_PiM_infinite:
   1.577    assumes [simp]: "sets P = PiM I M" "sets Q = PiM I M"
   1.578    assumes eq: "\<And>A J. finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow>
   1.579      P (prod_emb I M J (Pi\<^sub>E J A)) = Q (prod_emb I M J (Pi\<^sub>E J A))"
   1.580    assumes A: "finite_measure P"
   1.581    shows "P = Q"
   1.582 -proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space])
   1.583 +proof%unimportant (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space])
   1.584    interpret finite_measure P by fact
   1.585    define i where "i = (SOME i. i \<in> I)"
   1.586    have i: "I \<noteq> {} \<Longrightarrow> i \<in> I"
   1.587 @@ -829,23 +829,23 @@
   1.588      by (auto intro!: eq)
   1.589  qed (auto simp: sets_PiM)
   1.590  
   1.591 -locale product_sigma_finite =
   1.592 +locale%unimportant product_sigma_finite =
   1.593    fixes M :: "'i \<Rightarrow> 'a measure"
   1.594    assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
   1.595  
   1.596 -sublocale product_sigma_finite \<subseteq> M?: sigma_finite_measure "M i" for i
   1.597 +sublocale%unimportant product_sigma_finite \<subseteq> M?: sigma_finite_measure "M i" for i
   1.598    by (rule sigma_finite_measures)
   1.599  
   1.600 -locale finite_product_sigma_finite = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" +
   1.601 +locale%unimportant finite_product_sigma_finite = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" +
   1.602    fixes I :: "'i set"
   1.603    assumes finite_index: "finite I"
   1.604  
   1.605 -lemma (in finite_product_sigma_finite) sigma_finite_pairs:
   1.606 +lemma%important (in finite_product_sigma_finite) sigma_finite_pairs:
   1.607    "\<exists>F::'i \<Rightarrow> nat \<Rightarrow> 'a set.
   1.608      (\<forall>i\<in>I. range (F i) \<subseteq> sets (M i)) \<and>
   1.609      (\<forall>k. \<forall>i\<in>I. emeasure (M i) (F i k) \<noteq> \<infinity>) \<and> incseq (\<lambda>k. \<Pi>\<^sub>E i\<in>I. F i k) \<and>
   1.610      (\<Union>k. \<Pi>\<^sub>E i\<in>I. F i k) = space (PiM I M)"
   1.611 -proof -
   1.612 +proof%unimportant -
   1.613    have "\<forall>i::'i. \<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> sets (M i) \<and> incseq F \<and> (\<Union>i. F i) = space (M i) \<and> (\<forall>k. emeasure (M i) (F k) \<noteq> \<infinity>)"
   1.614      using M.sigma_finite_incseq by metis
   1.615    from choice[OF this] guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
   1.616 @@ -871,7 +871,7 @@
   1.617    qed
   1.618  qed
   1.619  
   1.620 -lemma emeasure_PiM_empty[simp]: "emeasure (PiM {} M) {\<lambda>_. undefined} = 1"
   1.621 +lemma%unimportant emeasure_PiM_empty[simp]: "emeasure (PiM {} M) {\<lambda>_. undefined} = 1"
   1.622  proof -
   1.623    let ?\<mu> = "\<lambda>A. if A = {} then 0 else (1::ennreal)"
   1.624    have "emeasure (Pi\<^sub>M {} M) (prod_emb {} M {} (\<Pi>\<^sub>E i\<in>{}. {})) = 1"
   1.625 @@ -888,12 +888,12 @@
   1.626      by simp
   1.627  qed
   1.628  
   1.629 -lemma PiM_empty: "PiM {} M = count_space {\<lambda>_. undefined}"
   1.630 +lemma%unimportant PiM_empty: "PiM {} M = count_space {\<lambda>_. undefined}"
   1.631    by (rule measure_eqI) (auto simp add: sets_PiM_empty)
   1.632  
   1.633 -lemma (in product_sigma_finite) emeasure_PiM:
   1.634 +lemma%important (in product_sigma_finite) emeasure_PiM:
   1.635    "finite I \<Longrightarrow> (\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (PiM I M) (Pi\<^sub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
   1.636 -proof (induct I arbitrary: A rule: finite_induct)
   1.637 +proof%unimportant (induct I arbitrary: A rule: finite_induct)
   1.638    case (insert i I)
   1.639    interpret finite_product_sigma_finite M I by standard fact
   1.640    have "finite (insert i I)" using \<open>finite I\<close> by auto
   1.641 @@ -948,7 +948,7 @@
   1.642      by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space)
   1.643  qed simp
   1.644  
   1.645 -lemma (in product_sigma_finite) PiM_eqI:
   1.646 +lemma%unimportant (in product_sigma_finite) PiM_eqI:
   1.647    assumes I[simp]: "finite I" and P: "sets P = PiM I M"
   1.648    assumes eq: "\<And>A. (\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> P (Pi\<^sub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
   1.649    shows "P = PiM I M"
   1.650 @@ -966,7 +966,7 @@
   1.651    qed
   1.652  qed
   1.653  
   1.654 -lemma (in product_sigma_finite) sigma_finite:
   1.655 +lemma%unimportant (in product_sigma_finite) sigma_finite:
   1.656    assumes "finite I"
   1.657    shows "sigma_finite_measure (PiM I M)"
   1.658  proof
   1.659 @@ -987,19 +987,19 @@
   1.660  sublocale finite_product_sigma_finite \<subseteq> sigma_finite_measure "Pi\<^sub>M I M"
   1.661    using sigma_finite[OF finite_index] .
   1.662  
   1.663 -lemma (in finite_product_sigma_finite) measure_times:
   1.664 +lemma%unimportant (in finite_product_sigma_finite) measure_times:
   1.665    "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (Pi\<^sub>M I M) (Pi\<^sub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
   1.666    using emeasure_PiM[OF finite_index] by auto
   1.667  
   1.668 -lemma (in product_sigma_finite) nn_integral_empty:
   1.669 +lemma%unimportant (in product_sigma_finite) nn_integral_empty:
   1.670    "0 \<le> f (\<lambda>k. undefined) \<Longrightarrow> integral\<^sup>N (Pi\<^sub>M {} M) f = f (\<lambda>k. undefined)"
   1.671    by (simp add: PiM_empty nn_integral_count_space_finite max.absorb2)
   1.672  
   1.673 -lemma (in product_sigma_finite) distr_merge:
   1.674 +lemma%important (in product_sigma_finite) distr_merge:
   1.675    assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
   1.676    shows "distr (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M) (merge I J) = Pi\<^sub>M (I \<union> J) M"
   1.677     (is "?D = ?P")
   1.678 -proof (rule PiM_eqI)
   1.679 +proof%unimportant (rule PiM_eqI)
   1.680    interpret I: finite_product_sigma_finite M I by standard fact
   1.681    interpret J: finite_product_sigma_finite M J by standard fact
   1.682    fix A assume A: "\<And>i. i \<in> I \<union> J \<Longrightarrow> A i \<in> sets (M i)"
   1.683 @@ -1011,12 +1011,12 @@
   1.684         (auto simp: * J.emeasure_pair_measure_Times I.measure_times J.measure_times prod.union_disjoint)
   1.685  qed (insert fin, simp_all)
   1.686  
   1.687 -lemma (in product_sigma_finite) product_nn_integral_fold:
   1.688 +lemma%important (in product_sigma_finite) product_nn_integral_fold:
   1.689    assumes IJ: "I \<inter> J = {}" "finite I" "finite J"
   1.690    and f[measurable]: "f \<in> borel_measurable (Pi\<^sub>M (I \<union> J) M)"
   1.691    shows "integral\<^sup>N (Pi\<^sub>M (I \<union> J) M) f =
   1.692      (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (merge I J (x, y)) \<partial>(Pi\<^sub>M J M)) \<partial>(Pi\<^sub>M I M))"
   1.693 -proof -
   1.694 +proof%unimportant -
   1.695    interpret I: finite_product_sigma_finite M I by standard fact
   1.696    interpret J: finite_product_sigma_finite M J by standard fact
   1.697    interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by standard
   1.698 @@ -1031,7 +1031,7 @@
   1.699      done
   1.700  qed
   1.701  
   1.702 -lemma (in product_sigma_finite) distr_singleton:
   1.703 +lemma%unimportant (in product_sigma_finite) distr_singleton:
   1.704    "distr (Pi\<^sub>M {i} M) (M i) (\<lambda>x. x i) = M i" (is "?D = _")
   1.705  proof (intro measure_eqI[symmetric])
   1.706    interpret I: finite_product_sigma_finite M "{i}" by standard simp
   1.707 @@ -1043,7 +1043,7 @@
   1.708      by (simp add: emeasure_distr measurable_component_singleton)
   1.709  qed simp
   1.710  
   1.711 -lemma (in product_sigma_finite) product_nn_integral_singleton:
   1.712 +lemma%unimportant (in product_sigma_finite) product_nn_integral_singleton:
   1.713    assumes f: "f \<in> borel_measurable (M i)"
   1.714    shows "integral\<^sup>N (Pi\<^sub>M {i} M) (\<lambda>x. f (x i)) = integral\<^sup>N (M i) f"
   1.715  proof -
   1.716 @@ -1055,11 +1055,11 @@
   1.717      done
   1.718  qed
   1.719  
   1.720 -lemma (in product_sigma_finite) product_nn_integral_insert:
   1.721 +lemma%important (in product_sigma_finite) product_nn_integral_insert:
   1.722    assumes I[simp]: "finite I" "i \<notin> I"
   1.723      and f: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
   1.724    shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x(i := y)) \<partial>(M i)) \<partial>(Pi\<^sub>M I M))"
   1.725 -proof -
   1.726 +proof%unimportant -
   1.727    interpret I: finite_product_sigma_finite M I by standard auto
   1.728    interpret i: finite_product_sigma_finite M "{i}" by standard auto
   1.729    have IJ: "I \<inter> {i} = {}" and insert: "I \<union> {i} = insert i I"
   1.730 @@ -1079,7 +1079,7 @@
   1.731    qed
   1.732  qed
   1.733  
   1.734 -lemma (in product_sigma_finite) product_nn_integral_insert_rev:
   1.735 +lemma%unimportant (in product_sigma_finite) product_nn_integral_insert_rev:
   1.736    assumes I[simp]: "finite I" "i \<notin> I"
   1.737      and [measurable]: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
   1.738    shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x(i := y)) \<partial>(Pi\<^sub>M I M)) \<partial>(M i))"
   1.739 @@ -1090,7 +1090,7 @@
   1.740    apply measurable
   1.741    done
   1.742  
   1.743 -lemma (in product_sigma_finite) product_nn_integral_prod:
   1.744 +lemma%unimportant (in product_sigma_finite) product_nn_integral_prod:
   1.745    assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
   1.746    shows "(\<integral>\<^sup>+ x. (\<Prod>i\<in>I. f i (x i)) \<partial>Pi\<^sub>M I M) = (\<Prod>i\<in>I. integral\<^sup>N (M i) (f i))"
   1.747  using assms proof (induction I)
   1.748 @@ -1113,11 +1113,11 @@
   1.749      done
   1.750  qed (simp add: space_PiM)
   1.751  
   1.752 -lemma (in product_sigma_finite) product_nn_integral_pair:
   1.753 +lemma%important (in product_sigma_finite) product_nn_integral_pair:
   1.754    assumes [measurable]: "case_prod f \<in> borel_measurable (M x \<Otimes>\<^sub>M M y)"
   1.755    assumes xy: "x \<noteq> y"
   1.756    shows "(\<integral>\<^sup>+\<sigma>. f (\<sigma> x) (\<sigma> y) \<partial>PiM {x, y} M) = (\<integral>\<^sup>+z. f (fst z) (snd z) \<partial>(M x \<Otimes>\<^sub>M M y))"
   1.757 -proof-
   1.758 +proof%unimportant -
   1.759    interpret psm: pair_sigma_finite "M x" "M y"
   1.760      unfolding pair_sigma_finite_def using sigma_finite_measures by simp_all
   1.761    have "{x, y} = {y, x}" by auto
   1.762 @@ -1130,7 +1130,7 @@
   1.763    finally show ?thesis .
   1.764  qed
   1.765  
   1.766 -lemma (in product_sigma_finite) distr_component:
   1.767 +lemma%unimportant (in product_sigma_finite) distr_component:
   1.768    "distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^sub>M {i} M" (is "?D = ?P")
   1.769  proof (intro PiM_eqI)
   1.770    fix A assume A: "\<And>ia. ia \<in> {i} \<Longrightarrow> A ia \<in> sets (M ia)"
   1.771 @@ -1140,7 +1140,7 @@
   1.772      by (subst emeasure_distr) (auto intro!: sets_PiM_I_finite measurable_restrict)
   1.773  qed simp_all
   1.774  
   1.775 -lemma (in product_sigma_finite)
   1.776 +lemma%unimportant (in product_sigma_finite)
   1.777    assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^sub>M (I \<union> J) M)"
   1.778    shows emeasure_fold_integral:
   1.779      "emeasure (Pi\<^sub>M (I \<union> J) M) A = (\<integral>\<^sup>+x. emeasure (Pi\<^sub>M J M) ((\<lambda>y. merge I J (x, y)) -` A \<inter> space (Pi\<^sub>M J M)) \<partial>Pi\<^sub>M I M)" (is ?I)
   1.780 @@ -1165,11 +1165,11 @@
   1.781      by (simp add: vimage_comp comp_def space_pair_measure cong: measurable_cong)
   1.782  qed
   1.783  
   1.784 -lemma sets_Collect_single:
   1.785 +lemma%unimportant sets_Collect_single:
   1.786    "i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> { x \<in> space (Pi\<^sub>M I M). x i \<in> A } \<in> sets (Pi\<^sub>M I M)"
   1.787    by simp
   1.788  
   1.789 -lemma pair_measure_eq_distr_PiM:
   1.790 +lemma%unimportant pair_measure_eq_distr_PiM:
   1.791    fixes M1 :: "'a measure" and M2 :: "'a measure"
   1.792    assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
   1.793    shows "(M1 \<Otimes>\<^sub>M M2) = distr (Pi\<^sub>M UNIV (case_bool M1 M2)) (M1 \<Otimes>\<^sub>M M2) (\<lambda>x. (x True, x False))"
   1.794 @@ -1196,7 +1196,7 @@
   1.795      by (subst emeasure_distr) (auto simp: measurable_pair_iff)
   1.796  qed simp
   1.797  
   1.798 -lemma infprod_in_sets[intro]:
   1.799 +lemma%unimportant infprod_in_sets[intro]:
   1.800    fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets (M i)"
   1.801    shows "Pi UNIV E \<in> sets (\<Pi>\<^sub>M i\<in>UNIV::nat set. M i)"
   1.802  proof -