Zulip Chat Archive

Stream: Is there code for X?

Topic: interchange sum


view this post on Zulip Kevin Buzzard (Dec 11 2020 at 10:02):

0ijnF(i,j)\sum_{0\leq i\leq j\leq n}F(i,j) can be written as i=0nj=inF(i,j)\sum_{i=0}^n\sum_{j=i}^nF(i,j) and also as j=0ni=0jF(i,j)\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.

view this post on Zulip Mario Carneiro (Dec 11 2020 at 10:03):

There should be a general purpose 2D summation lemma

view this post on Zulip Mario Carneiro (Dec 11 2020 at 10:04):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 11 2020 at 10:05):

I'm just perusing big_ops.basic

view this post on Zulip Mario Carneiro (Dec 11 2020 at 10:06):

docs#finset.prod_sigma

view this post on Zulip Mario Carneiro (Dec 11 2020 at 10:07):

and docs#finset.prod_bij'

view this post on Zulip Kevin Buzzard (Dec 11 2020 at 10:12):

hells bells

view this post on Zulip 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 :-)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 N2\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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 11 2020 at 10:57):

Double @!?

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 11 2020 at 10:58):

(deleted)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 11 2020 at 11:32):

@Ashvni Narayanan there's what you needed :D

view this post on Zulip Ashvni Narayanan (Dec 11 2020 at 11:35):

Yayy!! Thank you!

view this post on Zulip 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⟩)

view this post on Zulip Mario Carneiro (Dec 11 2020 at 11:50):

have you tried using it?

view this post on Zulip Eric Wieser (Dec 11 2020 at 11:51):

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

view this post on Zulip Mario Carneiro (Dec 11 2020 at 11:51):

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

view this post on Zulip Mario Carneiro (Dec 11 2020 at 11:51):

that seems awkward compared to a function alpha -> gamma

view this post on Zulip Eric Wieser (Dec 11 2020 at 11:52):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 11 2020 at 11:53):

You're right that univ is a bad example

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 11 2020 at 11:53):

...like that

view this post on Zulip Eric Wieser (Dec 11 2020 at 11:53):

Should I PR the above?

view this post on Zulip 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

view this post on Zulip Anne Baanen (Dec 11 2020 at 11:54):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 11 2020 at 11:55):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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