Stream: Beginner Questions

Topic: I don't know how to prove this simple lemma.

view this post on Zulip chem snu (Jun 23 2025 at 07:58):

lemma my_lemma:
  fixes f :: "nat ⇒ ennreal"
    and g :: "nat ⇒ nat set"
  assumes "disjoint_family g"
  shows "(∑k∈(⋃i. g i). f k) = (∑i. ∑k∈g i. f k)"

It's obvious intuitively, but I don't know how to formally prove it. Sledgehammer doesn't help. ChatGPT doesn't help too.

Please somebody give me some hint!

Thanks.

view this post on Zulip Christian Pardillo Laursen (Jun 23 2025 at 09:58):

I think the issue here is that this theorem doesn't hold. Summing over sets (term sum), as you're doing on the left side, only works for finite sets. On the right side, you have a series (term suminf), which admits infinite series but needs convergence proofs.

If you add assumption finite (⋃i. g i) it should be possible to prove this, but if you need an infinite g then you'll have to rephrase the conclusion

view this post on Zulip chem snu (Jun 23 2025 at 10:46):

Thank you for very helpful advice!!
I didn't know that LHS only works for finite sets.
Then the question is, what's the best way to rephrase LHS for infinite g??
I have some idea, but it's too verbose..

view this post on Zulip chem snu (Jun 23 2025 at 11:05):

I rephrased it:

lemma my_lemma:
  fixes f :: "nat ⇒ ennreal"
    and g :: "nat ⇒ nat set"
    and h :: "nat ⇒ nat"
  assumes "disjoint_family g"
    and "inj_on h UNIV"
    and "range h = (⋃i. g i)"
  shows "(∑k. f (h k)) = (∑i. ∑k∈g i. f k)"

I still don't know how to prove it. :smiling_face_with_tear:

view this post on Zulip chem snu (Jun 23 2025 at 11:12):

Ah, I need to also change inner summation of RHS....
It's hard to make a correct statement...

view this post on Zulip chem snu (Jun 23 2025 at 15:53):

Now I know there is ∑⇩∞ notation for infinite sum, so my lemma becomes

lemma my_lemma:
  fixes f :: "nat ⇒ ennreal"
    and g :: "nat ⇒ nat set"
  assumes "disjoint_family g"
  shows "(∑⇩∞k∈(⋃i. g i). f k) = (∑i. ∑⇩∞k∈g i. f k)"

view this post on Zulip Manuel Eberl (Jun 24 2025 at 13:40):

That doesn't really work either because infinite sums do not always exist. You will need summability as an additional assumption. Nested infinite sums are painful.

view this post on Zulip Manuel Eberl (Jun 24 2025 at 14:01):

All you need for this is there in the library. In the library, the theorems in question all use Sigma A B, which just means {(x,y)∣x∈A,y∈B(x)}\{(x,y) \mid x\in A, y \in B(x)\} (the dependent sum operator).

view this post on Zulip Manuel Eberl (Jun 24 2025 at 14:02):

You can derive theorems similar to what you want from the versions for Sigma, e.g. like this:

lemma has_sum_UN_D:
  fixes f :: "'b ⇒ 'a :: {topological_comm_monoid_add,t3_space}"
  assumes disj: "disjoint_family_on B A"
  assumes g: "⋀x. x ∈ A ⟹ (f has_sum g x) (B x)"
  assumes "(f has_sum S) (⋃x∈A. B x)"
  shows   "(g has_sum S) A"
proof -
  have "(⋃x∈A. B x) = snd ` (SIGMA x:A. B x)"
    by force
  hence bij: "bij_betw snd (SIGMA x:A. B x) (⋃x∈A. B x)"
    using disj unfolding bij_betw_def
    by (auto simp: inj_on_def disjoint_family_on_def)

  have "(f has_sum S) (⋃x∈A. B x)"
    by fact
  also have "?this ⟷ ((λ(x,y). f y) has_sum S) (SIGMA x:A. B x)"
    using has_sum_reindex_bij_betw[OF bij, of f S]
    by (simp add: case_prod_unfold)
  finally have *: "((λ(x,y). f y) has_sum S) (SIGMA x:A. B x)" .

  thus "(g has_sum S) A"
    using g has_sum_SigmaD[OF *, of g] by simp
qed

lemma infsum_UN:
  fixes f :: "'b ⇒ 'a ::
    {topological_comm_monoid_add,t3_space,uniform_topological_group_add, ab_group_add,
     complete_uniform_space}"
  assumes disj: "disjoint_family_on B A"
  assumes summable: "f summable_on (⋃x∈A. B x)"
  defines "S ≡ (∑⇩∞y∈(⋃x∈A. B x). f y)"
  shows   "((λx. ∑⇩∞y∈B x. f y) has_sum S) A"
proof -
  have *: "(f has_sum (∑⇩∞y∈B x. f y)) (B x)" if x: "x ∈ A" for x
  proof -
    have "f summable_on (B x)"
      using summable by (rule summable_on_subset) (use x in auto)
    thus ?thesis
      by (simp add: summable_iff_has_sum_infsum)
  qed

  have **: "(f has_sum S) (⋃x∈A. B x)"
    using summable by (simp add: S_def summable_iff_has_sum_infsum)
  show ?thesis
    using disj * ** by (rule has_sum_UN_D)
qed

view this post on Zulip Manuel Eberl (Jun 24 2025 at 14:02):

You will however have to establish summability, otherwise none of this is going to work. Whenever you have infinite sums, summability becomes a side condition to everything. And for nested sums it's especially tricky.

view this post on Zulip Manuel Eberl (Jun 24 2025 at 14:03):

Feel free to ask me if you need more guidance here. I co-wrote the library for indexed infinite sums in HOL-Analysis.

view this post on Zulip chem snu (Jun 26 2025 at 04:15):

@Manuel Eberl Thank you very much! Using your lemma has_sum_UN_D, I almost completed my goal:

instantiation ennreal :: t3_space
begin

instance sorry

end

lemma my_lemma:
  fixes f :: "'a ⇒ ennreal"
    and g :: "nat ⇒ 'a set"
  assumes "disjoint_family g"
  shows "(∑⇩∞k∈(⋃i. g i). f k) = (∑⇩∞i∈UNIV. ∑⇩∞k∈g i. f k)"
proof -
  have *: "⋀x. (f has_sum infsum f (g x)) (g x)" by (simp add: nonneg_summable_on_complete)
  have "(f has_sum infsum f (⋃ (range g))) (⋃ (range g))"
    by (simp add: nonneg_summable_on_complete)
  hence "((λx. infsum f (g x)) has_sum infsum f (⋃ (range g))) UNIV"
    by (meson "*" assms has_sum_UN_D)
  thus ?thesis by (metis infsumI)
qed

As you can see, I skipped the proof that ennreal is a t3_space, but I think I can do this myself.

view this post on Zulip Manuel Eberl (Jun 27 2025 at 09:24):

I just saw that you use ennreal. That indeed makes the summability assumptions go away, since everything is summable in ennreal.

Everything becomes a lot easier in ennreal, since infinite sums can be expressed as suprema.

Last updated: Jun 30 2025 at 20:23 UTC