Sylvester-Schur Basic Term Comparison Lemma: where to start?

Stream: new members

[J. J. Issai (project started by GRP)]

I have a basic Lemma I am attempting formalize. It is about sequences of distinct natural numbers. The form is : Given natural numbers $n, k$ , and $k$ many naturals $a_i , 0 \le i < k$, and suppose $a_i$ are distinct. If $\prod_{i=1}^k (n+i) \le \prod_{i=0}^{k-1} a_i$, then the maximum $a_{max}$ of the $a_i$ is $\ge n+k$, with equality only if (after some rearranging) the $a_i$ are the set $\{n+1,\ldots,n+k\}$.

[Aaron Liu]

Do you have an informal proof? Maybe you can start there.

[J. J. Issai (project started by GRP)]

I think so, but my questions are a little different.

[J. J. Issai (project started by GRP)]

My first question is: should I try to formalize it with the equality condition in the same unit/object/proof, or should I settle for nonstrict inequality, and prove strictness in a different unit/object/proof?

[Kenny Lau]

depends on your proof

[Kenny Lau]

most likely you'll have a separate lemma that you use for the equality condition

[Kenny Lau]

so factor that lemma out

[Kenny Lau]

in general, every step in your proof should ideally be factored out as a separate lemma, if possible

[Kenny Lau]

it's better to have 100 short lemmas than to have 1 long theorem

[J. J. Issai (project started by GRP)]

OK. Is there something similar to this in MathLib that I can study?

[Aaron Liu]

In file#Analysis/InnerProductSpace/Basic, cauchy schwartz inequality and equality are proved separately

[J. J. Issai (project started by GRP)]

OK. My use case is the following: I have n+1 through n+k, I have some distinct numbers a_i, and I know max(a_i)-min(a_i)>k, so that there is a gap. I want to use that fact along with this Term Comparison tool to conclude n+k < max(a_i), where I want strictness.

[J. J. Issai (project started by GRP)]

Is there a way I can package the separate parts so that I can use the thing I really want, which is the strict inequality?

[J. J. Issai (project started by GRP)]

of course, I have prod a_i >= prod (n+i)

[J. J. Issai (project started by GRP)]

Or do I need to develop a use case tactic, like: show a_i are distinct, show product a_i \ge \prod(n+i) , deduce n+k<= max a_k, show max(a_i) - min(a_i)>k, deduce max a_k > n+k?
And then reuse this tactic every time I need to use the tool?

[J. J. Issai (project started by GRP)]

Perhaps tactic is the wrong word here. Repeated inline code template perhaps?

[Kenny Lau]

what you call a tactic is what i call a lemma

[J. J. Issai (project started by GRP)]

OK. Then I guess in addition to the Term Comparison Lemma, I need a Get strictness lemma as well.

[J. J. Issai (project started by GRP)]

So that if I satisfy the conditions of the strictness Lemma, I get a strictness result. Is there somewhere in MathLib which expresses that a sequence of naturals is distinct, i.e. if a_i=a_j then i=j?

[J. J. Issai (project started by GRP)]

Right now my informal proof is by contraposition: If I have $k$ many distinct naturals $a_i$, and I relabel them to $b_i$ where now $b_i < b_j$ iff $i<j$, and if $b_i \le n+i$ for all the $i$, and there is at least one $j$ such that $b_j < n+j$, then $\prod b_i < \prod(n+i)$.

[J. J. Issai (project started by GRP)]

However, when I take the contrapositive, I get something not far from $\prod a_i \ge \prod(n+i)$ implies either there is no $j$ with $b_j < n+j$, or else there is one $i$ with $b_i > n+i$. It is hard to unwrap this to get a statement like max $a_i > n+k$. Perhaps I should just make a Lemma using ordered sequences?

[Matt Diamond]

Is there somewhere in MathLib which expresses that a sequence of naturals is distinct, i.e. if a_i=a_j then i=j?

I can't help with the rest but this is docs#Function.Injective

[J. J. Issai (project started by GRP)]

Hmm. It's sounding like I have to take my sequence and turn it into a function, and work with that internally. Will I be able to set up an interface so that I can pass a sequence into a Lemma (along with , say, four other parameters) and get out the result? I would prefer not to have to rephrase all my other work into functions.

[Aaron Liu]

What do you mean by this?

[Aaron Liu]

How are you representing your sequences right now?

[Aaron Liu]

The standard way is using a function.

[Kenny Lau]

i hope you aren't using List

[Aaron Liu]

List is hard to work with

[Aaron Liu]

You should use Fin k → Nat

[J. J. Issai (project started by GRP)]

I have not committed to a Lean representation. I would like to hear options.

[J. J. Issai (project started by GRP)]

As the "natural" proof is written, I have a number N which I can factor into $k-t$ many divisors, since N is the RHS of an inequality and the lefthandside is a product of $k-t$ many consecutive terms of the form $n+i$.

[Aaron Liu]

If you use a function you get to have fun with docs#Finset.prod

[J. J. Issai (project started by GRP)]

and the divisors are tweaked into a sequence which I use to conclude that max(sequence) > max(n+i) where I take the maximum of the left hand side (usually n+k-t).

[J. J. Issai (project started by GRP)]

And so if I use a function I guess I can take advantage of things like Finset.prod. But it is unclear if the Lemma I seek already exists in mathlib, after several search attempts.

[J. J. Issai (project started by GRP)]

It may be that I have to deal with Finset.prod and related objects. Who has experience using it to compare it with other similar representations? I am willing to use it if it is relatively fast. I also wouldn't mind building some things from scratch if I have a good example to trim down to what I need.