Bochner integral: prove dominated convergence at_top

--- 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"

--- a/src/HOL/Probability/Interval_Integral.thy	Mon Dec 21 23:24:05 2015 +0100
+++ b/src/HOL/Probability/Interval_Integral.thy	Mon Dec 21 19:08:26 2015 +0100
@@ -302,6 +302,19 @@
              split: split_indicator)
 qed
 
+lemma interval_lebesgue_integral_0_infty:
+  "interval_lebesgue_integrable M 0 \<infinity> f \<longleftrightarrow> set_integrable M {0<..} f"
+  "interval_lebesgue_integral M 0 \<infinity> f = (LINT x:{0<..}|M. f x)"
+  unfolding zero_ereal_def 
+  by (auto simp: interval_lebesgue_integral_le_eq interval_lebesgue_integrable_def)
+
+lemma interval_integral_to_infinity_eq: "(LINT x=ereal a..\<infinity> | M. f x) = (LINT x : {a<..} | M. f x)"
+  unfolding interval_lebesgue_integral_def by auto
+
+lemma interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \<infinity> f) = 
+  (set_integrable M {a<..} f)"
+  unfolding interval_lebesgue_integrable_def by auto
+
 (*
     Basic properties of integration over an interval wrt lebesgue measure.
 *)