Trouble with to_additive

Stream: general

[María Inés de Frutos Fernández]

While porting a file from my joint project with @Antoine Chambert-Loir to Lean 4, I run into the following issue with to_additive. In the last definition, I get the error message "The additive declaration already exists. Please specify this explicitly using @[to_additive existing]. [linter.toAdditiveExisting]" (even though tsum is not imported):

import Mathlib.Topology.Algebra.UniformGroup

open Classical Filter Finset Function

open scoped BigOperators Classical Topology

variable {α β : Type _} [TopologicalSpace α] [CommMonoid α]

@[to_additive]
def HasProd (f : β → α) (a : α) : Prop :=
  Tendsto (fun s : Finset β => ∏ b in s, f b) atTop (𝓝 a)

@[to_additive Summable]
def Multipliable (f : β → α) : Prop :=
  ∃ a, HasProd f a

/- ERROR MESSAGE: The additive declaration already exists. Please specify this explicitly
  using `@[to_additive existing]`. [linter.toAdditiveExisting]-/
@[to_additive tsum]
noncomputable irreducible_def tprod {β} (f : β → α) :=
  if h : Multipliable f then Classical.choose h else 1

However, if I add existing as suggested, the linter now tells me that the additive version does not exist.

/- ERROR MESSAGE: The additive declaration doesn't exist. Please remove the option
  `existing`. [linter.toAdditiveExisting]-/
@[to_additive existing tsum]
noncomputable irreducible_def tprod {β} (f : β → α) :=
  if h : Multipliable f then Classical.choose h else 1

In both cases, I also get the error tprod_def and tsum do not generate the same number of equation lemmas. Any ideas? Thanks!

[Eric Wieser]

I assume the cause is irreducible_def?

[María Inés de Frutos Fernández]

Thanks! Removing irreducible indeed fixes the issue. However, tsum is an irreducible_def in Mathlib; I guess the solution could be to write the definitions separately and then try to use to_additive for the theorems.

[Floris van Doorn]

@[to_additive] and irreducible_def are not compatible with each other yet.

[Floris van Doorn]

Note that if you do multiplicativize tsum, you probably want to add a translation rule here, so that to_additive correctly guesses the names.

[Floris van Doorn]

If you do that, then your code (after removing the tsum name hint) will not give an error, but it will also not do quite the right thing, since it won't mark the additive version as irreducible, and it might also not make the additive version have the correct equation lemmas. So it's still good to give the definitions separately and then additivize the theorems.

[Yury G. Kudryashov]

Recently, there were at least 2 attempts to add a multiplicative version of HasSum/tsum.

[Yury G. Kudryashov]

And @Sebastien Gouezel explained that the definition of HasSum should be changed so that the multiplicative version works better with zeros.

[Antoine Chambert-Loir]

Indeed, there is another pr by @Yaël Dillies which apparently does more than we do. But we need that file now.

Regarding @Sebastien Gouezel's suggestion, I think we fell in agreement that ‘HasSum‘ and ‘HasProd‘ should keep their standard meaning, but that another definition might be useful to introduce, if you need to use that remove a finite number of terms of your series and stay summable.

[Sebastien Gouezel]

Antoine Chambert-Loir said:

Regarding Sebastien Gouezel's suggestion, I think we fell in agreement that ‘HasSum‘ and ‘HasProd‘ should keep their standard meaning, but that another definition might be useful to introduce, if you need to use that remove a finite number of terms of your series and stay summable.

Yes, I agree with that. Note however that the definition of tsum has changed recently in Mathlib4, so you should probably adapt your code to the new definition.