Zulip Chat Archive

Stream: Is there code for X?

Topic: Splitting a finset.sum over an involutive function


view this post on Zulip Eric Wieser (Nov 28 2020 at 10:56):

If I have an involutive function f : A -> A where there is no a st f a = a, then I can argue that sum a \in finset.univ A, g a can be rewritten into sum a \in half_of_univ, g a + g (f a). How would I begin to formalize this?

view this post on Zulip Kevin Buzzard (Nov 28 2020 at 11:09):

I ran into this problem in 2018 and I think there ended up being a lemma in mathlib which could help.

view this post on Zulip Kevin Buzzard (Nov 28 2020 at 11:11):

I'm thinking of docs#finset.prod_involution which probably isn't much help for you. It's related, but probably not enough.

view this post on Zulip Eric Wieser (Nov 28 2020 at 11:15):

Now that I have vs code to hand to type stuff, I think an auxiliary lemma that would be enough is

example {α : Type*} (f : α  α) (hf : function.involutive f) (hf' :  a, f a  a) :
   (x : set α), x  f '' x = set.univ  x  f '' x =  := sorry

view this post on Zulip Kevin Buzzard (Nov 28 2020 at 11:15):

As a mathematician my immediate instinct would be to be summing over equivalence classes. half_of_univ could be the noncomputable out or whatever it's called. You'll have to do something to choose the x.

view this post on Zulip Kevin Buzzard (Nov 28 2020 at 11:16):

Right, that set is the image of the noncomputable injection that you get from the surjection from alpha to alpha/~

view this post on Zulip Kevin Buzzard (Nov 28 2020 at 11:17):

the noncomputable injection gives you an isomorphism alpha = q x bool where q is the quotient.

view this post on Zulip Eric Wieser (Nov 28 2020 at 11:18):

docs#finset.sum_involution looks like it has everything I need

view this post on Zulip Kevin Buzzard (Nov 28 2020 at 11:18):

the definition of the equivalence associated to an involution is in TPIL near the end

view this post on Zulip Eric Wieser (Nov 28 2020 at 11:19):

https://leanprover.github.io/theorem_proving_in_lean/search.html?q=involution gives nothing

view this post on Zulip Kevin Buzzard (Nov 28 2020 at 11:19):

it's in the bit about quotients at the very end

view this post on Zulip Kevin Buzzard (Nov 28 2020 at 11:20):

oh I misremembered, it's making unordered pairs from ordered pairs. Section 11.4.

view this post on Zulip Eric Wieser (Nov 28 2020 at 11:30):

docs#finset.sum_cancels_of_partition_cancels is also close to what I want


Last updated: May 07 2021 at 22:14 UTC