Evaluating multivariable functions

Stream: maths

[Hyunsang Hwang]

Is there a way to evaluate functions in Lean? I am trying to find a way to express
$$Q{\big (}e_{1}(X_{1},\ldots ,X_{n}),\ldots ,e_{n}(X_{1},\ldots ,X_{n}){\big )}}$$
using the package data.mv_polynomial.

[Eric Rodriguez]

$Q{\big(e_{1}(X_{1},\ldots ,X_{n}),\ldots ,e_{n}(X_{1},\ldots ,X_{n}){\big)}}$ (you had a typo and Zulip needs double $$s)

[Eric Rodriguez]

what are the $e_i$?

[Hyunsang Hwang]

Eric Rodriguez said:

what are the $e_i$?

Thank you for clearing that out. The $e_i$ are supposed to be
def esymm (n : ℕ) : mv_polynomial σ R :=∑ t in powerset_len n univ, ∏ i in t, X i
included in data.mv_polynomial.

[Eric Rodriguez]

docs#mv_polynomial.esymm

[Adam Topaz]

You can consider the subfield of the fraction field of $\mathbb{Q}[X_1,\ldots,X_n]$ generated over $\mathbb{Q}$ by the symmetric polynomials.

[Adam Topaz]

All the ingredients are there.

[Adam Topaz]

But that doesn't match the title of this thread.... what do you mean by "Evaluating multivariable functions" in relation to this?

[Hyunsang Hwang]

Adam Topaz said:

All the ingredients are there.

The Q is not supposed to be mathbb{Q}. I meant to write Q as a function and not as the field of rational numbers.

[Adam Topaz]

This seems like a #xy issue

[Adam Topaz]

I don't know whether mathlib knows that the symmetric polys are algebraically independent.

[Adam Topaz]

what are you trying to do?

[Hyunsang Hwang]

Adam Topaz said:

I don't know whether mathlib knows that the symmetric polys are algebraically independent.

I'm actually trying to prove this. I'm trying to prove the fundamental theorem of symmetric polynomials.

[Adam Topaz]

Ah okay.

[Eric Rodriguez]

(sorry about messing up your Q!)

[Adam Topaz]

What's the informal proof that you're trying to formalize?

[Adam Topaz]

There are various options

[Eric Rodriguez]

there's a lot of options for evaluating polynomials, including docs#mv_polynomial.aeval

[Hyunsang Hwang]

Adam Topaz said:

There are various options

I'm trying to use the double induction suggested here https://en.wikipedia.org/wiki/Elementary_symmetric_polynomial

[Hyunsang Hwang]

Eric Rodriguez said:

there's a lot of options for evaluating polynomials, including docs#mv_polynomial.aeval

Thank you. I'll try this.

[Adam Topaz]

(deleted)

[Adam Topaz]

Sorry, yeah Eric gave the right link :)