interchange sum

Stream: Is there code for X?

[Kevin Buzzard]

$\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]

There should be a general purpose 2D summation lemma

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

I'm just perusing big_ops.basic

[Mario Carneiro]

docs#finset.prod_sigma

[Mario Carneiro]

and docs#finset.prod_bij'

[Kevin Buzzard]

hells bells

[Kevin Buzzard]

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]

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

[Mario Carneiro]

@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]

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]

@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]

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

[Mario Carneiro]

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]

Double @!?

[Mario Carneiro]

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

[Eric Wieser]

(deleted)

[Eric Wieser]

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

[Kevin Buzzard]

@Ashvni Narayanan there's what you needed :D

[Ashvni Narayanan]

Yayy!! Thank you!

[Eric Wieser]

@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]

have you tried using it?

[Eric Wieser]

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

[Mario Carneiro]

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

[Mario Carneiro]

that seems awkward compared to a function alpha -> gamma

[Eric Wieser]

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

[Mario Carneiro]

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]

You're right that univ is a bad example

[Eric Wieser]

@[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]

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

[Mario Carneiro]

...like that

[Eric Wieser]

Should I PR the above?

[Mario Carneiro]

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

[Anne Baanen]

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

[Mario Carneiro]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Mario Carneiro]

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]

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)