author hoelzl Tue Dec 04 20:44:18 2012 +0100 (2012-12-04 ago) changeset 50384 b9b967da28e9 parent 50383 4274b25ff4e7 child 50385 837e38a42d8c
rules for improper Lebesgue integrals (using tendsto at_top)
 src/HOL/Probability/Lebesgue_Integration.thy file | annotate | diff | revisions src/HOL/SEQ.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Dec 05 13:25:06 2012 +0100
1.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Dec 04 20:44:18 2012 +0100
1.3 @@ -2274,6 +2274,87 @@
1.4      using int(2) by simp
1.5  qed
1.6
1.7 +lemma integrable_mult_indicator:
1.8 +  "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. f x * indicator A x)"
1.9 +  by (rule integrable_bound[where f="\<lambda>x. \<bar>f x\<bar>"])
1.10 +     (auto intro: integrable_abs split: split_indicator)
1.11 +
1.12 +lemma tendsto_integral_at_top:
1.13 +  fixes M :: "real measure"
1.14 +  assumes M: "sets M = sets borel" and f[measurable]: "integrable M f"
1.15 +  shows "((\<lambda>y. \<integral> x. f x * indicator {.. y} x \<partial>M) ---> \<integral> x. f x \<partial>M) at_top"
1.16 +proof -
1.17 +  have M_measure[simp]: "borel_measurable M = borel_measurable borel"
1.18 +    using M by (simp add: sets_eq_imp_space_eq measurable_def)
1.19 +  { fix f assume f: "integrable M f" "\<And>x. 0 \<le> f x"
1.20 +    then have [measurable]: "f \<in> borel_measurable borel"
1.21 +      by (simp add: integrable_def)
1.22 +    have "((\<lambda>y. \<integral> x. f x * indicator {.. y} x \<partial>M) ---> \<integral> x. f x \<partial>M) at_top"
1.23 +    proof (rule tendsto_at_topI_sequentially)
1.24 +      have "\<And>j. AE x in M. \<bar>f x * indicator {.. j} x\<bar> \<le> f x"
1.25 +        using f(2) by (intro AE_I2) (auto split: split_indicator)
1.26 +      have int: "\<And>n. integrable M (\<lambda>x. f x * indicator {.. n} x)"
1.27 +        by (rule integrable_mult_indicator) (auto simp: M f)
1.28 +      show "(\<lambda>n. \<integral> x. f x * indicator {..real n} x \<partial>M) ----> integral\<^isup>L M f"
1.29 +      proof (rule integral_dominated_convergence)
1.30 +        { fix x have "eventually (\<lambda>n. f x * indicator {..real n} x = f x) sequentially"
1.31 +            by (rule eventually_sequentiallyI[of "natceiling x"])
1.32 +               (auto split: split_indicator simp: natceiling_le_eq) }
1.33 +        from filterlim_cong[OF refl refl this]
1.34 +        show "AE x in M. (\<lambda>n. f x * indicator {..real n} x) ----> f x"
1.35 +          by (simp add: tendsto_const)
1.36 +      qed (fact+, simp)
1.37 +      show "mono (\<lambda>y. \<integral> x. f x * indicator {..y} x \<partial>M)"
1.38 +        by (intro monoI integral_mono int) (auto split: split_indicator intro: f)
1.39 +    qed }
1.40 +  note nonneg = this
1.41 +  let ?P = "\<lambda>y. \<integral> x. max 0 (f x) * indicator {..y} x \<partial>M"
1.42 +  let ?N = "\<lambda>y. \<integral> x. max 0 (- f x) * indicator {..y} x \<partial>M"
1.43 +  let ?p = "integral\<^isup>L M (\<lambda>x. max 0 (f x))"
1.44 +  let ?n = "integral\<^isup>L M (\<lambda>x. max 0 (- f x))"
1.45 +  have "(?P ---> ?p) at_top" "(?N ---> ?n) at_top"
1.46 +    by (auto intro!: nonneg integrable_max f)
1.47 +  note tendsto_diff[OF this]
1.48 +  also have "(\<lambda>y. ?P y - ?N y) = (\<lambda>y. \<integral> x. f x * indicator {..y} x \<partial>M)"
1.49 +    by (subst integral_diff(2)[symmetric])
1.50 +       (auto intro!: integrable_mult_indicator integrable_max f integral_cong ext
1.51 +             simp: M split: split_max)
1.52 +  also have "?p - ?n = integral\<^isup>L M f"
1.53 +    by (subst integral_diff(2)[symmetric])
1.54 +       (auto intro!: integrable_max f integral_cong ext simp: M split: split_max)
1.55 +  finally show ?thesis .
1.56 +qed
1.57 +
1.58 +lemma integral_monotone_convergence_at_top:
1.59 +  fixes M :: "real measure"
1.60 +  assumes M: "sets M = sets borel"
1.61 +  assumes nonneg: "AE x in M. 0 \<le> f x"
1.62 +  assumes borel: "f \<in> borel_measurable borel"
1.63 +  assumes int: "\<And>y. integrable M (\<lambda>x. f x * indicator {.. y} x)"
1.64 +  assumes conv: "((\<lambda>y. \<integral> x. f x * indicator {.. y} x \<partial>M) ---> x) at_top"
1.65 +  shows "integrable M f" "integral\<^isup>L M f = x"
1.66 +proof -
1.67 +  from nonneg have "AE x in M. mono (\<lambda>n::nat. f x * indicator {..real n} x)"
1.68 +    by (auto split: split_indicator intro!: monoI)
1.69 +  { fix x have "eventually (\<lambda>n. f x * indicator {..real n} x = f x) sequentially"
1.70 +      by (rule eventually_sequentiallyI[of "natceiling x"])
1.71 +         (auto split: split_indicator simp: natceiling_le_eq) }
1.72 +  from filterlim_cong[OF refl refl this]
1.73 +  have "AE x in M. (\<lambda>i. f x * indicator {..real i} x) ----> f x"
1.74 +    by (simp add: tendsto_const)
1.75 +  have "(\<lambda>i. \<integral> x. f x * indicator {..real i} x \<partial>M) ----> x"
1.76 +    using conv filterlim_real_sequentially by (rule filterlim_compose)
1.77 +  have M_measure[simp]: "borel_measurable M = borel_measurable borel"
1.78 +    using M by (simp add: sets_eq_imp_space_eq measurable_def)
1.79 +  have "f \<in> borel_measurable M"
1.80 +    using borel by simp
1.81 +  show "integrable M f"
1.82 +    by (rule integral_monotone_convergence) fact+
1.83 +  show "integral\<^isup>L M f = x"
1.84 +    by (rule integral_monotone_convergence) fact+
1.85 +qed
1.86 +
1.87 +
1.88  section "Lebesgue integration on countable spaces"
1.89
1.90  lemma integral_on_countable:
```
```     2.1 --- a/src/HOL/SEQ.thy	Wed Dec 05 13:25:06 2012 +0100
2.2 +++ b/src/HOL/SEQ.thy	Tue Dec 04 20:44:18 2012 +0100
2.3 @@ -911,4 +911,33 @@
2.4  lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n :: real) ----> 0"
2.5    by (rule LIMSEQ_power_zero) simp
2.6
2.7 +lemma tendsto_at_topI_sequentially:
2.8 +  fixes f :: "real \<Rightarrow> real"
2.9 +  assumes mono: "mono f"
2.10 +  assumes limseq: "(\<lambda>n. f (real n)) ----> y"
2.11 +  shows "(f ---> y) at_top"
2.12 +proof (rule tendstoI)
2.13 +  fix e :: real assume "0 < e"
2.14 +  with limseq obtain N :: nat where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>f (real n) - y\<bar> < e"
2.15 +    by (auto simp: LIMSEQ_def dist_real_def)
2.16 +  { fix x :: real
2.17 +    from ex_le_of_nat[of x] guess n ..
2.18 +    note monoD[OF mono this]
2.19 +    also have "f (real_of_nat n) \<le> y"
2.20 +      by (rule LIMSEQ_le_const[OF limseq])
2.21 +         (auto intro: exI[of _ n] monoD[OF mono] simp: real_eq_of_nat[symmetric])
2.22 +    finally have "f x \<le> y" . }
2.23 +  note le = this
2.24 +  have "eventually (\<lambda>x. real N \<le> x) at_top"
2.25 +    by (rule eventually_ge_at_top)
2.26 +  then show "eventually (\<lambda>x. dist (f x) y < e) at_top"
2.27 +  proof eventually_elim
2.28 +    fix x assume N': "real N \<le> x"
2.29 +    with N[of N] le have "y - f (real N) < e" by auto
2.30 +    moreover note monoD[OF mono N']
2.31 +    ultimately show "dist (f x) y < e"
2.32 +      using le[of x] by (auto simp: dist_real_def field_simps)
2.33 +  qed
2.34 +qed
2.35 +
2.36  end
```