[Merged by Bors] - chore(RingTheory/Polynomial/Basic): add lemma aeval_natDegree_le

[jcommelin]

This lemma is used in the proof of existence of Cartan subalgebras

---

[acmepjz]

golf (untested)

Suggested change

	rw [MvPolynomial.aeval_def, MvPolynomial.eval₂]
	apply (Polynomial.natDegree_sum_le _ _).trans
	apply Finset.sup_le
	intro d hd
	simp_rw [Function.comp_apply, ← C_eq_algebraMap]
	apply (Polynomial.natDegree_C_mul_le _ _).trans
	apply (Polynomial.natDegree_prod_le _ _).trans
	have : ∑ i in d.support, (d i) * n ≤ m * n := by
	rw [← Finset.sum_mul]
	apply mul_le_mul' (.trans _ hF) le_rfl
	rw [MvPolynomial.totalDegree]
	exact Finset.le_sup_of_le hd le_rfl
	apply (Finset.sum_le_sum _).trans this
	rintro i -
	apply Polynomial.natDegree_pow_le.trans
	exact mul_le_mul' le_rfl (hf i)
	rw [aeval_def, eval₂]
	refine (natDegree_sum_le _ _).trans <| Finset.sup_le fun d hd ↦ ?_
	simp_rw [Function.comp_apply, ← C_eq_algebraMap]
	refine (natDegree_C_mul_le _ _).trans <| (natDegree_prod_le _ _).trans <|
	(Finset.sum_le_sum fun i _ ↦ natDegree_pow_le.trans (mul_le_mul' le_rfl (hf i))).trans ?_
	rw [← Finset.sum_mul]
	exact mul_le_mul' (.trans (Finset.le_sup_of_le hd le_rfl) hF) le_rfl

[j-loreaux]

Let's not golf quite this much (although some of it is probably okay). For instance, the original with the separate .trans applications is much more readable.

apply (Polynomial.natDegree_C_mul_le _ _).trans
apply (Polynomial.natDegree_prod_le _ _).trans

Arguably, with this many .trans applications (there's one other), this should be a calc block.

[jcommelin]

The calc proof looks like this. I'm not sure it actually increases readability.

Suggested change

	rw [MvPolynomial.aeval_def, MvPolynomial.eval₂]
	apply (Polynomial.natDegree_sum_le _ _).trans
	apply Finset.sup_le
	intro d hd
	simp_rw [Function.comp_apply, ← C_eq_algebraMap]
	apply (Polynomial.natDegree_C_mul_le _ _).trans
	apply (Polynomial.natDegree_prod_le _ _).trans
	have : ∑ i in d.support, (d i) * n ≤ m * n := by
	rw [← Finset.sum_mul]
	apply mul_le_mul' (.trans _ hF) le_rfl
	rw [MvPolynomial.totalDegree]
	exact Finset.le_sup_of_le hd le_rfl
	apply (Finset.sum_le_sum _).trans this
	rintro i -
	apply Polynomial.natDegree_pow_le.trans
	exact mul_le_mul' le_rfl (hf i)
	calc natDegree ((aeval f) F)
	= natDegree (F.sum fun s a ↦ (algebraMap R R[X]) a * s.prod fun n e ↦ f n ^ e) := by
	rw [MvPolynomial.aeval_def, MvPolynomial.eval₂]
	_ ≤ F.support.fold max 0
	(natDegree ∘ fun i ↦ ((algebraMap R R[X]) (F.coeff i) * i.prod fun n e ↦ f n ^ e)) :=
	Polynomial.natDegree_sum_le _ _
	_ ≤ m * n := Finset.sup_le ?_
	intro d hd
	have aux : ∑ i in d.support, (d i) * n ≤ m * n := by
	rw [← Finset.sum_mul]
	apply mul_le_mul' (.trans _ hF) le_rfl
	rw [MvPolynomial.totalDegree]
	exact Finset.le_sup_of_le hd le_rfl
	calc natDegree ((algebraMap R R[X]) (coeff d F) * d.prod fun n e ↦ f n ^ e)
	= natDegree (Polynomial.C (coeff d F) * d.prod fun n e ↦ f n ^ e) := by rw [C_eq_algebraMap]
	_ ≤ natDegree (Finsupp.prod d fun n e ↦ f n ^ e) := Polynomial.natDegree_C_mul_le _ _
	_ ≤ ∑ i in d.support, natDegree (f i ^ (d i)) := Polynomial.natDegree_prod_le _ _
	_ ≤ m * n := (Finset.sum_le_sum ?_).trans aux
	rintro i -
	calc natDegree (f i ^ d i)
	≤ d i * natDegree (f i) := Polynomial.natDegree_pow_le
	_ ≤ d i * n := mul_le_mul' le_rfl (hf i)

[j-loreaux]

Consider a calc block for part of the proof for increased readability, but it's acceptable as is.

bors d+

[mathlib-bors]

✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ocfnash]

We seem to have several reasonable proofs none of which is obviously superior. More importantly, the statement is good.

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style