equal
deleted
inserted
replaced
2098 by (simp flip: ennreal_0) |
2098 by (simp flip: ennreal_0) |
2099 then have "((\<lambda>n. ((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M))) \<longlongrightarrow> 0) F" using tendsto_norm_zero_iff by blast |
2099 then have "((\<lambda>n. ((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M))) \<longlongrightarrow> 0) F" using tendsto_norm_zero_iff by blast |
2100 then show ?thesis using Lim_null by auto |
2100 then show ?thesis using Lim_null by auto |
2101 qed |
2101 qed |
2102 |
2102 |
2103 text \<open>The next lemma asserts that, if a sequence of functions converges in $L^1$, then |
2103 text \<open>The next lemma asserts that, if a sequence of functions converges in \<open>L\<^sup>1\<close>, then |
2104 it admits a subsequence that converges almost everywhere.\<close> |
2104 it admits a subsequence that converges almost everywhere.\<close> |
2105 |
2105 |
2106 lemma%important tendsto_L1_AE_subseq: |
2106 lemma%important tendsto_L1_AE_subseq: |
2107 fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}" |
2107 fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}" |
2108 assumes [measurable]: "\<And>n. integrable M (u n)" |
2108 assumes [measurable]: "\<And>n. integrable M (u n)" |