src/HOL/Probability/Lebesgue_Measure.thy
 changeset 47757 5e6fe71e2390 parent 47694 05663f75964c child 49777 6ac97ab9b295
```     1.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Apr 25 15:06:59 2012 +0200
1.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Apr 25 15:09:18 2012 +0200
1.3 @@ -59,7 +59,7 @@
1.4  lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)"
1.5    unfolding cube_def subset_eq apply safe unfolding mem_interval apply auto done
1.6
1.7 -subsection {* Lebesgue measure *}
1.8 +subsection {* Lebesgue measure *}
1.9
1.10  definition lebesgue :: "'a::ordered_euclidean_space measure" where
1.11    "lebesgue = measure_of UNIV {A. \<forall>n. (indicator A :: 'a \<Rightarrow> real) integrable_on cube n}
1.12 @@ -129,7 +129,7 @@
1.13  lemma lebesgueD: "A \<in> sets lebesgue \<Longrightarrow> (indicator A :: _ \<Rightarrow> real) integrable_on cube n"
1.14    unfolding sets_lebesgue by simp
1.15
1.16 -lemma emeasure_lebesgue:
1.17 +lemma emeasure_lebesgue:
1.18    assumes "A \<in> sets lebesgue"
1.19    shows "emeasure lebesgue A = (SUP n. ereal (integral (cube n) (indicator A)))"
1.20      (is "_ = ?\<mu> A")
1.21 @@ -231,6 +231,10 @@
1.22    finally show ?thesis .
1.23  qed
1.24
1.25 +lemma borel_measurable_lebesgueI:
1.26 +  "f \<in> borel_measurable borel \<Longrightarrow> f \<in> borel_measurable lebesgue"
1.27 +  unfolding measurable_def by simp
1.28 +
1.29  lemma lebesgueI_negligible[dest]: fixes s::"'a::ordered_euclidean_space set"
1.30    assumes "negligible s" shows "s \<in> sets lebesgue"
1.31    using assms by (force simp: cube_def integrable_on_def negligible_def intro!: lebesgueI)
1.32 @@ -735,6 +739,13 @@
1.33               intro!: measurable_If)
1.34  qed
1.35
1.36 +lemma lebesgue_simple_integral_eq_borel:
1.37 +  assumes f: "f \<in> borel_measurable borel"
1.38 +  shows "integral\<^isup>S lebesgue f = integral\<^isup>S lborel f"
1.39 +  using f[THEN measurable_sets]
1.40 +  by (auto intro!: setsum_cong arg_cong2[where f="op *"] emeasure_lborel[symmetric]
1.41 +           simp: simple_integral_def)
1.42 +
1.43  lemma lebesgue_positive_integral_eq_borel:
1.44    assumes f: "f \<in> borel_measurable borel"
1.45    shows "integral\<^isup>P lebesgue f = integral\<^isup>P lborel f"
1.46 @@ -839,7 +850,7 @@
1.47    let ?E = "range (\<lambda>(a, b). {a..b} :: 'a set)"
1.48    show "?E \<subseteq> Pow UNIV" "sets lborel = sigma_sets UNIV ?E" "sets M = sigma_sets UNIV ?E"
1.49      by (simp_all add: borel_eq_atLeastAtMost sets_eq)
1.50 -
1.51 +
1.52    show "range cube \<subseteq> ?E" unfolding cube_def [abs_def] by auto
1.53    show "incseq cube" using cube_subset_Suc by (auto intro!: incseq_SucI)
1.54    { fix x :: 'a have "\<exists>n. x \<in> cube n" using mem_big_cube[of x] by fastforce }
1.55 @@ -940,4 +951,122 @@
1.56    qed
1.57  qed simp
1.58
1.59 +lemma borel_cube[intro]: "cube n \<in> sets borel"
1.60 +  unfolding cube_def by auto
1.61 +
1.62 +lemma integrable_on_cmult_iff:
1.63 +  fixes c :: real assumes "c \<noteq> 0"
1.64 +  shows "(\<lambda>x. c * f x) integrable_on s \<longleftrightarrow> f integrable_on s"
1.65 +  using integrable_cmul[of "\<lambda>x. c * f x" s "1 / c"] integrable_cmul[of f s c] `c \<noteq> 0`
1.66 +  by auto
1.67 +
1.68 +lemma positive_integral_borel_has_integral:
1.69 +  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
1.70 +  assumes f_borel: "f \<in> borel_measurable borel" and nonneg: "\<And>x. 0 \<le> f x"
1.71 +  assumes I: "(f has_integral I) UNIV"
1.72 +  shows "(\<integral>\<^isup>+x. f x \<partial>lborel) = I"
1.73 +proof -
1.74 +  from f_borel have "(\<lambda>x. ereal (f x)) \<in> borel_measurable borel" by auto
1.75 +  from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this
1.76 +
1.77 +  have lebesgue_eq: "(\<integral>\<^isup>+ x. ereal (f x) \<partial>lebesgue) = (\<integral>\<^isup>+ x. ereal (f x) \<partial>lborel)"
1.78 +    using f_borel by (intro lebesgue_positive_integral_eq_borel) auto
1.79 +  also have "\<dots> = (SUP i. integral\<^isup>S lborel (F i))"
1.80 +    using F
1.81 +    by (subst positive_integral_monotone_convergence_simple)
1.82 +       (simp_all add: positive_integral_max_0 simple_function_def)
1.83 +  also have "\<dots> \<le> ereal I"
1.84 +  proof (rule SUP_least)
1.85 +    fix i :: nat
1.86 +
1.87 +    { fix z
1.88 +      from F(4)[of z] have "F i z \<le> ereal (f z)"
1.89 +        by (metis SUP_upper UNIV_I ereal_max_0 min_max.sup_absorb2 nonneg)
1.90 +      with F(5)[of i z] have "real (F i z) \<le> f z"
1.91 +        by (cases "F i z") simp_all }
1.92 +    note F_bound = this
1.93 +
1.94 +    { fix x :: ereal assume x: "x \<noteq> 0" "x \<in> range (F i)"
1.95 +      with F(3,5)[of i] have [simp]: "real x \<noteq> 0"
1.96 +        by (metis image_iff order_eq_iff real_of_ereal_le_0)
1.97 +      let ?s = "(\<lambda>n z. real x * indicator (F i -` {x} \<inter> cube n) z) :: nat \<Rightarrow> 'a \<Rightarrow> real"
1.98 +      have "(\<lambda>z::'a. real x * indicator (F i -` {x}) z) integrable_on UNIV"
1.99 +      proof (rule dominated_convergence(1))
1.100 +        fix n :: nat
1.101 +        have "(\<lambda>z. indicator (F i -` {x} \<inter> cube n) z :: real) integrable_on cube n"
1.102 +          using x F(1)[of i]
1.103 +          by (intro lebesgueD) (auto simp: simple_function_def)
1.104 +        then have cube: "?s n integrable_on cube n"
1.105 +          by (simp add: integrable_on_cmult_iff)
1.106 +        show "?s n integrable_on UNIV"
1.107 +          by (rule integrable_on_superset[OF _ _ cube]) auto
1.108 +      next
1.109 +        show "f integrable_on UNIV"
1.110 +          unfolding integrable_on_def using I by auto
1.111 +      next
1.112 +        fix n from F_bound show "\<forall>x\<in>UNIV. norm (?s n x) \<le> f x"
1.113 +          using nonneg F(5) by (auto split: split_indicator)
1.114 +      next
1.115 +        show "\<forall>z\<in>UNIV. (\<lambda>n. ?s n z) ----> real x * indicator (F i -` {x}) z"
1.116 +        proof
1.117 +          fix z :: 'a
1.118 +          from mem_big_cube[of z] guess j .
1.119 +          then have x: "eventually (\<lambda>n. ?s n z = real x * indicator (F i -` {x}) z) sequentially"
1.120 +            by (auto intro!: eventually_sequentiallyI[where c=j] dest!: cube_subset split: split_indicator)
1.121 +          then show "(\<lambda>n. ?s n z) ----> real x * indicator (F i -` {x}) z"
1.122 +            by (rule Lim_eventually)
1.123 +        qed
1.124 +      qed
1.125 +      then have "(indicator (F i -` {x}) :: 'a \<Rightarrow> real) integrable_on UNIV"
1.126 +        by (simp add: integrable_on_cmult_iff) }
1.127 +    note F_finite = lmeasure_finite[OF this]
1.128 +
1.129 +    have "((\<lambda>x. real (F i x)) has_integral real (integral\<^isup>S lebesgue (F i))) UNIV"
1.130 +    proof (rule simple_function_has_integral[of "F i"])
1.131 +      show "simple_function lebesgue (F i)"
1.132 +        using F(1) by (simp add: simple_function_def)
1.133 +      show "range (F i) \<subseteq> {0..<\<infinity>}"
1.134 +        using F(3,5)[of i] by (auto simp: image_iff) metis
1.135 +    next
1.136 +      fix x assume "x \<in> range (F i)" "emeasure lebesgue (F i -` {x} \<inter> UNIV) = \<infinity>"
1.137 +      with F_finite[of x] show "x = 0" by auto
1.138 +    qed
1.139 +    from this I have "real (integral\<^isup>S lebesgue (F i)) \<le> I"
1.140 +      by (rule has_integral_le) (intro ballI F_bound)
1.141 +    moreover
1.142 +    { fix x assume x: "x \<in> range (F i)"
1.143 +      with F(3,5)[of i] have "x = 0 \<or> (0 < x \<and> x \<noteq> \<infinity>)"
1.144 +        by (auto  simp: image_iff le_less) metis
1.145 +      with F_finite[OF _ x] x have "x * emeasure lebesgue (F i -` {x} \<inter> UNIV) \<noteq> \<infinity>"
1.146 +        by auto }
1.147 +    then have "integral\<^isup>S lebesgue (F i) \<noteq> \<infinity>"
1.148 +      unfolding simple_integral_def setsum_Pinfty space_lebesgue by blast
1.149 +    moreover have "0 \<le> integral\<^isup>S lebesgue (F i)"
1.150 +      using F(1,5) by (intro simple_integral_positive) (auto simp: simple_function_def)
1.151 +    moreover have "integral\<^isup>S lebesgue (F i) = integral\<^isup>S lborel (F i)"
1.152 +      using F(1)[of i, THEN borel_measurable_simple_function]
1.153 +      by (rule lebesgue_simple_integral_eq_borel)
1.154 +    ultimately show "integral\<^isup>S lborel (F i) \<le> ereal I"
1.155 +      by (cases "integral\<^isup>S lborel (F i)") auto
1.156 +  qed
1.157 +  also have "\<dots> < \<infinity>" by simp
1.158 +  finally have finite: "(\<integral>\<^isup>+ x. ereal (f x) \<partial>lebesgue) \<noteq> \<infinity>" by simp
1.159 +  have borel: "(\<lambda>x. ereal (f x)) \<in> borel_measurable lebesgue"
1.160 +    using f_borel by (auto intro: borel_measurable_lebesgueI)
1.161 +  from positive_integral_has_integral[OF borel _ finite]
1.162 +  have "(f has_integral real (\<integral>\<^isup>+ x. ereal (f x) \<partial>lebesgue)) UNIV"
1.163 +    using nonneg by (simp add: subset_eq)
1.164 +  with I have "I = real (\<integral>\<^isup>+ x. ereal (f x) \<partial>lebesgue)"
1.165 +    by (rule has_integral_unique)
1.166 +  with finite positive_integral_positive[of _ "\<lambda>x. ereal (f x)"] show ?thesis
1.167 +    by (cases "\<integral>\<^isup>+ x. ereal (f x) \<partial>lborel") (auto simp: lebesgue_eq)
1.168 +qed
1.169 +
1.170 +lemma has_integral_iff_positive_integral:
1.171 +  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
1.172 +  assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x"
1.173 +  shows "(f has_integral I) UNIV \<longleftrightarrow> integral\<^isup>P lborel f = I"
1.174 +  using f positive_integral_borel_has_integral[of f I] positive_integral_has_integral[of f]
1.175 +  by (auto simp: subset_eq borel_measurable_lebesgueI lebesgue_positive_integral_eq_borel)
1.176 +
1.177  end
```