Theory Infinite_Sums_of_Positive_Reals

section ‹Infinite Sums of Positive Reals›


text ‹This is a theory of infinite sums of positive reals defined as limits of finite sums. 
The goal is to make reasoning about these infinite sums almost as easy as that about finite sums. 
›


theory Infinite_Sums_of_Positive_Reals
imports Complex_Main "HOL-Library.Countable_Set" 
begin


subsection ‹Preliminaries›

lemma real_pm_iff: 
  "⋀a b c. (a::real) + b ≤ c ⟷ a ≤ c - b"
  "⋀a b c. (a::real) + b ≤ c ⟷ b ≤ c - a"
  "⋀a b c. (a::real) ≤ b - c ⟷ c ≤ b - a"
  by auto

lemma real_md_iff: 
  "⋀a b c. a ≥ 0 ⟹ b > 0 ⟹ c ≥ 0 ⟹ (a::real) * b ≤ c ⟷ a ≤ c / b"
  "⋀a b c. a > 0 ⟹ b ≥ 0 ⟹ c ≥ 0 ⟹ (a::real) * b ≤ c ⟷ b ≤ c / a"
  "⋀a b c. a > 0 ⟹ b ≥ 0 ⟹ c > 0 ⟹ (a::real) ≤ b / c ⟷ c ≤ b / a"
  by (auto simp: field_simps)

lemma disjoint_finite_aux: 
  "∀i∈I. ∀j∈I. i ≠ j ⟶ A i ∩ A j = {} ⟹ B ⊆ ⋃ (A ` I) ⟹ finite B ⟹ finite {i ∈ I. B ∩ A i ≠ {}}"
  apply(rule inj_on_finite[of "λi. SOME b. b ∈ B ∩ A i" _ B])
  subgoal unfolding inj_on_def by auto (metis (no_types, lifting) IntI empty_iff someI)
  subgoal by auto (metis (no_types, lifting) someI)
  subgoal by auto .

lemma incl_UNION_aux: "B ⊆ ⋃ (A ` I) ⟹ B = ⋃ ((λi. (B ∩ A i)) ` {i ∈ I. B ∩ A i ≠ {}})"
  by fastforce

lemma incl_UNION_aux2: "B ⊆ ⋃ (A ` I) ⟷ B = ⋃ ((λi. (B ∩ A i)) ` I)"
  by fastforce

(*  *)
lemma sum_singl[simp]: "sum f {a} = f a"  
  by simp

lemma sum_two[simp]: "a1 ≠ a2 ⟹ sum f {a1,a2} = f a1 + f a2"  
  by simp

lemma sum_three[simp]: "a1 ≠ a2 ⟹ a1 ≠ a3 ⟹ a2 ≠ a3 ⟹ 
 sum f {a1,a2,a3} = f a1 + f a2 + f a3"  
  by (simp add: add.assoc)

(*  *)

lemma Sup_leq: 
  "A ≠ {} ⟹ ∀a∈A. ∃b∈B. (a::real) ≤ b ⟹ bdd_above B ⟹ Sup A ≤ Sup B"
  by (simp add: cSup_mono)

lemma Sup_image_leq: 
  "A ≠ {} ⟹  ∀a∈A. ∃b∈B. (f a::real) ≤ g b ⟹ bdd_above (g ` B) ⟹ 
 Sup (f ` A) ≤ Sup (g ` B)"
  by (rule Sup_leq) auto

lemma Sup_cong: 
  assumes "A ≠ {} ∨ B ≠ {}" "∀a∈A. ∃b∈B. (a::real) ≤ b" "∀b∈B. ∃a∈A. (b::real) ≤ a"
    "bdd_above A ∨ bdd_above B"
  shows "Sup A = Sup B" 
proof-
  have "A ≠ {} ∧ B ≠ {}" "bdd_above A ∧ bdd_above B"
    using assms unfolding bdd_above_def using order.trans by blast+
  thus ?thesis using assms by (smt Sup_leq)
qed

lemma Sup_image_cong: 
  "A ≠ {} ∨ B ≠ {} ⟹ ∀a∈A. ∃b∈B. (f a::real) ≤ g b ⟹ ∀b∈B. ∃a∈A. (g b::real) ≤ f a ⟹ 
 bdd_above (f ` A) ∨ bdd_above (g ` B) ⟹ 
 Sup (f ` A) = Sup (g ` B)"
  by (rule Sup_cong) auto

lemma Sup_congL: 
  "A ≠ {} ⟹ ∀a∈A. ∃b∈B. (a::real) ≤ b ⟹ ∀b∈B. b ≤ Sup A ⟹ Sup A = Sup B"
  by (metis Collect_empty_eq Collect_mem_eq Sup_leq bdd_aboveI cSup_least dual_order.antisym)

lemma Sup_image_congL: 
  "A ≠ {} ⟹ ∀a∈A. ∃b∈B. (f a::real) ≤ g b ⟹ ∀b∈B. g b ≤ Sup (f ` A) ⟹ Sup (f ` A) = Sup (g ` B)"
  by (rule Sup_congL) auto

lemma Sup_congR: 
  "B ≠ {} ⟹ ∀a∈A. a ≤ Sup B ⟹ ∀b∈B. ∃a∈A. (b::real) ≤ a ⟹ Sup A = Sup B"
  by (metis Collect_empty_eq Collect_mem_eq Sup_leq bdd_aboveI cSup_least dual_order.antisym)

lemma Sup_image_congR: 
  "B ≠ {} ⟹ ∀a∈A. f a ≤ Sup (g ` B) ⟹ ∀b∈B. ∃a∈A. (g b::real) ≤ f a ⟹ Sup (f ` A) = Sup (g ` B)"
  by (rule Sup_congR) auto

(* *) 

