# HG changeset patch
# User hoelzl
# Date 1354650258 -3600
# Node ID b9b967da28e9ee4e57bad0192d46388f1a202603
# Parent  4274b25ff4e7243273029db49bc4fdc0e69c3d2c
rules for improper Lebesgue integrals (using tendsto at_top)

diff -r 4274b25ff4e7 -r b9b967da28e9 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Dec 05 13:25:06 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Dec 04 20:44:18 2012 +0100
@@ -2274,6 +2274,87 @@
     using int(2) by simp
 qed
 
+lemma integrable_mult_indicator:
+  "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. f x * indicator A x)"
+  by (rule integrable_bound[where f="\<lambda>x. \<bar>f x\<bar>"])
+     (auto intro: integrable_abs split: split_indicator)
+
+lemma tendsto_integral_at_top:
+  fixes M :: "real measure"
+  assumes M: "sets M = sets borel" and f[measurable]: "integrable M f"
+  shows "((\<lambda>y. \<integral> x. f x * indicator {.. y} x \<partial>M) ---> \<integral> x. f x \<partial>M) at_top"
+proof -
+  have M_measure[simp]: "borel_measurable M = borel_measurable borel"
+    using M by (simp add: sets_eq_imp_space_eq measurable_def)
+  { fix f assume f: "integrable M f" "\<And>x. 0 \<le> f x"
+    then have [measurable]: "f \<in> borel_measurable borel"
+      by (simp add: integrable_def)
+    have "((\<lambda>y. \<integral> x. f x * indicator {.. y} x \<partial>M) ---> \<integral> x. f x \<partial>M) at_top"
+    proof (rule tendsto_at_topI_sequentially)
+      have "\<And>j. AE x in M. \<bar>f x * indicator {.. j} x\<bar> \<le> f x"
+        using f(2) by (intro AE_I2) (auto split: split_indicator)
+      have int: "\<And>n. integrable M (\<lambda>x. f x * indicator {.. n} x)"
+        by (rule integrable_mult_indicator) (auto simp: M f)
+      show "(\<lambda>n. \<integral> x. f x * indicator {..real n} x \<partial>M) ----> integral\<^isup>L M f"
+      proof (rule integral_dominated_convergence)
+        { fix x have "eventually (\<lambda>n. f x * indicator {..real n} x = f x) sequentially"
+            by (rule eventually_sequentiallyI[of "natceiling x"])
+               (auto split: split_indicator simp: natceiling_le_eq) }
+        from filterlim_cong[OF refl refl this]
+        show "AE x in M. (\<lambda>n. f x * indicator {..real n} x) ----> f x"
+          by (simp add: tendsto_const)
+      qed (fact+, simp)
+      show "mono (\<lambda>y. \<integral> x. f x * indicator {..y} x \<partial>M)"
+        by (intro monoI integral_mono int) (auto split: split_indicator intro: f)
+    qed }
+  note nonneg = this
+  let ?P = "\<lambda>y. \<integral> x. max 0 (f x) * indicator {..y} x \<partial>M"
+  let ?N = "\<lambda>y. \<integral> x. max 0 (- f x) * indicator {..y} x \<partial>M"
+  let ?p = "integral\<^isup>L M (\<lambda>x. max 0 (f x))"
+  let ?n = "integral\<^isup>L M (\<lambda>x. max 0 (- f x))"
+  have "(?P ---> ?p) at_top" "(?N ---> ?n) at_top"
+    by (auto intro!: nonneg integrable_max f)
+  note tendsto_diff[OF this]
+  also have "(\<lambda>y. ?P y - ?N y) = (\<lambda>y. \<integral> x. f x * indicator {..y} x \<partial>M)"
+    by (subst integral_diff(2)[symmetric])
+       (auto intro!: integrable_mult_indicator integrable_max f integral_cong ext
+             simp: M split: split_max)
+  also have "?p - ?n = integral\<^isup>L M f"
+    by (subst integral_diff(2)[symmetric])
+       (auto intro!: integrable_max f integral_cong ext simp: M split: split_max)
+  finally show ?thesis .
+qed
+
+lemma integral_monotone_convergence_at_top:
+  fixes M :: "real measure"
+  assumes M: "sets M = sets borel"
+  assumes nonneg: "AE x in M. 0 \<le> f x"
+  assumes borel: "f \<in> borel_measurable borel"
+  assumes int: "\<And>y. integrable M (\<lambda>x. f x * indicator {.. y} x)"
+  assumes conv: "((\<lambda>y. \<integral> x. f x * indicator {.. y} x \<partial>M) ---> x) at_top"
+  shows "integrable M f" "integral\<^isup>L M f = x"
+proof -
+  from nonneg have "AE x in M. mono (\<lambda>n::nat. f x * indicator {..real n} x)"
+    by (auto split: split_indicator intro!: monoI)
+  { fix x have "eventually (\<lambda>n. f x * indicator {..real n} x = f x) sequentially"
+      by (rule eventually_sequentiallyI[of "natceiling x"])
+         (auto split: split_indicator simp: natceiling_le_eq) }
+  from filterlim_cong[OF refl refl this]
+  have "AE x in M. (\<lambda>i. f x * indicator {..real i} x) ----> f x"
+    by (simp add: tendsto_const)
+  have "(\<lambda>i. \<integral> x. f x * indicator {..real i} x \<partial>M) ----> x"
+    using conv filterlim_real_sequentially by (rule filterlim_compose)
+  have M_measure[simp]: "borel_measurable M = borel_measurable borel"
+    using M by (simp add: sets_eq_imp_space_eq measurable_def)
+  have "f \<in> borel_measurable M"
+    using borel by simp
+  show "integrable M f"
+    by (rule integral_monotone_convergence) fact+
+  show "integral\<^isup>L M f = x"
+    by (rule integral_monotone_convergence) fact+
+qed
+
+
 section "Lebesgue integration on countable spaces"
 
 lemma integral_on_countable:
