multipliable !3#19219

Stream: PR reviews

[Antoine Chambert-Loir]

This PR furnishes infinite products in a commutative monoid.
It gives the companion of docs#summable, docs#has_tsum, docs#tsum and everything that was provided in that context, under the names summable, has_tsum, `tsum.
It was done by translating addition into multiplication in that file and adding tags @[to_additive] at essentially each definition.
I did the translation for the two files, the rest was about rings, modules or fields and didn't seem to need any modification.

Hopefully, all translations of names are correct, but for this, one needs to check that the compilation runs.

[Yaël Dillies]

You know I have an open PR for that, right?

[Yaël Dillies]

#18405

[Antoine Chambert-Loir]

No, I didn't…

[Antoine Chambert-Loir]

I just had a look there. You did more work than I did.
Terminological discussion :

• I can see whereprodable comes from, but isn't an English word such as multipliable more reasonable?
• For the multiplicative version of vanishing, I used mul_vanishing, by analogy with the already chosen mul_indicator…

[Sebastien Gouezel]

As I have mentioned in a message above (https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/infinite.20product.20clash.20with.20type.20product/near/327479289), just copying the definition of infinite sums to get infinite products is not going to give a nice behavior, because of additional issues due to 0 that do not show up in infinite sums. A better behaved definition would be: for any finite s, the product over finite subsets t in the complement of s converges as t exhausts the complement of s. The additivization of this definition coincides with our current definition of infinite sums in topological additive groups, so it would make sense to switch everything to this new definition. But this will be a very heavy refactor, so probably better to keep for after the port.

[Antoine Chambert-Loir]

I think complex analysis makes use of a particular use of infinite products, which is more restrictive than infinite products in arbitrary commutative monoids, and that should not make the natural definition disappear.

[Antoine Chambert-Loir]

Moreover, I have the impression that with a bit of additional complex analysis, infinite products (defined naively) can't behave too badly, because the log of the limit will likely be subharmonic,so can't be +infinity.

[Sebastien Gouezel]

Indeed, you're safe if you're sure you will never multiply by zero. But since there is a definition which works fine also when one multiplies by zero, it's the definition we should use as a basis for the theory.

[Sebastien Gouezel]

Note that we should have some API showing that, in reasonable cases, the complicated definition is equivalent to the naive one, hiding in practice the fact that we have used a complicated definition to start with.

[Antoine Chambert-Loir]

If I understand your definition correctly, and I may be wrong, if you convert an add_comm_monoid into a comm_monoid by just changing the name of the law, tsum won't goi to tprod..

[Sebastien Gouezel]

We should change both tsum and tprod so that they match, indeed. A way to do the refactor would be first to only change tsum and fix everything in the library. Then define tprod and let tsum be the additivization of tprod.

[Sebastien Gouezel]

One point which is not clear to me is if, in the definition I sketched in https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/multipliable.20!3.2319219/near/370844553, we should only take s finite, or allow any s.

[Antoine Chambert-Loir]

I may be confused, again, but your definition seems to exist in a lesser generality than the standard one.

[Antoine Chambert-Loir]

I agree that summable families in a commutative monoid for which all subfamilies are summable are a nice object to consider.

[Sebastien Gouezel]

Yes, it exists in less generality than the standard one. But they are equivalent in all interesting situations I can think of.

[Yakov Pechersky]

I have this complex product definition (and theorems about it) on a branch

[Yakov Pechersky]

https://github.com/leanprover-community/mathlib/tree/2301.10303

[Yakov Pechersky]

With things like

structure has_prod (f : β → α) (a : α) : Prop :=
(finite_not_unit : {b | ¬ is_unit (f b)}.finite)
(tendsto_units : ∃ x : αˣ, tendsto
  (λ s : finset β, ∏ b in s, surj_units (f b)) at_top (𝓝 x))
