Going from AM-GM to AM-GM 3

[Stanislas Polu]

Hi!

I've been trying to demonstrate a specialization of amgm to the case
where the sequence is explicit and of length k (say k=3 since we
already have amgm2).

The crucial part is obviously to demonstrate that amgm's "sums" are
equal to an explicit sum or product of k=3 elements. I've started with
trying to prove a statement along the lines of:

```
( ph -> ( CCfld gsum { { 1 , A } , { 1 , B } , { 1 , C } } ) = ( A + (
B + C ) ) )
```

But quickly realized how unsure I was how to represent F in amgm? Also
looking at set.mm I failed to find any theorem that would let me
decompose the `gsum` sequentially.

I was expecting to find something along the very broad lines of:

```
( CCfld gsum { { 1 , A } , { 1 , B } , { 1 , C } } ) = ( ( CCfld gsum
{ { 1 , A } , { 1 , B } } ) + ( CCfld gsum { { 1 , C } } ) )
```

Left with no clear path forward and a failure to find good examples in
set.mm, I revert to the community for help :)

Would any of you have indications on how to proceed with proving the
translation from a `gsum` format to ( `( A + ( B + C ) ) )`?

Thank you so much!

-stan

[Mario Carneiro]

On Tue, Sep 8, 2020 at 3:46 PM 'Stanislas Polu' via Metamath <meta...@googlegroups.com> wrote:

I was expecting to find something along the very broad lines of:

```
( CCfld gsum { { 1 , A } , { 1 , B } , { 1 , C } } ) = ( ( CCfld gsum
{ { 1 , A } , { 1 , B } } ) + ( CCfld gsum { { 1 , C } } ) )
```

Well, in the first place the statement is false, and a bit not well typed. The right argument of gsum is a finitely supported function, which is a set of ordered pairs, which means (1) you should use <. 1 , A >. for the points, and (2) the domain values should be distinct or it's not a function; that is, instead of { <. 1 , A >. , <. 1 , B >. , <. 1 , C >. } you should have { <. 1 , A >. , <. 2 , B >. , <. 3 , C >. }.The easiest way to construct finite functions on integers like this is using df-word, as in <" A B C ">, and the relevant lemmas for manipulating such expressions are gsumws1 and gsumccat, also specialized to gsumccatsn and gsumws2 (it might be good to fill out the matrix here and prove gsumwsN for n = 3..8).

 Mario

[Stanislas Polu]

Thanks Mario!

I will dig in that direction and hopefully will make a PR for gsumwsN
and amgmN for N=3..8 \o/

-stan

> --
> You received this message because you are subscribed to the Google Groups "Metamath" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSudhyg1zSUqiTspDwgoGoQ5wmBYBPuRf_xHPmsrnjzYgA%40mail.gmail.com.

[Stanislas Polu]

That worked out nicely (see screenshot).

I'll work on amgm{k}d and gsumws{k} for k={1,4} and should create a PR
soon. Thanks Mario!

-stan