generalized to big sum
authorimmler
Thu Dec 27 21:00:50 2018 +0100 (4 months ago)
changeset 695100f31dd2e540d
parent 69509 f9bf65d90b69
child 69511 4cc5e4a528f8
generalized to big sum
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Groups_Big.thy
     1.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Dec 27 19:48:41 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Dec 27 21:00:50 2018 +0100
     1.3 @@ -2637,9 +2637,9 @@
     1.4      }
     1.5      moreover
     1.6      have "(\<Sum>v\<in>y ` {1..k}. sum u {i \<in> {1..k}. y i = v}) = 1"
     1.7 -      unfolding sum_image_gen[OF fin, symmetric] using obt(2) by auto
     1.8 +      unfolding sum.image_gen[OF fin, symmetric] using obt(2) by auto
     1.9      moreover have "(\<Sum>v\<in>y ` {1..k}. sum u {i \<in> {1..k}. y i = v} *\<^sub>R v) = x"
    1.10 -      using sum_image_gen[OF fin, of "\<lambda>i. u i *\<^sub>R y i" y, symmetric]
    1.11 +      using sum.image_gen[OF fin, of "\<lambda>i. u i *\<^sub>R y i" y, symmetric]
    1.12        unfolding scaleR_left.sum using obt(3) by auto
    1.13      ultimately
    1.14      have "\<exists>S u. finite S \<and> S \<subseteq> p \<and> (\<forall>x\<in>S. 0 \<le> u x) \<and> sum u S = 1 \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = x"
    1.15 @@ -2683,8 +2683,8 @@
    1.16          by (auto simp: sum_constant_scaleR)
    1.17      }
    1.18      then have "(\<Sum>x = 1..card S. u (f x)) = 1" "(\<Sum>i = 1..card S. u (f i) *\<^sub>R f i) = y"
    1.19 -      unfolding sum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f]
    1.20 -        and sum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f]
    1.21 +      unfolding sum.image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f]
    1.22 +        and sum.image_gen[OF *(1), of "\<lambda>x. u (f x)" f]
    1.23        unfolding f
    1.24        using sum.cong [of S S "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card S}. f x = y}. u (f x) *\<^sub>R f x)" "\<lambda>v. u v *\<^sub>R v"]
    1.25        using sum.cong [of S S "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card S}. f x = y}. u (f x))" u]
     2.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Dec 27 19:48:41 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Dec 27 21:00:50 2018 +0100
     2.3 @@ -5924,7 +5924,7 @@
     2.4        next
     2.5          have "norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x) - (\<Sum>(x,K)\<in>\<D>. integral K (f (m x))))
     2.6                \<le> norm (\<Sum>j = 0..s. \<Sum>(x,K)\<in>{xk \<in> \<D>. m (fst xk) = j}. content K *\<^sub>R f (m x) x - integral K (f (m x)))"
     2.7 -          apply (subst sum_group)
     2.8 +          apply (subst sum.group)
     2.9            using s by (auto simp: sum_subtractf split_def p'(1))
    2.10          also have "\<dots> < e/2"
    2.11          proof -
     3.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Dec 27 19:48:41 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Dec 27 21:00:50 2018 +0100
     3.3 @@ -106,12 +106,6 @@
     3.4    using sum_norm_le[OF K] sum_constant[symmetric]
     3.5    by simp
     3.6  
     3.7 -lemma sum_group:
     3.8 -  assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"
     3.9 -  shows "sum (\<lambda>y. sum g {x. x \<in> S \<and> f x = y}) T = sum g S"
    3.10 -  unfolding sum_image_gen[OF fS, of g f]
    3.11 -  by (auto intro: sum.neutral sum.mono_neutral_right[OF fT fST])
    3.12 -
    3.13  lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
    3.14  proof
    3.15    assume "\<forall>x. x \<bullet> y = x \<bullet> z"
     4.1 --- a/src/HOL/Groups_Big.thy	Thu Dec 27 19:48:41 2018 +0100
     4.2 +++ b/src/HOL/Groups_Big.thy	Thu Dec 27 21:00:50 2018 +0100
     4.3 @@ -439,6 +439,25 @@
     4.4      F (\<lambda>x. F (g x) {y. y \<in> B \<and> R x y}) A = F (\<lambda>y. F (\<lambda>x. g x y) {x. x \<in> A \<and> R x y}) B"
     4.5    by (simp add: inter_filter) (rule swap)
     4.6  
     4.7 +lemma image_gen:
     4.8 +  assumes fin: "finite S"
     4.9 +  shows "F h S = F (\<lambda>y. F h {x. x \<in> S \<and> g x = y}) (g ` S)"
    4.10 +proof -
    4.11 +  have "{y. y\<in> g`S \<and> g x = y} = {g x}" if "x \<in> S" for x
    4.12 +    using that by auto
    4.13 +  then have "F h S = F (\<lambda>x. F (\<lambda>y. h x) {y. y\<in> g`S \<and> g x = y}) S"
    4.14 +    by simp
    4.15 +  also have "\<dots> = F (\<lambda>y. F h {x. x \<in> S \<and> g x = y}) (g ` S)"
    4.16 +    by (rule swap_restrict [OF fin finite_imageI [OF fin]])
    4.17 +  finally show ?thesis .
    4.18 +qed
    4.19 +
    4.20 +lemma group:
    4.21 +  assumes fS: "finite S" and fT: "finite T" and fST: "g ` S \<subseteq> T"
    4.22 +  shows "F (\<lambda>y. F h {x. x \<in> S \<and> g x = y}) T = F h S"
    4.23 +  unfolding image_gen[OF fS, of h g]
    4.24 +  by (auto intro: neutral mono_neutral_right[OF fT fST])
    4.25 +
    4.26  lemma Plus:
    4.27    fixes A :: "'b set" and B :: "'c set"
    4.28    assumes fin: "finite A" "finite B"
    4.29 @@ -534,21 +553,6 @@
    4.30  in [(@{const_syntax sum}, K sum_tr')] end
    4.31  \<close>
    4.32  
    4.33 -(* TODO generalization candidates *)
    4.34 -
    4.35 -lemma (in comm_monoid_add) sum_image_gen:
    4.36 -  assumes fin: "finite S"
    4.37 -  shows "sum g S = sum (\<lambda>y. sum g {x. x \<in> S \<and> f x = y}) (f ` S)"
    4.38 -proof -
    4.39 -  have "{y. y\<in> f`S \<and> f x = y} = {f x}" if "x \<in> S" for x
    4.40 -    using that by auto
    4.41 -  then have "sum g S = sum (\<lambda>x. sum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S"
    4.42 -    by simp
    4.43 -  also have "\<dots> = sum (\<lambda>y. sum g {x. x \<in> S \<and> f x = y}) (f ` S)"
    4.44 -    by (rule sum.swap_restrict [OF fin finite_imageI [OF fin]])
    4.45 -  finally show ?thesis .
    4.46 -qed
    4.47 -
    4.48  
    4.49  subsubsection \<open>Properties in more restricted classes of structures\<close>
    4.50  
    4.51 @@ -756,7 +760,7 @@
    4.52    also have "\<dots> \<le> sum (\<lambda>y. sum g {x. x\<in>t \<and> i x = y}) (i ` t)"
    4.53      using assms(2-4) by (auto intro!: sum_mono2 sum_nonneg)
    4.54    also have "\<dots> \<le> sum g t"
    4.55 -    using assms by (auto simp: sum_image_gen[symmetric])
    4.56 +    using assms by (auto simp: sum.image_gen[symmetric])
    4.57    finally show ?thesis .
    4.58  qed
    4.59