## Stream: Is there code for X?

### Topic: interchange sum

#### Kevin Buzzard (Dec 11 2020 at 10:02):

$\sum_{0\leq i\leq j\leq n}F(i,j)$ can be written as $\sum_{i=0}^n\sum_{j=i}^nF(i,j)$ and also as $\sum_{j=0}^n\sum_{i=0}^jF(i,j)$. Do we have the equality of these last two sums in Lean? I looked in algebra/big_operators/intervals but couldn't find any double sum lemmas in there.

#### Mario Carneiro (Dec 11 2020 at 10:03):

There should be a general purpose 2D summation lemma

#### Mario Carneiro (Dec 11 2020 at 10:04):

(but I agree this particular diagonal interchange lemma should be in there)

#### Kevin Buzzard (Dec 11 2020 at 10:04):

how do I search mathlib for it? library_search just took my machine down for some reason

#### Mario Carneiro (Dec 11 2020 at 10:05):

I'm just perusing big_ops.basic

#### Mario Carneiro (Dec 11 2020 at 10:06):

docs#finset.prod_sigma

hells bells

#### Kevin Buzzard (Dec 11 2020 at 10:17):

This just says that if X bijects with Y then some sum over X equals some sum over Y, and that a sum over a sigma type is what it obviously is. I can quite believe that I can put these together to make a proof! But my explicit lemma comes up a lot in basic undergraduate maths so I was hoping they'd be there already as a sum over Ico. I can make them, I just didn't want to waste my time if they were there already :-)

#### Eric Wieser (Dec 11 2020 at 10:21):

Is there someway to tidy up the statement of prod_bij to use function.bijective or docs#set.bij_on?

#### Mario Carneiro (Dec 11 2020 at 10:38):

@Kevin Buzzard You are right, this is certainly a hole in the library. I would start by copying all the lemmas around us.metamath.org/mpeuni/mmtheorems138.html#fsum0diag, which contains this diagonal lemma as well as a few additional useful variations

#### Kevin Buzzard (Dec 11 2020 at 10:39):

I've managed to write the first line using the sum_sigma approach and it wasn't much fun:

lemma dependent_double_sum {M : Type*} [add_comm_monoid M]
(a b : ℕ) (f : ℕ → ℕ → M) :
∑ i in Ico a b, ∑ j in Ico i b, f i j =
∑ j in Ico a b, ∑ i in Ico a (j+1), f i j :=
begin
rw ← @sum_sigma ℕ M _ (λ _, ℕ) (Ico a b) (λ i, Ico i b) (λ x, f x.1 x.2),
sorry
end


#### Kevin Buzzard (Dec 11 2020 at 10:42):

@Eric Wieser which function is bijective though? In my example, the function is probably not bijective on all of $\mathbb{N}^2$, it's only bijective on the finite sets in question. So you can use function.bijective but then you'll have to promote the sets to types and this adds an extra layer of confusion.

#### Eric Wieser (Dec 11 2020 at 10:45):

Right, you'd end up having to coerce sets to types; or use bij_on which takes the sets as arguments

#### Mario Carneiro (Dec 11 2020 at 10:56):

import tactic.linarith
import algebra.big_operators.intervals

open_locale big_operators nat

namespace finset

lemma dependent_double_sum {M : Type*} [add_comm_monoid M]
(a b : ℕ) (f : ℕ → ℕ → M) :
∑ i in Ico a b, ∑ j in Ico i b, f i j =
∑ j in Ico a b, ∑ i in Ico a (j+1), f i j :=
begin
rw ← @@sum_sigma _ _ (λ i, Ico i b) (λ x, f x.1 x.2),
rw ← @@sum_sigma _ _ (λ j, Ico a (j+1)) (λ x, f x.2 x.1),
refine sum_bij'
(λ (x : Σ (i : ℕ), ℕ) _, (⟨x.2, x.1⟩ : Σ (i : ℕ), ℕ)) _ (λ _ _, rfl)
(λ (x : Σ (i : ℕ), ℕ) _, (⟨x.2, x.1⟩ : Σ (i : ℕ), ℕ)) _
(by rintro ⟨⟩ _; refl) (by rintro ⟨⟩ _; refl);
simp only [Ico.mem, sigma.forall, mem_sigma];
rintros a b ⟨⟨h₁,h₂⟩, ⟨h₃, h₄⟩⟩; refine ⟨⟨_, _⟩, ⟨_, _⟩⟩; linarith
end

end finset


#### Eric Wieser (Dec 11 2020 at 10:57):

Double @!?

