src/HOL/Analysis/Radon_Nikodym.thy
changeset 64911 f0e07600de47
parent 64283 979cdfdf7a79
child 69173 38beaaebe736
     1.1 --- a/src/HOL/Analysis/Radon_Nikodym.thy	Tue Jan 17 11:26:21 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Radon_Nikodym.thy	Tue Jan 17 13:59:10 2017 +0100
     1.3 @@ -44,9 +44,9 @@
     1.4    qed
     1.5  qed fact
     1.6  
     1.7 -text {*An equivalent characterization of sigma-finite spaces is the existence of integrable
     1.8 +text \<open>An equivalent characterization of sigma-finite spaces is the existence of integrable
     1.9  positive functions (or, still equivalently, the existence of a probability measure which is in
    1.10 -the same measure class as the original measure).*}
    1.11 +the same measure class as the original measure).\<close>
    1.12  
    1.13  lemma (in sigma_finite_measure) obtain_positive_integrable_function:
    1.14    obtains f::"'a \<Rightarrow> real" where
    1.15 @@ -69,7 +69,7 @@
    1.16  
    1.17    have g_pos: "g x > 0" if "x \<in> space M" for x
    1.18    unfolding g_def proof (subst suminf_pos_iff[OF *[of x]], auto)
    1.19 -    obtain i where "x \<in> A i" using `(\<Union>i. A i) = space M` `x \<in> space M` by auto
    1.20 +    obtain i where "x \<in> A i" using \<open>(\<Union>i. A i) = space M\<close> \<open>x \<in> space M\<close> by auto
    1.21      then have "0 < (1 / 2) ^ Suc i * indicator (A i) x / (1 + Sigma_Algebra.measure M (A i))"
    1.22        unfolding indicator_def apply (auto simp add: divide_simps) using measure_nonneg[of M "A i"]
    1.23        by (auto, meson add_nonneg_nonneg linorder_not_le mult_nonneg_nonneg zero_le_numeral zero_le_one zero_le_power)
    1.24 @@ -81,7 +81,7 @@
    1.25    unfolding g_def proof (rule integrable_suminf)
    1.26      fix n
    1.27      show "integrable M (\<lambda>x. (1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n)))"
    1.28 -      using `emeasure M (A n) \<noteq> \<infinity>`
    1.29 +      using \<open>emeasure M (A n) \<noteq> \<infinity>\<close>
    1.30        by (auto intro!: integrable_mult_right integrable_divide_zero integrable_real_indicator simp add: top.not_eq_extremum)
    1.31    next
    1.32      show "AE x in M. summable (\<lambda>n. norm ((1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n))))"
    1.33 @@ -97,7 +97,7 @@
    1.34    moreover have "f x \<le> 1" for x unfolding f_def using g_le_1 by auto
    1.35    moreover have [measurable]: "f \<in> borel_measurable M" unfolding f_def by auto
    1.36    moreover have "integrable M f"
    1.37 -    apply (subst integrable_cong[of _ _ _ g]) unfolding f_def using `integrable M g` by auto
    1.38 +    apply (subst integrable_cong[of _ _ _ g]) unfolding f_def using \<open>integrable M g\<close> by auto
    1.39    ultimately show "(\<And>f. f \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 < f x) \<Longrightarrow> (\<And>x. f x \<le> 1) \<Longrightarrow> integrable M f \<Longrightarrow> thesis) \<Longrightarrow> thesis"
    1.40      by (meson that)
    1.41  qed
    1.42 @@ -314,7 +314,7 @@
    1.43  
    1.44      let ?f = "\<lambda>x. f x + b"
    1.45      have "nn_integral M f \<noteq> top"
    1.46 -      using `f \<in> G`[THEN G_D, of "space M"] by (auto simp: top_unique cong: nn_integral_cong)
    1.47 +      using \<open>f \<in> G\<close>[THEN G_D, of "space M"] by (auto simp: top_unique cong: nn_integral_cong)
    1.48      with \<open>b \<noteq> top\<close> interpret Mf: finite_measure "density M ?f"
    1.49        by (intro finite_measureI)
    1.50           (auto simp: field_simps mult_indicator_subset ennreal_mult_eq_top_iff