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