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.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.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.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.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.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.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.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.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.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.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
```