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.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)"
```