lemma Sup_eq_0_iff: 
  assumes "A ≠ {}" "bdd_above A" "(∀a∈A. (a::real) ≥ 0)" 
  shows "Sup A = 0 ⟷ (∀a∈A. a = 0)" 
  using assms by (metis all_not_in_conv cSup_eq_maximum cSup_upper leD less_eq_real_def)

lemma plus_Sup_commute:
  assumes f1: "{f1 b1 | b1. φ1 b1} ≠ {}" "bdd_above {f1 b1 | b1. φ1 b1}" and 
          f2: "{f2 b2 | b2. φ2 b2} ≠ {}" "bdd_above {f2 b2 | b2. φ2 b2}"
  shows 
    "Sup {(f1 b1::real) | b1 . φ1 b1} + Sup {f2 b2 | b2 . φ2 b2} = 
     Sup {f1 b1 + f2 b2 | b1 b2. φ1 b1 ∧ φ2 b2}" (is "?L1 + ?L2 = ?R")
proof-
  have f: 
    "{f1 b1 + f2 b2 | b1 b2. φ1 b1 ∧ φ2 b2} ≠ {}"
    "bdd_above {f1 b1 + f2 b2 | b1 b2. φ1 b1 ∧ φ2 b2}"  
    subgoal using f1 f2 by auto
    subgoal using f1(2) f2(2) unfolding bdd_above_def apply safe 
      subgoal for M1 M2
        apply(rule exI[of _ "M1 + M2"]) using add_mono by blast . .
  show ?thesis proof(rule order.antisym)
    show "?L1 + ?L2 ≤ ?R" unfolding real_pm_iff(1) cSup_le_iff[OF f1] apply safe
      apply(subst real_pm_iff(3)) unfolding cSup_le_iff[OF f2] apply safe
      unfolding real_pm_iff(2)[symmetric] apply(rule cSup_upper[OF _ f(2)]) by auto
  next
    show "?R ≤ ?L1 + ?L2" unfolding cSup_le_iff[OF f] apply safe 
      subgoal for _ b1 b2
        using cSup_upper[OF _ f1(2), of "f1 b1"] cSup_upper[OF _ f2(2), of "f2 b2"] 
        by fastforce .
  qed
qed

lemma plus_Sup_commute':
  assumes f1: "A1 ≠ {}" "bdd_above A1" and 
    f2: "A2 ≠ {}" "bdd_above A2"
  shows "Sup A1 + Sup A2 = Sup {(a1::real) + a2 | a1 a2. a1 ∈ A1 ∧ a2 ∈ A2}"  
  using plus_Sup_commute[of id "λa1. a1 ∈ A1" id "λa2. a2 ∈ A2"] assms 
  by auto

