Affine changes of variables for complex polynomials

This file records how evaluation, degree, and polynomialSupNorm behave when a complex polynomial is precomposed with the affine map z ↦ a * z + b.

Main declarations

• Polynomial.affineComposition — precomposition by z ↦ a * z + b;
• Polynomial.eval_affineComposition and Polynomial.aeval_affineComposition — scalar and algebra-valued evaluation;
• Polynomial.natDegree_affineComposition_le and Polynomial.natDegree_affineComposition — the degree bounds, with equality when a ≠ 0;
• polynomialSupNorm_affineComposition_image — exact transport of the polynomial sup-norm.

noncomputable def Polynomial.affineComposition (p : Polynomial ℂ) (a b : ℂ) : Polynomial ℂ

Precomposition of a complex polynomial with the affine map z ↦ a * z + b.

Equations

• p.affineComposition a b = p.comp (Polynomial.C a * Polynomial.X + Polynomial.C b)

@[simp]

theorem Polynomial.eval_affineComposition (p : Polynomial ℂ) (a b z : ℂ) : eval z (p.affineComposition a b) = eval (a * z + b) p

Evaluating an affine composition is evaluation after the corresponding scalar affine map.

@[simp]

theorem Polynomial.aeval_affineComposition {A : Type u_1} [Semiring A] [Algebra ℂ A] (p : Polynomial ℂ) (a b : ℂ) (x : A) : (aeval x) (p.affineComposition a b) = (aeval (a • x + b • 1)) p

Algebra-valued evaluation commutes with affine precomposition.

theorem Polynomial.natDegree_affineComposition_le (p : Polynomial ℂ) (a b : ℂ) : (p.affineComposition a b).natDegree ≤ p.natDegree

Affine precomposition cannot increase the natural degree of a polynomial.

theorem Polynomial.natDegree_affineComposition (p : Polynomial ℂ) {a b : ℂ} (ha : a ≠ 0) : (p.affineComposition a b).natDegree = p.natDegree

Precomposition by a nonconstant affine map preserves natural degree.

theorem polynomialSupNorm_affineComposition_image (p : Polynomial ℂ) (a b : ℂ) (X : Set ℂ) : polynomialSupNorm (p.affineComposition a b) X = polynomialSupNorm p ((fun (z : ℂ) => a * z + b) '' X)

The sup-norm of an affine composition on X is the original sup-norm on the affine image of X. This remains exact for unbounded sets: in that case both conditionally complete suprema use the same unbounded family of values.