diff -r 4274b25ff4e7 -r b9b967da28e9 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Wed Dec 05 13:25:06 2012 +0100
+++ b/src/HOL/SEQ.thy	Tue Dec 04 20:44:18 2012 +0100
@@ -911,4 +911,33 @@
 lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n :: real) ----> 0"
   by (rule LIMSEQ_power_zero) simp
 
+lemma tendsto_at_topI_sequentially:
+  fixes f :: "real \<Rightarrow> real"
+  assumes mono: "mono f"
+  assumes limseq: "(\<lambda>n. f (real n)) ----> y"
+  shows "(f ---> y) at_top"
+proof (rule tendstoI)
+  fix e :: real assume "0 < e"
+  with limseq obtain N :: nat where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>f (real n) - y\<bar> < e"
+    by (auto simp: LIMSEQ_def dist_real_def)
+  { fix x :: real
+    from ex_le_of_nat[of x] guess n ..
+    note monoD[OF mono this]
+    also have "f (real_of_nat n) \<le> y"
+      by (rule LIMSEQ_le_const[OF limseq])
+         (auto intro: exI[of _ n] monoD[OF mono] simp: real_eq_of_nat[symmetric])
+    finally have "f x \<le> y" . }
+  note le = this
+  have "eventually (\<lambda>x. real N \<le> x) at_top"
+    by (rule eventually_ge_at_top)
+  then show "eventually (\<lambda>x. dist (f x) y < e) at_top"
+  proof eventually_elim
+    fix x assume N': "real N \<le> x"
+    with N[of N] le have "y - f (real N) < e" by auto
+    moreover note monoD[OF mono N']
+    ultimately show "dist (f x) y < e"
+      using le[of x] by (auto simp: dist_real_def field_simps)
+  qed
+qed
+
 end