Promoting to the main body Scott Fenton's theorems about finite and infinite products ?

[Glauco]

I was checking if, recently, something similar to sum_ was added for multiplication, and I found these sections in Scott Fenton's mathbox:

21.8.8 Complex products

21.8.9 Finite products

21.8.10 Infinite products

Scott Fentons's comment for df-prod is

"Define the product of a series with an index set of integers  A. This definition takes most of the aspects of df-sum 13322 and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a non-zero tail of the sequence. This ensures that the convergence criteria match those of infinite sums."

(but prod_ also handles effectively products "indexed" by generic finite sets)

I've written a few theorems based on Scott Fenton's definition and theorems (only for finite products, for now) and it looks like we can really build a complete library, similar to what's available for sum_ (Scott already did most of the work)

I keep finding proofs that require finite products (and, occasionally, even infinite products), so I hope those sections could be promoted to the main part. Of course, if Scott Fenton doesn't object (I don't know if he expected to tweak some parts of those sections, I've only "tested" some theorems of the finite product part and the section looks really well written and useful)

Glauco

[David A. Wheeler]

On Sun, 29 Dec 2019 06:59:23 -0800 (PST), Glauco <glaform...@gmail.com> wrote:
> I was checking if, recently, something similar to sum_ was added for
> multiplication, and I found these sections in Scott Fenton's mathbox:
> 21.8.8 Complex products
> 21.8.9 Finite products
> 21.8.10 Infinite products

...

> I've written a few theorems based on Scott Fenton's definition and theorems
> (only for finite products, for now) and it looks like we can really build a
> complete library, similar to what's available for sum_ (Scott already did
> most of the work)
>
> I keep finding proofs that require finite products (and, occasionally, even
> infinite products), so I hope those sections could be promoted to the main
> part.

As a general rule, if someone else finds something useful in a mathbox,
then we promote it to the main body (unless there's some serious
known problem). Stuff in the main body is much easier to reuse
and tends to be organized more logically.

I'd like to see more assertions moved into the main body in general.
I just updated a graph that shows the number of proven statements
over time in set.mm. It shows that the mathboxes have grown much
faster than the main body, which I interpret as "some things in mathboxes
should be moved into the main body". The graph is here:

https://docs.google.com/spreadsheets/d/1TnuBekyUP918smZeJRD0WrPhJthi915Ose0cnUnB1uc

The graph certainly makes it clear that set.mm continues to grow,
but I think we already knew that :-).

--- David A. Wheeler

[Norman Megill]

I agree.  You can move these into the main part of set.mm.

[Alexander van der Vekens]

Hi David,

is the graph really up-to-date? The latest data points in the graph are for 2019-08-07 (all: 32759, main: 21953), whereas the table containing the data goes until 2019-12-25 (all: 33983, main: 22381).

Alexander

[David A. Wheeler]

On Sun, 29 Dec 2019 12:59:53 -0800 (PST), "'Alexander van der Vekens' via Metamath" <meta...@googlegroups.com> wrote:
> is the graph really up-to-date? The latest data points in the graph are for
> 2019-08-07 (all: 32759, main: 21953), whereas the table containing the data
> goes until 2019-12-25 (all: 33983, main: 22381).

Whups, I updated the data but the graph didn't include all the data.

It's fixed now, thanks for reporting that!

--- David A. Wheeler