#### Mario Carneiro (Dec 11 2020 at 10:57):

The statement of prod_bij is designed specifically to give you the goals in the form you actually want to prove them, rather than wrapped in another layer of abstraction

(deleted)

#### Eric Wieser (Dec 11 2020 at 11:16):

Created #5318 to make the hypotheses to prod_bij-adjacent lemmas slightly easier to parse, without changing their statement

#### Kevin Buzzard (Dec 11 2020 at 11:32):

@Ashvni Narayanan there's what you needed :D

#### Ashvni Narayanan (Dec 11 2020 at 11:35):

Yayy!! Thank you!

#### Eric Wieser (Dec 11 2020 at 11:50):

@Mario Carneiro, does that mean that in your opinion this statement is worse?

@[to_additive]
lemma prod_bij_subtype  {s : finset α} {t : finset γ} {f : α → β} {g : γ → β}
(i : (s : set α) → (t : set γ)) (h : ∀ a, f ↑a = g (i a)) (i_bij : function.bijective i) :
(∏ x in s, f x) = (∏ x in t, g x) :=
prod_bij (λ a ha, i ⟨a, ha⟩) (λ a ha, (i ⟨a, ha⟩).prop) (λ a ha, h ⟨a, ha⟩)
(λ a₁ a₂ ha₁ ha₂ h, subtype.ext_iff.mp (i_bij.1 (subtype.ext h)))
(λ b hb, let ⟨a, ha⟩ := i_bij.2 ⟨b, hb⟩ in ⟨a, a.prop, begin
convert subtype.ext_iff.mp ha.symm,
exact subtype.ext rfl,
end⟩)


#### Mario Carneiro (Dec 11 2020 at 11:50):

have you tried using it?

#### Eric Wieser (Dec 11 2020 at 11:51):

Not yet, but my use-case is only when s and t are set.univ anyway

#### Mario Carneiro (Dec 11 2020 at 11:51):

okay, so you have a function from univ -> univ then?

#### Mario Carneiro (Dec 11 2020 at 11:51):

that seems awkward compared to a function alpha -> gamma

#### Eric Wieser (Dec 11 2020 at 11:52):

My thinking was that there are various bits of API to produce bijective objects

#### Mario Carneiro (Dec 11 2020 at 11:52):

plus you need a proof that it's bijective, probably the off the shelf theorem is going to give you that the alpha -> gamma function is bijective

#### Eric Wieser (Dec 11 2020 at 11:53):

You're right that univ is a bad example

#### Eric Wieser (Dec 11 2020 at 11:53):

@[to_additive]
lemma prod_bij_univ [fintype α] [fintype γ] {f : α → β} {g : γ → β}
(i : α → γ) (h : ∀ a, f a = g (i a)) (i_bij : function.bijective i) :
(∏ x, f x) = (∏ x, g x) :=
prod_bij (λ a ha, i a) (λ a ha, mem_univ _) (λ a ha, h a) (λ a₁ a₂ ha₁ ha₂ h, i_bij.1 h)
(λ b hb, let ⟨a, ha⟩ := i_bij.2 b in ⟨a, mem_univ _, ha.symm⟩)


is the API that's convenient for univ

#### Mario Carneiro (Dec 11 2020 at 11:53):

For the particular case of univ, I would expect a specialization of the prod_bij theorem for univ

...like that

#### Eric Wieser (Dec 11 2020 at 11:53):

Should I PR the above?

#### Mario Carneiro (Dec 11 2020 at 11:54):

I mean there isn't any harm in having it, I am just doubtful that it is better

#### Anne Baanen (Dec 11 2020 at 11:54):

Perhaps bundling function.bijective i into i : equiv α γ?

#### Mario Carneiro (Dec 11 2020 at 11:54):

perhaps in some situations it's easier to use equiv theorems to prove facts about bundled finset functions, I don't know

#### Eric Wieser (Dec 11 2020 at 11:55):

Well, there's always docs#equiv.bijective if you want to work with equivs

#### Eric Wieser (Dec 11 2020 at 11:55):

I don't know whether there's a conversion in the other direction, but it would require choice

#### Mario Carneiro (Dec 11 2020 at 11:55):

the existing lemma has the drawback that the bijection property is splatted out so it's best for things like reindexing where you don't have anything packed up but you do have theorems a + b - b = a and such

#### Eric Wieser (Dec 11 2020 at 12:05):

Having just tried to express the _univ version in terms of the _subtype version - I think the missing piece is a helper to construct the bijective object on the function over the subtype (ie, to splat it out)

Last updated: May 19 2021 at 02:10 UTC