src/HOL/Probability/Lebesgue_Measure.thy

   note has_gmeasure_lmeasure[OF this]
   thus ?thesis .
 qed
 
 lemma lebesgue_simple_function_indicator:
-  fixes f::"'a::ordered_euclidean_space \<Rightarrow> pinfreal"
+  fixes f::"'a::ordered_euclidean_space \<Rightarrow> pextreal"
   assumes f:"lebesgue.simple_function f"
   shows "f = (\<lambda>x. (\<Sum>y \<in> f ` UNIV. y * indicator (f -` {y}) x))"
   apply(rule,subst lebesgue.simple_function_indicator_representation[OF f]) by auto
 
 lemma lmeasure_gmeasure:

   then show ?thesis by simp
 qed
 
 lemma lmeasure_singleton[simp]:
   fixes a :: "'a::ordered_euclidean_space" shows "lmeasure {a} = 0"
-  using has_gmeasure_interval[of a a] unfolding zero_pinfreal_def
+  using has_gmeasure_interval[of a a] unfolding zero_pextreal_def
   by (intro has_gmeasure_lmeasure)
      (simp add: content_closed_interval DIM_positive)
 
 declare content_real[simp]
 

   ultimately show "\<exists>A::nat \<Rightarrow> 'b set. range A \<subseteq> sets lebesgue \<and> (\<Union>i. A i) = space lebesgue \<and> (\<forall>i. lmeasure (A i) \<noteq> \<omega>)"
     by auto
 qed
 
 lemma simple_function_has_integral:
-  fixes f::"'a::ordered_euclidean_space \<Rightarrow> pinfreal"
+  fixes f::"'a::ordered_euclidean_space \<Rightarrow> pextreal"
   assumes f:"lebesgue.simple_function f"
   and f':"\<forall>x. f x \<noteq> \<omega>"
   and om:"\<forall>x\<in>range f. lmeasure (f -` {x} \<inter> UNIV) = \<omega> \<longrightarrow> x = 0"
   shows "((\<lambda>x. real (f x)) has_integral (real (lebesgue.simple_integral f))) UNIV"
   unfolding lebesgue.simple_integral_def
   apply(subst lebesgue_simple_function_indicator[OF f])
 proof- case goal1
   have *:"\<And>x. \<forall>y\<in>range f. y * indicator (f -` {y}) x \<noteq> \<omega>"
     "\<forall>x\<in>range f. x * lmeasure (f -` {x} \<inter> UNIV) \<noteq> \<omega>"
     using f' om unfolding indicator_def by auto
