src/HOL/Probability/Lebesgue_Measure.thy
changeset 41023 9118eb4eb8dc
parent 40874 f5a74b17a69e
child 41095 c335d880ff82
     1.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon Dec 06 19:18:02 2010 +0100
     1.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri Dec 03 15:25:14 2010 +0100
     1.3 @@ -357,7 +357,7 @@
     1.4  qed
     1.5  
     1.6  lemma lebesgue_simple_function_indicator:
     1.7 -  fixes f::"'a::ordered_euclidean_space \<Rightarrow> pinfreal"
     1.8 +  fixes f::"'a::ordered_euclidean_space \<Rightarrow> pextreal"
     1.9    assumes f:"lebesgue.simple_function f"
    1.10    shows "f = (\<lambda>x. (\<Sum>y \<in> f ` UNIV. y * indicator (f -` {y}) x))"
    1.11    apply(rule,subst lebesgue.simple_function_indicator_representation[OF f]) by auto
    1.12 @@ -421,7 +421,7 @@
    1.13  
    1.14  lemma lmeasure_singleton[simp]:
    1.15    fixes a :: "'a::ordered_euclidean_space" shows "lmeasure {a} = 0"
    1.16 -  using has_gmeasure_interval[of a a] unfolding zero_pinfreal_def
    1.17 +  using has_gmeasure_interval[of a a] unfolding zero_pextreal_def
    1.18    by (intro has_gmeasure_lmeasure)
    1.19       (simp add: content_closed_interval DIM_positive)
    1.20  
    1.21 @@ -475,7 +475,7 @@
    1.22  qed
    1.23  
    1.24  lemma simple_function_has_integral:
    1.25 -  fixes f::"'a::ordered_euclidean_space \<Rightarrow> pinfreal"
    1.26 +  fixes f::"'a::ordered_euclidean_space \<Rightarrow> pextreal"
    1.27    assumes f:"lebesgue.simple_function f"
    1.28    and f':"\<forall>x. f x \<noteq> \<omega>"
    1.29    and om:"\<forall>x\<in>range f. lmeasure (f -` {x} \<inter> UNIV) = \<omega> \<longrightarrow> x = 0"
    1.30 @@ -486,9 +486,9 @@
    1.31    have *:"\<And>x. \<forall>y\<in>range f. y * indicator (f -` {y}) x \<noteq> \<omega>"
    1.32      "\<forall>x\<in>range f. x * lmeasure (f -` {x} \<inter> UNIV) \<noteq> \<omega>"
    1.33      using f' om unfolding indicator_def by auto
    1.34 -  show ?case unfolding space_lebesgue real_of_pinfreal_setsum'[OF *(1),THEN sym]
    1.35 -    unfolding real_of_pinfreal_setsum'[OF *(2),THEN sym]
    1.36 -    unfolding real_of_pinfreal_setsum space_lebesgue
    1.37 +  show ?case unfolding space_lebesgue real_of_pextreal_setsum'[OF *(1),THEN sym]
    1.38 +    unfolding real_of_pextreal_setsum'[OF *(2),THEN sym]
    1.39 +    unfolding real_of_pextreal_setsum space_lebesgue
    1.40      apply(rule has_integral_setsum)
    1.41    proof safe show "finite (range f)" using f by (auto dest: lebesgue.simple_functionD)
    1.42      fix y::'a show "((\<lambda>x. real (f y * indicator (f -` {f y}) x)) has_integral
    1.43 @@ -496,8 +496,8 @@
    1.44      proof(cases "f y = 0") case False
    1.45        have mea:"gmeasurable (f -` {f y})" apply(rule lmeasure_finite_gmeasurable)
    1.46          using assms unfolding lebesgue.simple_function_def using False by auto
    1.47 -      have *:"\<And>x. real (indicator (f -` {f y}) x::pinfreal) = (if x \<in> f -` {f y} then 1 else 0)" by auto
    1.48 -      show ?thesis unfolding real_of_pinfreal_mult[THEN sym]
    1.49 +      have *:"\<And>x. real (indicator (f -` {f y}) x::pextreal) = (if x \<in> f -` {f y} then 1 else 0)" by auto
    1.50 +      show ?thesis unfolding real_of_pextreal_mult[THEN sym]
    1.51          apply(rule has_integral_cmul[where 'b=real, unfolded real_scaleR_def])
    1.52          unfolding Int_UNIV_right lmeasure_gmeasure[OF mea,THEN sym]
    1.53          unfolding measure_integral_univ[OF mea] * apply(rule integrable_integral)
    1.54 @@ -510,7 +510,7 @@
    1.55    using assms by auto
    1.56  
    1.57  lemma simple_function_has_integral':
    1.58 -  fixes f::"'a::ordered_euclidean_space \<Rightarrow> pinfreal"
    1.59 +  fixes f::"'a::ordered_euclidean_space \<Rightarrow> pextreal"
    1.60    assumes f:"lebesgue.simple_function f"
    1.61    and i: "lebesgue.simple_integral f \<noteq> \<omega>"
    1.62    shows "((\<lambda>x. real (f x)) has_integral (real (lebesgue.simple_integral f))) UNIV"
    1.63 @@ -544,7 +544,7 @@
    1.64  qed
    1.65  
    1.66  lemma (in measure_space) positive_integral_monotone_convergence:
    1.67 -  fixes f::"nat \<Rightarrow> 'a \<Rightarrow> pinfreal"
    1.68 +  fixes f::"nat \<Rightarrow> 'a \<Rightarrow> pextreal"
    1.69    assumes i: "\<And>i. f i \<in> borel_measurable M" and mono: "\<And>x. mono (\<lambda>n. f n x)"
    1.70    and lim: "\<And>x. (\<lambda>i. f i x) ----> u x"
    1.71    shows "u \<in> borel_measurable M"
    1.72 @@ -552,7 +552,7 @@
    1.73  proof -
    1.74    from positive_integral_isoton[unfolded isoton_fun_expand isoton_iff_Lim_mono, of f u]
    1.75    show ?ilim using mono lim i by auto
    1.76 -  have "(SUP i. f i) = u" using mono lim SUP_Lim_pinfreal
    1.77 +  have "(SUP i. f i) = u" using mono lim SUP_Lim_pextreal
    1.78      unfolding fun_eq_iff SUPR_fun_expand mono_def by auto
    1.79    moreover have "(SUP i. f i) \<in> borel_measurable M"
    1.80      using i by (rule borel_measurable_SUP)
    1.81 @@ -560,7 +560,7 @@
    1.82  qed
    1.83  
    1.84  lemma positive_integral_has_integral:
    1.85 -  fixes f::"'a::ordered_euclidean_space => pinfreal"
    1.86 +  fixes f::"'a::ordered_euclidean_space => pextreal"
    1.87    assumes f:"f \<in> borel_measurable lebesgue"
    1.88    and int_om:"lebesgue.positive_integral f \<noteq> \<omega>"
    1.89    and f_om:"\<forall>x. f x \<noteq> \<omega>" (* TODO: remove this *)
    1.90 @@ -581,14 +581,14 @@
    1.91    have "(\<lambda>x. real (f x)) integrable_on UNIV \<and>
    1.92      (\<lambda>k. Integration.integral UNIV (\<lambda>x. real (u k x))) ----> Integration.integral UNIV (\<lambda>x. real (f x))"
    1.93      apply(rule monotone_convergence_increasing) apply(rule,rule,rule u_int)
    1.94 -  proof safe case goal1 show ?case apply(rule real_of_pinfreal_mono) using u(2,3) by auto
    1.95 +  proof safe case goal1 show ?case apply(rule real_of_pextreal_mono) using u(2,3) by auto
    1.96    next case goal2 show ?case using u(3) apply(subst lim_Real[THEN sym])
    1.97        prefer 3 apply(subst Real_real') defer apply(subst Real_real')
    1.98        using isotone_Lim[OF u(3)[unfolded isoton_fun_expand, THEN spec]] using f_om u by auto
    1.99    next case goal3
   1.100      show ?case apply(rule bounded_realI[where B="real (lebesgue.positive_integral f)"])
   1.101        apply safe apply(subst abs_of_nonneg) apply(rule integral_nonneg,rule) apply(rule u_int)
   1.102 -      unfolding integral_unique[OF u_int] defer apply(rule real_of_pinfreal_mono[OF _ int_u_le])
   1.103 +      unfolding integral_unique[OF u_int] defer apply(rule real_of_pextreal_mono[OF _ int_u_le])
   1.104        using u int_om by auto
   1.105    qed note int = conjunctD2[OF this]
   1.106  
   1.107 @@ -921,7 +921,7 @@
   1.108  qed
   1.109  
   1.110  lemma borel_fubini_positiv_integral:
   1.111 -  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> pinfreal"
   1.112 +  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> pextreal"
   1.113    assumes f: "f \<in> borel_measurable borel"
   1.114    shows "borel.positive_integral f =
   1.115            borel_product.product_positive_integral {..<DIM('a)} (f \<circ> p2e)"