lemma plus_SupR: "A ≠ {} ⟹ bdd_above A ⟹ Sup A + (b::real) = Sup {a + b | a. a ∈ A}"
  apply(subst cSup_singleton[of b, symmetric])
  apply(subst plus_Sup_commute') by auto

lemma plus_SupL: "A ≠ {} ⟹ bdd_above A ⟹ (b::real) + Sup A = Sup {b + a | a. a ∈ A}"
  apply(subst cSup_singleton[of b, symmetric])
  apply(subst plus_Sup_commute') by auto 

(* *)

lemma mult_Sup_commute:
  assumes f1: "{f1 b1 | b1. φ1 b1} ≠ {}" "bdd_above {f1 b1 | b1. φ1 b1}" "∀b1. φ1 b1 ⟶ f1 b1 ≥ 0" and 
    f2: "{f2 b2 | b2. φ2 b2} ≠ {}" "bdd_above {f2 b2 | b2. φ2 b2}" "∀b2. φ2 b2 ⟶ f2 b2 ≥ 0"
  shows 
    "Sup {(f1 b1::real) | b1 . φ1 b1} * Sup {f2 b2 | b2 . φ2 b2} = 
 Sup {f1 b1 * f2 b2 | b1 b2. φ1 b1 ∧ φ2 b2}" (is "?L1 * ?L2 = ?R")
proof-
  have f: 
    "{f1 b1 * f2 b2 | b1 b2. φ1 b1 ∧ φ2 b2} ≠ {}"
    "bdd_above {f1 b1 * f2 b2 | b1 b2. φ1 b1 ∧ φ2 b2}" 
    "∀b1 b2. φ1 b1 ∧ φ2 b2 ⟶ f1 b1 * f2 b2 ≥ 0"
    subgoal using f1 f2 by auto
    subgoal using f1(2) f2(2) unfolding bdd_above_def apply safe 
      subgoal for M1 M2
        apply(rule exI[of _ "M1 * M2"]) using mult_mono f1(3) f2(3) by fastforce . 
    subgoal using f1(3) f2(3) by auto .
  show ?thesis
  proof(rule order.antisym)
    show "?L1 * ?L2 ≤ ?R" 
    proof(cases "?L1 = 0 ∨ ?L2 = 0")
      case True thus ?thesis using f 
        by (smt Collect_empty_eq cSup_upper mem_Collect_eq mult_not_zero) 
    next
      case False 
      have gez: "?L1 > 0" "?L2 > 0" "?R ≥ 0"  
          apply (smt Collect_empty_eq False cSup_upper f1 mem_Collect_eq)
         apply (smt Collect_empty_eq False cSup_upper f2 mem_Collect_eq)
        by (smt Collect_empty_eq cSup_upper f(1) f(2) f(3) mem_Collect_eq)
      hence ggez: "?L1 ≥ 0" "?L2 ≥ 0" by linarith+
      show ?thesis 
        unfolding real_md_iff(1)[OF ggez(1) gez(2) gez(3)] 
        unfolding cSup_le_iff[OF f1(1,2)] apply safe
        subgoal for _ b1
          apply(cases "f1 b1 = 0")
          subgoal using divide_nonneg_pos gez(2) gez(3) by auto
          subgoal apply(subst real_md_iff(3)) 
            subgoal using f1(3) by auto
            subgoal using gez(3) by blast
            subgoal using gez(2) by blast
            subgoal unfolding cSup_le_iff[OF f2(1,2)] apply safe
              apply(subst real_md_iff(2)[symmetric]) 
              using f1(3) f2(3) gez(3) by (auto intro: cSup_upper[OF _ f(2)]) . . . 
    qed
  next
    show "?R ≤ ?L1 * ?L2" unfolding cSup_le_iff[OF f(1,2)] apply safe subgoal for _ b1 b2
        using cSup_upper[OF _ f1(2), of "f1 b1"] cSup_upper[OF _ f2(2), of "f2 b2"] 
        by (metis (mono_tags, lifting) f1(3) f2(3) mem_Collect_eq mult_mono') .
  qed
qed

lemma mult_Sup_commute':
  assumes "A1 ≠ {}" "bdd_above A1" "∀a1∈A1. a1 ≥ 0" and 
    "A2 ≠ {}" "bdd_above A2" "∀a2∈A2. a2 ≥ 0"
  shows "Sup A1 * Sup A2 = Sup {(a1::real) * a2 | a1 a2. a1 ∈ A1 ∧ a2 ∈ A2}"  
  using mult_Sup_commute[of id "λa1. a1 ∈ A1" id "λa2. a2 ∈ A2"] assms 
  by auto

lemma mult_SupR: "A ≠ {} ⟹ bdd_above A ⟹ ∀a∈A. a ≥ 0 ⟹ b ≥ 0 ⟹ 
  Sup A * (b::real) = Sup {a * b | a. a ∈ A}"
  apply(subst cSup_singleton[of b, symmetric])
  apply(subst mult_Sup_commute') by auto

lemma mult_SupL: "A ≠ {} ⟹ bdd_above A ⟹ ∀a∈A. a ≥ 0 ⟹ b ≥ 0 ⟹ 
  (b::real) * Sup A = Sup {b * a | a. a ∈ A}"
  apply(subst cSup_singleton[of b, symmetric])
  apply(subst mult_Sup_commute') by auto 

(* *)

lemma sum_mono3: 
  "finite B ⟹ A ⊆ B ⟹ (⋀b. b ∈ B - A ⟹ 0 ≤ g b) ⟹ (⋀a. a ∈ A ⟹ (f a::real) ≤ g a) ⟹ 
 sum f A ≤ sum g B"
  by (smt (verit, best) sum_mono sum_mono2)

lemma sum_Sup_commute: 
  fixes h :: "'a ⇒ real"
  assumes "finite J" and "∀i∈J. {h b | b. φ i b} ≠ {} ∧ bdd_above {h b | b. φ i b}"
  shows "sum (λi. Sup {h b | b. φ i b}) J = 
       Sup {sum (λi. h (b i)) J | b . ∀i∈J. φ i (b i)}"
  using assms proof(induction J)
  case (insert j J)

  {assume "∀i∈J. Ex (φ i) ∧ bdd_above {h b |b. φ i b}"
      and 0: "{∑i∈J. h (b2 i) |b2. ∀i∈J. φ i (b2 i)} = {}"
    hence "∀i∈J. ∃b. φ i b" by auto
    hence "∃ b2. ∀i∈J. φ i (b2 i)" 
      by (intro exI[of _ "λi. SOME b. φ i b"]) (simp add: some_eq_ex)
    hence False using 0 by blast } note 1 = this

  {assume "∀i∈J. Ex (φ i) ∧ (∃M. ∀x∈{h b |b. φ i b}. x ≤ M)"
    then obtain Ms where 0: "∀i∈J. ∀b. φ i b ⟶ h b ≤ Ms i" 
      by simp metis
    have "∃M. ∀x∈{∑i∈J. h (b2 i) |b2. ∀i∈J. φ i (b2 i)}. x ≤ M"
      apply(rule exI[of _ "sum Ms J"]) using insert 0 
      by (auto simp: sum_mono) 
  } note 2 = this

  show ?case apply(subst sum.insert)
    subgoal by fact
    subgoal by fact
    subgoal apply(subst sum.insert)
      subgoal by fact
      subgoal by fact
      subgoal apply(subst insert.IH) 
        subgoal using insert by auto
        subgoal using insert apply(subst plus_Sup_commute) 
          subgoal by auto
          subgoal by auto 
          subgoal using 1 by auto
          subgoal unfolding bdd_above_def using 2 by auto 
          subgoal apply(rule arg_cong[of _ _ Sup]) apply(rule Collect_eqI) apply safe 
            subgoal for _ b1 b2 apply(rule exI[of _ "λj'. if j'=j then b1 else b2 j'"])  
              by (smt (verit, best) insertE sum.cong) 
            subgoal by auto . . . . .
qed auto


subsection ‹Positivity, boundedness and infinite summation›

definition positive :: "('a ⇒ real) ⇒ 'a set ⇒ bool" where 
  "positive f A ≡ ∀a∈A. f a ≥ 0"

(* sum-bounded: *)
definition sbounded :: "('a ⇒ real) ⇒ 'a set ⇒ bool" where 
  "sbounded f A ≡ ∃r. ∀B. B ⊆ A ∧ finite B ⟶ sum f B ≤ r"

(* Infinite sums *)
definition isum :: "('a ⇒ real) ⇒ 'a set ⇒ real" where 
  "isum f A ≡ Sup (sum f  ` {B | B . B ⊆ A ∧ finite B})"

lemma positive_mono: "positive p A ⟹ B ⊆ A ⟹ positive p B"
  unfolding positive_def by auto

lemma positive_eq:
  assumes "positive f A" and "∀a∈A. f1 a = f a"
  shows "positive f1 A"
  using assms unfolding positive_def by auto

(* *)

lemma sbounded_eq:
  assumes "sbounded f A" and "∀a∈A. f1 a = f a"
  shows "sbounded f1 A"
  using assms unfolding sbounded_def by (simp add: subset_eq) 

lemma finite_imp_sbounded: "positive f A ⟹ finite A ⟹ sbounded f A"
  unfolding sbounded_def positive_def apply(rule exI[of _ "sum f A"]) 
  by simp (meson DiffD1 sum_mono2) 

lemma sbounded_empty[simp,intro!]: "sbounded f {}"
  unfolding sbounded_def by auto

lemma sbounded_insert[simp]: "sbounded f (insert a A) ⟷ sbounded f A"
  unfolding sbounded_def apply safe 
	subgoal by (meson subset_insertI2) 
  subgoal for r apply(rule exI[of _ "r + max 0 (f a)"]) 
  	by simp (smt finite_Diff subset_insert_iff sum.remove) .

lemma sbounded_Un[simp]: "sbounded f (A1 ∪ A2) ⟷ sbounded f A1 ∧ sbounded f A2"
  unfolding sbounded_def apply safe
  subgoal by (meson sup.coboundedI1) 
  subgoal by (meson sup.coboundedI2) 
  subgoal for r1 r2 apply(rule exI[of _ "r1+r2"]) apply safe apply(elim subset_UnE) 
  	by simp (smt Diff_subset finite_Diff order.trans sum.union_diff2 sum.union_inter) .

lemma sbounded_UNION: 
  assumes "finite I" shows "sbounded f (⋃i∈I. A i) ⟷ (∀i∈I. sbounded f (A i))" 
  using assms by (induction I) auto

lemma sbounded_mono: "A ⊆ B ⟹ sbounded f B ⟹ sbounded f A"
  unfolding sbounded_def by (meson order_trans)

lemma sbounded_reindex: "sbounded (f o u) A ⟹ sbounded f (u ` A)"
  unfolding sbounded_def apply safe subgoal for r
    apply(rule exI[of _ r]) apply safe  
    by (metis finite_image_iff subset_image_inj sum.reindex) .

lemma sbounded_reindex_inj_on: "inj_on u A ⟹ sbounded f (u ` A) ⟷ sbounded (f o u) A"
  by (smt (verit, best) comp_apply f_the_inv_into_f sbounded_eq sbounded_reindex the_inv_into_onto)

lemma sbounded_swap: 
  "sbounded (λ(a,b). f a b) (A × B) ⟷ sbounded (λ(b,a). f a b) (B × A)"
proof-
  have 0: "A × B = (λ(a,b). (b,a)) ` (B × A)" by auto
  show ?thesis unfolding 0 apply(subst sbounded_reindex_inj_on)  
    by (auto simp: o_def inj_on_def intro!: arg_cong2[of _ _ _ _ sbounded])
qed

lemma sbounded_constant_0: 
  assumes "∀a∈A. f a = (0::real)"
  shows "sbounded f A"
  using assms unfolding sbounded_def  
  by (metis in_mono order_refl sum_nonpos)

lemma sbounded_setminus: 
  assumes "sbounded f A" and "∀b∈B-A. f b = 0"
  shows "sbounded f B"
  by (metis Un_Diff_cancel2 assms sbounded_Un sbounded_constant_0)


(* isum versus sum *)
lemma isum_eq_sum:
  "positive f A ⟹ finite A ⟹ isum f A = sum f A"
  unfolding isum_def positive_def apply(subst cSup_eq_maximum[of "sum f A"]) 
  subgoal by simp   
  subgoal using sum_mono3 by fastforce  
  subgoal by simp .

(* Congruence and monotonicity *)
(* thm sum.cong *)
lemma isum_cong: 
  assumes "A = B" and "⋀x. x ∈ B ⟹ g x = h x" 
  shows "isum g A = isum h B"
  using assms unfolding isum_def 
  by (auto intro!: SUP_cong comm_monoid_add_class.sum.cong)

(* thm sum_mono *)
lemma isum_mono: 
  assumes "sbounded h A" and "⋀x. x ∈ A ⟹ g x ≤ h x" 
  shows "isum g A ≤ isum h A"
  using assms unfolding isum_def  
  apply(intro cSup_mono)
  subgoal by auto
  subgoal unfolding bdd_above_def sbounded_def by auto
  subgoal for r apply safe 
    subgoal for _ B apply(rule bexI[of _ "sum h B"]) apply (auto intro: sum_mono) . . .

lemma isum_mono': 
  assumes "sbounded g B" and "A ⊆ B" 
  shows "isum g A ≤ isum g B"
  using assms unfolding isum_def
  apply(intro cSup_subset_mono)
  unfolding bdd_above_def sbounded_def by auto

(* isum vs. 0 *)
(* thm comm_monoid_add_class.sum.empty *)
lemma isum_empty[simp]: "isum g {} = 0"
  unfolding isum_def by auto

(* thm comm_monoid_add_class.sum.neutral_const *)
lemma isum_const_zero[simp]: "isum (λx. 0) A = 0"
  unfolding isum_def 
  by simp (metis cSUP_const empty_iff empty_subsetI finite.emptyI mem_Collect_eq)

(* thm sum.neutral  *)
lemma isum_const_zero': "∀x∈A. g x = 0 ⟹ isum g A = 0"
  by (simp add: isum_cong)

(* thm sum_eq_0_iff  *)
lemma isum_eq_0_iff: "positive f A ⟹ sbounded f A ⟹ isum f A = 0 ⟷ (∀a∈A. f a = 0)"
  unfolding isum_def apply(subst Sup_eq_0_iff) 
  subgoal by auto
  subgoal unfolding bdd_above_def sbounded_def by auto   
  subgoal by (auto simp: positive_def in_mono sum_nonneg)
  subgoal by (auto simp: positive_def in_mono sum_nonneg) .

(* Reindexing: *)
(* thm sum.reindex *)
lemma isum_reindex: "inj_on h A ⟹ isum g (h ` A) = isum (g ∘ h) A"
  unfolding isum_def apply(rule arg_cong[of _ _ Sup]) 
  unfolding image_def[of "sum g"] image_def[of "sum (g ∘ h)"] 
  apply(rule Collect_eqI) 
  by (smt (verit, del_insts) finite_image_iff inj_on_subset mem_Collect_eq subset_image_inj sum.reindex)

(* thm sum.reindex_cong *)
lemma isum_reindex_cong: "inj_on l B ⟹ A = l ` B ⟹ 
 (⋀x. x ∈ B ⟹ g (l x) = h x) ⟹ isum g A = isum h B"
  by (metis isum_cong comp_def isum_reindex)

(* thm sum.reindex_nontrivial *)
lemma isum_reindex_cong': 
  "(⋀x y. x ∈ A ⟹ y ∈ A ⟹ x ≠ y ⟹ h x = h y ⟹ g (h x) = 0) ⟹ isum g (h ` A) = isum (g ∘ h) A"
  unfolding isum_def apply(rule arg_cong[of _ _ Sup]) 
  unfolding image_def[of "sum g"] image_def[of "sum (g ∘ h)"] apply(rule Collect_eqI)
  apply safe  
  subgoal by(metis (no_types, lifting) finite_image_iff mem_Collect_eq subset_image_inj sum.reindex)
  subgoal by (smt finite_imageI image_mono in_mono mem_Collect_eq sum.reindex_nontrivial) .

(* thm sum.mono_neutral_cong *)
lemma isum_zeros_cong:
  assumes "sbounded g (S ∩ T) ∨ sbounded h (S ∩ T)"
    and "(⋀i. i ∈ T - S ⟹ h i = 0)" and "(⋀i. i ∈ S - T ⟹ g i = 0)"
    and "(⋀x. x ∈ S ∩ T ⟹ g x = h x)"
  shows "isum g S = isum h T"
proof-
  have 0: "sbounded g S ∨ sbounded h T" using assms  
    by (metis Diff_Int2 Int_absorb Int_commute sbounded_setminus)
  show ?thesis unfolding isum_def apply(rule Sup_image_cong)
    subgoal by auto
    subgoal apply safe
      subgoal for _ B
        apply(rule bexI[of _ "B ∩ T"], rule order_eq_refl)
         apply(rule sum.mono_neutral_cong) using assms by auto .
    subgoal apply safe
      subgoal for _ B
        apply(rule bexI[of _ "B ∩ S"], rule order_eq_refl)
         apply(rule sum.mono_neutral_cong) using assms by auto .
    subgoal using assms(2,3,4) 0 unfolding bdd_above_def sbounded_def apply (elim disjE exE)
      subgoal for r apply(rule disjI1) apply(rule exI[of _ r]) by auto
      subgoal for r apply(rule disjI2) apply(rule exI[of _ r]) by auto . .
qed

(* thm sum.mono_neutral_left *)
lemma isum_zeros_congL: 
  "sbounded g S ⟹ S ⊆ T ⟹ ∀i∈T - S. g i = 0 ⟹ isum g S = isum g T"
  by (metis Diff_eq_empty_iff emptyE isum_zeros_cong le_iff_inf)

(* thm sum.mono_neutral_right *)
lemma isum_zeros_congR:
  "sbounded g S ⟹ S ⊆ T ⟹ ∀i∈T - S. g i = 0 ⟹ isum g T = isum g S"
  by (simp add: isum_zeros_congL)

lemma isum_singl[simp]: "f a ≥ (0::real) ⟹ isum f {a} = f a"  
  by (simp add: positive_def isum_eq_sum)

lemma isum_two[simp]: "a1 ≠ a2 ⟹ f a1 ≥ (0::real) ⟹ f a2 ≥ 0 ⟹ isum f {a1,a2} = f a1 + f a2"  
  by (simp add: positive_def isum_eq_sum)

lemma isum_three[simp]: "a1 ≠ a2 ⟹ a1 ≠ a3 ⟹ a2 ≠ a3 ⟹ f a1 ≥ 0 ⟹ f a2 ≥ (0::real) ⟹ f a3 ≥ 0 ⟹ 
 isum f {a1,a2,a3} = f a1 + f a2 + f a3"  
  by (simp add: positive_def isum_eq_sum)

lemma isum_ge_0: "positive f A ⟹ sbounded f A ⟹ isum f A ≥ 0"
  using isum_mono' by fastforce

lemma in_le_isum: "positive f A ⟹ sbounded f A ⟹ a ∈ A ⟹ f a ≤ isum f A"
  by (metis (full_types) DiffE positive_def Set.set_insert equals0I 
      insert_mono isum_mono' isum_singl subsetI)

lemma isum_eq_singl: 
  assumes fx: "f a = x" and f: "∀a'. a' ≠ a ⟶ f a' = 0" and x: "x ≥ 0" and a: "a ∈ A"
  shows "isum f A = x"
  apply(subst fx[symmetric])
  apply(subst isum_singl[of f a, symmetric])
  subgoal using assms by simp
  subgoal apply(rule isum_zeros_cong) using assms by auto .

lemma isum_le_singl: 
  assumes fx: "f a ≤ x" and f: "∀a'. a' ≠ a ⟶ f a' = 0" and x: "f a ≥ 0" and a: "a ∈ A"
  shows "isum f A ≤ x"
  by (metis a f fx isum_eq_singl x)

lemma isum_insert[simp]: "a ∉ A ⟹ sbounded f A ⟹ f a ≥ 0 ⟹ isum f (insert a A) = isum f A + f a"
  unfolding isum_def apply(subst plus_SupR)
  subgoal by auto
  subgoal unfolding sbounded_def bdd_above_def by auto
  subgoal apply(rule Sup_cong) 
    subgoal by auto
    subgoal apply safe subgoal for _ _ B   
      apply(rule bexI[of _ "sum f (B - {a}) + f a"]) 
      subgoal by (cases "a ∈ B") (auto simp: image_def sum.remove) 
      subgoal by blast . . 
  subgoal apply safe subgoal for _ _ _ B 
    apply(rule bexI[of _ "sum f (insert a B)"]) 
    subgoal by (cases "a ∈ B") (auto simp: image_def sum.remove) 
    subgoal by blast . .
  subgoal unfolding sbounded_def bdd_above_def apply (elim exE)
    subgoal for r apply(rule disjI2, rule exI[of _ "r + f a"]) by auto . . .

(* thm sum.UNION_disjoint *)
lemma isum_UNION: 
  assumes dsj: "∀i∈I. ∀j∈I. i ≠ j ⟶ A i ∩ A j = {}" and sb: "sbounded g (⋃ (A ` I))" 
  shows "isum g (⋃ (A ` I)) = isum (λi. isum g (A i)) I"
proof-
  {fix J assume J: "J ⊆ I" "finite J"
    have "sum (λi. Sup {sum g B | B. B ⊆ A i ∧ finite B}) J = 
       Sup {sum (λi. sum g (B i)) J | B . ∀i∈J. B i ⊆ A i ∧ finite (B i)}"
      using J sb apply(subst sum_Sup_commute)
      subgoal by auto
      subgoal unfolding sbounded_def bdd_above_def  
        by simp (metis SUP_upper2 bot.extremum finite.emptyI in_mono)
      subgoal by auto .
    also have "… = 
       Sup {sum g (⋃ (B ` J)) | B . ∀i∈J. B i ⊆ A i ∧ finite (B i)}"
      apply(rule arg_cong[of _ _ Sup]) apply(rule Collect_eqI) apply(rule ex_cong1) 
      apply safe
      subgoal 
        apply(rule sum.UNION_disjoint[symmetric])
        using J dsj by auto (metis IntI empty_iff subsetD)
      subgoal 
        apply(rule sum.UNION_disjoint)
        using J dsj by auto (metis IntI empty_iff subsetD) .
    also have "… =  
       Sup {sum g B | B . B ⊆ ⋃ (A ` J) ∧ finite B}"  
      apply(rule Sup_cong) apply safe
      subgoal by auto
      subgoal for _ B
        apply(rule bexI[of _ "sum g (⋃ (B ` J))"]) using J by auto
      subgoal for _ B
        apply(rule bexI[of _ "sum g (⋃ ((λi. B ∩ A i) ` J))"])
        subgoal using J unfolding incl_UNION_aux2 by auto
        subgoal by blast .
      subgoal using J sb unfolding bdd_above_def sbounded_def  
      	by simp (metis UN_mono finite_UN_I) .
    also have "… ≤ 
       Sup {sum g B | B . B ⊆ ⋃ (A ` I) ∧ finite B}" 
      apply(rule cSup_subset_mono) apply safe
      subgoal by auto
      subgoal using J sb unfolding sbounded_def bdd_above_def by auto
      subgoal for _ B apply(rule exI[of _ B]) using J by auto . 
    finally 
    have "(∑i∈J. Sup {y. ∃B⊆A i. finite B ∧ y = sum g B}) ≤ 
           Sup {y. ∃B⊆⋃ (A ` I). finite B ∧ y = sum g B}" 
      by (smt Collect_cong sum_mono)
  } note 1 = this

  show ?thesis
    unfolding isum_def apply(rule Sup_image_congL)  
    unfolding image_def[of "sum g"] image_def[of "sum (λi. Sup {y. ∃x∈{B |B. B ⊆ A i ∧ finite B}. y = sum g x})"] 
      apply safe
    subgoal by auto
    subgoal for _ B using assms  
      apply(intro bexI[of _ "{i. i ∈ I ∧ B ∩ A i ≠ {}}"])
      subgoal apply(subst incl_UNION_aux[of B A I], assumption)
        apply(subst comm_monoid_add_class.sum.UNION_disjoint)
        subgoal by (simp add: disjoint_finite_aux)
        subgoal by auto
        subgoal by auto
        subgoal apply(rule sum_mono) 
          subgoal for i apply(rule cSup_upper) 
            subgoal by auto
            subgoal unfolding bdd_above_def sbounded_def by simp (metis UN_I in_mono subsetI) . . . 
      subgoal by (simp add: disjoint_finite_aux) . 
    subgoal using 1 by auto . 
qed

lemma isum_Un[simp]: 
  assumes "positive f A1" "sbounded f A1" "positive f A2" "sbounded f A2" "A1 ∩ A2 = {}"
  shows "isum f (A1 ∪ A2) = isum f A1 + isum f A2"
proof-
  have [simp]: "isum (λi. isum f (case i of 0 ⇒ A1 | Suc _ ⇒ A2)) {0, Suc 0} = isum f A1 + isum f A2"
    apply(subst isum_two) using assms by (auto intro!: isum_ge_0)
  show ?thesis using assms isum_UNION[of "{0,1::nat}" "λi. case i of 0 ⇒ A1 |_ ⇒ A2" f] by auto
qed

(* thm sum.Sigma *)
lemma isum_Sigma: 
  assumes sbd: "sbounded (λ(a,b). f a b) (Sigma A Bs)"
  shows "isum (λ(a,b). f a b) (Sigma A Bs) = isum (λa. isum (f a) (Bs a)) A"
proof-
  define g where "g ≡ λ(a,b). f a b"
  define Cs where "Cs ≡ λa. {a} × Bs a"
  have 1: "⋀a. {a} × Bs a = Pair a ` (Bs a)" by auto
  have 0: "Sigma A Bs = (⋃a∈A. Cs a)" unfolding Cs_def by auto
  show ?thesis unfolding 0 apply(subst isum_UNION)
    subgoal unfolding Cs_def by auto
    subgoal using sbd unfolding 0 .
    subgoal unfolding Cs_def apply(rule arg_cong2[of _ _ _ _ isum]) 
      subgoal unfolding 1  
        apply(subst isum_reindex_cong') by (auto simp: o_def) 
      subgoal .. . .
qed  

(* Redundant but visually useful: *)
(* thm sum.cartesian_product *)
lemma isum_Times: 
  assumes "sbounded (λ(a,b). f a b) (A × B)"
  shows "isum (λ(a,b). f a b) (A × B) = isum (λa. isum (f a) B) A"
  using isum_Sigma[OF assms] .

(* thm sum.swap *)
lemma isum_swap: 
  assumes "sbounded (λ(a,b). f a b) (A × B)"
  shows "isum (λa. isum (f a) B) A = isum (λb. isum (λa. f a b) A) B" (is "?L = ?R")
proof-
  have 0: "A × B = (λ(a,b). (b,a)) ` (B × A)" by auto
  have "?L = isum (λ(a,b). f a b) (A × B)" using isum_Times[OF assms] ..
  also have "… = isum (λ(b,a). f a b) (B × A)" unfolding 0 apply(subst isum_reindex_cong') 
    by (auto simp: o_def intro!: arg_cong2[of _ _ _ _ isum])
  also have "… = ?R" apply(subst isum_Times) using assms sbounded_swap by auto
  finally show ?thesis .
qed

lemma isum_plus:
  assumes f1: "positive f1 A" "sbounded f1 A"
    and f2: "positive f2 A" "sbounded f2 A"
  shows "isum (λa. f1 a + f2 a) A = isum f1 A + isum f2 A"
  unfolding isum_def apply(subst plus_Sup_commute')
  subgoal by auto
  subgoal using f1 unfolding sbounded_def bdd_above_def by auto
  subgoal by auto
  subgoal using f2 unfolding sbounded_def bdd_above_def by auto
  subgoal apply(rule Sup_cong)
    subgoal by auto
    subgoal apply safe 
      subgoal for _ _ B
        apply(rule bexI[of _ "∑a∈B. f1 a + f2 a"]) 
        subgoal by auto
        subgoal apply clarify apply(rule exI[of _ "sum f1 B"]) apply(rule exI[of _ "sum f2 B"])
          using sum.distrib by auto . .
    subgoal apply safe
      subgoal for _ _ _ _ _ B1 B2
        apply(rule bexI[of _ "∑a∈B1 ∪ B2. f1 a + f2 a"])
        subgoal apply(subst sum.distrib) apply(rule add_mono)
          subgoal apply(rule sum_mono2) using f1 unfolding positive_def by auto   
          subgoal apply(rule sum_mono2) using f2 unfolding positive_def by auto .
        subgoal by auto . . 
    subgoal apply(rule disjI2)
      using f1 f2 unfolding sbounded_def bdd_above_def apply (elim exE)
      subgoal for r1 r2 apply(rule exI[of _ "r1 + r2"]) apply safe
        by (auto simp: add_mono) . . .


(* Distributivity w.r.t. multiplication *) 

lemma sbounded_product:
  assumes f: "positive f A" "sbounded f A" and g: "positive g B" "sbounded g B"
  shows "sbounded (λ(a,b). f a * g b) (A × B)"
  using assms unfolding sbounded_def positive_def apply safe
  subgoal for r1 r2
    apply(rule exI[of _ "r1*r2"]) apply safe subgoal for Ba 
      apply(rule order.trans[OF sum_mono2[of "fst`Ba × snd`Ba" Ba "λ(a,b). f a * g b"]])
      subgoal by auto
      subgoal  by (simp add: subset_fst_snd)
      subgoal for ab apply(cases ab, simp) 
        by (metis (no_types, lifting) imageE mem_Sigma_iff mult_nonneg_nonneg prod.collapse subset_eq)
      subgoal apply(subst sum.cartesian_product[symmetric]) 
        apply(subst sum_product[symmetric])  
        by (smt finite_imageI imageE mem_Sigma_iff mult_mono prod.collapse subset_eq sum_nonneg) . . .

lemma sbounded_multL: "x ≥ 0 ⟹ sbounded f A ⟹ sbounded (λa. x * f a) A"
  unfolding sbounded_def apply safe 
  subgoal for r apply(rule exI[of _ "x * r"])
    by (metis mult.commute mult_right_mono sum_distrib_left) .

lemma sbounded_multL_strict[simp]: 
  assumes x: "x > 0"
  shows "sbounded (λa. x * f a) A ⟷ sbounded f A"
proof-
  have 0: "f = (λa. (1 / x) * (x * f a))" unfolding fun_eq_iff using x by auto
  show ?thesis apply safe
    subgoal apply(subst 0) apply(rule sbounded_multL) using x by auto
    subgoal apply(rule sbounded_multL) using x by auto . 
qed

lemma sbounded_multR: "x ≥ 0 ⟹ sbounded f A ⟹ sbounded (λa. f a * x) A"
  unfolding sbounded_def apply safe 
  subgoal for r apply(rule exI[of _ "r * x"])
    by (metis mult.commute mult_left_mono sum_distrib_right) .

lemma sbounded_multR_strict[simp]: 
  assumes x: "x > 0"
  shows "sbounded (λa. f a * x) A ⟷ sbounded f A"
proof-
  have 0: "f = (λa. (f a * x) * (1 / x))" unfolding fun_eq_iff using x by auto
  show ?thesis apply safe
    subgoal apply(subst 0) apply(rule sbounded_multR) using x by auto
    subgoal apply(rule sbounded_multR) using x by auto . 
qed

lemma positive_sbounded_multL: 
  assumes f: "positive f A" "sbounded f A" and g: "∀a∈A. g a ≤ x" 
  shows "sbounded (λa. f a * g a) A"
proof-
  define y where "y ≡ max x 0"
  have g: "∀a∈A. g a ≤ y ∧ y ≥ 0" using g unfolding y_def by auto
  show ?thesis using assms unfolding sbounded_def apply safe
    subgoal for r  apply(intro exI[of _ "r * y"]) apply safe
      subgoal for B 
        apply(rule order.trans[OF sum_mono[of B "λa. f a * g a" "λa. f a * y"]])
        subgoal unfolding positive_def  
          by (simp add: g in_mono mult_left_mono)
        subgoal apply(subst sum_distrib_right[symmetric]) 
          by (metis max.cobounded2 mult.commute mult_left_mono y_def) . . . 
qed

lemma positive_sbounded_multR: 
  assumes f: "positive f A" "sbounded f A" and g: "∀a∈A. g a ≤ x" 
  shows "sbounded (λa. g a * f a) A"
  using positive_sbounded_multL[OF assms]
  unfolding sbounded_def apply safe 
  subgoal for r apply(rule exI[of _ r]) apply safe 
    subgoal for B
      apply(subst sum.cong[of B B _ "λa. f a * g a"]) by auto . .

(* *)
lemma isum_product_Times:
  assumes f: "positive f A" "sbounded f A" and g: "positive g B" "sbounded g B"
  shows "isum f A * isum g B = isum (λ(a,b). f a * g b) (A × B)"
  unfolding isum_def apply(subst mult_Sup_commute')
  subgoal by auto
  subgoal using f(2) unfolding bdd_above_def sbounded_def by auto
  subgoal using f by (auto simp: positive_def subsetD sum_nonneg)
  subgoal by auto
  subgoal using g(2) unfolding bdd_above_def sbounded_def by auto
  subgoal using g by (auto simp: positive_def subsetD sum_nonneg)
  subgoal apply(rule Sup_cong)  
    subgoal by auto
    subgoal using f(2) g(2) unfolding sbounded_def apply safe
      subgoal for a r1 r2 a1 a2 x xa A1 B1
        apply(rule bexI[of _ "sum (λ(a, b). f a * g b) (A1 × B1)"])
        subgoal apply(subst sum_product) 
          apply(subst sum.cartesian_product) 
          apply(subst sum_mono2) by auto 
        subgoal by (simp add: image_def) (metis Sigma_mono finite_SigmaI) . .
    subgoal using f(2) g(2) unfolding sbounded_def apply safe
      subgoal for b x r ra AB1
        apply(rule bexI[of _ "sum f (fst ` AB1) * sum g (snd ` AB1)"])
        subgoal apply(subst sum_product) 
          apply(subst sum.cartesian_product) 
          apply(subst sum_mono2) 
          subgoal by (simp_all add: subset_fst_snd)
          subgoal by (simp_all add: subset_fst_snd)
          subgoal for ab using f(1) g(1) unfolding positive_def apply(cases ab)
            by simp (metis (no_types, lifting) imageE mem_Sigma_iff mult_nonneg_nonneg prod.collapse subsetD)
          subgoal .. . 
        subgoal apply (simp add: image_def)  
          apply(rule exI[of _ "sum f (fst ` AB1)"], rule exI[of _ "sum g (snd ` AB1)"])
          apply (simp add: image_def) apply safe 
          subgoal apply(rule exI[of _ "fst ` AB1"]) by (fastforce simp: image_def) 
          subgoal apply(rule exI[of _ "snd ` AB1"]) by (fastforce simp: image_def) . . . 
    subgoal apply(rule disjI1) using sbounded_product[OF assms]
      unfolding sbounded_def bdd_above_def image_def apply safe
      subgoal for r apply(rule exI[of _ r]) 
        by simp (metis (no_types) Sigma_mono finite_cartesian_product sum.cartesian_product sum_product) 
      . . .

(* thm sum_product *)
lemma isum_product:
  assumes f: "positive f A" "sbounded f A" and g: "positive g B" "sbounded g B"
  shows "isum f A * isum g B = isum (λa. isum (λb. f a * g b) B) A"
  by (simp add: assms isum_Times isum_product_Times sbounded_product)

(* thm sum_distrib_right *)
lemma isum_distribR: 
  assumes f: "positive f (A::'a set)" "sbounded f A" and r: "r ≥ 0"
  shows "isum f A * r = isum (λa. f a * r) A"
proof-
  have 0: "A × {0} = (λa. (a, 0::nat)) ` A" by auto 
  show ?thesis
    apply(subst isum_singl[of "λ_. r" "0::nat",symmetric, OF r])
    apply(subst isum_product_Times)
    subgoal by fact
    subgoal by fact
    subgoal using r unfolding positive_def by auto
    subgoal by simp
    subgoal apply (subst 0) apply(subst isum_reindex) unfolding inj_on_def o_def by auto .
qed

(* thm sum_distrib_left *)
lemma isum_distribL: 
  assumes f: "positive f (A::'a set)" "sbounded f A" and r: "r ≥ 0"
  shows "r * isum f A = isum (λa. r * f a) A"
proof-
  have 0: "r * isum f A = isum f A * r"
    "(λa. r * f a) = (λa. f a * r)" unfolding fun_eq_iff by auto
  show ?thesis unfolding 0 using isum_distribR[OF assms] .
qed


end