summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Analysis/Embed_Measure.thy

changeset 67399 | eab6ce8368fa |

parent 67241 | 73635a5bfa5c |

child 69180 | 922833cc6839 |

1.1 --- a/src/HOL/Analysis/Embed_Measure.thy Wed Jan 10 15:21:49 2018 +0100 1.2 +++ b/src/HOL/Analysis/Embed_Measure.thy Wed Jan 10 15:25:09 2018 +0100 1.3 @@ -159,15 +159,15 @@ 1.4 from assms(1) interpret sigma_finite_measure M . 1.5 from sigma_finite_countable obtain A where 1.6 A_props: "countable A" "A \<subseteq> sets M" "\<Union>A = space M" "\<And>X. X\<in>A \<Longrightarrow> emeasure M X \<noteq> \<infinity>" by blast 1.7 - from A_props have "countable (op ` f`A)" by auto 1.8 + from A_props have "countable ((`) f`A)" by auto 1.9 moreover 1.10 - from inj and A_props have "op ` f`A \<subseteq> sets (embed_measure M f)" 1.11 + from inj and A_props have "(`) f`A \<subseteq> sets (embed_measure M f)" 1.12 by (auto simp: sets_embed_measure) 1.13 moreover 1.14 - from A_props and inj have "\<Union>(op ` f`A) = space (embed_measure M f)" 1.15 + from A_props and inj have "\<Union>((`) f`A) = space (embed_measure M f)" 1.16 by (auto simp: space_embed_measure intro!: imageI) 1.17 moreover 1.18 - from A_props and inj have "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>" 1.19 + from A_props and inj have "\<forall>a\<in>(`) f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>" 1.20 by (intro ballI, subst emeasure_embed_measure) 1.21 (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure) 1.22 ultimately show ?thesis by - (standard, blast) 1.23 @@ -189,7 +189,7 @@ 1.24 by(rule embed_measure_count_space')(erule subset_inj_on, simp) 1.25 1.26 lemma sets_embed_measure_alt: 1.27 - "inj f \<Longrightarrow> sets (embed_measure M f) = (op` f) ` sets M" 1.28 + "inj f \<Longrightarrow> sets (embed_measure M f) = ((`) f) ` sets M" 1.29 by (auto simp: sets_embed_measure) 1.30 1.31 lemma emeasure_embed_measure_image': 1.32 @@ -210,7 +210,7 @@ 1.33 assumes "inj f" 1.34 shows "embed_measure A f = embed_measure B f \<longleftrightarrow> A = B" (is "?M = ?N \<longleftrightarrow> _") 1.35 proof 1.36 - from assms have I: "inj (op` f)" by (auto intro: injI dest: injD) 1.37 + from assms have I: "inj ((`) f)" by (auto intro: injI dest: injD) 1.38 assume asm: "?M = ?N" 1.39 hence "sets (embed_measure A f) = sets (embed_measure B f)" by simp 1.40 with assms have "sets A = sets B" by (simp only: I inj_image_eq_iff sets_embed_measure_alt) 1.41 @@ -369,7 +369,7 @@ 1.42 lemma nn_integral_monotone_convergence_SUP_countable: 1.43 fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ennreal" 1.44 assumes nonempty: "Y \<noteq> {}" 1.45 - and chain: "Complete_Partial_Order.chain op \<le> (f ` Y)" 1.46 + and chain: "Complete_Partial_Order.chain (\<le>) (f ` Y)" 1.47 and countable: "countable B" 1.48 shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space B) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space B))" 1.49 (is "?lhs = ?rhs") 1.50 @@ -383,7 +383,7 @@ 1.51 by(simp add: nn_integral_count_space_indicator ennreal_indicator[symmetric] SUP_mult_right_ennreal nonempty) 1.52 also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)" 1.53 proof(rule nn_integral_monotone_convergence_SUP_nat) 1.54 - show "Complete_Partial_Order.chain op \<le> (?f ` Y)" 1.55 + show "Complete_Partial_Order.chain (\<le>) (?f ` Y)" 1.56 by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD) 1.57 qed fact 1.58 also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))"