src/HOL/Analysis/Measure_Space.thy
changeset 69313 b021008c5397
parent 69286 e4d5a07fecb6
child 69517 dc20f278e8f3
     1.1 --- a/src/HOL/Analysis/Measure_Space.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -317,7 +317,7 @@
     1.4      (\<forall>A. range A \<subseteq> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Union>i. A i))"
     1.5    unfolding countably_additive_def
     1.6  proof safe
     1.7 -  assume count_sum: "\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> UNION UNIV A \<in> M \<longrightarrow> (\<Sum>i. f (A i)) = f (UNION UNIV A)"
     1.8 +  assume count_sum: "\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> \<Union>(A ` UNIV) \<in> M \<longrightarrow> (\<Sum>i. f (A i)) = f (\<Union>(A ` UNIV))"
     1.9    fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "incseq A" "(\<Union>i. A i) \<in> M"
    1.10    then have dA: "range (disjointed A) \<subseteq> M" by (auto simp: range_disjointed_sets)
    1.11    with count_sum[THEN spec, of "disjointed A"] A(3)
    1.12 @@ -1834,7 +1834,7 @@
    1.13    using I
    1.14  proof (induction I rule: finite_induct)
    1.15    case (insert x I)
    1.16 -  have "measure M (F x \<union> UNION I F) = measure M (F x) + measure M (UNION I F)"
    1.17 +  have "measure M (F x \<union> \<Union>(F ` I)) = measure M (F x) + measure M (\<Union>(F ` I))"
    1.18      by (rule measure_Un_AE) (use insert in \<open>auto simp: pairwise_insert\<close>)
    1.19      with insert show ?case
    1.20        by (simp add: pairwise_insert )
    1.21 @@ -3132,7 +3132,7 @@
    1.22  lemma le_measureD3: "A \<le> B \<Longrightarrow> sets A = sets B \<Longrightarrow> emeasure A X \<le> emeasure B X"
    1.23    by (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq split: if_split_asm)
    1.24  
    1.25 -lemma UN_space_closed: "UNION S sets \<subseteq> Pow (UNION S space)"
    1.26 +lemma UN_space_closed: "\<Union>(sets ` S) \<subseteq> Pow (\<Union>(space ` S))"
    1.27    using sets.space_closed by auto
    1.28  
    1.29  definition Sup_lexord :: "('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> 'a"
    1.30 @@ -3245,10 +3245,10 @@
    1.31        with ij show "\<exists>k\<in>{P. finite P \<and> P \<subseteq> M}. \<forall>n\<in>N. ?\<mu> i (F n) \<le> ?\<mu> k (F n) \<and> ?\<mu> j (F n) \<le> ?\<mu> k (F n)"
    1.32          by (safe intro!: bexI[of _ "i \<union> j"]) auto
    1.33      next
    1.34 -      show "(SUP P \<in> {P. finite P \<and> P \<subseteq> M}. \<Sum>n. ?\<mu> P (F n)) = (SUP P \<in> {P. finite P \<and> P \<subseteq> M}. ?\<mu> P (UNION UNIV F))"
    1.35 +      show "(SUP P \<in> {P. finite P \<and> P \<subseteq> M}. \<Sum>n. ?\<mu> P (F n)) = (SUP P \<in> {P. finite P \<and> P \<subseteq> M}. ?\<mu> P (\<Union>(F ` UNIV)))"
    1.36        proof (intro SUP_cong refl)
    1.37          fix i assume i: "i \<in> {P. finite P \<and> P \<subseteq> M}"
    1.38 -        show "(\<Sum>n. ?\<mu> i (F n)) = ?\<mu> i (UNION UNIV F)"
    1.39 +        show "(\<Sum>n. ?\<mu> i (F n)) = ?\<mu> i (\<Union>(F ` UNIV))"
    1.40          proof cases
    1.41            assume "i \<noteq> {}" with i ** show ?thesis
    1.42              apply (intro suminf_emeasure \<open>disjoint_family F\<close>)
    1.43 @@ -3294,9 +3294,9 @@
    1.44    next
    1.45      fix a S assume "a \<in> A" and a: "space a = (\<Union>a\<in>A. space a)" and S: "S = {a' \<in> A. space a' = space a}"
    1.46        and neq: "\<And>aa. aa \<in> S \<Longrightarrow> sets aa \<noteq> (\<Union>a\<in>S. sets a)"
    1.47 -    have sp_a: "space a = (UNION S space)"
    1.48 +    have sp_a: "space a = (\<Union>(space ` S))"
    1.49        using \<open>a\<in>A\<close> by (auto simp: S)
    1.50 -    show "x \<le> sigma (UNION S space) (UNION S sets)"
    1.51 +    show "x \<le> sigma (\<Union>(space ` S)) (\<Union>(sets ` S))"
    1.52      proof cases
    1.53        assume [simp]: "space x = space a"
    1.54        have "sets x \<subset> (\<Union>a\<in>S. sets a)"
    1.55 @@ -3363,19 +3363,19 @@
    1.56      unfolding Sup_measure_def
    1.57    proof (intro Sup_lexord[where P="\<lambda>y. y \<le> x"])
    1.58      assume "\<And>a. a \<in> A \<Longrightarrow> space a \<noteq> (\<Union>a\<in>A. space a)"
    1.59 -    show "sigma (UNION A space) {} \<le> x"
    1.60 +    show "sigma (\<Union>(space ` A)) {} \<le> x"
    1.61        using x[THEN le_measureD1] by (subst sigma_le_iff) auto
    1.62    next
    1.63      fix a S assume "a \<in> A" "space a = (\<Union>a\<in>A. space a)" and S: "S = {a' \<in> A. space a' = space a}"
    1.64        "\<And>a. a \<in> S \<Longrightarrow> sets a \<noteq> (\<Union>a\<in>S. sets a)"
    1.65 -    have "UNION S space \<subseteq> space x"
    1.66 +    have "\<Union>(space ` S) \<subseteq> space x"
    1.67        using S le_measureD1[OF x] by auto
    1.68      moreover
    1.69 -    have "UNION S space = space a"
    1.70 +    have "\<Union>(space ` S) = space a"
    1.71        using \<open>a\<in>A\<close> S by auto
    1.72 -    then have "space x = UNION S space \<Longrightarrow> UNION S sets \<subseteq> sets x"
    1.73 +    then have "space x = \<Union>(space ` S) \<Longrightarrow> \<Union>(sets ` S) \<subseteq> sets x"
    1.74        using \<open>a \<in> A\<close> le_measureD2[OF x] by (auto simp: S)
    1.75 -    ultimately show "sigma (UNION S space) (UNION S sets) \<le> x"
    1.76 +    ultimately show "sigma (\<Union>(space ` S)) (\<Union>(sets ` S)) \<le> x"
    1.77        by (subst sigma_le_iff) simp_all
    1.78    next
    1.79      fix a b S S' assume "a \<in> A" and a: "space a = (\<Union>a\<in>A. space a)" and S: "S = {a' \<in> A. space a' = space a}"
    1.80 @@ -3504,17 +3504,17 @@
    1.81    assumes ch: "Complete_Partial_Order.chain (\<le>) (M ` A)" and "A \<noteq> {}"
    1.82    shows "emeasure (SUP i\<in>A. M i) X = (SUP i\<in>A. emeasure (M i) X)"
    1.83  proof (subst emeasure_SUP[OF sets \<open>A \<noteq> {}\<close>])
    1.84 -  show "(SUP J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}. emeasure (SUPREMUM J M) X) = (SUP i\<in>A. emeasure (M i) X)"
    1.85 +  show "(SUP J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}. emeasure (Sup (M ` J)) X) = (SUP i\<in>A. emeasure (M i) X)"
    1.86    proof (rule SUP_eq)
    1.87      fix J assume "J \<in> {J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}"
    1.88      then have J: "Complete_Partial_Order.chain (\<le>) (M ` J)" "finite J" "J \<noteq> {}" and "J \<subseteq> A"
    1.89        using ch[THEN chain_subset, of "M`J"] by auto
    1.90      with in_chain_finite[OF J(1)] obtain j where "j \<in> J" "(SUP j\<in>J. M j) = M j"
    1.91        by auto
    1.92 -    with \<open>J \<subseteq> A\<close> show "\<exists>j\<in>A. emeasure (SUPREMUM J M) X \<le> emeasure (M j) X"
    1.93 +    with \<open>J \<subseteq> A\<close> show "\<exists>j\<in>A. emeasure (Sup (M ` J)) X \<le> emeasure (M j) X"
    1.94        by auto
    1.95    next
    1.96 -    fix j assume "j\<in>A" then show "\<exists>i\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}. emeasure (M j) X \<le> emeasure (SUPREMUM i M) X"
    1.97 +    fix j assume "j\<in>A" then show "\<exists>i\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}. emeasure (M j) X \<le> emeasure (Sup (M ` i)) X"
    1.98        by (intro bexI[of _ "{j}"]) auto
    1.99    qed
   1.100  qed
   1.101 @@ -3584,7 +3584,7 @@
   1.102    assumes "\<And>m. m \<in> M \<Longrightarrow> sets m \<subseteq> sets N"
   1.103    shows "sets (Sup M) \<subseteq> sets N"
   1.104  proof -
   1.105 -  have *: "UNION M space = space N"
   1.106 +  have *: "\<Union>(space ` M) = space N"
   1.107      using assms by auto
   1.108    show ?thesis
   1.109      unfolding * using assms by (subst sets_Sup_eq[of M "space N"]) (auto intro!: sets.sigma_sets_subset)
   1.110 @@ -3612,7 +3612,7 @@
   1.111      by (intro const_space \<open>m \<in> M\<close>)
   1.112    have "f \<in> measurable N (sigma (\<Union>m\<in>M. space m) (\<Union>m\<in>M. sets m))"
   1.113    proof (rule measurable_measure_of)
   1.114 -    show "f \<in> space N \<rightarrow> UNION M space"
   1.115 +    show "f \<in> space N \<rightarrow> \<Union>(space ` M)"
   1.116        using measurable_space[OF f] M by auto
   1.117    qed (auto intro: measurable_sets f dest: sets.sets_into_space)
   1.118    also have "measurable N (sigma (\<Union>m\<in>M. space m) (\<Union>m\<in>M. sets m)) = measurable N (Sup M)"