(prod_eq : a = tendsto_units.some * ∏ b in finite_not_unit.to_finset, f b)
[...]
lemma real.converges_prod_one_add_pow_two_pow {x : ℝ} (hx : 0 ≤ x) (hx' : x < 1) :
  converges_prod (λ n : ℕ, (1 : ℝ) + (x ^ (2 ^ n)))  :=

[Yaël Dillies]

Sébastien, I know about your concern. My idea was to first match the additive and multiplicative APIs, then modify them together so that they do the right thing for infinite products while still being usable for (better behaved) infinite sums.

[Yaël Dillies]

And the hope for the second step was to use Yakov's definition just above

[Yaël Dillies]

Antoine, the point of prodable is that it has the same number of letters as summable. This is quite useful in lemma names, I find.

[Sebastien Gouezel]

Yakov's definition does not work for tsums on nnreal: there are essentially no additive units on nnreal, and still there are many converging series.

[Yaël Dillies]

Do you have an alternative definition then?

[Sebastien Gouezel]

Yes, the one in https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/multipliable.20!3.2319219/near/370844553

[Yaël Dillies]

Ah sorry, I previously read it as equivalent to Yakov's definition.

[Jireh Loreaux]

Yaël Dillies said:

Antoine, the point of prodable is that it has the same number of letters as summable. This is quite useful in lemma names, I find.

Bikeshedding: I thoroughly dislike this as a reason for naming. However, I prefer prodable is over multipliable (despite the fact that as an English speaker I find the latter more natural) because prod is about ∏, whereas mul is about the binary operation *.

[Kyle Miller]

more :bike: :multipliable means you can bend it in multiple ways

[Yaël Dillies]

Someone has been in :flag_france: recently

[Frédéric Dupuis]

Right: you can fold it with mul :-)

[Heather Macbeth]

Kyle Miller said:

more :bike: :multipliable means you can bend it in multiple ways

For some reason engineers make a distinction between surfaces which bend in multiple ways (meaning practically all surfaces) and surfaces which don't (i.e., curvature-zero surfaces).

[Antoine Chambert-Loir]

Sebastien Gouezel said:

Yes, it exists in less generality than the standard one. But they are equivalent in all interesting situations I can think of.

I had understood — and found admirable — what I thought to be one of the features of mathlib, namely to allow the greatest reasonable/possible generality in definitions. The property you indicate is certainly useful, maybe frequent, and deserves a name in mathlib to be used whenever it intervenes, but I can't understand how it could be a basis for the definition of infinite sums/products in mathlib.

[Sebastien Gouezel]

Even before generality, the first criterion should be mathematical correctness: if a definition is broken, it should be fixed. My point is that our current definition of summable is broken, because of the following example: in the additive monoid [-\infty, +\infty), let u 0 be -\infty and u n = 1 for positive n. To me, this sequence is not summable (as just changing the value of u 0 makes it obviously not summable), although with our current definition it is. Our definition was probably not written with this kind of example in mind.

On the other hand, if most people think this sequence should be summable, we can keep the current definition, and add the other one as a new definition like strongly_summable. From a refactor point of view, this would in fact be much easier.

[Antoine Chambert-Loir]

Well, Bourbaki (Topologie générale, chap 3, §5) defines summable families in the context of commutative groups but they indicates in a remark that the definition applies in the context of commutative monoids. Moreover, they explicitly uses infinite products in the multiplicative monoid of power series (the topology of which is simple convergence on the coefficients, which have the discrete topology), without any condition on the ring of coefficients. (This is precisely the reason why I had to start this PR, because @María Inés de Frutos Fernández and I need it now!)

[Antoine Chambert-Loir]

(Not all definitions by Bourbaki are good, though. mathlib's version of filters, for example, is much better.)

[Johan Commelin]

Sebastien Gouezel said:

On the other hand, if most people think this sequence should be summable, we can keep the current definition, and add the other one as a new definition like strongly_summable. From a refactor point of view, this would in fact be much easier.

Bifurcations are suboptimal. But if we are still trying to figure out what the right definition is, then I think this is a good strategy.

[Antoine Chambert-Loir]

Yaël Dillies said:

You know I have an open PR for that, right?

Is there a companion PR for Lean4 ?