7 |
7 |
8 theory Nonnegative_Lebesgue_Integration |
8 theory Nonnegative_Lebesgue_Integration |
9 imports Measure_Space Borel_Space |
9 imports Measure_Space Borel_Space |
10 begin |
10 begin |
11 |
11 |
12 subsection \<open>Approximating functions\<close> |
12 subsection%unimportant \<open>Approximating functions\<close> |
13 |
13 |
14 lemma AE_upper_bound_inf_ennreal: |
14 lemma AE_upper_bound_inf_ennreal: |
15 fixes F G::"'a \<Rightarrow> ennreal" |
15 fixes F G::"'a \<Rightarrow> ennreal" |
16 assumes "\<And>e. (e::real) > 0 \<Longrightarrow> AE x in M. F x \<le> G x + e" |
16 assumes "\<And>e. (e::real) > 0 \<Longrightarrow> AE x in M. F x \<le> G x + e" |
17 shows "AE x in M. F x \<le> G x" |
17 shows "AE x in M. F x \<le> G x" |
113 they are just functions with a finite range and are measurable when singleton |
113 they are just functions with a finite range and are measurable when singleton |
114 sets are measurable. |
114 sets are measurable. |
115 |
115 |
116 \<close> |
116 \<close> |
117 |
117 |
118 definition "simple_function M g \<longleftrightarrow> |
118 definition%important "simple_function M g \<longleftrightarrow> |
119 finite (g ` space M) \<and> |
119 finite (g ` space M) \<and> |
120 (\<forall>x \<in> g ` space M. g -` {x} \<inter> space M \<in> sets M)" |
120 (\<forall>x \<in> g ` space M. g -` {x} \<inter> space M \<in> sets M)" |
121 |
121 |
122 lemma simple_functionD: |
122 lemma simple_functionD: |
123 assumes "simple_function M g" |
123 assumes "simple_function M g" |
299 lemma simple_function_real_of_nat[intro, simp]: |
299 lemma simple_function_real_of_nat[intro, simp]: |
300 fixes f g :: "'a \<Rightarrow> nat" assumes sf: "simple_function M f" |
300 fixes f g :: "'a \<Rightarrow> nat" assumes sf: "simple_function M f" |
301 shows "simple_function M (\<lambda>x. real (f x))" |
301 shows "simple_function M (\<lambda>x. real (f x))" |
302 by (rule simple_function_compose1[OF sf]) |
302 by (rule simple_function_compose1[OF sf]) |
303 |
303 |
304 lemma borel_measurable_implies_simple_function_sequence: |
304 lemma%important borel_measurable_implies_simple_function_sequence: |
305 fixes u :: "'a \<Rightarrow> ennreal" |
305 fixes u :: "'a \<Rightarrow> ennreal" |
306 assumes u[measurable]: "u \<in> borel_measurable M" |
306 assumes u[measurable]: "u \<in> borel_measurable M" |
307 shows "\<exists>f. incseq f \<and> (\<forall>i. (\<forall>x. f i x < top) \<and> simple_function M (f i)) \<and> u = (SUP i. f i)" |
307 shows "\<exists>f. incseq f \<and> (\<forall>i. (\<forall>x. f i x < top) \<and> simple_function M (f i)) \<and> u = (SUP i. f i)" |
308 proof - |
308 proof%unimportant - |
309 define f where [abs_def]: |
309 define f where [abs_def]: |
310 "f i x = real_of_int (floor (enn2real (min i (u x)) * 2^i)) / 2^i" for i x |
310 "f i x = real_of_int (floor (enn2real (min i (u x)) * 2^i)) / 2^i" for i x |
311 |
311 |
312 have [simp]: "0 \<le> f i x" for i x |
312 have [simp]: "0 \<le> f i x" for i x |
313 by (auto simp: f_def intro!: divide_nonneg_nonneg mult_nonneg_nonneg enn2real_nonneg) |
313 by (auto simp: f_def intro!: divide_nonneg_nonneg mult_nonneg_nonneg enn2real_nonneg) |
394 assumes u: "u \<in> borel_measurable M" |
394 assumes u: "u \<in> borel_measurable M" |
395 obtains f where |
395 obtains f where |
396 "\<And>i. simple_function M (f i)" "incseq f" "\<And>i x. f i x < top" "\<And>x. (SUP i. f i x) = u x" |
396 "\<And>i. simple_function M (f i)" "incseq f" "\<And>i x. f i x < top" "\<And>x. (SUP i. f i x) = u x" |
397 using borel_measurable_implies_simple_function_sequence[OF u] by (auto simp: fun_eq_iff) blast |
397 using borel_measurable_implies_simple_function_sequence[OF u] by (auto simp: fun_eq_iff) blast |
398 |
398 |
399 lemma simple_function_induct[consumes 1, case_names cong set mult add, induct set: simple_function]: |
399 lemma%important simple_function_induct |
|
400 [consumes 1, case_names cong set mult add, induct set: simple_function]: |
400 fixes u :: "'a \<Rightarrow> ennreal" |
401 fixes u :: "'a \<Rightarrow> ennreal" |
401 assumes u: "simple_function M u" |
402 assumes u: "simple_function M u" |
402 assumes cong: "\<And>f g. simple_function M f \<Longrightarrow> simple_function M g \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow> P f \<Longrightarrow> P g" |
403 assumes cong: "\<And>f g. simple_function M f \<Longrightarrow> simple_function M g \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow> P f \<Longrightarrow> P g" |
403 assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)" |
404 assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)" |
404 assumes mult: "\<And>u c. P u \<Longrightarrow> P (\<lambda>x. c * u x)" |
405 assumes mult: "\<And>u c. P u \<Longrightarrow> P (\<lambda>x. c * u x)" |
405 assumes add: "\<And>u v. P u \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)" |
406 assumes add: "\<And>u v. P u \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)" |
406 shows "P u" |
407 shows "P u" |
407 proof (rule cong) |
408 proof%unimportant (rule cong) |
408 from AE_space show "AE x in M. (\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x) = u x" |
409 from AE_space show "AE x in M. (\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x) = u x" |
409 proof eventually_elim |
410 proof eventually_elim |
410 fix x assume x: "x \<in> space M" |
411 fix x assume x: "x \<in> space M" |
411 from simple_function_indicator_representation[OF u x] |
412 from simple_function_indicator_representation[OF u x] |
412 show "(\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x) = u x" .. |
413 show "(\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x) = u x" .. |
464 by (auto intro!: add mult set simple_functionD u simple_function_sum disj) |
465 by (auto intro!: add mult set simple_functionD u simple_function_sum disj) |
465 qed |
466 qed |
466 qed fact |
467 qed fact |
467 qed |
468 qed |
468 |
469 |
469 lemma borel_measurable_induct[consumes 1, case_names cong set mult add seq, induct set: borel_measurable]: |
470 lemma%important borel_measurable_induct |
|
471 [consumes 1, case_names cong set mult add seq, induct set: borel_measurable]: |
470 fixes u :: "'a \<Rightarrow> ennreal" |
472 fixes u :: "'a \<Rightarrow> ennreal" |
471 assumes u: "u \<in> borel_measurable M" |
473 assumes u: "u \<in> borel_measurable M" |
472 assumes cong: "\<And>f g. f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P g \<Longrightarrow> P f" |
474 assumes cong: "\<And>f g. f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P g \<Longrightarrow> P f" |
473 assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)" |
475 assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)" |
474 assumes mult': "\<And>u c. c < top \<Longrightarrow> u \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x < top) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)" |
476 assumes mult': "\<And>u c. c < top \<Longrightarrow> u \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x < top) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)" |
475 assumes add: "\<And>u v. u \<in> borel_measurable M\<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x < top) \<Longrightarrow> P u \<Longrightarrow> v \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> v x < top) \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = 0 \<or> v x = 0) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)" |
477 assumes add: "\<And>u v. u \<in> borel_measurable M\<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x < top) \<Longrightarrow> P u \<Longrightarrow> v \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> v x < top) \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = 0 \<or> v x = 0) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)" |
476 assumes seq: "\<And>U. (\<And>i. U i \<in> borel_measurable M) \<Longrightarrow> (\<And>i x. x \<in> space M \<Longrightarrow> U i x < top) \<Longrightarrow> (\<And>i. P (U i)) \<Longrightarrow> incseq U \<Longrightarrow> u = (SUP i. U i) \<Longrightarrow> P (SUP i. U i)" |
478 assumes seq: "\<And>U. (\<And>i. U i \<in> borel_measurable M) \<Longrightarrow> (\<And>i x. x \<in> space M \<Longrightarrow> U i x < top) \<Longrightarrow> (\<And>i. P (U i)) \<Longrightarrow> incseq U \<Longrightarrow> u = (SUP i. U i) \<Longrightarrow> P (SUP i. U i)" |
477 shows "P u" |
479 shows "P u" |
478 using u |
480 using%unimportant u |
479 proof (induct rule: borel_measurable_implies_simple_function_sequence') |
481 proof%unimportant (induct rule: borel_measurable_implies_simple_function_sequence') |
480 fix U assume U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i x. U i x < top" and sup: "\<And>x. (SUP i. U i x) = u x" |
482 fix U assume U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i x. U i x < top" and sup: "\<And>x. (SUP i. U i x) = u x" |
481 have u_eq: "u = (SUP i. U i)" |
483 have u_eq: "u = (SUP i. U i)" |
482 using u sup by auto |
484 using u sup by auto |
483 |
485 |
484 have not_inf: "\<And>x i. x \<in> space M \<Longrightarrow> U i x < top" |
486 have not_inf: "\<And>x i. x \<in> space M \<Longrightarrow> U i x < top" |
575 finally show "(\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M" . |
577 finally show "(\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M" . |
576 qed |
578 qed |
577 |
579 |
578 subsection "Simple integral" |
580 subsection "Simple integral" |
579 |
581 |
580 definition simple_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal" ("integral\<^sup>S") where |
582 definition%important simple_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal" ("integral\<^sup>S") where |
581 "integral\<^sup>S M f = (\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M))" |
583 "integral\<^sup>S M f = (\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M))" |
582 |
584 |
583 syntax |
585 syntax |
584 "_simple_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" ("\<integral>\<^sup>S _. _ \<partial>_" [60,61] 110) |
586 "_simple_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" ("\<integral>\<^sup>S _. _ \<partial>_" [60,61] 110) |
585 |
587 |
808 then show ?thesis by simp |
810 then show ?thesis by simp |
809 qed |
811 qed |
810 |
812 |
811 subsection \<open>Integral on nonnegative functions\<close> |
813 subsection \<open>Integral on nonnegative functions\<close> |
812 |
814 |
813 definition nn_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal" ("integral\<^sup>N") where |
815 definition%important nn_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal" ("integral\<^sup>N") where |
814 "integral\<^sup>N M f = (SUP g \<in> {g. simple_function M g \<and> g \<le> f}. integral\<^sup>S M g)" |
816 "integral\<^sup>N M f = (SUP g \<in> {g. simple_function M g \<and> g \<le> f}. integral\<^sup>S M g)" |
815 |
817 |
816 syntax |
818 syntax |
817 "_nn_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" ("\<integral>\<^sup>+((2 _./ _)/ \<partial>_)" [60,61] 110) |
819 "_nn_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" ("\<integral>\<^sup>+((2 _./ _)/ \<partial>_)" [60,61] 110) |
818 |
820 |
993 with sup_continuous_mono[OF f] show "(\<integral>\<^sup>+ y. f y (Sup (C ` UNIV)) \<partial>M) = (SUP i. \<integral>\<^sup>+ y. f y (C i) \<partial>M)" |
995 with sup_continuous_mono[OF f] show "(\<integral>\<^sup>+ y. f y (Sup (C ` UNIV)) \<partial>M) = (SUP i. \<integral>\<^sup>+ y. f y (C i) \<partial>M)" |
994 unfolding sup_continuousD[OF f C] |
996 unfolding sup_continuousD[OF f C] |
995 by (subst nn_integral_monotone_convergence_SUP) (auto simp: mono_def le_fun_def) |
997 by (subst nn_integral_monotone_convergence_SUP) (auto simp: mono_def le_fun_def) |
996 qed |
998 qed |
997 |
999 |
998 lemma nn_integral_monotone_convergence_SUP_AE: |
1000 theorem nn_integral_monotone_convergence_SUP_AE: |
999 assumes f: "\<And>i. AE x in M. f i x \<le> f (Suc i) x" "\<And>i. f i \<in> borel_measurable M" |
1001 assumes f: "\<And>i. AE x in M. f i x \<le> f (Suc i) x" "\<And>i. f i \<in> borel_measurable M" |
1000 shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>N M (f i))" |
1002 shows "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^sup>N M (f i))" |
1001 proof - |
1003 proof - |
1002 from f have "AE x in M. \<forall>i. f i x \<le> f (Suc i) x" |
1004 from f have "AE x in M. \<forall>i. f i x \<le> f (Suc i) x" |
1003 by (simp add: AE_all_countable) |
1005 by (simp add: AE_all_countable) |
1129 |
1131 |
1130 lemma nn_integral_sum: |
1132 lemma nn_integral_sum: |
1131 "(\<And>i. i \<in> P \<Longrightarrow> f i \<in> borel_measurable M) \<Longrightarrow> (\<integral>\<^sup>+ x. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^sup>N M (f i))" |
1133 "(\<And>i. i \<in> P \<Longrightarrow> f i \<in> borel_measurable M) \<Longrightarrow> (\<integral>\<^sup>+ x. (\<Sum>i\<in>P. f i x) \<partial>M) = (\<Sum>i\<in>P. integral\<^sup>N M (f i))" |
1132 by (induction P rule: infinite_finite_induct) (auto simp: nn_integral_add) |
1134 by (induction P rule: infinite_finite_induct) (auto simp: nn_integral_add) |
1133 |
1135 |
1134 lemma nn_integral_suminf: |
1136 theorem nn_integral_suminf: |
1135 assumes f: "\<And>i. f i \<in> borel_measurable M" |
1137 assumes f: "\<And>i. f i \<in> borel_measurable M" |
1136 shows "(\<integral>\<^sup>+ x. (\<Sum>i. f i x) \<partial>M) = (\<Sum>i. integral\<^sup>N M (f i))" |
1138 shows "(\<integral>\<^sup>+ x. (\<Sum>i. f i x) \<partial>M) = (\<Sum>i. integral\<^sup>N M (f i))" |
1137 proof - |
1139 proof - |
1138 have all_pos: "AE x in M. \<forall>i. 0 \<le> f i x" |
1140 have all_pos: "AE x in M. \<forall>i. 0 \<le> f i x" |
1139 using assms by (auto simp: AE_all_countable) |
1141 using assms by (auto simp: AE_all_countable) |
1173 also have "\<dots> < \<infinity>" |
1175 also have "\<dots> < \<infinity>" |
1174 using bnd supp by (subst nn_integral_cmult) (auto simp: ennreal_mult_less_top) |
1176 using bnd supp by (subst nn_integral_cmult) (auto simp: ennreal_mult_less_top) |
1175 finally show ?thesis . |
1177 finally show ?thesis . |
1176 qed |
1178 qed |
1177 |
1179 |
1178 lemma nn_integral_Markov_inequality: |
1180 theorem nn_integral_Markov_inequality: |
1179 assumes u: "u \<in> borel_measurable M" and "A \<in> sets M" |
1181 assumes u: "u \<in> borel_measurable M" and "A \<in> sets M" |
1180 shows "(emeasure M) ({x\<in>space M. 1 \<le> c * u x} \<inter> A) \<le> c * (\<integral>\<^sup>+ x. u x * indicator A x \<partial>M)" |
1182 shows "(emeasure M) ({x\<in>space M. 1 \<le> c * u x} \<inter> A) \<le> c * (\<integral>\<^sup>+ x. u x * indicator A x \<partial>M)" |
1181 (is "(emeasure M) ?A \<le> _ * ?PI") |
1183 (is "(emeasure M) ?A \<le> _ * ?PI") |
1182 proof - |
1184 proof - |
1183 have "?A \<in> sets M" |
1185 have "?A \<in> sets M" |
1303 finally show "integral\<^sup>N M (f 0) - (\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) = |
1305 finally show "integral\<^sup>N M (f 0) - (\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) = |
1304 integral\<^sup>N M (f 0) - (INF i. \<integral>\<^sup>+ x. f i x \<partial>M)" |
1306 integral\<^sup>N M (f 0) - (INF i. \<integral>\<^sup>+ x. f i x \<partial>M)" |
1305 by (simp add: ennreal_INF_const_minus) |
1307 by (simp add: ennreal_INF_const_minus) |
1306 qed (insert *, auto intro!: nn_integral_mono intro: INF_lower) |
1308 qed (insert *, auto intro!: nn_integral_mono intro: INF_lower) |
1307 |
1309 |
1308 lemma nn_integral_monotone_convergence_INF_AE: |
1310 theorem nn_integral_monotone_convergence_INF_AE: |
1309 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ennreal" |
1311 fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ennreal" |
1310 assumes f: "\<And>i. AE x in M. f (Suc i) x \<le> f i x" |
1312 assumes f: "\<And>i. AE x in M. f (Suc i) x \<le> f i x" |
1311 and [measurable]: "\<And>i. f i \<in> borel_measurable M" |
1313 and [measurable]: "\<And>i. f i \<in> borel_measurable M" |
1312 and fin: "(\<integral>\<^sup>+ x. f i x \<partial>M) < \<infinity>" |
1314 and fin: "(\<integral>\<^sup>+ x. f i x \<partial>M) < \<infinity>" |
1313 shows "(\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) = (INF i. integral\<^sup>N M (f i))" |
1315 shows "(\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) = (INF i. integral\<^sup>N M (f i))" |
1335 lemma nn_integral_monotone_convergence_INF_decseq: |
1337 lemma nn_integral_monotone_convergence_INF_decseq: |
1336 assumes f: "decseq f" and *: "\<And>i. f i \<in> borel_measurable M" "(\<integral>\<^sup>+ x. f i x \<partial>M) < \<infinity>" |
1338 assumes f: "decseq f" and *: "\<And>i. f i \<in> borel_measurable M" "(\<integral>\<^sup>+ x. f i x \<partial>M) < \<infinity>" |
1337 shows "(\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) = (INF i. integral\<^sup>N M (f i))" |
1339 shows "(\<integral>\<^sup>+ x. (INF i. f i x) \<partial>M) = (INF i. integral\<^sup>N M (f i))" |
1338 using nn_integral_monotone_convergence_INF_AE[of f M i, OF _ *] f by (auto simp: decseq_Suc_iff le_fun_def) |
1340 using nn_integral_monotone_convergence_INF_AE[of f M i, OF _ *] f by (auto simp: decseq_Suc_iff le_fun_def) |
1339 |
1341 |
1340 lemma nn_integral_liminf: |
1342 theorem nn_integral_liminf: |
1341 fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ennreal" |
1343 fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ennreal" |
1342 assumes u: "\<And>i. u i \<in> borel_measurable M" |
1344 assumes u: "\<And>i. u i \<in> borel_measurable M" |
1343 shows "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^sup>N M (u n))" |
1345 shows "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^sup>N M (u n))" |
1344 proof - |
1346 proof - |
1345 have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) = (SUP n. \<integral>\<^sup>+ x. (INF i\<in>{n..}. u i x) \<partial>M)" |
1347 have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) = (SUP n. \<integral>\<^sup>+ x. (INF i\<in>{n..}. u i x) \<partial>M)" |
1349 also have "\<dots> \<le> liminf (\<lambda>n. integral\<^sup>N M (u n))" |
1351 also have "\<dots> \<le> liminf (\<lambda>n. integral\<^sup>N M (u n))" |
1350 by (auto simp: liminf_SUP_INF intro!: SUP_mono INF_greatest nn_integral_mono INF_lower) |
1352 by (auto simp: liminf_SUP_INF intro!: SUP_mono INF_greatest nn_integral_mono INF_lower) |
1351 finally show ?thesis . |
1353 finally show ?thesis . |
1352 qed |
1354 qed |
1353 |
1355 |
1354 lemma nn_integral_limsup: |
1356 theorem nn_integral_limsup: |
1355 fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ennreal" |
1357 fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ennreal" |
1356 assumes [measurable]: "\<And>i. u i \<in> borel_measurable M" "w \<in> borel_measurable M" |
1358 assumes [measurable]: "\<And>i. u i \<in> borel_measurable M" "w \<in> borel_measurable M" |
1357 assumes bounds: "\<And>i. AE x in M. u i x \<le> w x" and w: "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>" |
1359 assumes bounds: "\<And>i. AE x in M. u i x \<le> w x" and w: "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>" |
1358 shows "limsup (\<lambda>n. integral\<^sup>N M (u n)) \<le> (\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M)" |
1360 shows "limsup (\<lambda>n. integral\<^sup>N M (u n)) \<le> (\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M)" |
1359 proof - |
1361 proof - |
1382 also have "integral\<^sup>N M (\<lambda>x. SUP n. f n x) = integral\<^sup>N M (\<lambda>x. u x)" |
1384 also have "integral\<^sup>N M (\<lambda>x. SUP n. f n x) = integral\<^sup>N M (\<lambda>x. u x)" |
1383 using f by (subst LIMSEQ_SUP[THEN LIMSEQ_unique, OF _ u]) (auto simp: incseq_def le_fun_def) |
1385 using f by (subst LIMSEQ_SUP[THEN LIMSEQ_unique, OF _ u]) (auto simp: incseq_def le_fun_def) |
1384 finally show ?thesis . |
1386 finally show ?thesis . |
1385 qed |
1387 qed |
1386 |
1388 |
1387 lemma nn_integral_dominated_convergence: |
1389 theorem nn_integral_dominated_convergence: |
1388 assumes [measurable]: |
1390 assumes [measurable]: |
1389 "\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M" |
1391 "\<And>i. u i \<in> borel_measurable M" "u' \<in> borel_measurable M" "w \<in> borel_measurable M" |
1390 and bound: "\<And>j. AE x in M. u j x \<le> w x" |
1392 and bound: "\<And>j. AE x in M. u j x \<le> w x" |
1391 and w: "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>" |
1393 and w: "(\<integral>\<^sup>+x. w x \<partial>M) < \<infinity>" |
1392 and u': "AE x in M. (\<lambda>i. u i x) \<longlonglongrightarrow> u' x" |
1394 and u': "AE x in M. (\<lambda>i. u i x) \<longlonglongrightarrow> u' x" |
1570 by (simp add: nn_integral_suminf) |
1572 by (simp add: nn_integral_suminf) |
1571 finally show ?thesis |
1573 finally show ?thesis |
1572 by (simp add: F_def) |
1574 by (simp add: F_def) |
1573 qed |
1575 qed |
1574 |
1576 |
1575 lemma nn_integral_lfp: |
1577 theorem nn_integral_lfp: |
1576 assumes sets[simp]: "\<And>s. sets (M s) = sets N" |
1578 assumes sets[simp]: "\<And>s. sets (M s) = sets N" |
1577 assumes f: "sup_continuous f" |
1579 assumes f: "sup_continuous f" |
1578 assumes g: "sup_continuous g" |
1580 assumes g: "sup_continuous g" |
1579 assumes meas: "\<And>F. F \<in> borel_measurable N \<Longrightarrow> f F \<in> borel_measurable N" |
1581 assumes meas: "\<And>F. F \<in> borel_measurable N \<Longrightarrow> f F \<in> borel_measurable N" |
1580 assumes step: "\<And>F s. F \<in> borel_measurable N \<Longrightarrow> integral\<^sup>N (M s) (f F) = g (\<lambda>s. integral\<^sup>N (M s) F) s" |
1582 assumes step: "\<And>F s. F \<in> borel_measurable N \<Longrightarrow> integral\<^sup>N (M s) (f F) = g (\<lambda>s. integral\<^sup>N (M s) F) s" |
1585 unfolding SUP_apply[abs_def] |
1587 unfolding SUP_apply[abs_def] |
1586 by (subst nn_integral_monotone_convergence_SUP) |
1588 by (subst nn_integral_monotone_convergence_SUP) |
1587 (auto simp: mono_def fun_eq_iff intro!: arg_cong2[where f=emeasure] cong: measurable_cong_sets) |
1589 (auto simp: mono_def fun_eq_iff intro!: arg_cong2[where f=emeasure] cong: measurable_cong_sets) |
1588 qed (auto simp add: step le_fun_def SUP_apply[abs_def] bot_fun_def bot_ennreal intro!: meas f g) |
1590 qed (auto simp add: step le_fun_def SUP_apply[abs_def] bot_fun_def bot_ennreal intro!: meas f g) |
1589 |
1591 |
1590 lemma nn_integral_gfp: |
1592 theorem nn_integral_gfp: |
1591 assumes sets[simp]: "\<And>s. sets (M s) = sets N" |
1593 assumes sets[simp]: "\<And>s. sets (M s) = sets N" |
1592 assumes f: "inf_continuous f" and g: "inf_continuous g" |
1594 assumes f: "inf_continuous f" and g: "inf_continuous g" |
1593 assumes meas: "\<And>F. F \<in> borel_measurable N \<Longrightarrow> f F \<in> borel_measurable N" |
1595 assumes meas: "\<And>F. F \<in> borel_measurable N \<Longrightarrow> f F \<in> borel_measurable N" |
1594 assumes bound: "\<And>F s. F \<in> borel_measurable N \<Longrightarrow> (\<integral>\<^sup>+x. f F x \<partial>M s) < \<infinity>" |
1596 assumes bound: "\<And>F s. F \<in> borel_measurable N \<Longrightarrow> (\<integral>\<^sup>+x. f F x \<partial>M s) < \<infinity>" |
1595 assumes non_zero: "\<And>s. emeasure (M s) (space (M s)) \<noteq> 0" |
1597 assumes non_zero: "\<And>s. emeasure (M s) (space (M s)) \<noteq> 0" |
1617 show "\<And>x. x \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) x < \<infinity>) \<Longrightarrow> |
1619 show "\<And>x. x \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) x < \<infinity>) \<Longrightarrow> |
1618 (\<lambda>s. integral\<^sup>N (M s) (f x)) = g (\<lambda>s. integral\<^sup>N (M s) x)" |
1620 (\<lambda>s. integral\<^sup>N (M s) (f x)) = g (\<lambda>s. integral\<^sup>N (M s) x)" |
1619 by (subst step) auto |
1621 by (subst step) auto |
1620 qed (insert bound, auto simp add: le_fun_def INF_apply[abs_def] top_fun_def intro!: meas f g) |
1622 qed (insert bound, auto simp add: le_fun_def INF_apply[abs_def] top_fun_def intro!: meas f g) |
1621 |
1623 |
|
1624 (* TODO: rename? *) |
1622 subsection \<open>Integral under concrete measures\<close> |
1625 subsection \<open>Integral under concrete measures\<close> |
1623 |
1626 |
1624 lemma nn_integral_mono_measure: |
1627 lemma nn_integral_mono_measure: |
1625 assumes "sets M = sets N" "M \<le> N" shows "nn_integral M f \<le> nn_integral N f" |
1628 assumes "sets M = sets N" "M \<le> N" shows "nn_integral M f \<le> nn_integral N f" |
1626 unfolding nn_integral_def |
1629 unfolding nn_integral_def |
1643 qed |
1646 qed |
1644 |
1647 |
1645 lemma nn_integral_bot[simp]: "nn_integral bot f = 0" |
1648 lemma nn_integral_bot[simp]: "nn_integral bot f = 0" |
1646 by (simp add: nn_integral_empty) |
1649 by (simp add: nn_integral_empty) |
1647 |
1650 |
1648 subsubsection \<open>Distributions\<close> |
1651 subsubsection%unimportant \<open>Distributions\<close> |
1649 |
1652 |
1650 lemma nn_integral_distr: |
1653 lemma nn_integral_distr: |
1651 assumes T: "T \<in> measurable M M'" and f: "f \<in> borel_measurable (distr M M' T)" |
1654 assumes T: "T \<in> measurable M M'" and f: "f \<in> borel_measurable (distr M M' T)" |
1652 shows "integral\<^sup>N (distr M M' T) f = (\<integral>\<^sup>+ x. f (T x) \<partial>M)" |
1655 shows "integral\<^sup>N (distr M M' T) f = (\<integral>\<^sup>+ x. f (T x) \<partial>M)" |
1653 using f |
1656 using f |
1668 by (subst nn_integral_cong[OF eq]) |
1671 by (subst nn_integral_cong[OF eq]) |
1669 (auto simp add: emeasure_distr intro!: nn_integral_indicator[symmetric] measurable_sets) |
1672 (auto simp add: emeasure_distr intro!: nn_integral_indicator[symmetric] measurable_sets) |
1670 qed (simp_all add: measurable_compose[OF T] T nn_integral_cmult nn_integral_add |
1673 qed (simp_all add: measurable_compose[OF T] T nn_integral_cmult nn_integral_add |
1671 nn_integral_monotone_convergence_SUP le_fun_def incseq_def) |
1674 nn_integral_monotone_convergence_SUP le_fun_def incseq_def) |
1672 |
1675 |
1673 subsubsection \<open>Counting space\<close> |
1676 subsubsection%unimportant \<open>Counting space\<close> |
1674 |
1677 |
1675 lemma simple_function_count_space[simp]: |
1678 lemma simple_function_count_space[simp]: |
1676 "simple_function (count_space A) f \<longleftrightarrow> finite (f ` A)" |
1679 "simple_function (count_space A) f \<longleftrightarrow> finite (f ` A)" |
1677 unfolding simple_function_def by simp |
1680 unfolding simple_function_def by simp |
1678 |
1681 |
2081 finally show ?thesis . |
2084 finally show ?thesis . |
2082 qed |
2085 qed |
2083 |
2086 |
2084 subsubsection \<open>Measure spaces with an associated density\<close> |
2087 subsubsection \<open>Measure spaces with an associated density\<close> |
2085 |
2088 |
2086 definition density :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where |
2089 definition%important density :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where |
2087 "density M f = measure_of (space M) (sets M) (\<lambda>A. \<integral>\<^sup>+ x. f x * indicator A x \<partial>M)" |
2090 "density M f = measure_of (space M) (sets M) (\<lambda>A. \<integral>\<^sup>+ x. f x * indicator A x \<partial>M)" |
2088 |
2091 |
2089 lemma |
2092 lemma |
2090 shows sets_density[simp, measurable_cong]: "sets (density M f) = sets M" |
2093 shows sets_density[simp, measurable_cong]: "sets (density M f) = sets M" |
2091 and space_density[simp]: "space (density M f) = space M" |
2094 and space_density[simp]: "space (density M f) = space M" |
2168 using ae2 |
2171 using ae2 |
2169 unfolding eventually_ae_filter[of _ "density M f"] Bex_def null_sets_density_iff[OF f] |
2172 unfolding eventually_ae_filter[of _ "density M f"] Bex_def null_sets_density_iff[OF f] |
2170 by (intro exI[of _ "N \<union> {x\<in>space M. f x = 0}"] conjI *) (auto elim: eventually_elim2) |
2173 by (intro exI[of _ "N \<union> {x\<in>space M. f x = 0}"] conjI *) (auto elim: eventually_elim2) |
2171 qed |
2174 qed |
2172 |
2175 |
2173 lemma nn_integral_density: |
2176 lemma%important nn_integral_density: |
2174 assumes f: "f \<in> borel_measurable M" |
2177 assumes f: "f \<in> borel_measurable M" |
2175 assumes g: "g \<in> borel_measurable M" |
2178 assumes g: "g \<in> borel_measurable M" |
2176 shows "integral\<^sup>N (density M f) g = (\<integral>\<^sup>+ x. f x * g x \<partial>M)" |
2179 shows "integral\<^sup>N (density M f) g = (\<integral>\<^sup>+ x. f x * g x \<partial>M)" |
2177 using g proof induct |
2180 using%unimportant g proof%unimportant induct |
2178 case (cong u v) |
2181 case (cong u v) |
2179 then show ?case |
2182 then show ?case |
2180 apply (subst nn_integral_cong[OF cong(3)]) |
2183 apply (subst nn_integral_cong[OF cong(3)]) |
2181 apply (simp_all cong: nn_integral_cong) |
2184 apply (simp_all cong: nn_integral_cong) |
2182 done |
2185 done |
2291 apply (intro nn_integral_cong, simp split: split_indicator) |
2294 apply (intro nn_integral_cong, simp split: split_indicator) |
2292 done |
2295 done |
2293 |
2296 |
2294 subsubsection \<open>Point measure\<close> |
2297 subsubsection \<open>Point measure\<close> |
2295 |
2298 |
2296 definition point_measure :: "'a set \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where |
2299 definition%important point_measure :: "'a set \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where |
2297 "point_measure A f = density (count_space A) f" |
2300 "point_measure A f = density (count_space A) f" |
2298 |
2301 |
2299 lemma |
2302 lemma |
2300 shows space_point_measure: "space (point_measure A f) = A" |
2303 shows space_point_measure: "space (point_measure A f) = A" |
2301 and sets_point_measure: "sets (point_measure A f) = Pow A" |
2304 and sets_point_measure: "sets (point_measure A f) = Pow A" |
2357 "finite A \<Longrightarrow> integral\<^sup>N (point_measure A f) g = (\<Sum>a\<in>A. f a * g a)" |
2360 "finite A \<Longrightarrow> integral\<^sup>N (point_measure A f) g = (\<Sum>a\<in>A. f a * g a)" |
2358 by (subst nn_integral_point_measure) (auto intro!: sum.mono_neutral_left simp: less_le) |
2361 by (subst nn_integral_point_measure) (auto intro!: sum.mono_neutral_left simp: less_le) |
2359 |
2362 |
2360 subsubsection \<open>Uniform measure\<close> |
2363 subsubsection \<open>Uniform measure\<close> |
2361 |
2364 |
2362 definition "uniform_measure M A = density M (\<lambda>x. indicator A x / emeasure M A)" |
2365 definition%important "uniform_measure M A = density M (\<lambda>x. indicator A x / emeasure M A)" |
2363 |
2366 |
2364 lemma |
2367 lemma |
2365 shows sets_uniform_measure[simp, measurable_cong]: "sets (uniform_measure M A) = sets M" |
2368 shows sets_uniform_measure[simp, measurable_cong]: "sets (uniform_measure M A) = sets M" |
2366 and space_uniform_measure[simp]: "space (uniform_measure M A) = space M" |
2369 and space_uniform_measure[simp]: "space (uniform_measure M A) = space M" |
2367 by (auto simp: uniform_measure_def) |
2370 by (auto simp: uniform_measure_def) |
2432 by (cases "emeasure M A") (auto split: split_indicator simp: ennreal_zero_less_divide) |
2435 by (cases "emeasure M A") (auto split: split_indicator simp: ennreal_zero_less_divide) |
2433 ultimately show ?thesis |
2436 ultimately show ?thesis |
2434 unfolding uniform_measure_def by (simp add: AE_density) |
2437 unfolding uniform_measure_def by (simp add: AE_density) |
2435 qed |
2438 qed |
2436 |
2439 |
2437 subsubsection \<open>Null measure\<close> |
2440 subsubsection%unimportant \<open>Null measure\<close> |
2438 |
2441 |
2439 lemma null_measure_eq_density: "null_measure M = density M (\<lambda>_. 0)" |
2442 lemma null_measure_eq_density: "null_measure M = density M (\<lambda>_. 0)" |
2440 by (intro measure_eqI) (simp_all add: emeasure_density) |
2443 by (intro measure_eqI) (simp_all add: emeasure_density) |
2441 |
2444 |
2442 lemma nn_integral_null_measure[simp]: "(\<integral>\<^sup>+x. f x \<partial>null_measure M) = 0" |
2445 lemma nn_integral_null_measure[simp]: "(\<integral>\<^sup>+x. f x \<partial>null_measure M) = 0" |
2449 by (simp add: density_def) (simp only: null_measure_def[symmetric] emeasure_null_measure) |
2452 by (simp add: density_def) (simp only: null_measure_def[symmetric] emeasure_null_measure) |
2450 qed simp |
2453 qed simp |
2451 |
2454 |
2452 subsubsection \<open>Uniform count measure\<close> |
2455 subsubsection \<open>Uniform count measure\<close> |
2453 |
2456 |
2454 definition "uniform_count_measure A = point_measure A (\<lambda>x. 1 / card A)" |
2457 definition%important "uniform_count_measure A = point_measure A (\<lambda>x. 1 / card A)" |
2455 |
2458 |
2456 lemma |
2459 lemma |
2457 shows space_uniform_count_measure: "space (uniform_count_measure A) = A" |
2460 shows space_uniform_count_measure: "space (uniform_count_measure A) = A" |
2458 and sets_uniform_count_measure: "sets (uniform_count_measure A) = Pow A" |
2461 and sets_uniform_count_measure: "sets (uniform_count_measure A) = Pow A" |
2459 unfolding uniform_count_measure_def by (auto simp: space_point_measure sets_point_measure) |
2462 unfolding uniform_count_measure_def by (auto simp: space_point_measure sets_point_measure) |
2478 lemma sets_uniform_count_measure_eq_UNIV [simp]: |
2481 lemma sets_uniform_count_measure_eq_UNIV [simp]: |
2479 "sets (uniform_count_measure UNIV) = UNIV \<longleftrightarrow> True" |
2482 "sets (uniform_count_measure UNIV) = UNIV \<longleftrightarrow> True" |
2480 "UNIV = sets (uniform_count_measure UNIV) \<longleftrightarrow> True" |
2483 "UNIV = sets (uniform_count_measure UNIV) \<longleftrightarrow> True" |
2481 by(simp_all add: sets_uniform_count_measure) |
2484 by(simp_all add: sets_uniform_count_measure) |
2482 |
2485 |
2483 subsubsection \<open>Scaled measure\<close> |
2486 subsubsection%unimportant \<open>Scaled measure\<close> |
2484 |
2487 |
2485 lemma nn_integral_scale_measure: |
2488 lemma nn_integral_scale_measure: |
2486 assumes f: "f \<in> borel_measurable M" |
2489 assumes f: "f \<in> borel_measurable M" |
2487 shows "nn_integral (scale_measure r M) f = r * nn_integral M f" |
2490 shows "nn_integral (scale_measure r M) f = r * nn_integral M f" |
2488 using f |
2491 using f |