finsum over product of types

Stream: Is there code for X?

[Oliver Nash]

I'm using the finsum API for the first time. Do we have this anywhere?

import algebra.big_operators.finprod

open_locale big_operators

example {α β M : Type*} [add_comm_monoid M] (f : α → β → M) :
  ∑ᶠ (ab : α × β), f ab.fst ab.snd = ∑ᶠ a b, f a b := sorry

[Eric Wieser]

I think it's not true

[Eric Wieser]

Consider f (x : bool) (y : nat) = if (x and y = 0) or not x then 1 else 0

[Eric Wieser]

I think your example then reduces to 0 = 1

[Oliver Nash]

LOL, thanks.

[Eric Wieser]

Although proving that was awful:

example : ¬ ∀ {α β M : Type*} [add_comm_monoid M] (f : α → β → M), by exactI
  ∑ᶠ (ab : α × β), f ab.fst ab.snd = ∑ᶠ a b, f a b :=
begin
  intro h,
  let f := λ (b : bool) (n : nat), if b then 1 else (if n = 0 then 1 else 0),
  let f' := λ (p : bool × nat), f p.1 p.2,
  have : (function.support f').infinite,
  { refine set.infinite_of_injective_forall_mem (prod.mk.inj_left tt) (λ n : ℕ, _),
    dsimp [function.support, f', f],
    simp },
  specialize h f,
  rw finsum_of_infinite_support this at h,
  rw finsum_eq_sum_of_fintype at h,
  rw [fintype.sum_eq_single ff] at h,
  { dsimp [f] at h,
    rw @finsum_eq_sum_of_support_subset _ _ _ _ {0} at h,
    { rw finset.sum_singleton at h,
      simpa using h,},
    simp, },
  { rintros (b | b) hb,
    exact (hb rfl).elim,
    apply finsum_of_infinite_support,
    refine set.infinite_of_injective_forall_mem (@nat.succ.inj) (λ n : ℕ, _),
    simp [function.support,f], }
end

[Oliver Nash]

This is brilliant. Refutation by formal proof :joy:

[Eric Wieser]

How hard would it be to have a counterexample notation do you think?

[Eric Wieser]

That handles the ¬ and by exactI

[Oliver Nash]

I have no idea but it's an interesting thought.

[Oliver Nash]

Vaguely related thought: I have occasionally thought that if the machine learning people really are to have any chance of getting somewhere using Mathlib as a dataset then they would need a wealth of counterexamples.

[Eric Wieser]

This does sort of make me worry that the finsum API is awkward, in that "infinities" don't propagate

[Oliver Nash]

Like that's probably how we secretly reason about mathematics more than half the time.

[Oliver Nash]

Eric Wieser said:

This does sort of make me worry that the finsum API is awkward

I'm currently thinking about this too.

[Eric Wieser]

For instance, perhaps it should return with_top M instead

[Oliver Nash]

Exactly what I'm asking myself!

[Eric Wieser]

Although you need something clever somewhere to avoid ending up with with_top (with_top M)

[Kevin Buzzard]

@Damiano Testa had a counterexamples branch (but pre the huge changes so it might have rotted by now). I wonder if we could have a directory of counterexamples but not in src?

[Yaël Dillies]

Maybe it belongs to archive?

[Oliver Nash]

I'd be in favour of at least experimenting with a counterexamples section of archive.

[Johan Commelin]

Damiano has a branch with exactly that name (-;
(Edit: I now see that Kevin wrote this 3 posts up :face_palm:)

[David Wärn]

Eric Wieser said:

Although you need something clever somewhere to avoid ending up with with_top (with_top M)

This is what the option monad is for

[Oliver Nash]

I think with_top is just option.

[David Wärn]

Yes, so the monad multiplication takes you from with_top (with_top X) to with_top X

[Oliver Nash]

Agreed. I think this should work.

[Eric Wieser]

I don't really see how to apply that here - what would the signature of finsum become?

[David Wärn]

The first step would be to make its output option M

[Eric Wieser]

Currently its

finsum : Π {α : Sort u_1} {M : Type u_2} [_inst_3 : add_comm_monoid M], (α → M) → M

[Kevin Buzzard]

@David Wärn with_top := option

[Oliver Nash]

I think Eric's point is that the input would have to be with_top M also.

[Eric Wieser]

If you made it

finsum : Π {α : Sort u_1} {M : Type u_2} [_inst_3 : add_comm_monoid M], (α → M) → option M

then how do you prevent ∑ᶠ a b, f a b having type option (option m))?

[Eric Wieser]

That's certainly what my point should have been! Indeed,

finsum : Π {α : Sort u_1} {M : Type u_2} [_inst_3 : add_comm_monoid M], (α → option M) → option M

would solve the problem

[Eric Wieser]

I think we'd want to use def finsum.result M := option M rather than option directly

[Eric Wieser]

And then we could add a coercion from finsum.result M to M that sends top to 0

[Eric Wieser]

Which would preserve the current API in some form

[Oliver Nash]

If that last coercion trick works, it would be really neat. Best of all worlds.

[David Wärn]

You can sort of get the second signature from the first:

import data.option.basic
noncomputable theory
open_locale classical

def whats_this_called {α β : Type*} (f : α → option β) : option (α → β) :=
if h : ∀ a, (f a).is_some then some (λ a, option.get (h a)) else none

variables {α M : Type} (finsum : (α → M) → option M)
def finsum' (f : α → option M) : option M :=
whats_this_called f >>= finsum

[David Wärn]

The option monad is basically a principled way of making sure undefined values propagate. But mathlib generally prefers to use 0 for undefined values

[Yakov Pechersky]

For undefined values of add_monoid, 1 for monoid for finprod, of course

[Yakov Pechersky]

What's this called is ((>>= f) o pure) I think

[Mario Carneiro]

The whole point of this function is that it doesn't have undefinedness handling

[Mario Carneiro]

because that handling is exactly what causes all the pain

[Eric Wieser]

But we still have all that handling as obligations in the lemmas anyway

[Eric Wieser]

And the compromise finsum makes seems to make a bunch of "obvious" statements not true without annoying side conditions

[Mario Carneiro]

The statements are true as long as you ignore the fact that finsum is defined on useless inputs

[Mario Carneiro]

just assume everything is reasonable in the lemmas

[Mario Carneiro]

finsum is not actually any different from finset.sum in terms of assumptions

[Mario Carneiro]

it's just possible to state theorems that lie outside those assumptions now

[Mario Carneiro]

your first response to

example {α β M : Type*} [add_comm_monoid M] (f : α → β → M) :
  ∑ᶠ (ab : α × β), f ab.fst ab.snd = ∑ᶠ a b, f a b := sorry

should be "that doesn't typecheck, let me add assumptions so I don't have to deal with places where the function is crazy"

[Mario Carneiro]

for example [fintype α] [fintype β]

[Eric Wieser]

Oh, I guess an argument for why option wouldn't really help is the sum over f (z : units int \times int) := z.1 * z.2

[Mario Carneiro]

this is a little bit overconstrained, but the nice thing about finsum is that it is defined whenever it can possibly be defined so you can later revisit and generalize the theorem to any context where it remains reasonable. But the fully general statement is probably not the first thing you want

[Mario Carneiro]

You will need monads everywhere with the option approach

[Mario Carneiro]

plus it's not even computable, you need to use whats_this_called which is more naturally stated on roption

[Mario Carneiro]

If you want to propagate a well definedness condition through multiple operations, I would suggest roption instead of option. The latter is better when the function itself can tell you whether or not it is defined

[Mario Carneiro]

But at a certain point this starts to look like the situation with integrals and derivatives where you have to do everything twice, first prove that the value is defined and then prove it is equal to something (and neither implies the other)

[Mario Carneiro]

The nice thing about finset.sum is that it is always defined, so the first part is absent. It's still possible to have this with finsum provided the definedness proof is "easy" or typeclassable

[Eric Wieser]

Presumably having finsum match the design of integrals makes a lot of sense?

[Mario Carneiro]

not if it makes the easy case harder

[Mario Carneiro]

because the whole reason it exists is to make dealing with finite sums easier than the existing method using finset.sum

[Mario Carneiro]

It is a bit funny to me that finsum is converging on the design of finite sums that I did in metamath, df-gsum. The idea behind it is that it is defined to be the sum if it is at all reasonable to call a unique thing "the sum" of a function. It's still a bit more crazy than finsum since it also special cases when the summing set is a sequence of integers, in which case it is the left-associative ordered sum; otherwise it is the sum of the nonzero values up to associativity and commutativity

[Mario Carneiro]

doing something like that would be harder in lean since type equality tests don't work very well

[David Wärn]

My armchair understanding is that using roption / option for partial values like these could be really nice, if only we had some nice way of dealing with all the monad stuff (as well as whats_this_called, which I guess can't be defined in terms of monad operations since it's noncomputable). For example the false theorem at the start of this thread is a true unconditional equality in roption M. A lot of other lemmas, like finsum (f + g) = finsum f + finsum g aren't equalities since the LHS can be defined even when the RHS isn't. Here there's a directedness to the lemma: if you know the values offinsum f and finsum g, then you also know the value of finsum (f + g). Of course this is still easy to express with roption. Fubini's theorem for infinite sums is worse: knowing that some x = ∑ a b, f a b doesn't tell you that ∑ ab, f ab.fst ab.snd exists. Still the way you compute the latter sum in practice is that you compute the former sum, and during these computations observe that ∑ a b, |f a b| is finite...

[Eric Wieser]

If you go too far in this direction you end up at docs#tsum

[Mario Carneiro]

and during these computations observe that ∑ a b, |f a b| is finite...

This of course assumes that |f a b| is a thing

[Mario Carneiro]

If the target type is canonically ordered, then I think you do have Fubini's theorem (with suitable undefinedness preserving sum operations)

[David Wärn]

Yes, the problem is with negative terms

[Mario Carneiro]

But eric is right that if you want to handle convergence of absolute values that's what tsum does

[Mario Carneiro]

Personally, I think the lemmas should just assume the indexing set is finite because that's the easy case where all the lemmas go through

[Mario Carneiro]

There will be a second series of lemmas with more subtle conditions when you only have finite support

[David Wärn]

This sounds like a reasonable pragmatic approach

[David Wärn]

BTW, a sum where some term is ill-defined should be thought of as ill-defined. This is why you should be able to factor the sum of f : A -> roption B through whats_this_called as sketched above. This is not true of integrals: the integral of f : A -> roption B should only require f to be a.e. well-defined.

[Mario Carneiro]

You should be able to do so, since I think roption A is a comm monoid if A is

[Mario Carneiro]

maybe that instance doesn't exist

[Mario Carneiro]

I guess that's what with_top will do for you

[David Wärn]

Aha, that's nice!

[Mario Carneiro]

Oh, actually if there are infinitely many tops then you will get 0 instead of top

[Mario Carneiro]

so the finsum implementation has to be aware of the top element

[Mario Carneiro]

BTW here's the roption version of whats_this_called

import data.pfun

def pfun.totalize {α β} (f : α →. β) : roption (α → β) :=
⟨∀ a, (f a).1, λ h a, (f a).2 (h a)⟩

[David Wärn]

But pfun.totalize isn't in mathlib yet right?

[Mario Carneiro]

no, I just made it up

[Damiano Testa]

Dear All,

I have not followed the discussion yet, but indeed there is a counterexamples branch to mathlib. I have maintained it by merging master into it every once in a whole, but have not done so after the two big nat/int refactors.

The branch might break now, but I would still love to have more counterexamples! Feel free to push something onto it: in the branch counterexamples, there is a counterexamples folder in src.

[Damiano Testa]

I am on holidays for a week, so I will not have a chance to update master soon, but will do so as soon as I can!

[Oliver Nash]

Thanks @Damiano Testa Enjoy your holidays. I will keep the counterexamples branch in mind.

[Aaron Anderson]

I’ve also wanted a Fubini for finsum for my work on Hahn series, and an analog of finset.sum_sigma. An option version would be great because you could use simp and only have to check finiteness at the beginning and end, but it would also be awful because yet. another. API.

[Oliver Nash]

I don't have time right now but I might at least try to prove this version (which would suffice for my purposes) this evening:

import algebra.big_operators.finprod

open_locale big_operators

example {α β M : Type*} [add_comm_monoid M] (s : finset (α × β)) (f : α × β → M) :
  ∑ᶠ ab (h : ab ∈ s), f ab = ∑ᶠ a b (h : (a, b) ∈ s), f (a, b) := sorry

[Oliver Nash]

(On the off chance some good citizen was going to work on :point_up: I now have a proof of this which I will PR tomorrow)

[Oliver Nash]

Just pushed up my attempt as #7439