src/HOL/Analysis/Bochner_Integration.thy
changeset 68833 fde093888c16
parent 68798 07714b60f653
child 69064 5840724b1d71
     1.1 --- a/src/HOL/Analysis/Bochner_Integration.thy	Mon Aug 27 22:58:36 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Bochner_Integration.thy	Tue Aug 28 13:28:39 2018 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Johannes Hölzl, TU München
     1.5  *)
     1.6  
     1.7 -section \<open>Bochner Integration for Vector-Valued Functions\<close>
     1.8 +section%important \<open>Bochner Integration for Vector-Valued Functions\<close>
     1.9  
    1.10  theory Bochner_Integration
    1.11    imports Finite_Product_Measure
    1.12 @@ -15,12 +15,12 @@
    1.13  
    1.14  \<close>
    1.15  
    1.16 -lemma borel_measurable_implies_sequence_metric:
    1.17 +lemma%important borel_measurable_implies_sequence_metric:
    1.18    fixes f :: "'a \<Rightarrow> 'b :: {metric_space, second_countable_topology}"
    1.19    assumes [measurable]: "f \<in> borel_measurable M"
    1.20    shows "\<exists>F. (\<forall>i. simple_function M (F i)) \<and> (\<forall>x\<in>space M. (\<lambda>i. F i x) \<longlonglongrightarrow> f x) \<and>
    1.21      (\<forall>i. \<forall>x\<in>space M. dist (F i x) z \<le> 2 * dist (f x) z)"
    1.22 -proof -
    1.23 +proof%unimportant -
    1.24    obtain D :: "'b set" where "countable D" and D: "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d\<in>D. d \<in> X"
    1.25      by (erule countable_dense_setE)
    1.26  
    1.27 @@ -155,14 +155,14 @@
    1.28    qed
    1.29  qed
    1.30  
    1.31 -lemma
    1.32 +lemma%unimportant
    1.33    fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A"
    1.34    shows sum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator (B x) (g x)) = (\<Sum>x\<in>{x\<in>A. g x \<in> B x}. f x)"
    1.35    and sum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator (B x) (g x) * f x) = (\<Sum>x\<in>{x\<in>A. g x \<in> B x}. f x)"
    1.36    unfolding indicator_def
    1.37    using assms by (auto intro!: sum.mono_neutral_cong_right split: if_split_asm)
    1.38  
    1.39 -lemma borel_measurable_induct_real[consumes 2, case_names set mult add seq]:
    1.40 +lemma%unimportant borel_measurable_induct_real[consumes 2, case_names set mult add seq]:
    1.41    fixes P :: "('a \<Rightarrow> real) \<Rightarrow> bool"
    1.42    assumes u: "u \<in> borel_measurable M" "\<And>x. 0 \<le> u x"
    1.43    assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"
    1.44 @@ -227,7 +227,7 @@
    1.45    qed
    1.46  qed
    1.47  
    1.48 -lemma scaleR_cong_right:
    1.49 +lemma%unimportant scaleR_cong_right:
    1.50    fixes x :: "'a :: real_vector"
    1.51    shows "(x \<noteq> 0 \<Longrightarrow> r = p) \<Longrightarrow> r *\<^sub>R x = p *\<^sub>R x"
    1.52    by (cases "x = 0") auto
    1.53 @@ -236,7 +236,7 @@
    1.54    "simple_function M f \<Longrightarrow> emeasure M {y\<in>space M. f y \<noteq> 0} \<noteq> \<infinity> \<Longrightarrow>
    1.55      simple_bochner_integrable M f"
    1.56  
    1.57 -lemma simple_bochner_integrable_compose2:
    1.58 +lemma%unimportant simple_bochner_integrable_compose2:
    1.59    assumes p_0: "p 0 0 = 0"
    1.60    shows "simple_bochner_integrable M f \<Longrightarrow> simple_bochner_integrable M g \<Longrightarrow>
    1.61      simple_bochner_integrable M (\<lambda>x. p (f x) (g x))"
    1.62 @@ -261,7 +261,7 @@
    1.63      using fin by (auto simp: top_unique)
    1.64  qed
    1.65  
    1.66 -lemma simple_function_finite_support:
    1.67 +lemma%unimportant simple_function_finite_support:
    1.68    assumes f: "simple_function M f" and fin: "(\<integral>\<^sup>+x. f x \<partial>M) < \<infinity>" and nn: "\<And>x. 0 \<le> f x"
    1.69    shows "emeasure M {x\<in>space M. f x \<noteq> 0} \<noteq> \<infinity>"
    1.70  proof cases
    1.71 @@ -296,7 +296,7 @@
    1.72    show ?thesis unfolding * by simp
    1.73  qed
    1.74  
    1.75 -lemma simple_bochner_integrableI_bounded:
    1.76 +lemma%unimportant simple_bochner_integrableI_bounded:
    1.77    assumes f: "simple_function M f" and fin: "(\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
    1.78    shows "simple_bochner_integrable M f"
    1.79  proof
    1.80 @@ -309,16 +309,16 @@
    1.81    then show "emeasure M {y \<in> space M. f y \<noteq> 0} \<noteq> \<infinity>" by simp
    1.82  qed fact
    1.83  
    1.84 -definition simple_bochner_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b::real_vector) \<Rightarrow> 'b" where
    1.85 +definition%important simple_bochner_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b::real_vector) \<Rightarrow> 'b" where
    1.86    "simple_bochner_integral M f = (\<Sum>y\<in>f`space M. measure M {x\<in>space M. f x = y} *\<^sub>R y)"
    1.87  
    1.88 -lemma simple_bochner_integral_partition:
    1.89 +lemma%important simple_bochner_integral_partition:
    1.90    assumes f: "simple_bochner_integrable M f" and g: "simple_function M g"
    1.91    assumes sub: "\<And>x y. x \<in> space M \<Longrightarrow> y \<in> space M \<Longrightarrow> g x = g y \<Longrightarrow> f x = f y"
    1.92    assumes v: "\<And>x. x \<in> space M \<Longrightarrow> f x = v (g x)"
    1.93    shows "simple_bochner_integral M f = (\<Sum>y\<in>g ` space M. measure M {x\<in>space M. g x = y} *\<^sub>R v y)"
    1.94      (is "_ = ?r")
    1.95 -proof -
    1.96 +proof%unimportant -
    1.97    from f g have [simp]: "finite (f`space M)" "finite (g`space M)"
    1.98      by (auto simp: simple_function_def elim: simple_bochner_integrable.cases)
    1.99  
   1.100 @@ -394,7 +394,7 @@
   1.101      by (simp add: sum.distrib[symmetric] scaleR_add_right)
   1.102  qed
   1.103  
   1.104 -lemma simple_bochner_integral_linear:
   1.105 +lemma%unimportant simple_bochner_integral_linear:
   1.106    assumes "linear f"
   1.107    assumes g: "simple_bochner_integrable M g"
   1.108    shows "simple_bochner_integral M (\<lambda>x. f (g x)) = f (simple_bochner_integral M g)"
   1.109 @@ -484,14 +484,14 @@
   1.110    finally show ?thesis .
   1.111  qed
   1.112  
   1.113 -lemma simple_bochner_integral_bounded:
   1.114 +lemma%important simple_bochner_integral_bounded:
   1.115    fixes f :: "'a \<Rightarrow> 'b::{real_normed_vector, second_countable_topology}"
   1.116    assumes f[measurable]: "f \<in> borel_measurable M"
   1.117    assumes s: "simple_bochner_integrable M s" and t: "simple_bochner_integrable M t"
   1.118    shows "ennreal (norm (simple_bochner_integral M s - simple_bochner_integral M t)) \<le>
   1.119      (\<integral>\<^sup>+ x. norm (f x - s x) \<partial>M) + (\<integral>\<^sup>+ x. norm (f x - t x) \<partial>M)"
   1.120      (is "ennreal (norm (?s - ?t)) \<le> ?S + ?T")
   1.121 -proof -
   1.122 +proof%unimportant -
   1.123    have [measurable]: "s \<in> borel_measurable M" "t \<in> borel_measurable M"
   1.124      using s t by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases)
   1.125  
   1.126 @@ -520,13 +520,13 @@
   1.127      (\<lambda>i. simple_bochner_integral M (s i)) \<longlonglongrightarrow> x \<Longrightarrow>
   1.128      has_bochner_integral M f x"
   1.129  
   1.130 -lemma has_bochner_integral_cong:
   1.131 +lemma%unimportant has_bochner_integral_cong:
   1.132    assumes "M = N" "\<And>x. x \<in> space N \<Longrightarrow> f x = g x" "x = y"
   1.133    shows "has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral N g y"
   1.134    unfolding has_bochner_integral.simps assms(1,3)
   1.135    using assms(2) by (simp cong: measurable_cong_strong nn_integral_cong_strong)
   1.136  
   1.137 -lemma has_bochner_integral_cong_AE:
   1.138 +lemma%unimportant has_bochner_integral_cong_AE:
   1.139    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow>
   1.140      has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral M g x"
   1.141    unfolding has_bochner_integral.simps
   1.142 @@ -534,22 +534,22 @@
   1.143              nn_integral_cong_AE)
   1.144       auto
   1.145  
   1.146 -lemma borel_measurable_has_bochner_integral:
   1.147 +lemma%unimportant borel_measurable_has_bochner_integral:
   1.148    "has_bochner_integral M f x \<Longrightarrow> f \<in> borel_measurable M"
   1.149    by (rule has_bochner_integral.cases)
   1.150  
   1.151 -lemma borel_measurable_has_bochner_integral'[measurable_dest]:
   1.152 +lemma%unimportant borel_measurable_has_bochner_integral'[measurable_dest]:
   1.153    "has_bochner_integral M f x \<Longrightarrow> g \<in> measurable N M \<Longrightarrow> (\<lambda>x. f (g x)) \<in> borel_measurable N"
   1.154    using borel_measurable_has_bochner_integral[measurable] by measurable
   1.155  
   1.156 -lemma has_bochner_integral_simple_bochner_integrable:
   1.157 +lemma%unimportant has_bochner_integral_simple_bochner_integrable:
   1.158    "simple_bochner_integrable M f \<Longrightarrow> has_bochner_integral M f (simple_bochner_integral M f)"
   1.159    by (rule has_bochner_integral.intros[where s="\<lambda>_. f"])
   1.160       (auto intro: borel_measurable_simple_function
   1.161             elim: simple_bochner_integrable.cases
   1.162             simp: zero_ennreal_def[symmetric])
   1.163  
   1.164 -lemma has_bochner_integral_real_indicator:
   1.165 +lemma%unimportant has_bochner_integral_real_indicator:
   1.166    assumes [measurable]: "A \<in> sets M" and A: "emeasure M A < \<infinity>"
   1.167    shows "has_bochner_integral M (indicator A) (measure M A)"
   1.168  proof -
   1.169 @@ -567,7 +567,7 @@
   1.170      by (metis has_bochner_integral_simple_bochner_integrable)
   1.171  qed
   1.172  
   1.173 -lemma has_bochner_integral_add[intro]:
   1.174 +lemma%unimportant has_bochner_integral_add[intro]:
   1.175    "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M g y \<Longrightarrow>
   1.176      has_bochner_integral M (\<lambda>x. f x + g x) (x + y)"
   1.177  proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
   1.178 @@ -604,7 +604,7 @@
   1.179    qed
   1.180  qed (auto simp: simple_bochner_integral_add tendsto_add)
   1.181  
   1.182 -lemma has_bochner_integral_bounded_linear:
   1.183 +lemma%unimportant has_bochner_integral_bounded_linear:
   1.184    assumes "bounded_linear T"
   1.185    shows "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M (\<lambda>x. T (f x)) (T x)"
   1.186  proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
   1.187 @@ -650,79 +650,79 @@
   1.188      by (auto intro!: T.tendsto simp: simple_bochner_integral_linear T.linear_axioms)
   1.189  qed
   1.190  
   1.191 -lemma has_bochner_integral_zero[intro]: "has_bochner_integral M (\<lambda>x. 0) 0"
   1.192 +lemma%unimportant has_bochner_integral_zero[intro]: "has_bochner_integral M (\<lambda>x. 0) 0"
   1.193    by (auto intro!: has_bochner_integral.intros[where s="\<lambda>_ _. 0"]
   1.194             simp: zero_ennreal_def[symmetric] simple_bochner_integrable.simps
   1.195                   simple_bochner_integral_def image_constant_conv)
   1.196  
   1.197 -lemma has_bochner_integral_scaleR_left[intro]:
   1.198 +lemma%unimportant has_bochner_integral_scaleR_left[intro]:
   1.199    "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x *\<^sub>R c) (x *\<^sub>R c)"
   1.200    by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_scaleR_left])
   1.201  
   1.202 -lemma has_bochner_integral_scaleR_right[intro]:
   1.203 +lemma%unimportant has_bochner_integral_scaleR_right[intro]:
   1.204    "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. c *\<^sub>R f x) (c *\<^sub>R x)"
   1.205    by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_scaleR_right])
   1.206  
   1.207 -lemma has_bochner_integral_mult_left[intro]:
   1.208 +lemma%unimportant has_bochner_integral_mult_left[intro]:
   1.209    fixes c :: "_::{real_normed_algebra,second_countable_topology}"
   1.210    shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x * c) (x * c)"
   1.211    by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_mult_left])
   1.212  
   1.213 -lemma has_bochner_integral_mult_right[intro]:
   1.214 +lemma%unimportant has_bochner_integral_mult_right[intro]:
   1.215    fixes c :: "_::{real_normed_algebra,second_countable_topology}"
   1.216    shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. c * f x) (c * x)"
   1.217    by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_mult_right])
   1.218  
   1.219 -lemmas has_bochner_integral_divide =
   1.220 +lemmas%unimportant has_bochner_integral_divide =
   1.221    has_bochner_integral_bounded_linear[OF bounded_linear_divide]
   1.222  
   1.223 -lemma has_bochner_integral_divide_zero[intro]:
   1.224 +lemma%unimportant has_bochner_integral_divide_zero[intro]:
   1.225    fixes c :: "_::{real_normed_field, field, second_countable_topology}"
   1.226    shows "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x / c) (x / c)"
   1.227    using has_bochner_integral_divide by (cases "c = 0") auto
   1.228  
   1.229 -lemma has_bochner_integral_inner_left[intro]:
   1.230 +lemma%unimportant has_bochner_integral_inner_left[intro]:
   1.231    "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. f x \<bullet> c) (x \<bullet> c)"
   1.232    by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_inner_left])
   1.233  
   1.234 -lemma has_bochner_integral_inner_right[intro]:
   1.235 +lemma%unimportant has_bochner_integral_inner_right[intro]:
   1.236    "(c \<noteq> 0 \<Longrightarrow> has_bochner_integral M f x) \<Longrightarrow> has_bochner_integral M (\<lambda>x. c \<bullet> f x) (c \<bullet> x)"
   1.237    by (cases "c = 0") (auto simp add: has_bochner_integral_bounded_linear[OF bounded_linear_inner_right])
   1.238  
   1.239 -lemmas has_bochner_integral_minus =
   1.240 +lemmas%unimportant has_bochner_integral_minus =
   1.241    has_bochner_integral_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]]
   1.242 -lemmas has_bochner_integral_Re =
   1.243 +lemmas%unimportant has_bochner_integral_Re =
   1.244    has_bochner_integral_bounded_linear[OF bounded_linear_Re]
   1.245 -lemmas has_bochner_integral_Im =
   1.246 +lemmas%unimportant has_bochner_integral_Im =
   1.247    has_bochner_integral_bounded_linear[OF bounded_linear_Im]
   1.248 -lemmas has_bochner_integral_cnj =
   1.249 +lemmas%unimportant has_bochner_integral_cnj =
   1.250    has_bochner_integral_bounded_linear[OF bounded_linear_cnj]
   1.251 -lemmas has_bochner_integral_of_real =
   1.252 +lemmas%unimportant has_bochner_integral_of_real =
   1.253    has_bochner_integral_bounded_linear[OF bounded_linear_of_real]
   1.254 -lemmas has_bochner_integral_fst =
   1.255 +lemmas%unimportant has_bochner_integral_fst =
   1.256    has_bochner_integral_bounded_linear[OF bounded_linear_fst]
   1.257 -lemmas has_bochner_integral_snd =
   1.258 +lemmas%unimportant has_bochner_integral_snd =
   1.259    has_bochner_integral_bounded_linear[OF bounded_linear_snd]
   1.260  
   1.261 -lemma has_bochner_integral_indicator:
   1.262 +lemma%unimportant has_bochner_integral_indicator:
   1.263    "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
   1.264      has_bochner_integral M (\<lambda>x. indicator A x *\<^sub>R c) (measure M A *\<^sub>R c)"
   1.265    by (intro has_bochner_integral_scaleR_left has_bochner_integral_real_indicator)
   1.266  
   1.267 -lemma has_bochner_integral_diff:
   1.268 +lemma%unimportant has_bochner_integral_diff:
   1.269    "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M g y \<Longrightarrow>
   1.270      has_bochner_integral M (\<lambda>x. f x - g x) (x - y)"
   1.271    unfolding diff_conv_add_uminus
   1.272    by (intro has_bochner_integral_add has_bochner_integral_minus)
   1.273  
   1.274 -lemma has_bochner_integral_sum:
   1.275 +lemma%unimportant has_bochner_integral_sum:
   1.276    "(\<And>i. i \<in> I \<Longrightarrow> has_bochner_integral M (f i) (x i)) \<Longrightarrow>
   1.277      has_bochner_integral M (\<lambda>x. \<Sum>i\<in>I. f i x) (\<Sum>i\<in>I. x i)"
   1.278    by (induct I rule: infinite_finite_induct) auto
   1.279  
   1.280 -lemma has_bochner_integral_implies_finite_norm:
   1.281 +lemma%important has_bochner_integral_implies_finite_norm:
   1.282    "has_bochner_integral M f x \<Longrightarrow> (\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
   1.283 -proof (elim has_bochner_integral.cases)
   1.284 +proof%unimportant (elim has_bochner_integral.cases)
   1.285    fix s v
   1.286    assume [measurable]: "f \<in> borel_measurable M" and s: "\<And>i. simple_bochner_integrable M (s i)" and
   1.287      lim_0: "(\<lambda>i. \<integral>\<^sup>+ x. ennreal (norm (f x - s i x)) \<partial>M) \<longlonglongrightarrow> 0"
   1.288 @@ -756,10 +756,10 @@
   1.289    finally show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>" .
   1.290  qed
   1.291  
   1.292 -lemma has_bochner_integral_norm_bound:
   1.293 +lemma%important has_bochner_integral_norm_bound:
   1.294    assumes i: "has_bochner_integral M f x"
   1.295    shows "norm x \<le> (\<integral>\<^sup>+x. norm (f x) \<partial>M)"
   1.296 -using assms proof
   1.297 +using assms proof%unimportant
   1.298    fix s assume
   1.299      x: "(\<lambda>i. simple_bochner_integral M (s i)) \<longlonglongrightarrow> x" (is "?s \<longlonglongrightarrow> x") and
   1.300      s[simp]: "\<And>i. simple_bochner_integrable M (s i)" and
   1.301 @@ -797,9 +797,9 @@
   1.302    qed
   1.303  qed
   1.304  
   1.305 -lemma has_bochner_integral_eq:
   1.306 +lemma%important has_bochner_integral_eq:
   1.307    "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M f y \<Longrightarrow> x = y"
   1.308 -proof (elim has_bochner_integral.cases)
   1.309 +proof%unimportant (elim has_bochner_integral.cases)
   1.310    assume f[measurable]: "f \<in> borel_measurable M"
   1.311  
   1.312    fix s t
   1.313 @@ -834,7 +834,7 @@
   1.314    then show "x = y" by simp
   1.315  qed
   1.316  
   1.317 -lemma has_bochner_integralI_AE:
   1.318 +lemma%unimportant has_bochner_integralI_AE:
   1.319    assumes f: "has_bochner_integral M f x"
   1.320      and g: "g \<in> borel_measurable M"
   1.321      and ae: "AE x in M. f x = g x"
   1.322 @@ -848,7 +848,7 @@
   1.323    finally show "(\<lambda>i. \<integral>\<^sup>+ x. ennreal (norm (g x - s i x)) \<partial>M) \<longlonglongrightarrow> 0" .
   1.324  qed (auto intro: g)
   1.325  
   1.326 -lemma has_bochner_integral_eq_AE:
   1.327 +lemma%unimportant has_bochner_integral_eq_AE:
   1.328    assumes f: "has_bochner_integral M f x"
   1.329      and g: "has_bochner_integral M g y"
   1.330      and ae: "AE x in M. f x = g x"
   1.331 @@ -860,7 +860,7 @@
   1.332      by (rule has_bochner_integral_eq)
   1.333  qed
   1.334  
   1.335 -lemma simple_bochner_integrable_restrict_space:
   1.336 +lemma%unimportant simple_bochner_integrable_restrict_space:
   1.337    fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
   1.338    assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
   1.339    shows "simple_bochner_integrable (restrict_space M \<Omega>) f \<longleftrightarrow>
   1.340 @@ -869,13 +869,13 @@
   1.341      simple_function_restrict_space[OF \<Omega>] emeasure_restrict_space[OF \<Omega>] Collect_restrict
   1.342      indicator_eq_0_iff conj_left_commute)
   1.343  
   1.344 -lemma simple_bochner_integral_restrict_space:
   1.345 +lemma%important simple_bochner_integral_restrict_space:
   1.346    fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
   1.347    assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
   1.348    assumes f: "simple_bochner_integrable (restrict_space M \<Omega>) f"
   1.349    shows "simple_bochner_integral (restrict_space M \<Omega>) f =
   1.350      simple_bochner_integral M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
   1.351 -proof -
   1.352 +proof%unimportant -
   1.353    have "finite ((\<lambda>x. indicator \<Omega> x *\<^sub>R f x)`space M)"
   1.354      using f simple_bochner_integrable_restrict_space[OF \<Omega>, of f]
   1.355      by (simp add: simple_bochner_integrable.simps simple_function_def)
   1.356 @@ -895,7 +895,7 @@
   1.357  
   1.358  end
   1.359  
   1.360 -definition lebesgue_integral ("integral\<^sup>L") where
   1.361 +definition%important lebesgue_integral ("integral\<^sup>L") where
   1.362    "integral\<^sup>L M f = (if \<exists>x. has_bochner_integral M f x then THE x. has_bochner_integral M f x else 0)"
   1.363  
   1.364  syntax
   1.365 @@ -910,155 +910,155 @@
   1.366  translations
   1.367    "LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)"
   1.368  
   1.369 -lemma has_bochner_integral_integral_eq: "has_bochner_integral M f x \<Longrightarrow> integral\<^sup>L M f = x"
   1.370 +lemma%unimportant has_bochner_integral_integral_eq: "has_bochner_integral M f x \<Longrightarrow> integral\<^sup>L M f = x"
   1.371    by (metis the_equality has_bochner_integral_eq lebesgue_integral_def)
   1.372  
   1.373 -lemma has_bochner_integral_integrable:
   1.374 +lemma%unimportant has_bochner_integral_integrable:
   1.375    "integrable M f \<Longrightarrow> has_bochner_integral M f (integral\<^sup>L M f)"
   1.376    by (auto simp: has_bochner_integral_integral_eq integrable.simps)
   1.377  
   1.378 -lemma has_bochner_integral_iff:
   1.379 +lemma%unimportant has_bochner_integral_iff:
   1.380    "has_bochner_integral M f x \<longleftrightarrow> integrable M f \<and> integral\<^sup>L M f = x"
   1.381    by (metis has_bochner_integral_integrable has_bochner_integral_integral_eq integrable.intros)
   1.382  
   1.383 -lemma simple_bochner_integrable_eq_integral:
   1.384 +lemma%unimportant simple_bochner_integrable_eq_integral:
   1.385    "simple_bochner_integrable M f \<Longrightarrow> simple_bochner_integral M f = integral\<^sup>L M f"
   1.386    using has_bochner_integral_simple_bochner_integrable[of M f]
   1.387    by (simp add: has_bochner_integral_integral_eq)
   1.388  
   1.389 -lemma not_integrable_integral_eq: "\<not> integrable M f \<Longrightarrow> integral\<^sup>L M f = 0"
   1.390 +lemma%unimportant not_integrable_integral_eq: "\<not> integrable M f \<Longrightarrow> integral\<^sup>L M f = 0"
   1.391    unfolding integrable.simps lebesgue_integral_def by (auto intro!: arg_cong[where f=The])
   1.392  
   1.393 -lemma integral_eq_cases:
   1.394 +lemma%unimportant integral_eq_cases:
   1.395    "integrable M f \<longleftrightarrow> integrable N g \<Longrightarrow>
   1.396      (integrable M f \<Longrightarrow> integrable N g \<Longrightarrow> integral\<^sup>L M f = integral\<^sup>L N g) \<Longrightarrow>
   1.397      integral\<^sup>L M f = integral\<^sup>L N g"
   1.398    by (metis not_integrable_integral_eq)
   1.399  
   1.400 -lemma borel_measurable_integrable[measurable_dest]: "integrable M f \<Longrightarrow> f \<in> borel_measurable M"
   1.401 +lemma%unimportant borel_measurable_integrable[measurable_dest]: "integrable M f \<Longrightarrow> f \<in> borel_measurable M"
   1.402    by (auto elim: integrable.cases has_bochner_integral.cases)
   1.403  
   1.404 -lemma borel_measurable_integrable'[measurable_dest]:
   1.405 +lemma%unimportant borel_measurable_integrable'[measurable_dest]:
   1.406    "integrable M f \<Longrightarrow> g \<in> measurable N M \<Longrightarrow> (\<lambda>x. f (g x)) \<in> borel_measurable N"
   1.407    using borel_measurable_integrable[measurable] by measurable
   1.408  
   1.409 -lemma integrable_cong:
   1.410 +lemma%unimportant integrable_cong:
   1.411    "M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integrable M f \<longleftrightarrow> integrable N g"
   1.412    by (simp cong: has_bochner_integral_cong add: integrable.simps)
   1.413  
   1.414 -lemma integrable_cong_AE:
   1.415 +lemma%unimportant integrable_cong_AE:
   1.416    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
   1.417      integrable M f \<longleftrightarrow> integrable M g"
   1.418    unfolding integrable.simps
   1.419    by (intro has_bochner_integral_cong_AE arg_cong[where f=Ex] ext)
   1.420  
   1.421 -lemma integrable_cong_AE_imp:
   1.422 +lemma%unimportant integrable_cong_AE_imp:
   1.423    "integrable M g \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> (AE x in M. g x = f x) \<Longrightarrow> integrable M f"
   1.424    using integrable_cong_AE[of f M g] by (auto simp: eq_commute)
   1.425  
   1.426 -lemma integral_cong:
   1.427 +lemma%unimportant integral_cong:
   1.428    "M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integral\<^sup>L M f = integral\<^sup>L N g"
   1.429    by (simp cong: has_bochner_integral_cong cong del: if_weak_cong add: lebesgue_integral_def)
   1.430  
   1.431 -lemma integral_cong_AE:
   1.432 +lemma%unimportant integral_cong_AE:
   1.433    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
   1.434      integral\<^sup>L M f = integral\<^sup>L M g"
   1.435    unfolding lebesgue_integral_def
   1.436    by (rule arg_cong[where x="has_bochner_integral M f"]) (intro has_bochner_integral_cong_AE ext)
   1.437  
   1.438 -lemma integrable_add[simp, intro]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> integrable M (\<lambda>x. f x + g x)"
   1.439 +lemma%unimportant integrable_add[simp, intro]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> integrable M (\<lambda>x. f x + g x)"
   1.440    by (auto simp: integrable.simps)
   1.441  
   1.442 -lemma integrable_zero[simp, intro]: "integrable M (\<lambda>x. 0)"
   1.443 +lemma%unimportant integrable_zero[simp, intro]: "integrable M (\<lambda>x. 0)"
   1.444    by (metis has_bochner_integral_zero integrable.simps)
   1.445  
   1.446 -lemma integrable_sum[simp, intro]: "(\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)) \<Longrightarrow> integrable M (\<lambda>x. \<Sum>i\<in>I. f i x)"
   1.447 +lemma%unimportant integrable_sum[simp, intro]: "(\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)) \<Longrightarrow> integrable M (\<lambda>x. \<Sum>i\<in>I. f i x)"
   1.448    by (metis has_bochner_integral_sum integrable.simps)
   1.449  
   1.450 -lemma integrable_indicator[simp, intro]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
   1.451 +lemma%unimportant integrable_indicator[simp, intro]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
   1.452    integrable M (\<lambda>x. indicator A x *\<^sub>R c)"
   1.453    by (metis has_bochner_integral_indicator integrable.simps)
   1.454  
   1.455 -lemma integrable_real_indicator[simp, intro]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
   1.456 +lemma%unimportant integrable_real_indicator[simp, intro]: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow>
   1.457    integrable M (indicator A :: 'a \<Rightarrow> real)"
   1.458    by (metis has_bochner_integral_real_indicator integrable.simps)
   1.459  
   1.460 -lemma integrable_diff[simp, intro]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> integrable M (\<lambda>x. f x - g x)"
   1.461 +lemma%unimportant integrable_diff[simp, intro]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> integrable M (\<lambda>x. f x - g x)"
   1.462    by (auto simp: integrable.simps intro: has_bochner_integral_diff)
   1.463  
   1.464 -lemma integrable_bounded_linear: "bounded_linear T \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. T (f x))"
   1.465 +lemma%unimportant integrable_bounded_linear: "bounded_linear T \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. T (f x))"
   1.466    by (auto simp: integrable.simps intro: has_bochner_integral_bounded_linear)
   1.467  
   1.468 -lemma integrable_scaleR_left[simp, intro]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x *\<^sub>R c)"
   1.469 +lemma%unimportant integrable_scaleR_left[simp, intro]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x *\<^sub>R c)"
   1.470    unfolding integrable.simps by fastforce
   1.471  
   1.472 -lemma integrable_scaleR_right[simp, intro]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c *\<^sub>R f x)"
   1.473 +lemma%unimportant integrable_scaleR_right[simp, intro]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c *\<^sub>R f x)"
   1.474    unfolding integrable.simps by fastforce
   1.475  
   1.476 -lemma integrable_mult_left[simp, intro]:
   1.477 +lemma%unimportant integrable_mult_left[simp, intro]:
   1.478    fixes c :: "_::{real_normed_algebra,second_countable_topology}"
   1.479    shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x * c)"
   1.480    unfolding integrable.simps by fastforce
   1.481  
   1.482 -lemma integrable_mult_right[simp, intro]:
   1.483 +lemma%unimportant integrable_mult_right[simp, intro]:
   1.484    fixes c :: "_::{real_normed_algebra,second_countable_topology}"
   1.485    shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c * f x)"
   1.486    unfolding integrable.simps by fastforce
   1.487  
   1.488 -lemma integrable_divide_zero[simp, intro]:
   1.489 +lemma%unimportant integrable_divide_zero[simp, intro]:
   1.490    fixes c :: "_::{real_normed_field, field, second_countable_topology}"
   1.491    shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x / c)"
   1.492    unfolding integrable.simps by fastforce
   1.493  
   1.494 -lemma integrable_inner_left[simp, intro]:
   1.495 +lemma%unimportant integrable_inner_left[simp, intro]:
   1.496    "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. f x \<bullet> c)"
   1.497    unfolding integrable.simps by fastforce
   1.498  
   1.499 -lemma integrable_inner_right[simp, intro]:
   1.500 +lemma%unimportant integrable_inner_right[simp, intro]:
   1.501    "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> integrable M (\<lambda>x. c \<bullet> f x)"
   1.502    unfolding integrable.simps by fastforce
   1.503  
   1.504 -lemmas integrable_minus[simp, intro] =
   1.505 +lemmas%unimportant integrable_minus[simp, intro] =
   1.506    integrable_bounded_linear[OF bounded_linear_minus[OF bounded_linear_ident]]
   1.507 -lemmas integrable_divide[simp, intro] =
   1.508 +lemmas%unimportant integrable_divide[simp, intro] =
   1.509    integrable_bounded_linear[OF bounded_linear_divide]
   1.510 -lemmas integrable_Re[simp, intro] =
   1.511 +lemmas%unimportant integrable_Re[simp, intro] =
   1.512    integrable_bounded_linear[OF bounded_linear_Re]
   1.513 -lemmas integrable_Im[simp, intro] =
   1.514 +lemmas%unimportant integrable_Im[simp, intro] =
   1.515    integrable_bounded_linear[OF bounded_linear_Im]
   1.516 -lemmas integrable_cnj[simp, intro] =
   1.517 +lemmas%unimportant integrable_cnj[simp, intro] =
   1.518    integrable_bounded_linear[OF bounded_linear_cnj]
   1.519 -lemmas integrable_of_real[simp, intro] =
   1.520 +lemmas%unimportant integrable_of_real[simp, intro] =
   1.521    integrable_bounded_linear[OF bounded_linear_of_real]
   1.522 -lemmas integrable_fst[simp, intro] =
   1.523 +lemmas%unimportant integrable_fst[simp, intro] =
   1.524    integrable_bounded_linear[OF bounded_linear_fst]
   1.525 -lemmas integrable_snd[simp, intro] =
   1.526 +lemmas%unimportant integrable_snd[simp, intro] =
   1.527    integrable_bounded_linear[OF bounded_linear_snd]
   1.528  
   1.529 -lemma integral_zero[simp]: "integral\<^sup>L M (\<lambda>x. 0) = 0"
   1.530 +lemma%unimportant integral_zero[simp]: "integral\<^sup>L M (\<lambda>x. 0) = 0"
   1.531    by (intro has_bochner_integral_integral_eq has_bochner_integral_zero)
   1.532  
   1.533 -lemma integral_add[simp]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow>
   1.534 +lemma%unimportant integral_add[simp]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow>
   1.535      integral\<^sup>L M (\<lambda>x. f x + g x) = integral\<^sup>L M f + integral\<^sup>L M g"
   1.536    by (intro has_bochner_integral_integral_eq has_bochner_integral_add has_bochner_integral_integrable)
   1.537  
   1.538 -lemma integral_diff[simp]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow>
   1.539 +lemma%unimportant integral_diff[simp]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow>
   1.540      integral\<^sup>L M (\<lambda>x. f x - g x) = integral\<^sup>L M f - integral\<^sup>L M g"
   1.541    by (intro has_bochner_integral_integral_eq has_bochner_integral_diff has_bochner_integral_integrable)
   1.542  
   1.543 -lemma integral_sum: "(\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)) \<Longrightarrow>
   1.544 +lemma%unimportant integral_sum: "(\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)) \<Longrightarrow>
   1.545    integral\<^sup>L M (\<lambda>x. \<Sum>i\<in>I. f i x) = (\<Sum>i\<in>I. integral\<^sup>L M (f i))"
   1.546    by (intro has_bochner_integral_integral_eq has_bochner_integral_sum has_bochner_integral_integrable)
   1.547  
   1.548 -lemma integral_sum'[simp]: "(\<And>i. i \<in> I =simp=> integrable M (f i)) \<Longrightarrow>
   1.549 +lemma%unimportant integral_sum'[simp]: "(\<And>i. i \<in> I =simp=> integrable M (f i)) \<Longrightarrow>
   1.550    integral\<^sup>L M (\<lambda>x. \<Sum>i\<in>I. f i x) = (\<Sum>i\<in>I. integral\<^sup>L M (f i))"
   1.551    unfolding simp_implies_def by (rule integral_sum)
   1.552  
   1.553 -lemma integral_bounded_linear: "bounded_linear T \<Longrightarrow> integrable M f \<Longrightarrow>
   1.554 +lemma%unimportant integral_bounded_linear: "bounded_linear T \<Longrightarrow> integrable M f \<Longrightarrow>
   1.555      integral\<^sup>L M (\<lambda>x. T (f x)) = T (integral\<^sup>L M f)"
   1.556    by (metis has_bochner_integral_bounded_linear has_bochner_integral_integrable has_bochner_integral_integral_eq)
   1.557  
   1.558 -lemma integral_bounded_linear':
   1.559 +lemma%unimportant integral_bounded_linear':
   1.560    assumes T: "bounded_linear T" and T': "bounded_linear T'"
   1.561    assumes *: "\<not> (\<forall>x. T x = 0) \<Longrightarrow> (\<forall>x. T' (T x) = x)"
   1.562    shows "integral\<^sup>L M (\<lambda>x. T (f x)) = T (integral\<^sup>L M f)"
   1.563 @@ -1085,76 +1085,76 @@
   1.564    qed
   1.565  qed
   1.566  
   1.567 -lemma integral_scaleR_left[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. f x *\<^sub>R c \<partial>M) = integral\<^sup>L M f *\<^sub>R c"
   1.568 +lemma%unimportant integral_scaleR_left[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. f x *\<^sub>R c \<partial>M) = integral\<^sup>L M f *\<^sub>R c"
   1.569    by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_scaleR_left)
   1.570  
   1.571 -lemma integral_scaleR_right[simp]: "(\<integral> x. c *\<^sub>R f x \<partial>M) = c *\<^sub>R integral\<^sup>L M f"
   1.572 +lemma%unimportant integral_scaleR_right[simp]: "(\<integral> x. c *\<^sub>R f x \<partial>M) = c *\<^sub>R integral\<^sup>L M f"
   1.573    by (rule integral_bounded_linear'[OF bounded_linear_scaleR_right bounded_linear_scaleR_right[of "1 / c"]]) simp
   1.574  
   1.575 -lemma integral_mult_left[simp]:
   1.576 +lemma%unimportant integral_mult_left[simp]:
   1.577    fixes c :: "_::{real_normed_algebra,second_countable_topology}"
   1.578    shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. f x * c \<partial>M) = integral\<^sup>L M f * c"
   1.579    by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_left)
   1.580  
   1.581 -lemma integral_mult_right[simp]:
   1.582 +lemma%unimportant integral_mult_right[simp]:
   1.583    fixes c :: "_::{real_normed_algebra,second_countable_topology}"
   1.584    shows "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. c * f x \<partial>M) = c * integral\<^sup>L M f"
   1.585    by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_mult_right)
   1.586  
   1.587 -lemma integral_mult_left_zero[simp]:
   1.588 +lemma%unimportant integral_mult_left_zero[simp]:
   1.589    fixes c :: "_::{real_normed_field,second_countable_topology}"
   1.590    shows "(\<integral> x. f x * c \<partial>M) = integral\<^sup>L M f * c"
   1.591    by (rule integral_bounded_linear'[OF bounded_linear_mult_left bounded_linear_mult_left[of "1 / c"]]) simp
   1.592  
   1.593 -lemma integral_mult_right_zero[simp]:
   1.594 +lemma%unimportant integral_mult_right_zero[simp]:
   1.595    fixes c :: "_::{real_normed_field,second_countable_topology}"
   1.596    shows "(\<integral> x. c * f x \<partial>M) = c * integral\<^sup>L M f"
   1.597    by (rule integral_bounded_linear'[OF bounded_linear_mult_right bounded_linear_mult_right[of "1 / c"]]) simp
   1.598  
   1.599 -lemma integral_inner_left[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. f x \<bullet> c \<partial>M) = integral\<^sup>L M f \<bullet> c"
   1.600 +lemma%unimportant integral_inner_left[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. f x \<bullet> c \<partial>M) = integral\<^sup>L M f \<bullet> c"
   1.601    by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_left)
   1.602  
   1.603 -lemma integral_inner_right[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. c \<bullet> f x \<partial>M) = c \<bullet> integral\<^sup>L M f"
   1.604 +lemma%unimportant integral_inner_right[simp]: "(c \<noteq> 0 \<Longrightarrow> integrable M f) \<Longrightarrow> (\<integral> x. c \<bullet> f x \<partial>M) = c \<bullet> integral\<^sup>L M f"
   1.605    by (intro has_bochner_integral_integral_eq has_bochner_integral_integrable has_bochner_integral_inner_right)
   1.606  
   1.607 -lemma integral_divide_zero[simp]:
   1.608 +lemma%unimportant integral_divide_zero[simp]:
   1.609    fixes c :: "_::{real_normed_field, field, second_countable_topology}"
   1.610    shows "integral\<^sup>L M (\<lambda>x. f x / c) = integral\<^sup>L M f / c"
   1.611    by (rule integral_bounded_linear'[OF bounded_linear_divide bounded_linear_mult_left[of c]]) simp
   1.612  
   1.613 -lemma integral_minus[simp]: "integral\<^sup>L M (\<lambda>x. - f x) = - integral\<^sup>L M f"
   1.614 +lemma%unimportant integral_minus[simp]: "integral\<^sup>L M (\<lambda>x. - f x) = - integral\<^sup>L M f"
   1.615    by (rule integral_bounded_linear'[OF bounded_linear_minus[OF bounded_linear_ident] bounded_linear_minus[OF bounded_linear_ident]]) simp
   1.616  
   1.617 -lemma integral_complex_of_real[simp]: "integral\<^sup>L M (\<lambda>x. complex_of_real (f x)) = of_real (integral\<^sup>L M f)"
   1.618 +lemma%unimportant integral_complex_of_real[simp]: "integral\<^sup>L M (\<lambda>x. complex_of_real (f x)) = of_real (integral\<^sup>L M f)"
   1.619    by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_Re]) simp
   1.620  
   1.621 -lemma integral_cnj[simp]: "integral\<^sup>L M (\<lambda>x. cnj (f x)) = cnj (integral\<^sup>L M f)"
   1.622 +lemma%unimportant integral_cnj[simp]: "integral\<^sup>L M (\<lambda>x. cnj (f x)) = cnj (integral\<^sup>L M f)"
   1.623    by (rule integral_bounded_linear'[OF bounded_linear_cnj bounded_linear_cnj]) simp
   1.624  
   1.625 -lemmas integral_divide[simp] =
   1.626 +lemmas%unimportant integral_divide[simp] =
   1.627    integral_bounded_linear[OF bounded_linear_divide]
   1.628 -lemmas integral_Re[simp] =
   1.629 +lemmas%unimportant integral_Re[simp] =
   1.630    integral_bounded_linear[OF bounded_linear_Re]
   1.631 -lemmas integral_Im[simp] =
   1.632 +lemmas%unimportant integral_Im[simp] =
   1.633    integral_bounded_linear[OF bounded_linear_Im]
   1.634 -lemmas integral_of_real[simp] =
   1.635 +lemmas%unimportant integral_of_real[simp] =
   1.636    integral_bounded_linear[OF bounded_linear_of_real]
   1.637 -lemmas integral_fst[simp] =
   1.638 +lemmas%unimportant integral_fst[simp] =
   1.639    integral_bounded_linear[OF bounded_linear_fst]
   1.640 -lemmas integral_snd[simp] =
   1.641 +lemmas%unimportant integral_snd[simp] =
   1.642    integral_bounded_linear[OF bounded_linear_snd]
   1.643  
   1.644 -lemma integral_norm_bound_ennreal:
   1.645 +lemma%unimportant integral_norm_bound_ennreal:
   1.646    "integrable M f \<Longrightarrow> norm (integral\<^sup>L M f) \<le> (\<integral>\<^sup>+x. norm (f x) \<partial>M)"
   1.647    by (metis has_bochner_integral_integrable has_bochner_integral_norm_bound)
   1.648  
   1.649 -lemma integrableI_sequence:
   1.650 +lemma%important integrableI_sequence:
   1.651    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   1.652    assumes f[measurable]: "f \<in> borel_measurable M"
   1.653    assumes s: "\<And>i. simple_bochner_integrable M (s i)"
   1.654    assumes lim: "(\<lambda>i. \<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) \<longlonglongrightarrow> 0" (is "?S \<longlonglongrightarrow> 0")
   1.655    shows "integrable M f"
   1.656 -proof -
   1.657 +proof%unimportant -
   1.658    let ?s = "\<lambda>n. simple_bochner_integral M (s n)"
   1.659  
   1.660    have "\<exists>x. ?s \<longlonglongrightarrow> x"
   1.661 @@ -1184,7 +1184,7 @@
   1.662      by (rule, rule) fact+
   1.663  qed
   1.664  
   1.665 -lemma nn_integral_dominated_convergence_norm:
   1.666 +lemma%important nn_integral_dominated_convergence_norm:
   1.667    fixes u' :: "_ \<Rightarrow> _::{real_normed_vector, second_countable_topology}"
   1.668    assumes [measurable]:
   1.669         "\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M"
   1.670 @@ -1192,7 +1192,7 @@
   1.671      and w: "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>"
   1.672      and u': "AE x in M. (\<lambda>i. u i x) \<longlonglongrightarrow> u' x"
   1.673    shows "(\<lambda>i. (\<integral>\<^sup>+x. norm (u' x - u i x) \<partial>M)) \<longlonglongrightarrow> 0"
   1.674 -proof -
   1.675 +proof%unimportant -
   1.676    have "AE x in M. \<forall>j. norm (u j x) \<le> w x"
   1.677      unfolding AE_all_countable by rule fact
   1.678    with u' have bnd: "AE x in M. \<forall>j. norm (u' x - u j x) \<le> 2 * w x"
   1.679 @@ -1225,11 +1225,11 @@
   1.680    then show ?thesis by simp
   1.681  qed
   1.682  
   1.683 -lemma integrableI_bounded:
   1.684 +lemma%important integrableI_bounded:
   1.685    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   1.686    assumes f[measurable]: "f \<in> borel_measurable M" and fin: "(\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
   1.687    shows "integrable M f"
   1.688 -proof -
   1.689 +proof%unimportant -
   1.690    from borel_measurable_implies_sequence_metric[OF f, of 0] obtain s where
   1.691      s: "\<And>i. simple_function M (s i)" and
   1.692      pointwise: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) \<longlonglongrightarrow> f x" and
   1.693 @@ -1266,14 +1266,14 @@
   1.694    qed fact
   1.695  qed
   1.696  
   1.697 -lemma integrableI_bounded_set:
   1.698 +lemma%important integrableI_bounded_set:
   1.699    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   1.700    assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M"
   1.701    assumes finite: "emeasure M A < \<infinity>"
   1.702      and bnd: "AE x in M. x \<in> A \<longrightarrow> norm (f x) \<le> B"
   1.703      and null: "AE x in M. x \<notin> A \<longrightarrow> f x = 0"
   1.704    shows "integrable M f"
   1.705 -proof (rule integrableI_bounded)
   1.706 +proof%unimportant (rule integrableI_bounded)
   1.707    { fix x :: 'b have "norm x \<le> B \<Longrightarrow> 0 \<le> B"
   1.708        using norm_ge_zero[of x] by arith }
   1.709    with bnd null have "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) \<le> (\<integral>\<^sup>+ x. ennreal (max 0 B) * indicator A x \<partial>M)"
   1.710 @@ -1283,37 +1283,37 @@
   1.711    finally show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>" .
   1.712  qed simp
   1.713  
   1.714 -lemma integrableI_bounded_set_indicator:
   1.715 +lemma%unimportant integrableI_bounded_set_indicator:
   1.716    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   1.717    shows "A \<in> sets M \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow>
   1.718      emeasure M A < \<infinity> \<Longrightarrow> (AE x in M. x \<in> A \<longrightarrow> norm (f x) \<le> B) \<Longrightarrow>
   1.719      integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
   1.720    by (rule integrableI_bounded_set[where A=A]) auto
   1.721  
   1.722 -lemma integrableI_nonneg:
   1.723 +lemma%important integrableI_nonneg:
   1.724    fixes f :: "'a \<Rightarrow> real"
   1.725    assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>M) < \<infinity>"
   1.726    shows "integrable M f"
   1.727 -proof -
   1.728 +proof%unimportant -
   1.729    have "(\<integral>\<^sup>+x. norm (f x) \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
   1.730      using assms by (intro nn_integral_cong_AE) auto
   1.731    then show ?thesis
   1.732      using assms by (intro integrableI_bounded) auto
   1.733  qed
   1.734  
   1.735 -lemma integrable_iff_bounded:
   1.736 +lemma%important integrable_iff_bounded:
   1.737    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   1.738    shows "integrable M f \<longleftrightarrow> f \<in> borel_measurable M \<and> (\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
   1.739    using integrableI_bounded[of f M] has_bochner_integral_implies_finite_norm[of M f]
   1.740    unfolding integrable.simps has_bochner_integral.simps[abs_def] by auto
   1.741  
   1.742 -lemma integrable_bound:
   1.743 +lemma%important integrable_bound:
   1.744    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   1.745      and g :: "'a \<Rightarrow> 'c::{banach, second_countable_topology}"
   1.746    shows "integrable M f \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. norm (g x) \<le> norm (f x)) \<Longrightarrow>
   1.747      integrable M g"
   1.748    unfolding integrable_iff_bounded
   1.749 -proof safe
   1.750 +proof%unimportant safe
   1.751    assume "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   1.752    assume "AE x in M. norm (g x) \<le> norm (f x)"
   1.753    then have "(\<integral>\<^sup>+ x. ennreal (norm (g x)) \<partial>M) \<le> (\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M)"
   1.754 @@ -1322,71 +1322,71 @@
   1.755    finally show "(\<integral>\<^sup>+ x. ennreal (norm (g x)) \<partial>M) < \<infinity>" .
   1.756  qed
   1.757  
   1.758 -lemma integrable_mult_indicator:
   1.759 +lemma%unimportant integrable_mult_indicator:
   1.760    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   1.761    shows "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
   1.762    by (rule integrable_bound[of M f]) (auto split: split_indicator)
   1.763  
   1.764 -lemma integrable_real_mult_indicator:
   1.765 +lemma%unimportant integrable_real_mult_indicator:
   1.766    fixes f :: "'a \<Rightarrow> real"
   1.767    shows "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. f x * indicator A x)"
   1.768    using integrable_mult_indicator[of A M f] by (simp add: mult_ac)
   1.769  
   1.770 -lemma integrable_abs[simp, intro]:
   1.771 +lemma%unimportant integrable_abs[simp, intro]:
   1.772    fixes f :: "'a \<Rightarrow> real"
   1.773    assumes [measurable]: "integrable M f" shows "integrable M (\<lambda>x. \<bar>f x\<bar>)"
   1.774    using assms by (rule integrable_bound) auto
   1.775  
   1.776 -lemma integrable_norm[simp, intro]:
   1.777 +lemma%unimportant integrable_norm[simp, intro]:
   1.778    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   1.779    assumes [measurable]: "integrable M f" shows "integrable M (\<lambda>x. norm (f x))"
   1.780    using assms by (rule integrable_bound) auto
   1.781  
   1.782 -lemma integrable_norm_cancel:
   1.783 +lemma%unimportant integrable_norm_cancel:
   1.784    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   1.785    assumes [measurable]: "integrable M (\<lambda>x. norm (f x))" "f \<in> borel_measurable M" shows "integrable M f"
   1.786    using assms by (rule integrable_bound) auto
   1.787  
   1.788 -lemma integrable_norm_iff:
   1.789 +lemma%unimportant integrable_norm_iff:
   1.790    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   1.791    shows "f \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda>x. norm (f x)) \<longleftrightarrow> integrable M f"
   1.792    by (auto intro: integrable_norm_cancel)
   1.793  
   1.794 -lemma integrable_abs_cancel:
   1.795 +lemma%unimportant integrable_abs_cancel:
   1.796    fixes f :: "'a \<Rightarrow> real"
   1.797    assumes [measurable]: "integrable M (\<lambda>x. \<bar>f x\<bar>)" "f \<in> borel_measurable M" shows "integrable M f"
   1.798    using assms by (rule integrable_bound) auto
   1.799  
   1.800 -lemma integrable_abs_iff:
   1.801 +lemma%unimportant integrable_abs_iff:
   1.802    fixes f :: "'a \<Rightarrow> real"
   1.803    shows "f \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda>x. \<bar>f x\<bar>) \<longleftrightarrow> integrable M f"
   1.804    by (auto intro: integrable_abs_cancel)
   1.805  
   1.806 -lemma integrable_max[simp, intro]:
   1.807 +lemma%unimportant integrable_max[simp, intro]:
   1.808    fixes f :: "'a \<Rightarrow> real"
   1.809    assumes fg[measurable]: "integrable M f" "integrable M g"
   1.810    shows "integrable M (\<lambda>x. max (f x) (g x))"
   1.811    using integrable_add[OF integrable_norm[OF fg(1)] integrable_norm[OF fg(2)]]
   1.812    by (rule integrable_bound) auto
   1.813  
   1.814 -lemma integrable_min[simp, intro]:
   1.815 +lemma%unimportant integrable_min[simp, intro]:
   1.816    fixes f :: "'a \<Rightarrow> real"
   1.817    assumes fg[measurable]: "integrable M f" "integrable M g"
   1.818    shows "integrable M (\<lambda>x. min (f x) (g x))"
   1.819    using integrable_add[OF integrable_norm[OF fg(1)] integrable_norm[OF fg(2)]]
   1.820    by (rule integrable_bound) auto
   1.821  
   1.822 -lemma integral_minus_iff[simp]:
   1.823 +lemma%unimportant integral_minus_iff[simp]:
   1.824    "integrable M (\<lambda>x. - f x ::'a::{banach, second_countable_topology}) \<longleftrightarrow> integrable M f"
   1.825    unfolding integrable_iff_bounded
   1.826    by (auto intro: borel_measurable_uminus[of "\<lambda>x. - f x" M, simplified])
   1.827  
   1.828 -lemma integrable_indicator_iff:
   1.829 +lemma%unimportant integrable_indicator_iff:
   1.830    "integrable M (indicator A::_ \<Rightarrow> real) \<longleftrightarrow> A \<inter> space M \<in> sets M \<and> emeasure M (A \<inter> space M) < \<infinity>"
   1.831    by (simp add: integrable_iff_bounded borel_measurable_indicator_iff ennreal_indicator nn_integral_indicator'
   1.832             cong: conj_cong)
   1.833  
   1.834 -lemma integral_indicator[simp]: "integral\<^sup>L M (indicator A) = measure M (A \<inter> space M)"
   1.835 +lemma%unimportant integral_indicator[simp]: "integral\<^sup>L M (indicator A) = measure M (A \<inter> space M)"
   1.836  proof cases
   1.837    assume *: "A \<inter> space M \<in> sets M \<and> emeasure M (A \<inter> space M) < \<infinity>"
   1.838    have "integral\<^sup>L M (indicator A) = integral\<^sup>L M (indicator (A \<inter> space M))"
   1.839 @@ -1405,7 +1405,7 @@
   1.840    finally show ?thesis .
   1.841  qed
   1.842  
   1.843 -lemma integrable_discrete_difference:
   1.844 +lemma%unimportant integrable_discrete_difference:
   1.845    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   1.846    assumes X: "countable X"
   1.847    assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0"
   1.848 @@ -1429,7 +1429,7 @@
   1.849      by simp
   1.850  qed
   1.851  
   1.852 -lemma integral_discrete_difference:
   1.853 +lemma%unimportant integral_discrete_difference:
   1.854    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   1.855    assumes X: "countable X"
   1.856    assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0"
   1.857 @@ -1453,7 +1453,7 @@
   1.858    qed
   1.859  qed
   1.860  
   1.861 -lemma has_bochner_integral_discrete_difference:
   1.862 +lemma%unimportant has_bochner_integral_discrete_difference:
   1.863    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   1.864    assumes X: "countable X"
   1.865    assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0"
   1.866 @@ -1464,7 +1464,7 @@
   1.867    using integral_discrete_difference[of X M f g, OF assms]
   1.868    by (metis has_bochner_integral_iff)
   1.869  
   1.870 -lemma
   1.871 +lemma%important (*FIX ME needs name *)
   1.872    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and w :: "'a \<Rightarrow> real"
   1.873    assumes "f \<in> borel_measurable M" "\<And>i. s i \<in> borel_measurable M" "integrable M w"
   1.874    assumes lim: "AE x in M. (\<lambda>i. s i x) \<longlonglongrightarrow> f x"
   1.875 @@ -1472,7 +1472,7 @@
   1.876    shows integrable_dominated_convergence: "integrable M f"
   1.877      and integrable_dominated_convergence2: "\<And>i. integrable M (s i)"
   1.878      and integral_dominated_convergence: "(\<lambda>i. integral\<^sup>L M (s i)) \<longlonglongrightarrow> integral\<^sup>L M f"
   1.879 -proof -
   1.880 +proof%unimportant -
   1.881    have w_nonneg: "AE x in M. 0 \<le> w x"
   1.882      using bound[of 0] by eventually_elim (auto intro: norm_ge_zero order_trans)
   1.883    then have "(\<integral>\<^sup>+x. w x \<partial>M) = (\<integral>\<^sup>+x. norm (w x) \<partial>M)"
   1.884 @@ -1539,7 +1539,7 @@
   1.885    assumes bound: "\<forall>\<^sub>F i in at_top. AE x in M. norm (s i x) \<le> w x"
   1.886  begin
   1.887  
   1.888 -lemma integral_dominated_convergence_at_top: "((\<lambda>t. integral\<^sup>L M (s t)) \<longlongrightarrow> integral\<^sup>L M f) at_top"
   1.889 +lemma%unimportant integral_dominated_convergence_at_top: "((\<lambda>t. integral\<^sup>L M (s t)) \<longlongrightarrow> integral\<^sup>L M f) at_top"
   1.890  proof (rule tendsto_at_topI_sequentially)
   1.891    fix X :: "nat \<Rightarrow> real" assume X: "filterlim X at_top sequentially"
   1.892    from filterlim_iff[THEN iffD1, OF this, rule_format, OF bound]
   1.893 @@ -1560,7 +1560,7 @@
   1.894    qed fact+
   1.895  qed
   1.896  
   1.897 -lemma integrable_dominated_convergence_at_top: "integrable M f"
   1.898 +lemma%unimportant integrable_dominated_convergence_at_top: "integrable M f"
   1.899  proof -
   1.900    from bound obtain N where w: "\<And>n. N \<le> n \<Longrightarrow> AE x in M. norm (s n x) \<le> w x"
   1.901      by (auto simp: eventually_at_top_linorder)
   1.902 @@ -1581,13 +1581,13 @@
   1.903  
   1.904  end
   1.905  
   1.906 -lemma integrable_mult_left_iff:
   1.907 +lemma%unimportant integrable_mult_left_iff:
   1.908    fixes f :: "'a \<Rightarrow> real"
   1.909    shows "integrable M (\<lambda>x. c * f x) \<longleftrightarrow> c = 0 \<or> integrable M f"
   1.910    using integrable_mult_left[of c M f] integrable_mult_left[of "1 / c" M "\<lambda>x. c * f x"]
   1.911    by (cases "c = 0") auto
   1.912  
   1.913 -lemma integrableI_nn_integral_finite:
   1.914 +lemma%unimportant integrableI_nn_integral_finite:
   1.915    assumes [measurable]: "f \<in> borel_measurable M"
   1.916      and nonneg: "AE x in M. 0 \<le> f x"
   1.917      and finite: "(\<integral>\<^sup>+x. f x \<partial>M) = ennreal x"
   1.918 @@ -1599,7 +1599,7 @@
   1.919      by auto
   1.920  qed simp
   1.921  
   1.922 -lemma integral_nonneg_AE:
   1.923 +lemma%unimportant integral_nonneg_AE:
   1.924    fixes f :: "'a \<Rightarrow> real"
   1.925    assumes nonneg: "AE x in M. 0 \<le> f x"
   1.926    shows "0 \<le> integral\<^sup>L M f"
   1.927 @@ -1635,16 +1635,16 @@
   1.928    finally show ?thesis .
   1.929  qed (simp add: not_integrable_integral_eq)
   1.930  
   1.931 -lemma integral_nonneg[simp]:
   1.932 +lemma%unimportant integral_nonneg[simp]:
   1.933    fixes f :: "'a \<Rightarrow> real"
   1.934    shows "(\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> 0 \<le> integral\<^sup>L M f"
   1.935    by (intro integral_nonneg_AE) auto
   1.936  
   1.937 -lemma nn_integral_eq_integral:
   1.938 +lemma%important nn_integral_eq_integral:
   1.939    assumes f: "integrable M f"
   1.940    assumes nonneg: "AE x in M. 0 \<le> f x"
   1.941    shows "(\<integral>\<^sup>+ x. f x \<partial>M) = integral\<^sup>L M f"
   1.942 -proof -
   1.943 +proof%unimportant -
   1.944    { fix f :: "'a \<Rightarrow> real" assume f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" "integrable M f"
   1.945      then have "(\<integral>\<^sup>+ x. f x \<partial>M) = integral\<^sup>L M f"
   1.946      proof (induct rule: borel_measurable_induct_real)
   1.947 @@ -1687,7 +1687,7 @@
   1.948    finally show ?thesis .
   1.949  qed
   1.950  
   1.951 -lemma nn_integral_eq_integrable:
   1.952 +lemma%unimportant nn_integral_eq_integrable:
   1.953    assumes f: "f \<in> M \<rightarrow>\<^sub>M borel" "AE x in M. 0 \<le> f x" and "0 \<le> x"
   1.954    shows "(\<integral>\<^sup>+x. f x \<partial>M) = ennreal x \<longleftrightarrow> (integrable M f \<and> integral\<^sup>L M f = x)"
   1.955  proof (safe intro!: nn_integral_eq_integral assms)
   1.956 @@ -1697,7 +1697,7 @@
   1.957      by (simp_all add: * assms integral_nonneg_AE)
   1.958  qed
   1.959  
   1.960 -lemma
   1.961 +lemma%unimportant (* FIX ME needs name*)
   1.962    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   1.963    assumes integrable[measurable]: "\<And>i. integrable M (f i)"
   1.964    and summable: "AE x in M. summable (\<lambda>i. norm (f i x))"
   1.965 @@ -1748,10 +1748,10 @@
   1.966      unfolding sums_iff by auto
   1.967  qed
   1.968  
   1.969 -lemma integral_norm_bound [simp]:
   1.970 +lemma%important integral_norm_bound [simp]:
   1.971    fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   1.972    shows "norm (integral\<^sup>L M f) \<le> (\<integral>x. norm (f x) \<partial>M)"
   1.973 -proof (cases "integrable M f")
   1.974 +proof%unimportant (cases "integrable M f")
   1.975    case True then show ?thesis
   1.976      using nn_integral_eq_integral[of M "\<lambda>x. norm (f x)"] integral_norm_bound_ennreal[of M f]
   1.977      by (simp add: integral_nonneg_AE)
   1.978 @@ -1762,11 +1762,11 @@
   1.979    ultimately show ?thesis by simp
   1.980  qed
   1.981  
   1.982 -lemma integral_abs_bound [simp]:
   1.983 +lemma%unimportant integral_abs_bound [simp]:
   1.984    fixes f :: "'a \<Rightarrow> real" shows "abs (\<integral>x. f x \<partial>M) \<le> (\<integral>x. \<bar>f x\<bar> \<partial>M)"
   1.985  using integral_norm_bound[of M f] by auto
   1.986  
   1.987 -lemma integral_eq_nn_integral:
   1.988 +lemma%unimportant integral_eq_nn_integral:
   1.989    assumes [measurable]: "f \<in> borel_measurable M"
   1.990    assumes nonneg: "AE x in M. 0 \<le> f x"
   1.991    shows "integral\<^sup>L M f = enn2real (\<integral>\<^sup>+ x. ennreal (f x) \<partial>M)"
   1.992 @@ -1787,7 +1787,7 @@
   1.993      by (simp add: integral_nonneg_AE)
   1.994  qed
   1.995  
   1.996 -lemma enn2real_nn_integral_eq_integral:
   1.997 +lemma%unimportant enn2real_nn_integral_eq_integral:
   1.998    assumes eq: "AE x in M. f x = ennreal (g x)" and nn: "AE x in M. 0 \<le> g x"
   1.999      and fin: "(\<integral>\<^sup>+x. f x \<partial>M) < top"
  1.1000      and [measurable]: "g \<in> M \<rightarrow>\<^sub>M borel"
  1.1001 @@ -1812,20 +1812,20 @@
  1.1002      using nn by (simp add: integral_nonneg_AE)
  1.1003  qed
  1.1004  
  1.1005 -lemma has_bochner_integral_nn_integral:
  1.1006 +lemma%unimportant has_bochner_integral_nn_integral:
  1.1007    assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "0 \<le> x"
  1.1008    assumes "(\<integral>\<^sup>+x. f x \<partial>M) = ennreal x"
  1.1009    shows "has_bochner_integral M f x"
  1.1010    unfolding has_bochner_integral_iff
  1.1011    using assms by (auto simp: assms integral_eq_nn_integral intro: integrableI_nn_integral_finite)
  1.1012  
  1.1013 -lemma integrableI_simple_bochner_integrable:
  1.1014 +lemma%unimportant integrableI_simple_bochner_integrable:
  1.1015    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1016    shows "simple_bochner_integrable M f \<Longrightarrow> integrable M f"
  1.1017    by (intro integrableI_sequence[where s="\<lambda>_. f"] borel_measurable_simple_function)
  1.1018       (auto simp: zero_ennreal_def[symmetric] simple_bochner_integrable.simps)
  1.1019  
  1.1020 -lemma integrable_induct[consumes 1, case_names base add lim, induct pred: integrable]:
  1.1021 +lemma%important integrable_induct[consumes 1, case_names base add lim, induct pred: integrable]:
  1.1022    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1023    assumes "integrable M f"
  1.1024    assumes base: "\<And>A c. A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> P (\<lambda>x. indicator A x *\<^sub>R c)"
  1.1025 @@ -1834,7 +1834,7 @@
  1.1026     (\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) \<longlonglongrightarrow> f x) \<Longrightarrow>
  1.1027     (\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)) \<Longrightarrow> integrable M f \<Longrightarrow> P f"
  1.1028    shows "P f"
  1.1029 -proof -
  1.1030 +proof%unimportant -
  1.1031    from \<open>integrable M f\<close> have f: "f \<in> borel_measurable M" "(\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
  1.1032      unfolding integrable_iff_bounded by auto
  1.1033    from borel_measurable_implies_sequence_metric[OF f(1)]
  1.1034 @@ -1895,12 +1895,12 @@
  1.1035    qed fact
  1.1036  qed
  1.1037  
  1.1038 -lemma integral_eq_zero_AE:
  1.1039 +lemma%unimportant integral_eq_zero_AE:
  1.1040    "(AE x in M. f x = 0) \<Longrightarrow> integral\<^sup>L M f = 0"
  1.1041    using integral_cong_AE[of f M "\<lambda>_. 0"]
  1.1042    by (cases "integrable M f") (simp_all add: not_integrable_integral_eq)
  1.1043  
  1.1044 -lemma integral_nonneg_eq_0_iff_AE:
  1.1045 +lemma%unimportant integral_nonneg_eq_0_iff_AE:
  1.1046    fixes f :: "_ \<Rightarrow> real"
  1.1047    assumes f[measurable]: "integrable M f" and nonneg: "AE x in M. 0 \<le> f x"
  1.1048    shows "integral\<^sup>L M f = 0 \<longleftrightarrow> (AE x in M. f x = 0)"
  1.1049 @@ -1914,7 +1914,7 @@
  1.1050      by auto
  1.1051  qed (auto simp add: integral_eq_zero_AE)
  1.1052  
  1.1053 -lemma integral_mono_AE:
  1.1054 +lemma%unimportant integral_mono_AE:
  1.1055    fixes f :: "'a \<Rightarrow> real"
  1.1056    assumes "integrable M f" "integrable M g" "AE x in M. f x \<le> g x"
  1.1057    shows "integral\<^sup>L M f \<le> integral\<^sup>L M g"
  1.1058 @@ -1926,7 +1926,7 @@
  1.1059    finally show ?thesis by simp
  1.1060  qed
  1.1061  
  1.1062 -lemma integral_mono:
  1.1063 +lemma%unimportant integral_mono:
  1.1064    fixes f :: "'a \<Rightarrow> real"
  1.1065    shows "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x \<le> g x) \<Longrightarrow>
  1.1066      integral\<^sup>L M f \<le> integral\<^sup>L M g"
  1.1067 @@ -1936,11 +1936,11 @@
  1.1068  integrability assumption. The price to pay is that the upper function has to be nonnegative,
  1.1069  but this is often true and easy to check in computations.\<close>
  1.1070  
  1.1071 -lemma integral_mono_AE':
  1.1072 +lemma%important integral_mono_AE':
  1.1073    fixes f::"_ \<Rightarrow> real"
  1.1074    assumes "integrable M f" "AE x in M. g x \<le> f x" "AE x in M. 0 \<le> f x"
  1.1075    shows "(\<integral>x. g x \<partial>M) \<le> (\<integral>x. f x \<partial>M)"
  1.1076 -proof (cases "integrable M g")
  1.1077 +proof%unimportant (cases "integrable M g")
  1.1078    case True
  1.1079    show ?thesis by (rule integral_mono_AE, auto simp add: assms True)
  1.1080  next
  1.1081 @@ -1950,16 +1950,16 @@
  1.1082    finally show ?thesis by simp
  1.1083  qed
  1.1084  
  1.1085 -lemma integral_mono':
  1.1086 +lemma%important integral_mono':
  1.1087    fixes f::"_ \<Rightarrow> real"
  1.1088    assumes "integrable M f" "\<And>x. x \<in> space M \<Longrightarrow> g x \<le> f x" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
  1.1089    shows "(\<integral>x. g x \<partial>M) \<le> (\<integral>x. f x \<partial>M)"
  1.1090  by (rule integral_mono_AE', insert assms, auto)
  1.1091  
  1.1092 -lemma (in finite_measure) integrable_measure:
  1.1093 +lemma%important (in finite_measure) integrable_measure:
  1.1094    assumes I: "disjoint_family_on X I" "countable I"
  1.1095    shows "integrable (count_space I) (\<lambda>i. measure M (X i))"
  1.1096 -proof -
  1.1097 +proof%unimportant -
  1.1098    have "(\<integral>\<^sup>+i. measure M (X i) \<partial>count_space I) = (\<integral>\<^sup>+i. measure M (if X i \<in> sets M then X i else {}) \<partial>count_space I)"
  1.1099      by (auto intro!: nn_integral_cong measure_notin_sets)
  1.1100    also have "\<dots> = measure M (\<Union>i\<in>I. if X i \<in> sets M then X i else {})"
  1.1101 @@ -1969,7 +1969,7 @@
  1.1102      by (auto intro!: integrableI_bounded)
  1.1103  qed
  1.1104  
  1.1105 -lemma integrableI_real_bounded:
  1.1106 +lemma%unimportant integrableI_real_bounded:
  1.1107    assumes f: "f \<in> borel_measurable M" and ae: "AE x in M. 0 \<le> f x" and fin: "integral\<^sup>N M f < \<infinity>"
  1.1108    shows "integrable M f"
  1.1109  proof (rule integrableI_bounded)
  1.1110 @@ -1979,13 +1979,13 @@
  1.1111    finally show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>" .
  1.1112  qed fact
  1.1113  
  1.1114 -lemma nn_integral_nonneg_infinite:
  1.1115 +lemma%unimportant nn_integral_nonneg_infinite:
  1.1116    fixes f::"'a \<Rightarrow> real"
  1.1117    assumes "f \<in> borel_measurable M" "\<not> integrable M f" "AE x in M. f x \<ge> 0"
  1.1118    shows "(\<integral>\<^sup>+x. f x \<partial>M) = \<infinity>"
  1.1119  using assms integrableI_real_bounded less_top by auto
  1.1120  
  1.1121 -lemma integral_real_bounded:
  1.1122 +lemma%unimportant integral_real_bounded:
  1.1123    assumes "0 \<le> r" "integral\<^sup>N M f \<le> ennreal r"
  1.1124    shows "integral\<^sup>L M f \<le> r"
  1.1125  proof cases
  1.1126 @@ -2009,22 +2009,22 @@
  1.1127      using \<open>0 \<le> r\<close> by (simp add: not_integrable_integral_eq)
  1.1128  qed
  1.1129  
  1.1130 -lemma integrable_MIN:
  1.1131 +lemma%unimportant integrable_MIN:
  1.1132    fixes f:: "_ \<Rightarrow> _ \<Rightarrow> real"
  1.1133    shows "\<lbrakk> finite I;  I \<noteq> {}; \<And>i. i \<in> I \<Longrightarrow> integrable M (f i) \<rbrakk>
  1.1134     \<Longrightarrow> integrable M (\<lambda>x. MIN i\<in>I. f i x)"
  1.1135  by (induct rule: finite_ne_induct) simp+
  1.1136  
  1.1137 -lemma integrable_MAX:
  1.1138 +lemma%unimportant integrable_MAX:
  1.1139    fixes f:: "_ \<Rightarrow> _ \<Rightarrow> real"
  1.1140    shows "\<lbrakk> finite I;  I \<noteq> {};  \<And>i. i \<in> I \<Longrightarrow> integrable M (f i) \<rbrakk>
  1.1141    \<Longrightarrow> integrable M (\<lambda>x. MAX i\<in>I. f i x)"
  1.1142  by (induct rule: finite_ne_induct) simp+
  1.1143  
  1.1144 -lemma integral_Markov_inequality:
  1.1145 +lemma%important integral_Markov_inequality:
  1.1146    assumes [measurable]: "integrable M u" and "AE x in M. 0 \<le> u x" "0 < (c::real)"
  1.1147    shows "(emeasure M) {x\<in>space M. u x \<ge> c} \<le> (1/c) * (\<integral>x. u x \<partial>M)"
  1.1148 -proof -
  1.1149 +proof%unimportant -
  1.1150    have "(\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M) \<le> (\<integral>\<^sup>+ x. u x \<partial>M)"
  1.1151      by (rule nn_integral_mono_AE, auto simp add: \<open>c>0\<close> less_eq_real_def)
  1.1152    also have "... = (\<integral>x. u x \<partial>M)"
  1.1153 @@ -2044,7 +2044,7 @@
  1.1154      using \<open>0<c\<close> by (simp add: ennreal_mult'[symmetric])
  1.1155  qed
  1.1156  
  1.1157 -lemma integral_ineq_eq_0_then_AE:
  1.1158 +lemma%unimportant integral_ineq_eq_0_then_AE:
  1.1159    fixes f::"_ \<Rightarrow> real"
  1.1160    assumes "AE x in M. f x \<le> g x" "integrable M f" "integrable M g"
  1.1161            "(\<integral>x. f x \<partial>M) = (\<integral>x. g x \<partial>M)"
  1.1162 @@ -2057,7 +2057,7 @@
  1.1163    then show ?thesis unfolding h_def by auto
  1.1164  qed
  1.1165  
  1.1166 -lemma not_AE_zero_int_E:
  1.1167 +lemma%unimportant not_AE_zero_int_E:
  1.1168    fixes f::"'a \<Rightarrow> real"
  1.1169    assumes "AE x in M. f x \<ge> 0" "(\<integral>x. f x \<partial>M) > 0"
  1.1170        and [measurable]: "f \<in> borel_measurable M"
  1.1171 @@ -2069,12 +2069,12 @@
  1.1172    then show False using assms(2) by simp
  1.1173  qed
  1.1174  
  1.1175 -lemma tendsto_L1_int:
  1.1176 +lemma%important tendsto_L1_int:
  1.1177    fixes u :: "_ \<Rightarrow> _ \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1178    assumes [measurable]: "\<And>n. integrable M (u n)" "integrable M f"
  1.1179            and "((\<lambda>n. (\<integral>\<^sup>+x. norm(u n x - f x) \<partial>M)) \<longlongrightarrow> 0) F"
  1.1180    shows "((\<lambda>n. (\<integral>x. u n x \<partial>M)) \<longlongrightarrow> (\<integral>x. f x \<partial>M)) F"
  1.1181 -proof -
  1.1182 +proof%unimportant -
  1.1183    have "((\<lambda>n. norm((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M))) \<longlongrightarrow> (0::ennreal)) F"
  1.1184    proof (rule tendsto_sandwich[of "\<lambda>_. 0", where ?h = "\<lambda>n. (\<integral>\<^sup>+x. norm(u n x - f x) \<partial>M)"], auto simp add: assms)
  1.1185      {
  1.1186 @@ -2103,12 +2103,12 @@
  1.1187  text \<open>The next lemma asserts that, if a sequence of functions converges in $L^1$, then
  1.1188  it admits a subsequence that converges almost everywhere.\<close>
  1.1189  
  1.1190 -lemma tendsto_L1_AE_subseq:
  1.1191 +lemma%important tendsto_L1_AE_subseq:
  1.1192    fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1193    assumes [measurable]: "\<And>n. integrable M (u n)"
  1.1194        and "(\<lambda>n. (\<integral>x. norm(u n x) \<partial>M)) \<longlonglongrightarrow> 0"
  1.1195    shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0)"
  1.1196 -proof -
  1.1197 +proof%unimportant -
  1.1198    {
  1.1199      fix k
  1.1200      have "eventually (\<lambda>n. (\<integral>x. norm(u n x) \<partial>M) < (1/2)^k) sequentially"
  1.1201 @@ -2201,9 +2201,9 @@
  1.1202    then show ?thesis using \<open>strict_mono r\<close> by auto
  1.1203  qed
  1.1204  
  1.1205 -subsection \<open>Restricted measure spaces\<close>
  1.1206 -
  1.1207 -lemma integrable_restrict_space:
  1.1208 +subsection%important \<open>Restricted measure spaces\<close>
  1.1209 +
  1.1210 +lemma%unimportant integrable_restrict_space:
  1.1211    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1212    assumes \<Omega>[simp]: "\<Omega> \<inter> space M \<in> sets M"
  1.1213    shows "integrable (restrict_space M \<Omega>) f \<longleftrightarrow> integrable M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
  1.1214 @@ -2212,11 +2212,11 @@
  1.1215      nn_integral_restrict_space[OF \<Omega>]
  1.1216    by (simp add: ac_simps ennreal_indicator ennreal_mult)
  1.1217  
  1.1218 -lemma integral_restrict_space:
  1.1219 +lemma%important integral_restrict_space:
  1.1220    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1221    assumes \<Omega>[simp]: "\<Omega> \<inter> space M \<in> sets M"
  1.1222    shows "integral\<^sup>L (restrict_space M \<Omega>) f = integral\<^sup>L M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
  1.1223 -proof (rule integral_eq_cases)
  1.1224 +proof%unimportant (rule integral_eq_cases)
  1.1225    assume "integrable (restrict_space M \<Omega>) f"
  1.1226    then show ?thesis
  1.1227    proof induct
  1.1228 @@ -2243,7 +2243,7 @@
  1.1229    qed
  1.1230  qed (simp add: integrable_restrict_space)
  1.1231  
  1.1232 -lemma integral_empty:
  1.1233 +lemma%unimportant integral_empty:
  1.1234    assumes "space M = {}"
  1.1235    shows "integral\<^sup>L M f = 0"
  1.1236  proof -
  1.1237 @@ -2252,9 +2252,9 @@
  1.1238    thus ?thesis by simp
  1.1239  qed
  1.1240  
  1.1241 -subsection \<open>Measure spaces with an associated density\<close>
  1.1242 -
  1.1243 -lemma integrable_density:
  1.1244 +subsection%important \<open>Measure spaces with an associated density\<close>
  1.1245 +
  1.1246 +lemma%unimportant integrable_density:
  1.1247    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
  1.1248    assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  1.1249      and nn: "AE x in M. 0 \<le> g x"
  1.1250 @@ -2265,12 +2265,12 @@
  1.1251    apply (auto simp: ennreal_mult)
  1.1252    done
  1.1253  
  1.1254 -lemma integral_density:
  1.1255 +lemma%important integral_density:
  1.1256    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
  1.1257    assumes f: "f \<in> borel_measurable M"
  1.1258      and g[measurable]: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
  1.1259    shows "integral\<^sup>L (density M g) f = integral\<^sup>L M (\<lambda>x. g x *\<^sub>R f x)"
  1.1260 -proof (rule integral_eq_cases)
  1.1261 +proof%unimportant (rule integral_eq_cases)
  1.1262    assume "integrable (density M g) f"
  1.1263    then show ?thesis
  1.1264    proof induct
  1.1265 @@ -2325,38 +2325,38 @@
  1.1266    qed
  1.1267  qed (simp add: f g integrable_density)
  1.1268  
  1.1269 -lemma
  1.1270 +lemma%unimportant (*FIX ME needs name *)
  1.1271    fixes g :: "'a \<Rightarrow> real"
  1.1272    assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "g \<in> borel_measurable M"
  1.1273    shows integral_real_density: "integral\<^sup>L (density M f) g = (\<integral> x. f x * g x \<partial>M)"
  1.1274      and integrable_real_density: "integrable (density M f) g \<longleftrightarrow> integrable M (\<lambda>x. f x * g x)"
  1.1275    using assms integral_density[of g M f] integrable_density[of g M f] by auto
  1.1276  
  1.1277 -lemma has_bochner_integral_density:
  1.1278 +lemma%important has_bochner_integral_density:
  1.1279    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
  1.1280    shows "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. 0 \<le> g x) \<Longrightarrow>
  1.1281      has_bochner_integral M (\<lambda>x. g x *\<^sub>R f x) x \<Longrightarrow> has_bochner_integral (density M g) f x"
  1.1282    by (simp add: has_bochner_integral_iff integrable_density integral_density)
  1.1283  
  1.1284 -subsection \<open>Distributions\<close>
  1.1285 -
  1.1286 -lemma integrable_distr_eq:
  1.1287 +subsection%important \<open>Distributions\<close>
  1.1288 +
  1.1289 +lemma%unimportant integrable_distr_eq:
  1.1290    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1291    assumes [measurable]: "g \<in> measurable M N" "f \<in> borel_measurable N"
  1.1292    shows "integrable (distr M N g) f \<longleftrightarrow> integrable M (\<lambda>x. f (g x))"
  1.1293    unfolding integrable_iff_bounded by (simp_all add: nn_integral_distr)
  1.1294  
  1.1295 -lemma integrable_distr:
  1.1296 +lemma%unimportant integrable_distr:
  1.1297    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1298    shows "T \<in> measurable M M' \<Longrightarrow> integrable (distr M M' T) f \<Longrightarrow> integrable M (\<lambda>x. f (T x))"
  1.1299    by (subst integrable_distr_eq[symmetric, where g=T])
  1.1300       (auto dest: borel_measurable_integrable)
  1.1301  
  1.1302 -lemma integral_distr:
  1.1303 +lemma%important integral_distr:
  1.1304    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1305    assumes g[measurable]: "g \<in> measurable M N" and f: "f \<in> borel_measurable N"
  1.1306    shows "integral\<^sup>L (distr M N g) f = integral\<^sup>L M (\<lambda>x. f (g x))"
  1.1307 -proof (rule integral_eq_cases)
  1.1308 +proof%unimportant (rule integral_eq_cases)
  1.1309    assume "integrable (distr M N g) f"
  1.1310    then show ?thesis
  1.1311    proof induct
  1.1312 @@ -2404,27 +2404,27 @@
  1.1313    qed
  1.1314  qed (simp add: f g integrable_distr_eq)
  1.1315  
  1.1316 -lemma has_bochner_integral_distr:
  1.1317 +lemma%important has_bochner_integral_distr:
  1.1318    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1319    shows "f \<in> borel_measurable N \<Longrightarrow> g \<in> measurable M N \<Longrightarrow>
  1.1320      has_bochner_integral M (\<lambda>x. f (g x)) x \<Longrightarrow> has_bochner_integral (distr M N g) f x"
  1.1321 -  by (simp add: has_bochner_integral_iff integrable_distr_eq integral_distr)
  1.1322 -
  1.1323 -subsection \<open>Lebesgue integration on @{const count_space}\<close>
  1.1324 -
  1.1325 -lemma integrable_count_space:
  1.1326 +  by%unimportant (simp add: has_bochner_integral_iff integrable_distr_eq integral_distr)
  1.1327 +
  1.1328 +subsection%important \<open>Lebesgue integration on @{const count_space}\<close>
  1.1329 +
  1.1330 +lemma%unimportant integrable_count_space:
  1.1331    fixes f :: "'a \<Rightarrow> 'b::{banach,second_countable_topology}"
  1.1332    shows "finite X \<Longrightarrow> integrable (count_space X) f"
  1.1333    by (auto simp: nn_integral_count_space integrable_iff_bounded)
  1.1334  
  1.1335 -lemma measure_count_space[simp]:
  1.1336 +lemma%unimportant measure_count_space[simp]:
  1.1337    "B \<subseteq> A \<Longrightarrow> finite B \<Longrightarrow> measure (count_space A) B = card B"
  1.1338    unfolding measure_def by (subst emeasure_count_space ) auto
  1.1339  
  1.1340 -lemma lebesgue_integral_count_space_finite_support:
  1.1341 +lemma%important lebesgue_integral_count_space_finite_support:
  1.1342    assumes f: "finite {a\<in>A. f a \<noteq> 0}"
  1.1343    shows "(\<integral>x. f x \<partial>count_space A) = (\<Sum>a | a \<in> A \<and> f a \<noteq> 0. f a)"
  1.1344 -proof -
  1.1345 +proof%unimportant -
  1.1346    have eq: "\<And>x. x \<in> A \<Longrightarrow> (\<Sum>a | x = a \<and> a \<in> A \<and> f a \<noteq> 0. f a) = (\<Sum>x\<in>{x}. f x)"
  1.1347      by (intro sum.mono_neutral_cong_left) auto
  1.1348  
  1.1349 @@ -2436,17 +2436,17 @@
  1.1350      by auto
  1.1351  qed
  1.1352  
  1.1353 -lemma lebesgue_integral_count_space_finite: "finite A \<Longrightarrow> (\<integral>x. f x \<partial>count_space A) = (\<Sum>a\<in>A. f a)"
  1.1354 +lemma%unimportant lebesgue_integral_count_space_finite: "finite A \<Longrightarrow> (\<integral>x. f x \<partial>count_space A) = (\<Sum>a\<in>A. f a)"
  1.1355    by (subst lebesgue_integral_count_space_finite_support)
  1.1356       (auto intro!: sum.mono_neutral_cong_left)
  1.1357  
  1.1358 -lemma integrable_count_space_nat_iff:
  1.1359 +lemma%unimportant integrable_count_space_nat_iff:
  1.1360    fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
  1.1361    shows "integrable (count_space UNIV) f \<longleftrightarrow> summable (\<lambda>x. norm (f x))"
  1.1362    by (auto simp add: integrable_iff_bounded nn_integral_count_space_nat ennreal_suminf_neq_top
  1.1363             intro:  summable_suminf_not_top)
  1.1364  
  1.1365 -lemma sums_integral_count_space_nat:
  1.1366 +lemma%unimportant sums_integral_count_space_nat:
  1.1367    fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
  1.1368    assumes *: "integrable (count_space UNIV) f"
  1.1369    shows "f sums (integral\<^sup>L (count_space UNIV) f)"
  1.1370 @@ -2471,18 +2471,18 @@
  1.1371    finally show ?thesis .
  1.1372  qed
  1.1373  
  1.1374 -lemma integral_count_space_nat:
  1.1375 +lemma%unimportant integral_count_space_nat:
  1.1376    fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
  1.1377    shows "integrable (count_space UNIV) f \<Longrightarrow> integral\<^sup>L (count_space UNIV) f = (\<Sum>x. f x)"
  1.1378    using sums_integral_count_space_nat by (rule sums_unique)
  1.1379  
  1.1380 -lemma integrable_bij_count_space:
  1.1381 +lemma%unimportant integrable_bij_count_space:
  1.1382    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1383    assumes g: "bij_betw g A B"
  1.1384    shows "integrable (count_space A) (\<lambda>x. f (g x)) \<longleftrightarrow> integrable (count_space B) f"
  1.1385    unfolding integrable_iff_bounded by (subst nn_integral_bij_count_space[OF g]) auto
  1.1386  
  1.1387 -lemma integral_bij_count_space:
  1.1388 +lemma%important integral_bij_count_space:
  1.1389    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1390    assumes g: "bij_betw g A B"
  1.1391    shows "integral\<^sup>L (count_space A) (\<lambda>x. f (g x)) = integral\<^sup>L (count_space B) f"
  1.1392 @@ -2492,49 +2492,49 @@
  1.1393    apply auto
  1.1394    done
  1.1395  
  1.1396 -lemma has_bochner_integral_count_space_nat:
  1.1397 +lemma%important has_bochner_integral_count_space_nat:
  1.1398    fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
  1.1399    shows "has_bochner_integral (count_space UNIV) f x \<Longrightarrow> f sums x"
  1.1400    unfolding has_bochner_integral_iff by (auto intro!: sums_integral_count_space_nat)
  1.1401  
  1.1402 -subsection \<open>Point measure\<close>
  1.1403 -
  1.1404 -lemma lebesgue_integral_point_measure_finite:
  1.1405 +subsection%important \<open>Point measure\<close>
  1.1406 +
  1.1407 +lemma%unimportant lebesgue_integral_point_measure_finite:
  1.1408    fixes g :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1409    shows "finite A \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> 0 \<le> f a) \<Longrightarrow>
  1.1410      integral\<^sup>L (point_measure A f) g = (\<Sum>a\<in>A. f a *\<^sub>R g a)"
  1.1411    by (simp add: lebesgue_integral_count_space_finite AE_count_space integral_density point_measure_def)
  1.1412  
  1.1413 -lemma integrable_point_measure_finite:
  1.1414 +lemma%important integrable_point_measure_finite:
  1.1415    fixes g :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and f :: "'a \<Rightarrow> real"
  1.1416    shows "finite A \<Longrightarrow> integrable (point_measure A f) g"
  1.1417 -  unfolding point_measure_def
  1.1418 +  unfolding%unimportant point_measure_def
  1.1419    apply (subst density_cong[where f'="\<lambda>x. ennreal (max 0 (f x))"])
  1.1420    apply (auto split: split_max simp: ennreal_neg)
  1.1421    apply (subst integrable_density)
  1.1422    apply (auto simp: AE_count_space integrable_count_space)
  1.1423    done
  1.1424  
  1.1425 -subsection \<open>Lebesgue integration on @{const null_measure}\<close>
  1.1426 -
  1.1427 -lemma has_bochner_integral_null_measure_iff[iff]:
  1.1428 +subsection%important \<open>Lebesgue integration on @{const null_measure}\<close>
  1.1429 +
  1.1430 +lemma%unimportant has_bochner_integral_null_measure_iff[iff]:
  1.1431    "has_bochner_integral (null_measure M) f 0 \<longleftrightarrow> f \<in> borel_measurable M"
  1.1432    by (auto simp add: has_bochner_integral.simps simple_bochner_integral_def[abs_def]
  1.1433             intro!: exI[of _ "\<lambda>n x. 0"] simple_bochner_integrable.intros)
  1.1434  
  1.1435 -lemma integrable_null_measure_iff[iff]: "integrable (null_measure M) f \<longleftrightarrow> f \<in> borel_measurable M"
  1.1436 -  by (auto simp add: integrable.simps)
  1.1437 -
  1.1438 -lemma integral_null_measure[simp]: "integral\<^sup>L (null_measure M) f = 0"
  1.1439 +lemma%important integrable_null_measure_iff[iff]: "integrable (null_measure M) f \<longleftrightarrow> f \<in> borel_measurable M"
  1.1440 +  by%unimportant (auto simp add: integrable.simps)
  1.1441 +
  1.1442 +lemma%unimportant integral_null_measure[simp]: "integral\<^sup>L (null_measure M) f = 0"
  1.1443    by (cases "integrable (null_measure M) f")
  1.1444       (auto simp add: not_integrable_integral_eq has_bochner_integral_integral_eq)
  1.1445  
  1.1446 -subsection \<open>Legacy lemmas for the real-valued Lebesgue integral\<close>
  1.1447 -
  1.1448 -lemma real_lebesgue_integral_def:
  1.1449 +subsection%important \<open>Legacy lemmas for the real-valued Lebesgue integral\<close>
  1.1450 +
  1.1451 +lemma%important real_lebesgue_integral_def:
  1.1452    assumes f[measurable]: "integrable M f"
  1.1453    shows "integral\<^sup>L M f = enn2real (\<integral>\<^sup>+x. f x \<partial>M) - enn2real (\<integral>\<^sup>+x. ennreal (- f x) \<partial>M)"
  1.1454 -proof -
  1.1455 +proof%unimportant -
  1.1456    have "integral\<^sup>L M f = integral\<^sup>L M (\<lambda>x. max 0 (f x) - max 0 (- f x))"
  1.1457      by (auto intro!: arg_cong[where f="integral\<^sup>L M"])
  1.1458    also have "\<dots> = integral\<^sup>L M (\<lambda>x. max 0 (f x)) - integral\<^sup>L M (\<lambda>x. max 0 (- f x))"
  1.1459 @@ -2546,11 +2546,11 @@
  1.1460    finally show ?thesis .
  1.1461  qed
  1.1462  
  1.1463 -lemma real_integrable_def:
  1.1464 +lemma%important real_integrable_def:
  1.1465    "integrable M f \<longleftrightarrow> f \<in> borel_measurable M \<and>
  1.1466      (\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) \<noteq> \<infinity> \<and> (\<integral>\<^sup>+ x. ennreal (- f x) \<partial>M) \<noteq> \<infinity>"
  1.1467    unfolding integrable_iff_bounded
  1.1468 -proof (safe del: notI)
  1.1469 +proof%unimportant (safe del: notI)
  1.1470    assume *: "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>"
  1.1471    have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M)"
  1.1472      by (intro nn_integral_mono) auto
  1.1473 @@ -2574,12 +2574,12 @@
  1.1474    finally show "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) < \<infinity>" .
  1.1475  qed
  1.1476  
  1.1477 -lemma integrableD[dest]:
  1.1478 +lemma%unimportant integrableD[dest]:
  1.1479    assumes "integrable M f"
  1.1480    shows "f \<in> borel_measurable M" "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>M) \<noteq> \<infinity>" "(\<integral>\<^sup>+ x. ennreal (- f x) \<partial>M) \<noteq> \<infinity>"
  1.1481    using assms unfolding real_integrable_def by auto
  1.1482  
  1.1483 -lemma integrableE:
  1.1484 +lemma%unimportant integrableE:
  1.1485    assumes "integrable M f"
  1.1486    obtains r q where "0 \<le> r" "0 \<le> q"
  1.1487      "(\<integral>\<^sup>+x. ennreal (f x)\<partial>M) = ennreal r"
  1.1488 @@ -2588,7 +2588,7 @@
  1.1489    using assms unfolding real_integrable_def real_lebesgue_integral_def[OF assms]
  1.1490    by (cases rule: ennreal2_cases[of "(\<integral>\<^sup>+x. ennreal (-f x)\<partial>M)" "(\<integral>\<^sup>+x. ennreal (f x)\<partial>M)"]) auto
  1.1491  
  1.1492 -lemma integral_monotone_convergence_nonneg:
  1.1493 +lemma%important integral_monotone_convergence_nonneg:
  1.1494    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
  1.1495    assumes i: "\<And>i. integrable M (f i)" and mono: "AE x in M. mono (\<lambda>n. f n x)"
  1.1496      and pos: "\<And>i. AE x in M. 0 \<le> f i x"
  1.1497 @@ -2597,7 +2597,7 @@
  1.1498      and u: "u \<in> borel_measurable M"
  1.1499    shows "integrable M u"
  1.1500    and "integral\<^sup>L M u = x"
  1.1501 -proof -
  1.1502 +proof%unimportant -
  1.1503    have nn: "AE x in M. \<forall>i. 0 \<le> f i x"
  1.1504      using pos unfolding AE_all_countable by auto
  1.1505    with lim have u_nn: "AE x in M. 0 \<le> u x"
  1.1506 @@ -2629,7 +2629,7 @@
  1.1507      by (auto simp: real_integrable_def real_lebesgue_integral_def u)
  1.1508  qed
  1.1509  
  1.1510 -lemma
  1.1511 +lemma%unimportant (*FIX ME needs name *)
  1.1512    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
  1.1513    assumes f: "\<And>i. integrable M (f i)" and mono: "AE x in M. mono (\<lambda>n. f n x)"
  1.1514    and lim: "AE x in M. (\<lambda>i. f i x) \<longlonglongrightarrow> u x"
  1.1515 @@ -2660,7 +2660,7 @@
  1.1516      by (metis has_bochner_integral_integrable)
  1.1517  qed
  1.1518  
  1.1519 -lemma integral_norm_eq_0_iff:
  1.1520 +lemma%unimportant integral_norm_eq_0_iff:
  1.1521    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1522    assumes f[measurable]: "integrable M f"
  1.1523    shows "(\<integral>x. norm (f x) \<partial>M) = 0 \<longleftrightarrow> emeasure M {x\<in>space M. f x \<noteq> 0} = 0"
  1.1524 @@ -2675,18 +2675,18 @@
  1.1525      by simp
  1.1526  qed
  1.1527  
  1.1528 -lemma integral_0_iff:
  1.1529 +lemma%unimportant integral_0_iff:
  1.1530    fixes f :: "'a \<Rightarrow> real"
  1.1531    shows "integrable M f \<Longrightarrow> (\<integral>x. \<bar>f x\<bar> \<partial>M) = 0 \<longleftrightarrow> emeasure M {x\<in>space M. f x \<noteq> 0} = 0"
  1.1532    using integral_norm_eq_0_iff[of M f] by simp
  1.1533  
  1.1534 -lemma (in finite_measure) integrable_const[intro!, simp]: "integrable M (\<lambda>x. a)"
  1.1535 +lemma%unimportant (in finite_measure) integrable_const[intro!, simp]: "integrable M (\<lambda>x. a)"
  1.1536    using integrable_indicator[of "space M" M a] by (simp cong: integrable_cong add: less_top[symmetric])
  1.1537  
  1.1538 -lemma lebesgue_integral_const[simp]:
  1.1539 +lemma%important lebesgue_integral_const[simp]:
  1.1540    fixes a :: "'a :: {banach, second_countable_topology}"
  1.1541    shows "(\<integral>x. a \<partial>M) = measure M (space M) *\<^sub>R a"
  1.1542 -proof -
  1.1543 +proof%unimportant -
  1.1544    { assume "emeasure M (space M) = \<infinity>" "a \<noteq> 0"
  1.1545      then have ?thesis
  1.1546        by (auto simp add: not_integrable_integral_eq ennreal_mult_less_top measure_def integrable_iff_bounded) }
  1.1547 @@ -2704,7 +2704,7 @@
  1.1548    ultimately show ?thesis by blast
  1.1549  qed
  1.1550  
  1.1551 -lemma (in finite_measure) integrable_const_bound:
  1.1552 +lemma%unimportant (in finite_measure) integrable_const_bound:
  1.1553    fixes f :: "'a \<Rightarrow> 'b::{banach,second_countable_topology}"
  1.1554    shows "AE x in M. norm (f x) \<le> B \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> integrable M f"
  1.1555    apply (rule integrable_bound[OF integrable_const[of B], of f])
  1.1556 @@ -2713,19 +2713,19 @@
  1.1557    apply auto
  1.1558    done
  1.1559  
  1.1560 -lemma (in finite_measure) integral_bounded_eq_bound_then_AE:
  1.1561 +lemma%unimportant (in finite_measure) integral_bounded_eq_bound_then_AE:
  1.1562    assumes "AE x in M. f x \<le> (c::real)"
  1.1563      "integrable M f" "(\<integral>x. f x \<partial>M) = c * measure M (space M)"
  1.1564    shows "AE x in M. f x = c"
  1.1565    apply (rule integral_ineq_eq_0_then_AE) using assms by auto
  1.1566  
  1.1567 -lemma integral_indicator_finite_real:
  1.1568 +lemma%important integral_indicator_finite_real:
  1.1569    fixes f :: "'a \<Rightarrow> real"
  1.1570    assumes [simp]: "finite A"
  1.1571    assumes [measurable]: "\<And>a. a \<in> A \<Longrightarrow> {a} \<in> sets M"
  1.1572    assumes finite: "\<And>a. a \<in> A \<Longrightarrow> emeasure M {a} < \<infinity>"
  1.1573    shows "(\<integral>x. f x * indicator A x \<partial>M) = (\<Sum>a\<in>A. f a * measure M {a})"
  1.1574 -proof -
  1.1575 +proof%unimportant -
  1.1576    have "(\<integral>x. f x * indicator A x \<partial>M) = (\<integral>x. (\<Sum>a\<in>A. f a * indicator {a} x) \<partial>M)"
  1.1577    proof (intro integral_cong refl)
  1.1578      fix x show "f x * indicator A x = (\<Sum>a\<in>A. f a * indicator {a} x)"
  1.1579 @@ -2736,7 +2736,7 @@
  1.1580    finally show ?thesis .
  1.1581  qed
  1.1582  
  1.1583 -lemma (in finite_measure) ennreal_integral_real:
  1.1584 +lemma%unimportant (in finite_measure) ennreal_integral_real:
  1.1585    assumes [measurable]: "f \<in> borel_measurable M"
  1.1586    assumes ae: "AE x in M. f x \<le> ennreal B" "0 \<le> B"
  1.1587    shows "ennreal (\<integral>x. enn2real (f x) \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
  1.1588 @@ -2747,7 +2747,7 @@
  1.1589      using ae by (intro nn_integral_cong_AE) (auto simp: le_less_trans[OF _ ennreal_less_top])
  1.1590  qed auto
  1.1591  
  1.1592 -lemma (in finite_measure) integral_less_AE:
  1.1593 +lemma%unimportant (in finite_measure) integral_less_AE:
  1.1594    fixes X Y :: "'a \<Rightarrow> real"
  1.1595    assumes int: "integrable M X" "integrable M Y"
  1.1596    assumes A: "(emeasure M) A \<noteq> 0" "A \<in> sets M" "AE x in M. x \<in> A \<longrightarrow> X x \<noteq> Y x"
  1.1597 @@ -2778,14 +2778,14 @@
  1.1598    ultimately show ?thesis by auto
  1.1599  qed
  1.1600  
  1.1601 -lemma (in finite_measure) integral_less_AE_space:
  1.1602 +lemma%unimportant (in finite_measure) integral_less_AE_space:
  1.1603    fixes X Y :: "'a \<Rightarrow> real"
  1.1604    assumes int: "integrable M X" "integrable M Y"
  1.1605    assumes gt: "AE x in M. X x < Y x" "emeasure M (space M) \<noteq> 0"
  1.1606    shows "integral\<^sup>L M X < integral\<^sup>L M Y"
  1.1607    using gt by (intro integral_less_AE[OF int, where A="space M"]) auto
  1.1608  
  1.1609 -lemma tendsto_integral_at_top:
  1.1610 +lemma%unimportant tendsto_integral_at_top:
  1.1611    fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
  1.1612    assumes [measurable_cong]: "sets M = sets borel" and f[measurable]: "integrable M f"
  1.1613    shows "((\<lambda>y. \<integral> x. indicator {.. y} x *\<^sub>R f x \<partial>M) \<longlongrightarrow> \<integral> x. f x \<partial>M) at_top"
  1.1614 @@ -2809,7 +2809,7 @@
  1.1615    qed auto
  1.1616  qed
  1.1617  
  1.1618 -lemma
  1.1619 +lemma%unimportant (*FIX ME needs name *)
  1.1620    fixes f :: "real \<Rightarrow> real"
  1.1621    assumes M: "sets M = sets borel"
  1.1622    assumes nonneg: "AE x in M. 0 \<le> f x"
  1.1623 @@ -2840,32 +2840,32 @@
  1.1624      by (auto simp: _has_bochner_integral_iff)
  1.1625  qed
  1.1626  
  1.1627 -subsection \<open>Product measure\<close>
  1.1628 -
  1.1629 -lemma (in sigma_finite_measure) borel_measurable_lebesgue_integrable[measurable (raw)]:
  1.1630 +subsection%important \<open>Product measure\<close>
  1.1631 +
  1.1632 +lemma%important (in sigma_finite_measure) borel_measurable_lebesgue_integrable[measurable (raw)]:
  1.1633    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
  1.1634    assumes [measurable]: "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
  1.1635    shows "Measurable.pred N (\<lambda>x. integrable M (f x))"
  1.1636 -proof -
  1.1637 +proof%unimportant -
  1.1638    have [simp]: "\<And>x. x \<in> space N \<Longrightarrow> integrable M (f x) \<longleftrightarrow> (\<integral>\<^sup>+y. norm (f x y) \<partial>M) < \<infinity>"
  1.1639      unfolding integrable_iff_bounded by simp
  1.1640    show ?thesis
  1.1641      by (simp cong: measurable_cong)
  1.1642  qed
  1.1643  
  1.1644 -lemma Collect_subset [simp]: "{x\<in>A. P x} \<subseteq> A" by auto
  1.1645 -
  1.1646 -lemma (in sigma_finite_measure) measurable_measure[measurable (raw)]:
  1.1647 +lemma%unimportant Collect_subset [simp]: "{x\<in>A. P x} \<subseteq> A" by auto
  1.1648 +
  1.1649 +lemma%unimportant (in sigma_finite_measure) measurable_measure[measurable (raw)]:
  1.1650    "(\<And>x. x \<in> space N \<Longrightarrow> A x \<subseteq> space M) \<Longrightarrow>
  1.1651      {x \<in> space (N \<Otimes>\<^sub>M M). snd x \<in> A (fst x)} \<in> sets (N \<Otimes>\<^sub>M M) \<Longrightarrow>
  1.1652      (\<lambda>x. measure M (A x)) \<in> borel_measurable N"
  1.1653    unfolding measure_def by (intro measurable_emeasure borel_measurable_enn2real) auto
  1.1654  
  1.1655 -lemma (in sigma_finite_measure) borel_measurable_lebesgue_integral[measurable (raw)]:
  1.1656 +lemma%important (in sigma_finite_measure) borel_measurable_lebesgue_integral[measurable (raw)]:
  1.1657    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
  1.1658    assumes f[measurable]: "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
  1.1659    shows "(\<lambda>x. \<integral>y. f x y \<partial>M) \<in> borel_measurable N"
  1.1660 -proof -
  1.1661 +proof%unimportant -
  1.1662    from borel_measurable_implies_sequence_metric[OF f, of 0] guess s ..
  1.1663    then have s: "\<And>i. simple_function (N \<Otimes>\<^sub>M M) (s i)"
  1.1664      "\<And>x y. x \<in> space N \<Longrightarrow> y \<in> space M \<Longrightarrow> (\<lambda>i. s i (x, y)) \<longlonglongrightarrow> f x y"
  1.1665 @@ -2936,7 +2936,7 @@
  1.1666    qed
  1.1667  qed
  1.1668  
  1.1669 -lemma (in pair_sigma_finite) integrable_product_swap:
  1.1670 +lemma%unimportant (in pair_sigma_finite) integrable_product_swap:
  1.1671    fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.1672    assumes "integrable (M1 \<Otimes>\<^sub>M M2) f"
  1.1673    shows "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x,y). f (y,x))"
  1.1674 @@ -2948,7 +2948,7 @@
  1.1675         (simp add: distr_pair_swap[symmetric] assms)
  1.1676  qed
  1.1677  
  1.1678 -lemma (in pair_sigma_finite) integrable_product_swap_iff:
  1.1679 +lemma%unimportant (in pair_sigma_finite) integrable_product_swap_iff:
  1.1680    fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.1681    shows "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x,y). f (y,x)) \<longleftrightarrow> integrable (M1 \<Otimes>\<^sub>M M2) f"
  1.1682  proof -
  1.1683 @@ -2957,7 +2957,7 @@
  1.1684    show ?thesis by auto
  1.1685  qed
  1.1686  
  1.1687 -lemma (in pair_sigma_finite) integral_product_swap:
  1.1688 +lemma%unimportant (in pair_sigma_finite) integral_product_swap:
  1.1689    fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.1690    assumes f: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
  1.1691    shows "(\<integral>(x,y). f (y,x) \<partial>(M2 \<Otimes>\<^sub>M M1)) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) f"
  1.1692 @@ -2967,13 +2967,13 @@
  1.1693      by (simp add: integral_distr[symmetric, OF measurable_pair_swap' f] distr_pair_swap[symmetric])
  1.1694  qed
  1.1695  
  1.1696 -lemma (in pair_sigma_finite) Fubini_integrable:
  1.1697 +lemma%important (in pair_sigma_finite) Fubini_integrable:
  1.1698    fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.1699    assumes f[measurable]: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
  1.1700      and integ1: "integrable M1 (\<lambda>x. \<integral> y. norm (f (x, y)) \<partial>M2)"
  1.1701      and integ2: "AE x in M1. integrable M2 (\<lambda>y. f (x, y))"
  1.1702    shows "integrable (M1 \<Otimes>\<^sub>M M2) f"
  1.1703 -proof (rule integrableI_bounded)
  1.1704 +proof%unimportant (rule integrableI_bounded)
  1.1705    have "(\<integral>\<^sup>+ p. norm (f p) \<partial>(M1 \<Otimes>\<^sub>M M2)) = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. norm (f (x, y)) \<partial>M2) \<partial>M1)"
  1.1706      by (simp add: M2.nn_integral_fst [symmetric])
  1.1707    also have "\<dots> = (\<integral>\<^sup>+ x. \<bar>\<integral>y. norm (f (x, y)) \<partial>M2\<bar> \<partial>M1)"
  1.1708 @@ -2994,7 +2994,7 @@
  1.1709    finally show "(\<integral>\<^sup>+ p. norm (f p) \<partial>(M1 \<Otimes>\<^sub>M M2)) < \<infinity>" .
  1.1710  qed fact
  1.1711  
  1.1712 -lemma (in pair_sigma_finite) emeasure_pair_measure_finite:
  1.1713 +lemma%unimportant (in pair_sigma_finite) emeasure_pair_measure_finite:
  1.1714    assumes A: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" and finite: "emeasure (M1 \<Otimes>\<^sub>M M2) A < \<infinity>"
  1.1715    shows "AE x in M1. emeasure M2 {y\<in>space M2. (x, y) \<in> A} < \<infinity>"
  1.1716  proof -
  1.1717 @@ -3008,7 +3008,7 @@
  1.1718    ultimately show ?thesis by (auto simp: less_top)
  1.1719  qed
  1.1720  
  1.1721 -lemma (in pair_sigma_finite) AE_integrable_fst':
  1.1722 +lemma%unimportant (in pair_sigma_finite) AE_integrable_fst':
  1.1723    fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.1724    assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) f"
  1.1725    shows "AE x in M1. integrable M2 (\<lambda>y. f (x, y))"
  1.1726 @@ -3025,7 +3025,7 @@
  1.1727         (auto simp: integrable_iff_bounded measurable_compose[OF _ borel_measurable_integrable[OF f]] less_top)
  1.1728  qed
  1.1729  
  1.1730 -lemma (in pair_sigma_finite) integrable_fst':
  1.1731 +lemma%unimportant (in pair_sigma_finite) integrable_fst':
  1.1732    fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.1733    assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) f"
  1.1734    shows "integrable M1 (\<lambda>x. \<integral>y. f (x, y) \<partial>M2)"
  1.1735 @@ -3042,11 +3042,11 @@
  1.1736    finally show "(\<integral>\<^sup>+ x. ennreal (norm (\<integral> y. f (x, y) \<partial>M2)) \<partial>M1) < \<infinity>" .
  1.1737  qed
  1.1738  
  1.1739 -lemma (in pair_sigma_finite) integral_fst':
  1.1740 +lemma%important (in pair_sigma_finite) integral_fst':
  1.1741    fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.1742    assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) f"
  1.1743    shows "(\<integral>x. (\<integral>y. f (x, y) \<partial>M2) \<partial>M1) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) f"
  1.1744 -using f proof induct
  1.1745 +using f proof%unimportant induct
  1.1746    case (base A c)
  1.1747    have A[measurable]: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" by fact
  1.1748  
  1.1749 @@ -3155,7 +3155,7 @@
  1.1750    qed
  1.1751  qed
  1.1752  
  1.1753 -lemma (in pair_sigma_finite)
  1.1754 +lemma%unimportant (in pair_sigma_finite) (* FIX ME needs name *)
  1.1755    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
  1.1756    assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
  1.1757    shows AE_integrable_fst: "AE x in M1. integrable M2 (\<lambda>y. f x y)" (is "?AE")
  1.1758 @@ -3163,7 +3163,7 @@
  1.1759      and integral_fst: "(\<integral>x. (\<integral>y. f x y \<partial>M2) \<partial>M1) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). f x y)" (is "?EQ")
  1.1760    using AE_integrable_fst'[OF f] integrable_fst'[OF f] integral_fst'[OF f] by auto
  1.1761  
  1.1762 -lemma (in pair_sigma_finite)
  1.1763 +lemma%unimportant (in pair_sigma_finite) (* FIX ME needs name *)
  1.1764    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
  1.1765    assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
  1.1766    shows AE_integrable_snd: "AE y in M2. integrable M1 (\<lambda>x. f x y)" (is "?AE")
  1.1767 @@ -3179,13 +3179,13 @@
  1.1768      using integral_product_swap[of "case_prod f"] by simp
  1.1769  qed
  1.1770  
  1.1771 -lemma (in pair_sigma_finite) Fubini_integral:
  1.1772 +lemma%unimportant (in pair_sigma_finite) Fubini_integral:
  1.1773    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: {banach, second_countable_topology}"
  1.1774    assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
  1.1775    shows "(\<integral>y. (\<integral>x. f x y \<partial>M1) \<partial>M2) = (\<integral>x. (\<integral>y. f x y \<partial>M2) \<partial>M1)"
  1.1776    unfolding integral_snd[OF assms] integral_fst[OF assms] ..
  1.1777  
  1.1778 -lemma (in product_sigma_finite) product_integral_singleton:
  1.1779 +lemma%unimportant (in product_sigma_finite) product_integral_singleton:
  1.1780    fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.1781    shows "f \<in> borel_measurable (M i) \<Longrightarrow> (\<integral>x. f (x i) \<partial>Pi\<^sub>M {i} M) = integral\<^sup>L (M i) f"
  1.1782    apply (subst distr_singleton[symmetric])
  1.1783 @@ -3193,7 +3193,7 @@
  1.1784    apply simp_all
  1.1785    done
  1.1786  
  1.1787 -lemma (in product_sigma_finite) product_integral_fold:
  1.1788 +lemma%unimportant (in product_sigma_finite) product_integral_fold:
  1.1789    fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.1790    assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
  1.1791    and f: "integrable (Pi\<^sub>M (I \<union> J) M) f"
  1.1792 @@ -3220,12 +3220,12 @@
  1.1793      done
  1.1794  qed
  1.1795  
  1.1796 -lemma (in product_sigma_finite) product_integral_insert:
  1.1797 +lemma%important (in product_sigma_finite) product_integral_insert:
  1.1798    fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
  1.1799    assumes I: "finite I" "i \<notin> I"
  1.1800      and f: "integrable (Pi\<^sub>M (insert i I) M) f"
  1.1801    shows "integral\<^sup>L (Pi\<^sub>M (insert i I) M) f = (\<integral>x. (\<integral>y. f (x(i:=y)) \<partial>M i) \<partial>Pi\<^sub>M I M)"
  1.1802 -proof -
  1.1803 +proof%unimportant -
  1.1804    have "integral\<^sup>L (Pi\<^sub>M (insert i I) M) f = integral\<^sup>L (Pi\<^sub>M (I \<union> {i}) M) f"
  1.1805      by simp
  1.1806    also have "\<dots> = (\<integral>x. (\<integral>y. f (merge I {i} (x,y)) \<partial>Pi\<^sub>M {i} M) \<partial>Pi\<^sub>M I M)"
  1.1807 @@ -3244,11 +3244,11 @@
  1.1808    finally show ?thesis .
  1.1809  qed
  1.1810  
  1.1811 -lemma (in product_sigma_finite) product_integrable_prod:
  1.1812 +lemma%important (in product_sigma_finite) product_integrable_prod:
  1.1813    fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> _::{real_normed_field,banach,second_countable_topology}"
  1.1814    assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
  1.1815    shows "integrable (Pi\<^sub>M I M) (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "integrable _ ?f")
  1.1816 -proof (unfold integrable_iff_bounded, intro conjI)
  1.1817 +proof%unimportant (unfold integrable_iff_bounded, intro conjI)
  1.1818    interpret finite_product_sigma_finite M I by standard fact
  1.1819  
  1.1820    show "?f \<in> borel_measurable (Pi\<^sub>M I M)"
  1.1821 @@ -3263,11 +3263,11 @@
  1.1822    finally show "(\<integral>\<^sup>+ x. ennreal (norm (\<Prod>i\<in>I. f i (x i))) \<partial>Pi\<^sub>M I M) < \<infinity>" .
  1.1823  qed
  1.1824  
  1.1825 -lemma (in product_sigma_finite) product_integral_prod:
  1.1826 +lemma%important (in product_sigma_finite) product_integral_prod:
  1.1827    fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> _::{real_normed_field,banach,second_countable_topology}"
  1.1828    assumes "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
  1.1829    shows "(\<integral>x. (\<Prod>i\<in>I. f i (x i)) \<partial>Pi\<^sub>M I M) = (\<Prod>i\<in>I. integral\<^sup>L (M i) (f i))"
  1.1830 -using assms proof induct
  1.1831 +using assms proof%unimportant induct
  1.1832    case empty
  1.1833    interpret finite_measure "Pi\<^sub>M {} M"
  1.1834      by rule (simp add: space_PiM)
  1.1835 @@ -3286,7 +3286,7 @@
  1.1836      by (simp add: * insert prod subset_insertI)
  1.1837  qed
  1.1838  
  1.1839 -lemma integrable_subalgebra:
  1.1840 +lemma%unimportant integrable_subalgebra:
  1.1841    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1842    assumes borel: "f \<in> borel_measurable N"
  1.1843    and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> emeasure N A = emeasure M A"
  1.1844 @@ -3298,12 +3298,12 @@
  1.1845      using assms by (auto simp: integrable_iff_bounded nn_integral_subalgebra)
  1.1846  qed
  1.1847  
  1.1848 -lemma integral_subalgebra:
  1.1849 +lemma%important integral_subalgebra:
  1.1850    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1.1851    assumes borel: "f \<in> borel_measurable N"
  1.1852    and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> emeasure N A = emeasure M A"
  1.1853    shows "integral\<^sup>L N f = integral\<^sup>L M f"
  1.1854 -proof cases
  1.1855 +proof%unimportant cases
  1.1856    assume "integrable N f"
  1.1857    then show ?thesis
  1.1858    proof induct