--- a/src/HOL/Probability/Bochner_Integration.thy Mon Dec 21 23:24:05 2015 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy Mon Dec 21 19:08:26 2015 +0100
@@ -1520,6 +1520,56 @@
show "(\<lambda>i. integral\<^sup>L M (s i)) ----> integral\<^sup>L M f" by simp
qed
+context
+ fixes s :: "real \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}" and w :: "'a \<Rightarrow> real"
+ and f :: "'a \<Rightarrow> 'b" and M
+ assumes "f \<in> borel_measurable M" "\<And>t. s t \<in> borel_measurable M" "integrable M w"
+ assumes lim: "AE x in M. ((\<lambda>i. s i x) ---> f x) at_top"
+ assumes bound: "\<forall>\<^sub>F i in at_top. AE x in M. norm (s i x) \<le> w x"
+begin
+
+lemma integral_dominated_convergence_at_top: "((\<lambda>t. integral\<^sup>L M (s t)) ---> integral\<^sup>L M f) at_top"
+proof (rule tendsto_at_topI_sequentially)
+ fix X :: "nat \<Rightarrow> real" assume X: "filterlim X at_top sequentially"
+ from filterlim_iff[THEN iffD1, OF this, rule_format, OF bound]
+ obtain N where w: "\<And>n. N \<le> n \<Longrightarrow> AE x in M. norm (s (X n) x) \<le> w x"
+ by (auto simp: eventually_sequentially)
+
+ show "(\<lambda>n. integral\<^sup>L M (s (X n))) ----> integral\<^sup>L M f"
+ proof (rule LIMSEQ_offset, rule integral_dominated_convergence)
+ show "AE x in M. norm (s (X (n + N)) x) \<le> w x" for n
+ by (rule w) auto
+ show "AE x in M. (\<lambda>n. s (X (n + N)) x) ----> f x"
+ using lim
+ proof eventually_elim
+ fix x assume "((\<lambda>i. s i x) ---> f x) at_top"
+ then show "(\<lambda>n. s (X (n + N)) x) ----> f x"
+ by (intro LIMSEQ_ignore_initial_segment filterlim_compose[OF _ X])
+ qed
+ qed fact+
+qed
+
+lemma integrable_dominated_convergence_at_top: "integrable M f"
+proof -
+ from bound obtain N where w: "\<And>n. N \<le> n \<Longrightarrow> AE x in M. norm (s n x) \<le> w x"
+ by (auto simp: eventually_at_top_linorder)
+ show ?thesis
+ proof (rule integrable_dominated_convergence)
+ show "AE x in M. norm (s (N + i) x) \<le> w x" for i :: nat
+ by (intro w) auto
+ show "AE x in M. (\<lambda>i. s (N + real i) x) ----> f x"
+ using lim
+ proof eventually_elim
+ fix x assume "((\<lambda>i. s i x) ---> f x) at_top"
+ then show "(\<lambda>n. s (N + n) x) ----> f x"
+ by (rule filterlim_compose)
+ (auto intro!: filterlim_tendsto_add_at_top filterlim_real_sequentially)
+ qed
+ qed fact+
+qed
+
+end
+
lemma integrable_mult_left_iff:
fixes f :: "'a \<Rightarrow> real"
shows "integrable M (\<lambda>x. c * f x) \<longleftrightarrow> c = 0 \<or> integrable M f"