819 translations |
819 translations |
820 "\<integral>\<^sup>+x. f \<partial>M" == "CONST nn_integral M (\<lambda>x. f)" |
820 "\<integral>\<^sup>+x. f \<partial>M" == "CONST nn_integral M (\<lambda>x. f)" |
821 |
821 |
822 lemma nn_integral_def_finite: |
822 lemma nn_integral_def_finite: |
823 "integral\<^sup>N M f = (SUP g \<in> {g. simple_function M g \<and> g \<le> f \<and> (\<forall>x. g x < top)}. integral\<^sup>S M g)" |
823 "integral\<^sup>N M f = (SUP g \<in> {g. simple_function M g \<and> g \<le> f \<and> (\<forall>x. g x < top)}. integral\<^sup>S M g)" |
824 (is "_ = SUPREMUM ?A ?f") |
824 (is "_ = Sup (?A ` ?f)") |
825 unfolding nn_integral_def |
825 unfolding nn_integral_def |
826 proof (safe intro!: antisym SUP_least) |
826 proof (safe intro!: antisym SUP_least) |
827 fix g assume g[measurable]: "simple_function M g" "g \<le> f" |
827 fix g assume g[measurable]: "simple_function M g" "g \<le> f" |
828 |
828 |
829 show "integral\<^sup>S M g \<le> SUPREMUM ?A ?f" |
829 show "integral\<^sup>S M g \<le> Sup (?A ` ?f)" |
830 proof cases |
830 proof cases |
831 assume ae: "AE x in M. g x \<noteq> top" |
831 assume ae: "AE x in M. g x \<noteq> top" |
832 let ?G = "{x \<in> space M. g x \<noteq> top}" |
832 let ?G = "{x \<in> space M. g x \<noteq> top}" |
833 have "integral\<^sup>S M g = integral\<^sup>S M (\<lambda>x. g x * indicator ?G x)" |
833 have "integral\<^sup>S M g = integral\<^sup>S M (\<lambda>x. g x * indicator ?G x)" |
834 proof (rule simple_integral_cong_AE) |
834 proof (rule simple_integral_cong_AE) |
835 show "AE x in M. g x = g x * indicator ?G x" |
835 show "AE x in M. g x = g x * indicator ?G x" |
836 using ae AE_space by eventually_elim auto |
836 using ae AE_space by eventually_elim auto |
837 qed (insert g, auto) |
837 qed (insert g, auto) |
838 also have "\<dots> \<le> SUPREMUM ?A ?f" |
838 also have "\<dots> \<le> Sup (?A ` ?f)" |
839 using g by (intro SUP_upper) (auto simp: le_fun_def less_top split: split_indicator) |
839 using g by (intro SUP_upper) (auto simp: le_fun_def less_top split: split_indicator) |
840 finally show ?thesis . |
840 finally show ?thesis . |
841 next |
841 next |
842 assume nAE: "\<not> (AE x in M. g x \<noteq> top)" |
842 assume nAE: "\<not> (AE x in M. g x \<noteq> top)" |
843 then have "emeasure M {x\<in>space M. g x = top} \<noteq> 0" (is "emeasure M ?G \<noteq> 0") |
843 then have "emeasure M {x\<in>space M. g x = top} \<noteq> 0" (is "emeasure M ?G \<noteq> 0") |
844 by (subst (asm) AE_iff_measurable[OF _ refl]) auto |
844 by (subst (asm) AE_iff_measurable[OF _ refl]) auto |
845 then have "top = (SUP n. (\<integral>\<^sup>Sx. of_nat n * indicator ?G x \<partial>M))" |
845 then have "top = (SUP n. (\<integral>\<^sup>Sx. of_nat n * indicator ?G x \<partial>M))" |
846 by (simp add: ennreal_SUP_of_nat_eq_top ennreal_top_eq_mult_iff SUP_mult_right_ennreal[symmetric]) |
846 by (simp add: ennreal_SUP_of_nat_eq_top ennreal_top_eq_mult_iff SUP_mult_right_ennreal[symmetric]) |
847 also have "\<dots> \<le> SUPREMUM ?A ?f" |
847 also have "\<dots> \<le> Sup (?A ` ?f)" |
848 using g |
848 using g |
849 by (safe intro!: SUP_least SUP_upper) |
849 by (safe intro!: SUP_least SUP_upper) |
850 (auto simp: le_fun_def of_nat_less_top top_unique[symmetric] split: split_indicator |
850 (auto simp: le_fun_def of_nat_less_top top_unique[symmetric] split: split_indicator |
851 intro: order_trans[of _ "g x" "f x" for x, OF order_trans[of _ top]]) |
851 intro: order_trans[of _ "g x" "f x" for x, OF order_trans[of _ top]]) |
852 finally show ?thesis |
852 finally show ?thesis |
988 assumes [measurable]: "\<And>x. (\<lambda>y. f y x) \<in> borel_measurable M" |
988 assumes [measurable]: "\<And>x. (\<lambda>y. f y x) \<in> borel_measurable M" |
989 shows "sup_continuous (\<lambda>x. (\<integral>\<^sup>+y. f y x \<partial>M))" |
989 shows "sup_continuous (\<lambda>x. (\<integral>\<^sup>+y. f y x \<partial>M))" |
990 unfolding sup_continuous_def |
990 unfolding sup_continuous_def |
991 proof safe |
991 proof safe |
992 fix C :: "nat \<Rightarrow> 'b" assume C: "incseq C" |
992 fix C :: "nat \<Rightarrow> 'b" assume C: "incseq C" |
993 with sup_continuous_mono[OF f] show "(\<integral>\<^sup>+ y. f y (SUPREMUM UNIV C) \<partial>M) = (SUP i. \<integral>\<^sup>+ y. f y (C i) \<partial>M)" |
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)" |
994 unfolding sup_continuousD[OF f C] |
994 unfolding sup_continuousD[OF f C] |
995 by (subst nn_integral_monotone_convergence_SUP) (auto simp: mono_def le_fun_def) |
995 by (subst nn_integral_monotone_convergence_SUP) (auto simp: mono_def le_fun_def) |
996 qed |
996 qed |
997 |
997 |
998 lemma nn_integral_monotone_convergence_SUP_AE: |
998 lemma nn_integral_monotone_convergence_SUP_AE: |
1011 show "incseq ?f" using N(1) by (force intro!: incseq_SucI le_funI) |
1011 show "incseq ?f" using N(1) by (force intro!: incseq_SucI le_funI) |
1012 { fix i show "(\<lambda>x. if x \<in> space M - N then f i x else 0) \<in> borel_measurable M" |
1012 { fix i show "(\<lambda>x. if x \<in> space M - N then f i x else 0) \<in> borel_measurable M" |
1013 using f N(3) by (intro measurable_If_set) auto } |
1013 using f N(3) by (intro measurable_If_set) auto } |
1014 qed |
1014 qed |
1015 also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. f i x \<partial>M))" |
1015 also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. f i x \<partial>M))" |
1016 using f_eq by (force intro!: arg_cong[where f="SUPREMUM UNIV"] nn_integral_cong_AE ext) |
1016 using f_eq by (force intro!: arg_cong[where f = "\<lambda>f. Sup (range f)"] nn_integral_cong_AE ext) |
1017 finally show ?thesis . |
1017 finally show ?thesis . |
1018 qed |
1018 qed |
1019 |
1019 |
1020 lemma nn_integral_monotone_convergence_simple: |
1020 lemma nn_integral_monotone_convergence_simple: |
1021 "incseq f \<Longrightarrow> (\<And>i. simple_function M (f i)) \<Longrightarrow> (SUP i. \<integral>\<^sup>S x. f i x \<partial>M) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)" |
1021 "incseq f \<Longrightarrow> (\<And>i. simple_function M (f i)) \<Longrightarrow> (SUP i. \<integral>\<^sup>S x. f i x \<partial>M) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)" |
1025 lemma SUP_simple_integral_sequences: |
1025 lemma SUP_simple_integral_sequences: |
1026 assumes f: "incseq f" "\<And>i. simple_function M (f i)" |
1026 assumes f: "incseq f" "\<And>i. simple_function M (f i)" |
1027 and g: "incseq g" "\<And>i. simple_function M (g i)" |
1027 and g: "incseq g" "\<And>i. simple_function M (g i)" |
1028 and eq: "AE x in M. (SUP i. f i x) = (SUP i. g i x)" |
1028 and eq: "AE x in M. (SUP i. f i x) = (SUP i. g i x)" |
1029 shows "(SUP i. integral\<^sup>S M (f i)) = (SUP i. integral\<^sup>S M (g i))" |
1029 shows "(SUP i. integral\<^sup>S M (f i)) = (SUP i. integral\<^sup>S M (g i))" |
1030 (is "SUPREMUM _ ?F = SUPREMUM _ ?G") |
1030 (is "Sup (?F ` _) = Sup (?G ` _)") |
1031 proof - |
1031 proof - |
1032 have "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)" |
1032 have "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)" |
1033 using f by (rule nn_integral_monotone_convergence_simple) |
1033 using f by (rule nn_integral_monotone_convergence_simple) |
1034 also have "\<dots> = (\<integral>\<^sup>+x. (SUP i. g i x) \<partial>M)" |
1034 also have "\<dots> = (\<integral>\<^sup>+x. (SUP i. g i x) \<partial>M)" |
1035 unfolding eq[THEN nn_integral_cong_AE] .. |
1035 unfolding eq[THEN nn_integral_cong_AE] .. |
1412 assumes bnd: "\<And>x. (\<integral>\<^sup>+ y. f y x \<partial>M) \<noteq> \<infinity>" |
1412 assumes bnd: "\<And>x. (\<integral>\<^sup>+ y. f y x \<partial>M) \<noteq> \<infinity>" |
1413 shows "inf_continuous (\<lambda>x. (\<integral>\<^sup>+y. f y x \<partial>M))" |
1413 shows "inf_continuous (\<lambda>x. (\<integral>\<^sup>+y. f y x \<partial>M))" |
1414 unfolding inf_continuous_def |
1414 unfolding inf_continuous_def |
1415 proof safe |
1415 proof safe |
1416 fix C :: "nat \<Rightarrow> 'b" assume C: "decseq C" |
1416 fix C :: "nat \<Rightarrow> 'b" assume C: "decseq C" |
1417 then show "(\<integral>\<^sup>+ y. f y (INFIMUM UNIV C) \<partial>M) = (INF i. \<integral>\<^sup>+ y. f y (C i) \<partial>M)" |
1417 then show "(\<integral>\<^sup>+ y. f y (Inf (C ` UNIV)) \<partial>M) = (INF i. \<integral>\<^sup>+ y. f y (C i) \<partial>M)" |
1418 using inf_continuous_mono[OF f] bnd |
1418 using inf_continuous_mono[OF f] bnd |
1419 by (auto simp add: inf_continuousD[OF f C] fun_eq_iff antimono_def mono_def le_fun_def less_top |
1419 by (auto simp add: inf_continuousD[OF f C] fun_eq_iff antimono_def mono_def le_fun_def less_top |
1420 intro!: nn_integral_monotone_convergence_INF_decseq) |
1420 intro!: nn_integral_monotone_convergence_INF_decseq) |
1421 qed |
1421 qed |
1422 |
1422 |
1607 by (subst step) |
1607 by (subst step) |
1608 (auto simp add: top_fun_def less_le non_zero le_fun_def ennreal_top_mult |
1608 (auto simp add: top_fun_def less_le non_zero le_fun_def ennreal_top_mult |
1609 cong del: if_weak_cong intro!: monoD[OF inf_continuous_mono[OF g], THEN le_funD]) |
1609 cong del: if_weak_cong intro!: monoD[OF inf_continuous_mono[OF g], THEN le_funD]) |
1610 next |
1610 next |
1611 fix C assume "\<And>i::nat. C i \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (C i) < \<infinity>)" "decseq C" |
1611 fix C assume "\<And>i::nat. C i \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (C i) < \<infinity>)" "decseq C" |
1612 with bound show "INFIMUM UNIV C \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (INFIMUM UNIV C) < \<infinity>)" |
1612 with bound show "Inf (C ` UNIV) \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (Inf (C ` UNIV)) < \<infinity>)" |
1613 unfolding INF_apply[abs_def] |
1613 unfolding INF_apply[abs_def] |
1614 by (subst nn_integral_monotone_convergence_INF_decseq) |
1614 by (subst nn_integral_monotone_convergence_INF_decseq) |
1615 (auto simp: INF_less_iff cong: measurable_cong_sets intro!: borel_measurable_INF) |
1615 (auto simp: INF_less_iff cong: measurable_cong_sets intro!: borel_measurable_INF) |
1616 next |
1616 next |
1617 show "\<And>x. x \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) x < \<infinity>) \<Longrightarrow> |
1617 show "\<And>x. x \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) x < \<infinity>) \<Longrightarrow> |
1799 qed (auto cong: nn_integral_cong_simp) |
1799 qed (auto cong: nn_integral_cong_simp) |
1800 |
1800 |
1801 lemma emeasure_UN_countable: |
1801 lemma emeasure_UN_countable: |
1802 assumes sets[measurable]: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets M" and I[simp]: "countable I" |
1802 assumes sets[measurable]: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets M" and I[simp]: "countable I" |
1803 assumes disj: "disjoint_family_on X I" |
1803 assumes disj: "disjoint_family_on X I" |
1804 shows "emeasure M (UNION I X) = (\<integral>\<^sup>+i. emeasure M (X i) \<partial>count_space I)" |
1804 shows "emeasure M (\<Union>(X ` I)) = (\<integral>\<^sup>+i. emeasure M (X i) \<partial>count_space I)" |
1805 proof - |
1805 proof - |
1806 have eq: "\<And>x. indicator (UNION I X) x = \<integral>\<^sup>+ i. indicator (X i) x \<partial>count_space I" |
1806 have eq: "\<And>x. indicator (\<Union>(X ` I)) x = \<integral>\<^sup>+ i. indicator (X i) x \<partial>count_space I" |
1807 proof cases |
1807 proof cases |
1808 fix x assume x: "x \<in> UNION I X" |
1808 fix x assume x: "x \<in> \<Union>(X ` I)" |
1809 then obtain j where j: "x \<in> X j" "j \<in> I" |
1809 then obtain j where j: "x \<in> X j" "j \<in> I" |
1810 by auto |
1810 by auto |
1811 with disj have "\<And>i. i \<in> I \<Longrightarrow> indicator (X i) x = (indicator {j} i::ennreal)" |
1811 with disj have "\<And>i. i \<in> I \<Longrightarrow> indicator (X i) x = (indicator {j} i::ennreal)" |
1812 by (auto simp: disjoint_family_on_def split: split_indicator) |
1812 by (auto simp: disjoint_family_on_def split: split_indicator) |
1813 with x j show "?thesis x" |
1813 with x j show "?thesis x" |
1814 by (simp cong: nn_integral_cong_simp) |
1814 by (simp cong: nn_integral_cong_simp) |
1815 qed (auto simp: nn_integral_0_iff_AE) |
1815 qed (auto simp: nn_integral_0_iff_AE) |
1816 |
1816 |
1817 note sets.countable_UN'[unfolded subset_eq, measurable] |
1817 note sets.countable_UN'[unfolded subset_eq, measurable] |
1818 have "emeasure M (UNION I X) = (\<integral>\<^sup>+x. indicator (UNION I X) x \<partial>M)" |
1818 have "emeasure M (\<Union>(X ` I)) = (\<integral>\<^sup>+x. indicator (\<Union>(X ` I)) x \<partial>M)" |
1819 by simp |
1819 by simp |
1820 also have "\<dots> = (\<integral>\<^sup>+i. \<integral>\<^sup>+x. indicator (X i) x \<partial>M \<partial>count_space I)" |
1820 also have "\<dots> = (\<integral>\<^sup>+i. \<integral>\<^sup>+x. indicator (X i) x \<partial>M \<partial>count_space I)" |
1821 by (simp add: eq nn_integral_count_space_nn_integral) |
1821 by (simp add: eq nn_integral_count_space_nn_integral) |
1822 finally show ?thesis |
1822 finally show ?thesis |
1823 by (simp cong: nn_integral_cong_simp) |
1823 by (simp cong: nn_integral_cong_simp) |