[isabelle-dev] Lemma "sum_image_le"

[Alexander Maletzky]

Dear list,

lemma "sum_image_le" in theory "Groups_Big", which is stated for
type-class "ordered_ab_group_add", holds more generally for
"ordered_comm_monoid_add" (proof below). May I propose to change it
accordingly?

Best regards,
Alexander


lemma sum_image_le:
  fixes g :: "'a ⇒ 'b::ordered_comm_monoid_add"
  assumes "finite I" and "⋀i. i ∈ I ⟹ 0 ≤ g(f i)"
    shows "sum g (f ` I) ≤ sum (g ∘ f) I"
  using assms
proof induction
  case empty
  then show ?case by auto
next
  case (insert x F)
  from insertI1 have "0 ≤ g (f x)" by (rule insert)
  hence 1: "sum g (f ` F) ≤ g (f x) + sum g (f ` F)" using
add_increasing by blast
  from insert have 2: "sum g (f ` F) ≤ sum (g ∘ f) F" by blast
  have "sum g (f ` insert x F) = sum g (insert (f x) (f ` F))" by simp
  also have "… ≤ g (f x) + sum g (f ` F)"
    by (simp add: 1 insert sum.insert_if)
  also from 2 have "… ≤ g (f x) + sum (g ∘ f) F" by (rule add_left_mono)
  also from insert(1, 2) have "… = sum (g ∘ f) (insert x F)" by (simp
add: sum.insert_if)
  finally show ?case .
qed