src/HOL/Analysis/Bochner_Integration.thy
changeset 64911 f0e07600de47
parent 64287 d85d88722745
child 65680 378a2f11bec9
     1.1 --- a/src/HOL/Analysis/Bochner_Integration.thy	Tue Jan 17 11:26:21 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Bochner_Integration.thy	Tue Jan 17 13:59:10 2017 +0100
     1.3 @@ -1931,9 +1931,9 @@
     1.4      integral\<^sup>L M f \<le> integral\<^sup>L M g"
     1.5    by (intro integral_mono_AE) auto
     1.6  
     1.7 -text {*The next two statements are useful to bound Lebesgue integrals, as they avoid one
     1.8 +text \<open>The next two statements are useful to bound Lebesgue integrals, as they avoid one
     1.9  integrability assumption. The price to pay is that the upper function has to be nonnegative,
    1.10 -but this is often true and easy to check in computations.*}
    1.11 +but this is often true and easy to check in computations.\<close>
    1.12  
    1.13  lemma integral_mono_AE':
    1.14    fixes f::"_ \<Rightarrow> real"
    1.15 @@ -2047,20 +2047,20 @@
    1.16    shows "(emeasure M) {x\<in>space M. u x \<ge> c} \<le> (1/c) * (\<integral>x. u x \<partial>M)"
    1.17  proof -
    1.18    have "(\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M) \<le> (\<integral>\<^sup>+ x. u x \<partial>M)"
    1.19 -    by (rule nn_integral_mono_AE, auto simp add: `c>0` less_eq_real_def)
    1.20 +    by (rule nn_integral_mono_AE, auto simp add: \<open>c>0\<close> less_eq_real_def)
    1.21    also have "... = (\<integral>x. u x \<partial>M)"
    1.22      by (rule nn_integral_eq_integral, auto simp add: assms)
    1.23    finally have *: "(\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M) \<le> (\<integral>x. u x \<partial>M)"
    1.24      by simp
    1.25  
    1.26    have "{x \<in> space M. u x \<ge> c} = {x \<in> space M. ennreal(1/c) * u x \<ge> 1} \<inter> (space M)"
    1.27 -    using `c>0` by (auto simp: ennreal_mult'[symmetric])
    1.28 +    using \<open>c>0\<close> by (auto simp: ennreal_mult'[symmetric])
    1.29    then have "emeasure M {x \<in> space M. u x \<ge> c} = emeasure M ({x \<in> space M. ennreal(1/c) * u x \<ge> 1} \<inter> (space M))"
    1.30      by simp
    1.31    also have "... \<le> ennreal(1/c) * (\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M)"
    1.32      by (rule nn_integral_Markov_inequality) (auto simp add: assms)
    1.33    also have "... \<le> ennreal(1/c) * (\<integral>x. u x \<partial>M)"
    1.34 -    apply (rule mult_left_mono) using * `c>0` by auto
    1.35 +    apply (rule mult_left_mono) using * \<open>c>0\<close> by auto
    1.36    finally show ?thesis
    1.37      using \<open>0<c\<close> by (simp add: ennreal_mult'[symmetric])
    1.38  qed
    1.39 @@ -2121,8 +2121,8 @@
    1.40    then show ?thesis using Lim_null by auto
    1.41  qed
    1.42  
    1.43 -text {*The next lemma asserts that, if a sequence of functions converges in $L^1$, then
    1.44 -it admits a subsequence that converges almost everywhere.*}
    1.45 +text \<open>The next lemma asserts that, if a sequence of functions converges in $L^1$, then
    1.46 +it admits a subsequence that converges almost everywhere.\<close>
    1.47  
    1.48  lemma tendsto_L1_AE_subseq:
    1.49    fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
    1.50 @@ -2146,8 +2146,8 @@
    1.51    have "subseq r" unfolding r_def using r0(1) by (simp add: subseq_Suc_iff)
    1.52    have I: "(\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M) < ennreal((1/2)^n)" for n
    1.53    proof -
    1.54 -    have "r0 n \<ge> n" using `subseq r0` by (simp add: seq_suble)
    1.55 -    have "(1/2::real)^(r0 n) \<le> (1/2)^n" by (rule power_decreasing[OF `r0 n \<ge> n`], auto)
    1.56 +    have "r0 n \<ge> n" using \<open>subseq r0\<close> by (simp add: seq_suble)
    1.57 +    have "(1/2::real)^(r0 n) \<le> (1/2)^n" by (rule power_decreasing[OF \<open>r0 n \<ge> n\<close>], auto)
    1.58      then have "(\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^n" using r0(2) less_le_trans by auto
    1.59      then have "(\<integral>x. norm(u (r n) x) \<partial>M) < (1/2)^n" unfolding r_def by auto
    1.60      moreover have "(\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M) = (\<integral>x. norm(u (r n) x) \<partial>M)"
    1.61 @@ -2168,13 +2168,13 @@
    1.62        also have "... \<le> (\<integral>\<^sup>+x. (1/e) * ennreal(norm(u (r n) x)) \<partial>M)"
    1.63          apply (rule nn_integral_mono) using * by auto
    1.64        also have "... = (1/e) * (\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M)"
    1.65 -        apply (rule nn_integral_cmult) using `e > 0` by auto
    1.66 +        apply (rule nn_integral_cmult) using \<open>e > 0\<close> by auto
    1.67        also have "... < (1/e) * ennreal((1/2)^n)"
    1.68 -        using I[of n] `e > 0` by (intro ennreal_mult_strict_left_mono) auto
    1.69 +        using I[of n] \<open>e > 0\<close> by (intro ennreal_mult_strict_left_mono) auto
    1.70        finally show ?thesis by simp
    1.71      qed
    1.72      have A_fin: "emeasure M (A n) < \<infinity>" for n
    1.73 -      using `e > 0` A_bound[of n]
    1.74 +      using \<open>e > 0\<close> A_bound[of n]
    1.75        by (auto simp add: ennreal_mult less_top[symmetric])
    1.76  
    1.77      have A_sum: "summable (\<lambda>n. measure M (A n))"
    1.78 @@ -2219,7 +2219,7 @@
    1.79        by (simp add: tendsto_norm_zero_iff)
    1.80    }
    1.81    ultimately have "AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0" by auto
    1.82 -  then show ?thesis using `subseq r` by auto
    1.83 +  then show ?thesis using \<open>subseq r\<close> by auto
    1.84  qed
    1.85  
    1.86  subsection \<open>Restricted measure spaces\<close>