-  show ?case unfolding space_lebesgue real_of_pinfreal_setsum'[OF *(1),THEN sym]
-    unfolding real_of_pinfreal_setsum'[OF *(2),THEN sym]
-    unfolding real_of_pinfreal_setsum space_lebesgue
+  show ?case unfolding space_lebesgue real_of_pextreal_setsum'[OF *(1),THEN sym]
+    unfolding real_of_pextreal_setsum'[OF *(2),THEN sym]
+    unfolding real_of_pextreal_setsum space_lebesgue
     apply(rule has_integral_setsum)
   proof safe show "finite (range f)" using f by (auto dest: lebesgue.simple_functionD)
     fix y::'a show "((\<lambda>x. real (f y * indicator (f -` {f y}) x)) has_integral
       real (f y * lmeasure (f -` {f y} \<inter> UNIV))) UNIV"
     proof(cases "f y = 0") case False
       have mea:"gmeasurable (f -` {f y})" apply(rule lmeasure_finite_gmeasurable)
         using assms unfolding lebesgue.simple_function_def using False by auto
-      have *:"\<And>x. real (indicator (f -` {f y}) x::pinfreal) = (if x \<in> f -` {f y} then 1 else 0)" by auto
-      show ?thesis unfolding real_of_pinfreal_mult[THEN sym]
+      have *:"\<And>x. real (indicator (f -` {f y}) x::pextreal) = (if x \<in> f -` {f y} then 1 else 0)" by auto
+      show ?thesis unfolding real_of_pextreal_mult[THEN sym]
         apply(rule has_integral_cmul[where 'b=real, unfolded real_scaleR_def])
         unfolding Int_UNIV_right lmeasure_gmeasure[OF mea,THEN sym]
         unfolding measure_integral_univ[OF mea] * apply(rule integrable_integral)
         unfolding gmeasurable_integrable[THEN sym] using mea .
     qed auto

 lemma bounded_realI: assumes "\<forall>x\<in>s. abs (x::real) \<le> B" shows "bounded s"
   unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI)
   using assms by auto
 
 lemma simple_function_has_integral':
-  fixes f::"'a::ordered_euclidean_space \<Rightarrow> pinfreal"
+  fixes f::"'a::ordered_euclidean_space \<Rightarrow> pextreal"
   assumes f:"lebesgue.simple_function f"
   and i: "lebesgue.simple_integral f \<noteq> \<omega>"
   shows "((\<lambda>x. real (f x)) has_integral (real (lebesgue.simple_integral f))) UNIV"
 proof- let ?f = "\<lambda>x. if f x = \<omega> then 0 else f x"
   { fix x have "real (f x) = real (?f x)" by (cases "f x") auto } note * = this

     qed
   qed
 qed
 
 lemma (in measure_space) positive_integral_monotone_convergence:
-  fixes f::"nat \<Rightarrow> 'a \<Rightarrow> pinfreal"
+  fixes f::"nat \<Rightarrow> 'a \<Rightarrow> pextreal"
   assumes i: "\<And>i. f i \<in> borel_measurable M" and mono: "\<And>x. mono (\<lambda>n. f n x)"
   and lim: "\<And>x. (\<lambda>i. f i x) ----> u x"
   shows "u \<in> borel_measurable M"
   and "(\<lambda>i. positive_integral (f i)) ----> positive_integral u" (is ?ilim)
 proof -
   from positive_integral_isoton[unfolded isoton_fun_expand isoton_iff_Lim_mono, of f u]
   show ?ilim using mono lim i by auto
-  have "(SUP i. f i) = u" using mono lim SUP_Lim_pinfreal
+  have "(SUP i. f i) = u" using mono lim SUP_Lim_pextreal
     unfolding fun_eq_iff SUPR_fun_expand mono_def by auto
   moreover have "(SUP i. f i) \<in> borel_measurable M"
     using i by (rule borel_measurable_SUP)
   ultimately show "u \<in> borel_measurable M" by simp
 qed
 
 lemma positive_integral_has_integral:
-  fixes f::"'a::ordered_euclidean_space => pinfreal"
+  fixes f::"'a::ordered_euclidean_space => pextreal"
   assumes f:"f \<in> borel_measurable lebesgue"
   and int_om:"lebesgue.positive_integral f \<noteq> \<omega>"
   and f_om:"\<forall>x. f x \<noteq> \<omega>" (* TODO: remove this *)
   shows "((\<lambda>x. real (f x)) has_integral (real (lebesgue.positive_integral f))) UNIV"
 proof- let ?i = "lebesgue.positive_integral f"

 
   note u_int = simple_function_has_integral'[OF u(1) this]
   have "(\<lambda>x. real (f x)) integrable_on UNIV \<and>
     (\<lambda>k. Integration.integral UNIV (\<lambda>x. real (u k x))) ----> Integration.integral UNIV (\<lambda>x. real (f x))"
     apply(rule monotone_convergence_increasing) apply(rule,rule,rule u_int)
-  proof safe case goal1 show ?case apply(rule real_of_pinfreal_mono) using u(2,3) by auto
+  proof safe case goal1 show ?case apply(rule real_of_pextreal_mono) using u(2,3) by auto
   next case goal2 show ?case using u(3) apply(subst lim_Real[THEN sym])
       prefer 3 apply(subst Real_real') defer apply(subst Real_real')
       using isotone_Lim[OF u(3)[unfolded isoton_fun_expand, THEN spec]] using f_om u by auto
   next case goal3
     show ?case apply(rule bounded_realI[where B="real (lebesgue.positive_integral f)"])
       apply safe apply(subst abs_of_nonneg) apply(rule integral_nonneg,rule) apply(rule u_int)
-      unfolding integral_unique[OF u_int] defer apply(rule real_of_pinfreal_mono[OF _ int_u_le])
+      unfolding integral_unique[OF u_int] defer apply(rule real_of_pextreal_mono[OF _ int_u_le])
       using u int_om by auto
   qed note int = conjunctD2[OF this]
 
   have "(\<lambda>i. lebesgue.simple_integral (u i)) ----> ?i" unfolding u_simple
     apply(rule lebesgue.positive_integral_monotone_convergence(2))

   show "\<exists>xa\<in>Chi -` A \<inter> extensional {..<DIM('a)}. x = Chi xa" apply(rule_tac x="?y" in bexI)
     apply(subst euclidean_eq) unfolding extensional_def using `x\<in>A` by(auto simp: *)
 qed
 
 lemma borel_fubini_positiv_integral:
-  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> pinfreal"
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> pextreal"
   assumes f: "f \<in> borel_measurable borel"
   shows "borel.positive_integral f =
           borel_product.product_positive_integral {..<DIM('a)} (f \<circ> p2e)"
 proof- def U \<equiv> "(({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)}):: (nat \<Rightarrow> real) set"
   interpret fprod: finite_product_sigma_finite "\<lambda>x. borel" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto