src/HOL/Analysis/Embed_Measure.thy
changeset 69260 0a9688695a1b
parent 69180 922833cc6839
child 69313 b021008c5397
     1.1 --- a/src/HOL/Analysis/Embed_Measure.thy	Wed Nov 07 23:03:45 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Embed_Measure.thy	Thu Nov 08 09:11:52 2018 +0100
     1.3 @@ -381,24 +381,24 @@
     1.4    assumes nonempty: "Y \<noteq> {}"
     1.5    and chain: "Complete_Partial_Order.chain (\<le>) (f ` Y)"
     1.6    and countable: "countable B"
     1.7 -  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.8 +  shows "(\<integral>\<^sup>+ x. (SUP i\<in>Y. f i x) \<partial>count_space B) = (SUP i\<in>Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space B))"
     1.9    (is "?lhs = ?rhs")
    1.10  proof -
    1.11    let ?f = "(\<lambda>i x. f i (from_nat_into B x) * indicator (to_nat_on B ` B) x)"
    1.12 -  have "?lhs = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B (to_nat_on B x))) \<partial>count_space B"
    1.13 +  have "?lhs = \<integral>\<^sup>+ x. (SUP i\<in>Y. f i (from_nat_into B (to_nat_on B x))) \<partial>count_space B"
    1.14      by(rule nn_integral_cong)(simp add: countable)
    1.15 -  also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B x)) \<partial>count_space (to_nat_on B ` B)"
    1.16 +  also have "\<dots> = \<integral>\<^sup>+ x. (SUP i\<in>Y. f i (from_nat_into B x)) \<partial>count_space (to_nat_on B ` B)"
    1.17      by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
    1.18 -  also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. ?f i x) \<partial>count_space UNIV"
    1.19 +  also have "\<dots> = \<integral>\<^sup>+ x. (SUP i\<in>Y. ?f i x) \<partial>count_space UNIV"
    1.20      by(simp add: nn_integral_count_space_indicator ennreal_indicator[symmetric] SUP_mult_right_ennreal nonempty)
    1.21 -  also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)"
    1.22 +  also have "\<dots> = (SUP i\<in>Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)"
    1.23    proof(rule nn_integral_monotone_convergence_SUP_nat)
    1.24      show "Complete_Partial_Order.chain (\<le>) (?f ` Y)"
    1.25        by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD)
    1.26    qed fact
    1.27 -  also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))"
    1.28 +  also have "\<dots> = (SUP i\<in>Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))"
    1.29      by(simp add: nn_integral_count_space_indicator)
    1.30 -  also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \<partial>count_space B)"
    1.31 +  also have "\<dots> = (SUP i\<in>Y. \<integral>\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \<partial>count_space B)"
    1.32      by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
    1.33    also have "\<dots> = ?rhs"
    1.34      by(intro arg_cong2[where f="SUPREMUM"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable)