A theorem of Pólya on polynomials

Formalizes the polynomial sublevel-set bounds, the real-rooted polynomial facts, Chebyshev's theorem and its equality cases, and the chapter's examples.

Contents of former file Chapter_23/Chebyshev.lean

Chebyshev's theorem (Appendix of Chapter 23)

We prove Chebyshev's theorem: a real polynomial of degree n ≥ 1 with leading coefficient c attains at some point of [-1, 1] an absolute value of at least |c| / 2 ^ (n - 1).

The proof is the one of the book, transported from cosine polynomials to ordinary polynomials via x = cos θ: we compare p with the scaled Chebyshev polynomial c / 2^(n-1) * T_n, which alternates in sign at the n + 1 nodes cos (kπ/n).

theorem Chapter23.exists_root_of_mul_neg {f : ℝ → ℝ} (hf : Continuous f) {a b : ℝ} (hab : a < b) (h : f a * f b < 0) : ∃ c ∈ Set.Ioo a b, f c = 0

Intermediate value theorem in the form of a sign change.

noncomputable def Chapter23.chebNode (n k : ℕ) : ℝ

The Chebyshev nodes cos (k π / n).

Equations

• Chapter23.chebNode n k = Real.cos (↑k * Real.pi / ↑n)

theorem Chapter23.chebNode_strictAnti {n j k : ℕ} (hn : 1 ≤ n) (hjk : j < k) (hk : k ≤ n) : chebNode n k < chebNode n j

theorem Chapter23.chebNode_mem {n k : ℕ} : chebNode n k ∈ Set.Icc (-1) 1

theorem Chapter23.eval_chebNode {n k : ℕ} (hn : 1 ≤ n) : Polynomial.eval (chebNode n k) (Polynomial.Chebyshev.T ℝ ↑n) = (-1) ^ k

The Chebyshev polynomial T_n evaluated at the node cos (kπ/n) is (-1)^k.

theorem Chapter23.chebyshev_leadingCoeff (p : Polynomial ℝ) (n : ℕ) (hn : 1 ≤ n) (hdeg : p.natDegree = n) : ∃ x ∈ Set.Icc (-1) 1, |p.leadingCoeff| / 2 ^ (n - 1) ≤ |Polynomial.eval x p|

Chebyshev's theorem, general leading coefficient: if p has degree n ≥ 1, then max_{-1 ≤ x ≤ 1} |p x| ≥ |lc p| / 2^(n-1).

theorem Chapter23.chebyshev (p : Polynomial ℝ) (hp : p.Monic) (hn : 1 ≤ p.natDegree) : ∃ x ∈ Set.Icc (-1) 1, 1 / 2 ^ (p.natDegree - 1) ≤ |Polynomial.eval x p|

Chebyshev's theorem. Let p be a real polynomial of degree n ≥ 1 with leading coefficient 1. Then max_{-1 ≤ x ≤ 1} |p x| ≥ 1 / 2^(n-1).

theorem Chapter23.corollary (p : Polynomial ℝ) (hp : p.Monic) (hn : 1 ≤ p.natDegree) (a b : ℝ) (h : ∀ x ∈ Set.Icc a b, |Polynomial.eval x p| ≤ 2) : b - a ≤ 4

Corollary. Let p be a real polynomial of degree n ≥ 1 with leading coefficient 1, and suppose |p x| ≤ 2 for all x ∈ [a, b]. Then b - a ≤ 4.

Contents of former file Chapter_23/Facts.lean

Two facts about polynomials with real roots (box in Chapter 23)

Let p be a real polynomial all of whose roots are real (i.e. the number of roots counted with multiplicity equals the degree).

• Fact 1. If b is a multiple root of p', then b is also a root of p.
• Fact 2. p'(x)² ≥ p(x) p''(x) for all x ∈ ℝ.

theorem Chapter23.fact_2_prod (s : Multiset ℝ) (x : ℝ) : Polynomial.eval x (Multiset.map (fun (a : ℝ) => Polynomial.X - Polynomial.C a) s).prod * Polynomial.eval x (Polynomial.derivative (Polynomial.derivative (Multiset.map (fun (a : ℝ) => Polynomial.X - Polynomial.C a) s).prod)) ≤ Polynomial.eval x (Polynomial.derivative (Multiset.map (fun (a : ℝ) => Polynomial.X - Polynomial.C a) s).prod) ^ 2

Fact 2 for a product ∏ (X - a), by induction on the roots.

theorem Chapter23.fact_2 (p : Polynomial ℝ) (hroots : p.roots.card = p.natDegree) (x : ℝ) : Polynomial.eval x p * Polynomial.eval x (Polynomial.derivative (Polynomial.derivative p)) ≤ Polynomial.eval x (Polynomial.derivative p) ^ 2

Fact 2. If all roots of the real polynomial p are real, then p'(x)² ≥ p(x) p''(x) for all real x.

theorem Chapter23.fact_1 (p : Polynomial ℝ) (hroots : p.roots.card = p.natDegree) (b : ℝ) (hb : 2 ≤ Polynomial.rootMultiplicity b (Polynomial.derivative p)) : p.IsRoot b

Fact 1. If all roots of the real polynomial p are real and b is a multiple root of p' (i.e. (X - b)² divides p', with p' ≠ 0), then b is a root of p.

Contents of former file Chapter_23/RootProd.lean

Products ∏ (x - a) over a multiset of real roots

For a multiset s of real numbers we study rootProd s x = ∏_{a ∈ s} (x - a), i.e. the evaluation of the monic real-rooted polynomial with root multiset s. We collect:

• elementary algebraic facts and comparison lemmas for |rootProd s x|;
• log-concavity between consecutive roots, which yields the "quasi-concavity" statement two_lt_abs_rootProd_of_between: between two consecutive roots, the set where |rootProd s x| > 2 is an interval;
• the structure of a "gap" of the set {x | |rootProd s x| ≤ 2} between consecutive roots;
• finite interval covers (Coverable) and the cut-and-shift lemma used in Pólya's argument.

noncomputable def Chapter23.rootProd (s : Multiset ℝ) (x : ℝ) : ℝ

rootProd s x = ∏_{a ∈ s} (x - a).

Equations

• Chapter23.rootProd s x = (Multiset.map (fun (a : ℝ) => x - a) s).prod

@[simp]

theorem Chapter23.rootProd_zero (x : ℝ) : rootProd 0 x = 1

@[simp]

theorem Chapter23.rootProd_cons (a : ℝ) (s : Multiset ℝ) (x : ℝ) : rootProd (a ::ₘ s) x = (x - a) * rootProd s x

theorem Chapter23.rootProd_add (s t : Multiset ℝ) (x : ℝ) : rootProd (s + t) x = rootProd s x * rootProd t x

theorem Chapter23.rootProd_map_sub (s : Multiset ℝ) (d x : ℝ) : rootProd (Multiset.map (fun (x : ℝ) => x - d) s) x = rootProd s (x + d)

theorem Chapter23.eval_prod_X_sub_C (s : Multiset ℝ) (x : ℝ) : Polynomial.eval x (Multiset.map (fun (a : ℝ) => Polynomial.X - Polynomial.C a) s).prod = rootProd s x

theorem Chapter23.continuous_rootProd (s : Multiset ℝ) : Continuous (rootProd s)

theorem Chapter23.rootProd_eq_zero_of_mem {s : Multiset ℝ} {a : ℝ} (h : a ∈ s) : rootProd s a = 0

theorem Chapter23.rootProd_ne_zero {s : Multiset ℝ} {x : ℝ} (h : x ∉ s) : rootProd s x ≠ 0

theorem Chapter23.abs_rootProd_le {s : Multiset ℝ} {x y : ℝ} (h : ∀ a ∈ s, |y - a| ≤ |x - a|) : |rootProd s y| ≤ |rootProd s x|

Comparison of absolute values of rootProd factor by factor.

theorem Chapter23.monic_prod_X_sub_C (s : Multiset ℝ) : (Multiset.map (fun (a : ℝ) => Polynomial.X - Polynomial.C a) s).prod.Monic

The monic polynomial with root multiset s.

Log-concavity between consecutive roots

noncomputable def Chapter23.logRootSum (s : Multiset ℝ) (x : ℝ) : ℝ

∑_{a ∈ s} log (x - a); equal to log |rootProd s x| away from the roots.

Equations

• Chapter23.logRootSum s x = (Multiset.map (fun (a : ℝ) => Real.log (x - a)) s).sum

theorem Chapter23.log_abs_rootProd {s : Multiset ℝ} {x : ℝ} (h : x ∉ s) : Real.log |rootProd s x| = logRootSum s x

theorem Chapter23.concaveOn_log_sub {a α β : ℝ} (h : a ≤ α ∨ β ≤ a) : ConcaveOn ℝ (Set.Ioo α β) fun (x : ℝ) => Real.log (x - a)

theorem Chapter23.concaveOn_logRootSum {s : Multiset ℝ} {α β : ℝ} (h : ∀ a ∈ s, a ≤ α ∨ β ≤ a) : ConcaveOn ℝ (Set.Ioo α β) (logRootSum s)

theorem Chapter23.two_lt_abs_rootProd_of_between {s : Multiset ℝ} {α β : ℝ} (hroots : ∀ a ∈ s, a ≤ α ∨ β ≤ a) {x y z : ℝ} (hx : α < x) (hxy : x ≤ y) (hyz : y ≤ z) (hz : z < β) (hfx : 2 < |rootProd s x|) (hfz : 2 < |rootProd s z|) : 2 < |rootProd s y|

Quasi-concavity of |rootProd s| between consecutive roots: if |rootProd s| > 2 at x and z, then also at every y between them.

theorem Chapter23.gap_structure {s : Multiset ℝ} {α β c : ℝ} (hroots : ∀ a ∈ s, a ≤ α ∨ β ≤ a) (hα : |rootProd s α| ≤ 2) (hβ : |rootProd s β| ≤ 2) (hc : c ∈ Set.Ioo α β) (hfc : 2 < |rootProd s c|) : ∃ (u : ℝ) (v : ℝ), α ≤ u ∧ u ≤ v ∧ v ≤ β ∧ (∀ x ∈ Set.Icc α u, |rootProd s x| ≤ 2) ∧ (∀ x ∈ Set.Icc v β, |rootProd s x| ≤ 2) ∧ ∀ x ∈ Set.Ioo u v, 2 < |rootProd s x|

Structure of a gap of {x | |rootProd s x| ≤ 2} between two consecutive roots α < β: the set where |rootProd s x| > 2 inside (α, β) is an open interval (u, v).

theorem Chapter23.abs_le_of_abs_rootProd_le {s : Multiset ℝ} (hs : s ≠ 0) : ∃ (M : ℝ), ∀ (x : ℝ), |rootProd s x| ≤ 2 → |x| ≤ M

{x | |rootProd s x| ≤ 2} is bounded when s is nonempty.

Finite interval covers

def Chapter23.Coverable (S : Set ℝ) (L : ℝ) : Prop

S can be covered by finitely many closed intervals [a_i, b_i] of total length at most L.

Equations

• Chapter23.Coverable S L = ∃ (I : List (ℝ × ℝ)), (∀ i ∈ I, i.1 ≤ i.2) ∧ S ⊆ ⋃ i ∈ I, Set.Icc i.1 i.2 ∧ (List.map (fun (i : ℝ × ℝ) => i.2 - i.1) I).sum ≤ L

theorem Chapter23.Coverable.mono {S T : Set ℝ} {L : ℝ} (h : Coverable T L) (hST : S ⊆ T) : Coverable S L

theorem Chapter23.Coverable.cut_shift {S T : Set ℝ} {L u d : ℝ} (hT : Coverable T L) (h : ∀ x ∈ S, x ≤ u ∧ x ∈ T ∨ u ≤ x - d ∧ x - d ∈ T) : Coverable S L

The cut-and-shift lemma: if every point of S either lies in T ∩ (-∞, u], or is mapped by x ↦ x - d into T ∩ [u, ∞), then a cover of T yields a cover of S of no larger total length.

Contents of former file Chapter_23/Polya.lean

Pólya's theorem (Theorems 1 and 2 of Chapter 23)

We prove

• Theorem 2: if p is a monic real polynomial of degree n ≥ 1 all of whose roots are real, then P = {x | |p x| ≤ 2} can be covered by finitely many intervals of total length at most 4;
• Theorem 1: if f is a monic complex polynomial of degree n ≥ 1, then the orthogonal projection onto the real axis of C = {z | |f z| ≤ 2} can be covered by finitely many intervals of total length at most 4.

The proof of Theorem 2 follows Pólya's idea: as long as P is not an interval, we take the gap of P between the rightmost "bad" root α and the next root β and shift all roots to the right of the gap to the left by the length d of the gap. The new set P₁ contains P ∩ (-∞, u] and (P ∩ [v, ∞)) - d, so covers transfer back (Coverable.cut_shift), and the number of "bad" roots strictly decreases. When no bad root remains, P is a single interval on which |p| ≤ 2, and the Corollary of Chebyshev's theorem bounds its length by 4.

def Chapter23.sublevel (s : Multiset ℝ) : Set ℝ

The sublevel set {x | |∏_{a ∈ s} (x - a)| ≤ 2}.

Equations

• Chapter23.sublevel s = {x : ℝ | |Chapter23.rootProd s x| ≤ 2}

def Chapter23.Good (s : Multiset ℝ) (a : ℝ) : Prop

A root a is good if |p| ≤ 2 on the whole segment from a to the largest root.

Equations

• Chapter23.Good s a = ∀ (x : ℝ), a ≤ x → (∃ b ∈ s, x ≤ b) → |Chapter23.rootProd s x| ≤ 2

noncomputable def Chapter23.badCount (s : Multiset ℝ) : ℕ

The number of distinct roots which are not good.

Equations

• Chapter23.badCount s = {a ∈ s.toFinset | ¬Chapter23.Good s a}.card

theorem Chapter23.coverable_of_all_good {s : Multiset ℝ} (hs : s ≠ 0) (hgood : ∀ a ∈ s, Good s a) : Coverable (sublevel s) 4

If every root is good, then P is a single interval of length at most 4.

theorem Chapter23.shift_step {s : Multiset ℝ} (hbad : 0 < badCount s) : ∃ (s1 : Multiset ℝ), s1.card = s.card ∧ badCount s1 < badCount s ∧ ∃ (u : ℝ) (d : ℝ), ∀ x ∈ sublevel s, x ≤ u ∧ x ∈ sublevel s1 ∨ u ≤ x - d ∧ x - d ∈ sublevel s1

Pólya's shift. If some root is bad, shifting the roots to the right of the gap after the rightmost bad root to the left produces a new root multiset of the same size with fewer bad roots, whose sublevel set receives P by a cut-and-shift map.

theorem Chapter23.coverable_sublevel (s : Multiset ℝ) (hs : s ≠ 0) : Coverable (sublevel s) 4

Theorem 2 for the product ∏_{a ∈ s} (x - a).

theorem Chapter23.theorem_2 (p : Polynomial ℝ) (hp : p.Monic) (hn : 1 ≤ p.natDegree) (hroots : p.roots.card = p.natDegree) : ∃ (I : List (ℝ × ℝ)), (∀ i ∈ I, i.1 ≤ i.2) ∧ {x : ℝ | |Polynomial.eval x p| ≤ 2} ⊆ ⋃ i ∈ I, Set.Icc i.1 i.2 ∧ (List.map (fun (i : ℝ × ℝ) => i.2 - i.1) I).sum ≤ 4

Theorem 2. Let p be a real polynomial of degree n ≥ 1 with leading coefficient 1 and all roots real. Then P = {x ∈ ℝ | |p x| ≤ 2} can be covered by finitely many intervals [a_i, b_i] of total length at most 4.

theorem Chapter23.abs_rootProd_re_le_norm (t : Multiset ℂ) (z : ℂ) : |rootProd (Multiset.map Complex.re t) z.re| ≤ ‖(Multiset.map (fun (c : ℂ) => z - c) t).prod‖

The first step of the proof of Theorem 1 ("by the theorem of Pythagoras"): if f(z) = (z - c₁) ⋯ (z - cₙ) and p(x) = (x - Re c₁) ⋯ (x - Re cₙ), then |p (Re z)| ≤ |f z|.

theorem Chapter23.abs_eval_re_le_norm_eval (f : Polynomial ℂ) (hf : f.Monic) (z : ℂ) : |Polynomial.eval z.re (Multiset.map (fun (c : ℂ) => Polynomial.X - Polynomial.C c.re) f.roots).prod| ≤ ‖Polynomial.eval z f‖

With f monic complex and p(x) = ∏ (x - Re cₖ) over the roots cₖ of f, we have |p (Re z)| ≤ |f z| for all z.

theorem Chapter23.theorem_1 (f : Polynomial ℂ) (hf : f.Monic) (hn : 1 ≤ f.natDegree) : ∃ (I : List (ℝ × ℝ)), (∀ i ∈ I, i.1 ≤ i.2) ∧ Complex.re '' {z : ℂ | ‖Polynomial.eval z f‖ ≤ 2} ⊆ ⋃ i ∈ I, Set.Icc i.1 i.2 ∧ (List.map (fun (i : ℝ × ℝ) => i.2 - i.1) I).sum ≤ 4

Theorem 1 (Pólya). Let f be a complex polynomial of degree at least 1 with leading coefficient 1. Set C = {z ∈ ℂ | |f z| ≤ 2} and let R be the orthogonal projection of C onto the real axis. Then there are intervals I₁, …, I_t on the real line which together cover R and satisfy ℓ(I₁) + ⋯ + ℓ(I_t) ≤ 4.

Measure-theoretic reformulation

theorem Chapter23.volume_le_of_coverable {S : Set ℝ} {L : ℝ} (h : Coverable S L) : MeasureTheory.volume S ≤ ENNReal.ofReal L

A set covered by intervals of total length at most L has Lebesgue measure at most L.

theorem Chapter23.theorem_2_volume (p : Polynomial ℝ) (hp : p.Monic) (hn : 1 ≤ p.natDegree) (hroots : p.roots.card = p.natDegree) : MeasureTheory.volume {x : ℝ | |Polynomial.eval x p| ≤ 2} ≤ 4

Theorem 2, measure version: P = {x | |p x| ≤ 2} has Lebesgue measure at most 4.

theorem Chapter23.theorem_1_volume (f : Polynomial ℂ) (hf : f.Monic) (hn : 1 ≤ f.natDegree) : MeasureTheory.volume (Complex.re '' {z : ℂ | ‖Polynomial.eval z f‖ ≤ 2}) ≤ 4

Theorem 1, measure version: the projection of C = {z | |f z| ≤ 2} onto the real axis has Lebesgue (outer) measure at most 4.

Contents of former file Chapter_23/Appendix.lean

Appendix of Chapter 23: cosine polynomials

• Equation (7): cos nθ is a polynomial in cos θ of degree n with leading coefficient 2^(n-1) (the Chebyshev polynomial T_n), and the binomial identity ∑_{ℓ} (n choose 2ℓ) = 2^(n-1) used to compute this leading coefficient.
• Step (A): p(cos θ) is a cosine polynomial ∑ b_k cos kθ whose leading coefficient is b_n = 1/2^(n-1).
• Step (B): a cosine polynomial h(θ) = ∑_{k ≤ n} λ_k cos kθ satisfies |λ_n| ≤ max |h(θ)|.
• Chebyshev's theorem obtained from (A) and (B), as in the book.
• The polynomials x, x² - 1/2, x³ - 3/4 x, and in general T_n(x) / 2^(n-1), attain equality in Chebyshev's theorem.

theorem Chapter23.cos_nat_mul_eq_poly (n : ℕ) : ∃ (P : Polynomial ℝ), P.natDegree = n ∧ P.leadingCoeff = 2 ^ (n - 1) ∧ ∀ (θ : ℝ), Polynomial.eval (Real.cos θ) P = Real.cos (↑n * θ)

Equation (7): cos nθ = c_n (cos θ)^n + ⋯ + c_0 with c_n = 2^(n-1).

theorem Chapter23.sum_even_choose (n : ℕ) (hn : 0 < n) : ∑ k ∈ Finset.range (n + 1) with Even k, n.choose k = 2 ^ (n - 1)

The margin identity: ∑_{k even} (n choose k) = 2^(n-1) for n > 0.

theorem Chapter23.exists_chebyshev_expansion (n : ℕ) (p : Polynomial ℝ) (hp : p.natDegree ≤ n) : ∃ (b : ℕ → ℝ), p = ∑ k ∈ Finset.range (n + 1), Polynomial.C (b k) * Polynomial.Chebyshev.T ℝ ↑k ∧ b n * 2 ^ (n - 1) = p.coeff n

Every real polynomial of degree ≤ n is a linear combination of the Chebyshev polynomials T_0, …, T_n, and the coefficient of T_n is coeff n / 2^(n-1).

theorem Chapter23.step_A (p : Polynomial ℝ) (hp : p.Monic) : ∃ (b : ℕ → ℝ), b p.natDegree = 1 / 2 ^ (p.natDegree - 1) ∧ ∀ (θ : ℝ), Polynomial.eval (Real.cos θ) p = ∑ k ∈ Finset.range (p.natDegree + 1), b k * Real.cos (↑k * θ)

Step (A). For a real polynomial p of degree n ≥ 1 with leading coefficient 1, g(θ) = p(cos θ) is a cosine polynomial b_n cos nθ + ⋯ + b_1 cos θ + b_0 whose leading coefficient is b_n = 1/2^(n-1).

theorem Chapter23.chebyshev_sum_natDegree_leadingCoeff (n : ℕ) (hn : 1 ≤ n) (l : ℕ → ℝ) (hl : l n ≠ 0) : (∑ k ∈ Finset.range (n + 1), Polynomial.C (l k) * Polynomial.Chebyshev.T ℝ ↑k).natDegree = n ∧ (∑ k ∈ Finset.range (n + 1), Polynomial.C (l k) * Polynomial.Chebyshev.T ℝ ↑k).leadingCoeff = l n * 2 ^ (n - 1)

The polynomial ∑_{k ≤ n} λ_k T_k has degree n and leading coefficient λ_n 2^(n-1) if λ_n ≠ 0 and n ≥ 1.

theorem Chapter23.step_B (n : ℕ) (l : ℕ → ℝ) : ∃ (θ : ℝ), |l n| ≤ |∑ k ∈ Finset.range (n + 1), l k * Real.cos (↑k * θ)|

Step (B). For any cosine polynomial h(θ) = λ_n cos nθ + ⋯ + λ_1 cos θ + λ_0, we have |λ_n| ≤ max_θ |h(θ)|.

theorem Chapter23.chebyshev_of_A_B (p : Polynomial ℝ) (hp : p.Monic) : ∃ x ∈ Set.Icc (-1) 1, 1 / 2 ^ (p.natDegree - 1) ≤ |Polynomial.eval x p|

Chebyshev's theorem deduced from (A) and (B), following the book: apply (B) to the cosine polynomial g(θ) = p(cos θ) provided by (A).

theorem Chapter23.chebyshev_equality (n : ℕ) : (Polynomial.C (1 / 2 ^ (n - 1)) * Polynomial.Chebyshev.T ℝ ↑n).Monic ∧ (Polynomial.C (1 / 2 ^ (n - 1)) * Polynomial.Chebyshev.T ℝ ↑n).natDegree = n ∧ (∀ x ∈ Set.Icc (-1) 1, |Polynomial.eval x (Polynomial.C (1 / 2 ^ (n - 1)) * Polynomial.Chebyshev.T ℝ ↑n)| ≤ 1 / 2 ^ (n - 1)) ∧ |Polynomial.eval 1 (Polynomial.C (1 / 2 ^ (n - 1)) * Polynomial.Chebyshev.T ℝ ↑n)| = 1 / 2 ^ (n - 1)

The polynomial T_n(x) / 2^(n-1) is monic of degree n and attains equality in Chebyshev's theorem: max_{-1 ≤ x ≤ 1} |T_n(x)/2^(n-1)| = 1/2^(n-1).

theorem Chapter23.chebyshev_equality_examples : ((∀ x ∈ Set.Icc (-1) 1, |x| ≤ 1) ∧ |1| = 1) ∧ ((∀ x ∈ Set.Icc (-1) 1, |x ^ 2 - 1 / 2| ≤ 1 / 2) ∧ |1 ^ 2 - 1 / 2| = 1 / 2) ∧ (∀ x ∈ Set.Icc (-1) 1, |x ^ 3 - 3 / 4 * x| ≤ 1 / 4) ∧ |1 ^ 3 - 3 / 4 * 1| = 1 / 4

The polynomials p₁(x) = x, p₂(x) = x² - 1/2 and p₃(x) = x³ - 3/4 x achieve equality in Chebyshev's theorem.

theorem Chapter23.neg_one_pow_mul_prod_chebNode_pos {n k : ℕ} (hn : 1 ≤ n) (hk : k ∈ Finset.range (n + 1)) : 0 < (-1) ^ k * ∏ j ∈ (Finset.range (n + 1)).erase k, (chebNode n k - chebNode n j)

The sign of ∏_{j ≠ k} (x_k - x_j) at the Chebyshev nodes is (-1)^k.

theorem Chapter23.chebyshev_equality_unique (p : Polynomial ℝ) (hp : p.Monic) (hn : 1 ≤ p.natDegree) (hmax : ∀ x ∈ Set.Icc (-1) 1, |Polynomial.eval x p| ≤ 1 / 2 ^ (p.natDegree - 1)) : p = Polynomial.C (1 / 2 ^ (p.natDegree - 1)) * Polynomial.Chebyshev.T ℝ ↑p.natDegree

Uniqueness of the extremal polynomial (the exercise at the end of the chapter): T_n(x) / 2^(n-1) is the only monic polynomial of degree n ≥ 1 with max_{-1 ≤ x ≤ 1} |p x| ≤ 1/2^(n-1), i.e. the only one achieving equality in Chebyshev's theorem.

Contents of former file Chapter_23/Examples.lean

Examples from Chapter 23

• For f(z) = z² - 2: x + iy ∈ C iff (x² + y²)² ≤ 4 (x² - y²), and the projection R of C onto the real axis is exactly [-2, 2], of length 4.
• For f(z) = z - c (degree 1), C is a disk of diameter 4, whose projection is an interval of length 4.
• For p(x) = x²(x - 3): P = [1 - √3, 1] ∪ [1 + √3, γ] with γ ≈ 3.2, the real root of x³ - 3x² - 2.

theorem Chapter23.sq_sub_two_mem_iff (x y : ℝ) : ‖(↑x + ↑y * Complex.I) ^ 2 - 2‖ ≤ 2 ↔ (x ^ 2 + y ^ 2) ^ 2 ≤ 4 * (x ^ 2 - y ^ 2)

For f(z) = z² - 2 and z = x + iy: |f z| ≤ 2 ↔ (x² + y²)² ≤ 4 (x² - y²).

theorem Chapter23.sq_sub_two_projection : Complex.re '' {z : ℂ | ‖z ^ 2 - 2‖ ≤ 2} = Set.Icc (-2) 2

For f(z) = z² - 2, the projection of C = {z | |f z| ≤ 2} to the real axis is [-2, 2].

theorem Chapter23.linear_projection (c : ℂ) : Complex.re '' {z : ℂ | ‖z - c‖ ≤ 2} = Set.Icc (c.re - 2) (c.re + 2)

For n = 1, i.e. f(z) = z - c, the set C is the closed disk of radius 2 (diameter 4) around c, and its projection onto the real axis is [Re c - 2, Re c + 2].

theorem Chapter23.example_two_intervals : ∃ (γ : ℝ), 3.19 < γ ∧ γ < 3.2 ∧ γ ^ 3 - 3 * γ ^ 2 - 2 = 0 ∧ {x : ℝ | |x ^ 2 * (x - 3)| ≤ 2} = Set.Icc (1 - √3) 1 ∪ Set.Icc (1 + √3) γ

For p(x) = x²(x - 3), the set P = {x | |p x| ≤ 2} consists of two intervals: P = [1 - √3, 1] ∪ [1 + √3, γ], where γ ≈ 3.2 is the real root of x³ - 3x² - 2.