rules for improper Lebesgue integrals (using tendsto at_top)
authorhoelzl
Tue Dec 04 20:44:18 2012 +0100 (2012-12-04 ago)
changeset 50384b9b967da28e9
parent 50383 4274b25ff4e7
child 50385 837e38a42d8c
rules for improper Lebesgue integrals (using tendsto at_top)
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/SEQ.thy
     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