Mathlib.Analysis.Finite­Polynomial­Alternation­Duality

theorem intervalSupNorm_le_iff {g : ℝ → ℝ} {r s C : ℝ} (hg : ContinuousOn g (Icc r s)) (hrs : r ≤ s) : intervalSupNorm g r s ≤ C ↔ ∀ x ∈ Icc r s, |g x| ≤ C := by -- Proof plan: apply `IsCompact.exists_sSup_image_eq_and_ge` to `x ↦ |g x|`, -- then unfold the image in `intervalSupNorm`. unfold intervalSupNorm constructor · intro h x hx exact (le_csSup (isCompact_Icc.bddAbove_image hg.abs) ⟨x, hx, rfl⟩).trans h · intro h apply csSup_le · exact ⟨|g r|, ⟨r, ⟨le_rfl, hrs⟩, rfl⟩⟩ · rintro y ⟨x, hx, rfl⟩ exact h x hx

theorem adjacentPairProduct_le_of_perm_sorted {t : ℝ} (ht : 0 ≤ t) {xs ys : List ℝ} (heven : Even xs.length) (hsorted : xs.Pairwise (fun a b => b ≤ a)) (hnonneg : ∀ a ∈ xs, 0 ≤ a) (hperm : ys.Perm xs) : adjacentPairProduct t ys ≤ adjacentPairProduct t xs := by -- Duffin--Schaeffer (1941), Lemma II. Induct on the number of pairs. -- In a nonempty permuted pairing, locate the two largest entries of `xs`. -- If they are not paired together, their partners and the four-term lemmas -- above give an exchange that does not decrease the product. Remove the -- resulting largest adjacent pair and apply the induction hypothesis to the -- remaining sorted tail. Nonnegativity makes multiplication monotone. have heven_ys : Even ys.length := hperm.length_eq ▸ heven rw [← pairedProduct_listPairs t ys] apply pairedProduct_le_of_perm_sorted ht heven hsorted hnonneg rw [pairedEntries_listPairs_of_even heven_ys] exact hperm

theorem exists_alternationDualCertificate {f : ℝ → ℝ} {r s : ℝ} (hrs : r < s) (hf : ContinuousOn f (Icc r s)) (L : ℕ) : Nonempty (AlternationDualCertificate f r s L) := by classical obtain ⟨E⟩ := exists_equioscillationWitness hrs hf L let w : Fin (L + 2) → ℝ := normalizedLagrangeWeight E.nodes have hwinj : Injective E.nodes := E.nodes_strictMono.injective have hwalt (i : Fin (L + 2)) : w i = (-1 : ℝ) ^ (L + 1 - (i : ℕ)) * |w i| := normalizedLagrangeWeight_alternates E.nodes_strictMono i have hpow (i : Fin (L + 2)) : (-1 : ℝ) ^ (L + 1 - (i : ℕ)) * (-1 : ℝ) ^ (i : ℕ) = (-1 : ℝ) ^ (L + 1) := by rw [← pow_add, Nat.sub_add_cancel] omega have hpoly : ∑ i, w i * E.approximant.eval (E.nodes i) = 0 := sum_normalizedLagrangeWeight_mul_eval_eq_zero hwinj E.approximant_degree have htarget : ∑ i, w i * f (E.nodes i) = E.orientation * (-1 : ℝ) ^ (L + 1) * bestUniformApproxError f r s L := by calc ∑ i, w i * f (E.nodes i) = (∑ i, w i * (f (E.nodes i) - E.approximant.eval (E.nodes i))) + ∑ i, w i * E.approximant.eval (E.nodes i) := by rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro i _ ring _ = ∑ i, w i * (f (E.nodes i) - E.approximant.eval (E.nodes i)) := by rw [hpoly, add_zero] _ = ∑ i, (E.orientation * (-1 : ℝ) ^ (L + 1) * bestUniformApproxError f r s L) * |w i| := by apply Finset.sum_congr rfl intro i _ rw [E.equioscillation i] calc w i * (E.orientation * (-1 : ℝ) ^ (i : ℕ) * bestUniformApproxError f r s L) = E.orientation * ((-1 : ℝ) ^ (L + 1 - (i : ℕ)) * (-1 : ℝ) ^ (i : ℕ)) * bestUniformApproxError f r s L * |w i| := by conv_lhs => rw [hwalt i] ring _ = (E.orientation * (-1 : ℝ) ^ (L + 1) * bestUniformApproxError f r s L) * |w i| := by rw [hpow i] _ = (E.orientation * (-1 : ℝ) ^ (L + 1) * bestUniformApproxError f r s L) * ∑ i, |w i| := by rw [Finset.mul_sum] _ = E.orientation * (-1 : ℝ) ^ (L + 1) * bestUniformApproxError f r s L := by rw [sum_abs_normalizedLagrangeWeight_eq_one hwinj, mul_one] exact ⟨ { approximant := E.approximant approximant_degree := E.approximant_degree approximant_best := E.approximant_best nodes := E.nodes nodes_strictMono := E.nodes_strictMono nodes_mem := E.nodes_mem orientation := E.orientation orientation_eq := E.orientation_eq equioscillation := E.equioscillation weights := w weights_eq := fun _ ↦ rfl weights_alternate := hwalt weights_normalized := sum_abs_normalizedLagrangeWeight_eq_one hwinj moments_zero := fun _ hj ↦ sum_normalizedLagrangeWeight_mul_pow_eq_zero hwinj hj target_eq := htarget }⟩

theorem intervalSupNorm_pullbackToUnitInterval (Q : Polynomial ℝ) {r s : ℝ} (hrs : r < s) : intervalSupNorm (fun t => (pullbackToUnitInterval Q r s).eval t) (-1) 1 = intervalSupNorm (fun x => Q.eval x) r s := by apply le_antisymm · rw [intervalSupNorm_le_iff (pullbackToUnitInterval Q r s).continuous.continuousOn (by norm_num : (-1 : ℝ) ≤ 1)] intro t ht rw [eval_pullbackToUnitInterval] apply (intervalSupNorm_le_iff Q.continuous.continuousOn hrs.le).mp le_rfl have hhalf : 0 ≤ (s - r) / 2 := by linarith constructor · nlinarith [mul_le_mul_of_nonneg_left ht.1 hhalf] · nlinarith [mul_le_mul_of_nonneg_left ht.2 hhalf] · rw [intervalSupNorm_le_iff Q.continuous.continuousOn hrs.le] intro x hx let t : ℝ := (2 * x - (r + s)) / (s - r) have hden : 0 < s - r := sub_pos.mpr hrs have ht : t ∈ Icc (-1 : ℝ) 1 := by constructor · apply (le_div_iff₀ hden).2 linarith [hx.1] · apply (div_le_iff₀ hden).2 linarith [hx.2] have hmap : ((s - r) / 2) * t + (r + s) / 2 = x := by dsimp [t] field_simp [ne_of_gt hden] ring have hbound := (intervalSupNorm_le_iff (pullbackToUnitInterval Q r s).continuous.continuousOn (by norm_num : (-1 : ℝ) ≤ 1)).mp le_rfl t ht rw [eval_pullbackToUnitInterval, hmap] at hbound exact hbound

theorem exists_bestPolynomial {f : ℝ → ℝ} {r s : ℝ} (hrs : r < s) (hf : ContinuousOn f (Icc r s)) (L : ℕ) : ∃ Q : Polynomial ℝ, Q.natDegree ≤ L ∧ uniformApproxError f r s Q = bestUniformApproxError f r s L := by letI : CompactSpace (Icc r s) := isCompact_iff_compactSpace.mp isCompact_Icc letI : Nonempty (Icc r s) := ⟨⟨r, left_mem_Icc.mpr hrs.le⟩⟩ let V := boundedPolynomialFunctions r s L let g := targetOnInterval f r s hf let R : ℝ := 2 * ‖g‖ + 1 let B : Set V := closedBall 0 R have hR : 0 ≤ R := by dsimp [R] positivity have hBcompact : IsCompact B := by exact ProperSpace.isCompact_closedBall 0 R have hzero : (0 : V) ∈ B := by simp [B, hR] have hcontinuous : Continuous (fun q : V => ‖g - (q : C(Icc r s, ℝ))‖) := by fun_prop obtain ⟨q, hqB, hqmin⟩ := hBcompact.exists_isMinOn ⟨0, hzero⟩ hcontinuous.continuousOn have hqzero : ‖g - (q : C(Icc r s, ℝ))‖ ≤ ‖g‖ := by simpa using hqmin hzero have hglobal (u : V) : ‖g - (q : C(Icc r s, ℝ))‖ ≤ ‖g - (u : C(Icc r s, ℝ))‖ := by by_cases hu : u ∈ B · exact hqmin hu · have hunorm : R < ‖u‖ := by simpa [B, Metric.mem_closedBall, dist_zero_left, not_le] using hu have hdiff := norm_sub_norm_le (u : C(Icc r s, ℝ)) g have hlower : ‖g‖ ≤ ‖(u : C(Icc r s, ℝ)) - g‖ := by dsimp [R] at hunorm change ‖(u : C(Icc r s, ℝ))‖ - ‖g‖ ≤ ‖(u : C(Icc r s, ℝ)) - g‖ at hdiff linarith rw [norm_sub_rev] at hlower exact hqzero.trans hlower obtain ⟨p, hpq⟩ := q.property have hpDegreeLE : (p : Polynomial ℝ) ∈ Polynomial.degreeLE ℝ L := by rw [← Polynomial.degreeLT_succ_eq_degreeLE] exact p.property have hpdeg : (p : Polynomial ℝ).natDegree ≤ L := Polynomial.natDegree_le_iff_degree_le.mpr (Polynomial.mem_degreeLE.mp hpDegreeLE) have hpq' : (p : Polynomial ℝ).toContinuousMapOn (Icc r s) = (q : C(Icc r s, ℝ)) := hpq have hminpoly : ∀ u : Polynomial ℝ, u.natDegree ≤ L → uniformApproxError f r s p ≤ uniformApproxError f r s u := by intro u hu have huDegreeLE : u ∈ Polynomial.degreeLE ℝ L := Polynomial.mem_degreeLE.mpr (Polynomial.natDegree_le_iff_degree_le.mp hu) have huDegreeLT : u ∈ Polynomial.degreeLT ℝ (L + 1) := by rw [Polynomial.degreeLT_succ_eq_degreeLE] simpa [Nat.succ_eq_add_one] using huDegreeLE let uv : V := ⟨u.toContinuousMapOn (Icc r s), ⟨⟨u, huDegreeLT⟩, rfl⟩⟩ rw [uniformApproxError_eq_norm hrs.le hf, uniformApproxError_eq_norm hrs.le hf] simpa [g, hpq'] using hglobal uv refine ⟨p, hpdeg, le_antisymm ?_ ?_⟩ · unfold bestUniformApproxError apply le_csInf · exact ⟨uniformApproxError f r s 0, 0, by simp⟩ · rintro e ⟨u, hu, rfl⟩ exact hminpoly u hu · unfold bestUniformApproxError apply csInf_le · refine ⟨0, ?_⟩ rintro e ⟨u, -, rfl⟩ exact uniformApproxError_nonneg hrs.le u · exact ⟨p, hpdeg, rfl⟩

theorem exists_int_abs_sub_mul_pi_div_le {L : ℕ} (hL : 0 < L) (θ : ℝ) : ∃ m : ℤ, |θ - (m : ℝ) * (pi / (L : ℝ))| ≤ pi / (2 * (L : ℝ)) := by -- Choose the nearest integer to `θ / (π/L)`. Mathlib's floor/round -- bounds give a remainder in `[-1/2,1/2]`; positivity of `π/L` then -- rescales that bound to the displayed interval. let d : ℝ := pi / (L : ℝ) have hd : 0 < d := div_pos Real.pi_pos (by exact_mod_cast hL) refine ⟨round (θ / d), ?_⟩ have hr : |θ / d - (round (θ / d) : ℝ)| ≤ (1 : ℝ) / 2 := abs_sub_round (θ / d) have heq : θ - (round (θ / d) : ℝ) * d = d * (θ / d - (round (θ / d) : ℝ)) := by field_simp rw [show pi / (L : ℝ) = d by rfl, heq, abs_mul, abs_of_pos hd] calc d * |θ / d - (round (θ / d) : ℝ)| ≤ d * ((1 : ℝ) / 2) := mul_le_mul_of_nonneg_left hr hd.le _ = pi / (2 * (L : ℝ)) := by dsimp [d] field_simp

theorem adjacentPairProduct_chebyshevPairedChordList (L : ℕ) (θ y : ℝ) : adjacentPairProduct (4 * y ^ 2) (chebyshevPairedChordList L θ) = ∏ k ∈ range L, 4 * ‖((Real.cos θ - chebyshevZero L k : ℝ) : ℂ) + (y : ℂ) * Complex.I‖ ^ 2 := by have pair_identity (α : ℝ) : (2 - 2 * Real.cos (θ + α)) * (2 - 2 * Real.cos (θ - α)) + 4 * y ^ 2 = 4 * ‖((Real.cos θ - Real.cos α : ℝ) : ℂ) + (y : ℂ) * Complex.I‖ ^ 2 := by rw [Complex.sq_norm, Complex.normSq_add_mul_I] rw [Real.cos_add, Real.cos_sub] nlinarith [Real.sin_sq_add_cos_sq θ, Real.sin_sq_add_cos_sq α] rw [chebyshevPairedChordList, adjacentPairProduct_flatMap_pairs] rw [Multiset.prod_map_toList] apply Finset.prod_congr rfl intro k hk rw [cosineChordSq, chebyshevZero] exact pair_identity (chebyshevRootAngle L k)

theorem exists_rootProduct_dominating_abscissa_past_chebyshevZeros {L : ℕ} (hL : 0 < L) {x : ℝ} (hx : x ∈ Icc (-1) 1) (y : ℝ) : ∃ x₀ ∈ Icc (-1 : ℝ) 1, (∀ k ∈ range L, chebyshevZero L k ≤ x₀) ∧ (∏ k ∈ range L, ‖((x - chebyshevZero L k : ℝ) : ℂ) + (y : ℂ) * Complex.I‖) ≤ ∏ k ∈ range L, ‖((x₀ - chebyshevZero L k : ℝ) : ℂ) + (y : ℂ) * Complex.I‖ := by let θ := arccos x rcases exists_int_abs_sub_mul_pi_div_le hL θ with ⟨m, hm⟩ let φ := θ - (m : ℝ) * (pi / (L : ℝ)) have hφ : |φ| ≤ pi / (2 * (L : ℝ)) := by simpa [φ] using hm have hshift : φ + (m : ℝ) * (pi / (L : ℝ)) = θ := by dsimp [φ] ring have hpermθφ : (chebyshevPairedChordList L θ).Perm (chebyshevPairedChordList L φ) := by rw [← hshift] exact chebyshevPairedChordList_add_int_mul_pi_div_perm hL φ m rcases exists_sorted_chebyshevChordList_with_adjacentPairProduct_eq_of_centered (t := 4 * y ^ 2) hL hφ with ⟨zs, hzsperm, hzssorted, hzsprod⟩ have hlen : (chebyshevPairedChordList L φ).length = 2 * L := by simp [chebyshevPairedChordList, Nat.mul_comm] have hzseven : Even zs.length := by rw [hzsperm.length_eq, hlen] exact ⟨L, by omega⟩ have hchord_nonneg (a : ℝ) : 0 ≤ cosineChordSq a := by unfold cosineChordSq nlinarith [Real.cos_le_one a] have hzsnonneg : ∀ a ∈ zs, 0 ≤ a := by intro a ha have ha' : a ∈ chebyshevPairedChordList L φ := hzsperm.mem_iff.mp ha simp only [chebyshevPairedChordList, List.mem_flatMap, Multiset.mem_toList, Finset.mem_val, Finset.mem_range, List.mem_cons, List.not_mem_nil, or_false] at ha' rcases ha' with ⟨k, hk, rfl | rfl⟩ · exact hchord_nonneg _ · exact hchord_nonneg _ have hadj : adjacentPairProduct (4 * y ^ 2) (chebyshevPairedChordList L θ) ≤ adjacentPairProduct (4 * y ^ 2) (chebyshevPairedChordList L φ) := by have h := adjacentPairProduct_le_of_perm_sorted (t := 4 * y ^ 2) (xs := zs) (ys := chebyshevPairedChordList L θ) (by positivity) hzseven hzssorted hzsnonneg (hpermθφ.trans hzsperm.symm) simpa [hzsprod] using h have hcosθ : cos θ = x := by dsimp [θ] exact Real.cos_arccos hx.1 hx.2 let A : ℝ := ∏ k ∈ range L, ‖((x - chebyshevZero L k : ℝ) : ℂ) + (y : ℂ) * Complex.I‖ let B : ℝ := ∏ k ∈ range L, ‖((cos φ - chebyshevZero L k : ℝ) : ℂ) + (y : ℂ) * Complex.I‖ have hfactor (u : ℕ → ℝ) : (∏ k ∈ range L, 4 * u k ^ 2) = 4 ^ L * (∏ k ∈ range L, u k) ^ 2 := by rw [Finset.prod_mul_distrib, Finset.prod_pow] simp have hsquares : 4 ^ L * A ^ 2 ≤ 4 ^ L * B ^ 2 := by rw [adjacentPairProduct_chebyshevPairedChordList, adjacentPairProduct_chebyshevPairedChordList] at hadj simpa [A, B, hcosθ, hfactor] using hadj have hA : 0 ≤ A := by dsimp [A] positivity have hB : 0 ≤ B := by dsimp [B] positivity have hAB : A ≤ B := by have hfour : 0 < (4 : ℝ) ^ L := pow_pos (by norm_num) L have hsq : A ^ 2 ≤ B ^ 2 := le_of_mul_le_mul_left hsquares hfour exact (sq_le_sq₀ hA hB).mp hsq refine ⟨Real.cos φ, ⟨Real.neg_one_le_cos φ, Real.cos_le_one φ⟩, ?_, ?_⟩ · intro k hk simp only [Finset.mem_range] at hk have hLr : 0 < (L : ℝ) := by exact_mod_cast hL have hkr : (k : ℝ) ≤ (L : ℝ) - 1 := by have : k + 1 ≤ L := by omega have hkr' : (k : ℝ) + 1 ≤ (L : ℝ) := by exact_mod_cast this linarith have hcoef : (((2 * k + 1 : ℕ) : ℝ)) = 2 * (k : ℝ) + 1 := by push_cast ring have hangle0 : 0 ≤ chebyshevRootAngle L k := by rw [chebyshevRootAngle] positivity have hanglepi : chebyshevRootAngle L k ≤ pi := by rw [chebyshevRootAngle] have hk0 : 0 ≤ (k : ℝ) := by positivity rw [hcoef] field_simp nlinarith [Real.pi_pos] have hφangle : |φ| ≤ chebyshevRootAngle L k := by apply hφ.trans rw [chebyshevRootAngle] rw [hcoef] field_simp nlinarith [Real.pi_pos] rw [chebyshevZero, ← Real.cos_abs φ] exact Real.cos_le_cos_of_nonneg_of_le_pi (abs_nonneg φ) hanglepi hφangle · simpa [A, B] using hAB

theorem exists_sorted_chebyshevChordList_with_adjacentPairProduct_eq_of_centered {L : ℕ} (hL : 0 < L) {φ t : ℝ} (hφ : |φ| ≤ pi / (2 * (L : ℝ))) : ∃ zs : List ℝ, zs.Perm (chebyshevPairedChordList L φ) ∧ zs.Pairwise (fun a b => b ≤ a) ∧ adjacentPairProduct t zs = adjacentPairProduct t (chebyshevPairedChordList L φ) := by let δ : ℝ := pi / (2 * (L : ℝ)) let u : ℝ := |φ| let a : ℕ → ℝ := fun k => cosineChordSq (chebyshevRootAngle L k + u) let b : ℕ → ℝ := fun k => cosineChordSq (chebyshevRootAngle L k - u) -- Reverse the roots, and put the larger circular distance first in each -- root block. At `u = δ`, neighboring blocks may tie. let zs := (List.range L).reverse.flatMap fun k => [a k, b k] have hLr : 0 < (L : ℝ) := by exact_mod_cast hL have hδ : 0 < δ := by dsimp [δ] positivity have hu0 : 0 ≤ u := abs_nonneg φ have huδ : u ≤ δ := hφ have hangle (k : ℕ) : chebyshevRootAngle L k = ((2 * k + 1 : ℕ) : ℝ) * δ := by simp only [chebyshevRootAngle, δ] ring have hcast (k : ℕ) : ((2 * k + 1 : ℕ) : ℝ) = 2 * (k : ℝ) + 1 := by push_cast ring have hδpi : 2 * (L : ℝ) * δ = pi := by dsimp [δ] field_simp have hbounds (k : ℕ) (hk : k < L) : 0 ≤ chebyshevRootAngle L k - u ∧ chebyshevRootAngle L k + u ≤ pi := by have hkcast : (k : ℝ) ≤ (L : ℝ) - 1 := by have hkn : k + 1 ≤ L := by omega have hkr : (k : ℝ) + 1 ≤ (L : ℝ) := by exact_mod_cast hkn linarith have hk0 : 0 ≤ (k : ℝ) := by positivity rw [hangle, hcast] constructor <;> nlinarith have hwithin (k : ℕ) (hk : k < L) : b k ≤ a k := by dsimp [a, b] apply cosineChordSq_mono_on_zero_pi · exact (hbounds k hk).1 · exact (hbounds k hk).2 · linarith have hcross (j k : ℕ) (hj : j < L) (hk : k < L) (hjk : j < k) : a j ≤ b k := by have hjk' : (j : ℝ) + 1 ≤ (k : ℝ) := by exact_mod_cast hjk dsimp [a, b] apply cosineChordSq_mono_on_zero_pi · have h := (hbounds j hj).1 rw [hangle, hcast] at h ⊢ nlinarith · have h := (hbounds k hk).2 rw [hangle, hcast] at h ⊢ nlinarith · rw [hangle, hangle, hcast, hcast] nlinarith have hsorted : zs.Pairwise (fun x y => y ≤ x) := by dsimp [zs] rw [List.pairwise_flatMap] constructor · intro k hk simp only [List.mem_reverse, List.mem_range] at hk simpa using hwithin k hk · rw [List.pairwise_reverse] have hrangePair : (List.range L).Pairwise (fun j k => j < k ∧ k < L) := by rw [List.pairwise_iff_getElem] intro i j hi hj hij simp only [List.length_range] at hi hj simp only [List.getElem_range] omega apply hrangePair.imp intro j k hjk x hx y hy have hj : j < L := lt_trans hjk.1 hjk.2 have hk : k < L := hjk.2 simp only [List.mem_cons, List.not_mem_nil, or_false] at hx hy rcases hx with rfl | rfl <;> rcases hy with rfl | rfl · exact (hcross j k hj hk hjk.1).trans (hwithin k hk) · exact (hwithin j hj).trans ((hcross j k hj hk hjk.1).trans (hwithin k hk)) · exact hcross j k hj hk hjk.1 · exact (hwithin j hj).trans (hcross j k hj hk hjk.1) -- Replacing `φ` by `|φ|` only swaps the two entries in each root block. have hpairs (k : ℕ) (hk : k < L) : [a k, b k].Perm [cosineChordSq (φ + chebyshevRootAngle L k), cosineChordSq (φ - chebyshevRootAngle L k)] := by by_cases hφ0 : 0 ≤ φ · have hu : u = φ := abs_of_nonneg hφ0 have ha : a k = cosineChordSq (φ + chebyshevRootAngle L k) := by dsimp [a] rw [hu] congr 1 <;> ring have hb : b k = cosineChordSq (φ - chebyshevRootAngle L k) := by dsimp [b] rw [hu] rw [show chebyshevRootAngle L k - φ = -(φ - chebyshevRootAngle L k) by ring] simp only [cosineChordSq] rw [Real.cos_neg] rw [ha, hb] · have hφ0' : φ ≤ 0 := le_of_not_ge hφ0 have hu : u = -φ := abs_of_nonpos hφ0' have ha : a k = cosineChordSq (φ - chebyshevRootAngle L k) := by dsimp [a] rw [hu] rw [show chebyshevRootAngle L k + -φ = -(φ - chebyshevRootAngle L k) by ring] simp only [cosineChordSq] rw [Real.cos_neg] have hb : b k = cosineChordSq (φ + chebyshevRootAngle L k) := by dsimp [b] rw [hu] congr 1 <;> ring rw [ha, hb] exact List.Perm.swap _ _ [] have hrange : (range L).val.toList.Perm (List.range L) := by refine (List.perm_ext_iff_of_nodup ?_ List.nodup_range).2 ?_ · rw [← Multiset.coe_nodup, Multiset.coe_toList] exact (range L).nodup · simp have hperm : zs.Perm (chebyshevPairedChordList L φ) := by dsimp [zs] rw [chebyshevPairedChordList] exact ((List.reverse_perm (List.range L)).flatMap (fun k hk => List.Perm.refl _)).trans <| hrange.symm.flatMap fun k hk => hpairs k (by simpa using hk) refine ⟨zs, hperm, hsorted, ?_⟩ rw [chebyshevPairedChordList] rw [adjacentPairProduct_flatMap_two, adjacentPairProduct_flatMap_two] rw [List.map_reverse, List.prod_reverse] rw [(hrange.symm.map (fun k => a k * b k + t)).prod_eq] congr 1 apply List.map_congr_left intro k hk have hp := (hpairs k (by simpa using hk)).prod_eq simpa [mul_comm, mul_left_comm, mul_assoc] using congrArg (fun z => z + t) hp

theorem chebyshevPairedChordList_add_int_mul_pi_div_perm {L : ℕ} (hL : 0 < L) (θ : ℝ) (m : ℤ) : (chebyshevPairedChordList L (θ + (m : ℝ) * (pi / (L : ℝ)))).Perm (chebyshevPairedChordList L θ) := by induction m using Int.induction_on with | zero => simp | @succ i ih => have hstep := chebyshevPairedChordList_add_pi_div_perm hL (θ + (i : ℝ) * (pi / (L : ℝ))) have heq : θ + (((i : ℤ) + 1 : ℤ) : ℝ) * (pi / (L : ℝ)) = θ + (i : ℝ) * (pi / (L : ℝ)) + pi / (L : ℝ) := by norm_num ring rw [heq] exact hstep.trans ih | @pred i ih => have hstep := chebyshevPairedChordList_add_pi_div_perm hL (θ + ((-(i : ℤ) - 1 : ℤ) : ℝ) * (pi / (L : ℝ))) have heq : θ + ((-(i : ℤ) - 1 : ℤ) : ℝ) * (pi / (L : ℝ)) + pi / (L : ℝ) = θ + ((-(i : ℤ) : ℤ) : ℝ) * (pi / (L : ℝ)) := by norm_num ring rw [heq] at hstep exact hstep.symm.trans ih

theorem sum_abs_chebyshevDerivativeWeight_le_sq {L : ℕ} (hL : 0 < L) {x : ℝ} (hx : x ∈ Icc (-1) 1) : ∑ i ∈ range (L + 1), |chebyshevDerivativeWeight L x i| ≤ (L : ℝ) ^ 2 := by classical let s : Finset ℕ := range (L + 1) let v : ℕ → ℝ := Polynomial.Chebyshev.node L let c : ℕ → ℝ := fun i ↦ chebyshevDerivativeWeight L x i let ε : ℕ → ℝ := fun i ↦ if c i < 0 then -1 else 1 let P : Polynomial ℝ := Lagrange.interpolate s v ε have hinj : InjOn v s := Polynomial.Chebyshev.strictAntiOn_node L |>.injOn have hPdeg : P.natDegree ≤ L := by rw [Polynomial.natDegree_le_iff_degree_le] have hdegree := Lagrange.degree_interpolate_le ε hinj simpa [P, s] using hdegree have hPnodes : ∀ i, i ≤ L → |P.eval (Polynomial.Chebyshev.node L i)| ≤ 1 := by intro i hi have his : i ∈ s := by simp [s, hi] rw [show Polynomial.Chebyshev.node L i = v i from rfl] rw [show P.eval (v i) = ε i by exact Lagrange.eval_interpolate_at_node ε hinj his] simp only [ε] split <;> norm_num have hroot : ∀ z : ℝ, (T ℝ (L : ℤ)).eval z = 0 → |P.derivative.eval z| ≤ |(T ℝ (L : ℤ)).derivative.eval z| := by intro z hz exact abs_eval_derivative_le_chebyshev_at_root hL P hPdeg hPnodes hz have hPder : P.derivative.eval x = ∑ i ∈ s, ε i * c i := by rw [eval_derivative_eq_sum_chebyshevDerivativeWeight P hPdeg x] apply Finset.sum_congr rfl intro i hi rw [show P.eval (Polynomial.Chebyshev.node L i) = ε i by exact Lagrange.eval_interpolate_at_node ε hinj hi] have hmass : ∑ i ∈ s, |c i| = P.derivative.eval x := by rw [hPder] apply Finset.sum_congr rfl intro i hi by_cases hci : c i < 0 · simp [ε, hci, abs_of_neg hci] · have hci' : 0 ≤ c i := le_of_not_gt hci simp [ε, hci, abs_of_nonneg hci'] calc ∑ i ∈ range (L + 1), |chebyshevDerivativeWeight L x i| = P.derivative.eval x := by simpa [s, c] using hmass _ ≤ |P.derivative.eval x| := le_abs_self _ _ ≤ (L : ℝ) ^ 2 := abs_eval_derivative_le_sq_of_chebyshev_root_control hL P hPdeg hroot hx

theorem abs_eval_derivative_le_sq_of_chebyshev_root_control {L : ℕ} (hL : 0 < L) (Q : Polynomial ℝ) (hQ : Q.natDegree ≤ L) (hroots : ∀ z : ℝ, (T ℝ (L : ℤ)).eval z = 0 → |Q.derivative.eval z| ≤ |(T ℝ (L : ℤ)).derivative.eval z|) {x : ℝ} (hx : x ∈ Icc (-1) 1) : |Q.derivative.eval x| ≤ (L : ℝ) ^ 2 := by have hendpoint := abs_eval_derivative_le_chebyshev_endpoint_of_root_control hL Q hQ hroots hx (fun y ↦ norm_eval_chebyshev_le_endpoint_vertical hx y) rw [Polynomial.Chebyshev.derivative_T_eval_one] at hendpoint simpa [abs_of_nonneg (sq_nonneg (L : ℝ))] using hendpoint

theorem norm_eval_chebyshev_eq_leadingCoeff_mul_rootProduct {L : ℕ} (hL : 0 < L) (x y : ℝ) : ‖(T ℂ (L : ℤ)).eval ((x : ℂ) + (y : ℂ) * Complex.I)‖ = ‖(T ℂ (L : ℤ)).leadingCoeff‖ * ∏ k ∈ range L, ‖((x - chebyshevZero L k : ℝ) : ℂ) + (y : ℂ) * Complex.I‖ := by let z : ℂ := (x : ℂ) + (y : ℂ) * Complex.I let pR : ℝ[X] := T ℝ (L : ℤ) let pC : ℂ[X] := T ℂ (L : ℤ) have hinj : InjOn (fun k : ℕ => cos ((2 * (k : ℝ) + 1) * pi / (2 * (L : ℝ)))) (range L) := (range L).nodup_map_iff_injOn.mp (Polynomial.Chebyshev.roots_T_real_nodup L) have hcard : pR.roots.card = pR.natDegree := by dsimp [pR] rw [Polynomial.Chebyshev.roots_T_real, Finset.card_val, Finset.card_image_of_injOn hinj, Finset.card_range, Polynomial.Chebyshev.natDegree_T, Int.natAbs_natCast] have hrootsMap : pR.roots.map ofReal = (pR.map Complex.ofRealHom).roots := by simpa using (Polynomial.roots_map_of_injective_of_card_eq_natDegree (p := pR) (f := Complex.ofRealHom) Complex.ofReal_injective hcard) have hmap : pR.map Complex.ofRealHom = pC := by dsimp [pR, pC] exact Polynomial.Chebyshev.map_T Complex.ofRealHom (L : ℤ) have hroots : pC.roots = (range L).val.map (fun k : ℕ => (chebyshevZero L k : ℂ)) := by rw [← hmap, ← hrootsMap] dsimp [pR] rw [Polynomial.Chebyshev.roots_T_real, Finset.image_val_of_injOn hinj, Multiset.map_map] congr 1 funext k apply congrArg ofReal apply congrArg cos norm_num [chebyshevZero, chebyshevRootAngle, Nat.cast_add, Nat.cast_mul] have hcardC : pC.roots.card = pC.natDegree := by rw [hroots, Multiset.card_map, Finset.card_val, Finset.card_range] dsimp [pC] rw [Polynomial.Chebyshev.natDegree_T, Int.natAbs_natCast] have hfac := Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C (p := pC) hcardC have heval := congrArg (eval z) hfac rw [eval_mul, eval_C, eval_multiset_prod, hroots] at heval simp only [Multiset.map_map, Function.comp_apply, eval_sub, eval_X, eval_C] at heval change pC.leadingCoeff * (∏ k ∈ range L, (z - (chebyshevZero L k : ℂ))) = pC.eval z at heval rw [← heval, norm_mul, Complex.norm_prod] congr 1 apply Finset.prod_congr rfl intro k hk congr 1 dsimp [z] push_cast ring

theorem exists_chebyshevRootReflection {L : ℕ} (hL : 0 < L) (Q : Polynomial ℝ) (hQ : Q.natDegree ≤ L) (hroots : ∀ z : ℝ, (T ℝ (L : ℤ)).eval z = 0 → |Q.derivative.eval z| ≤ |(T ℝ (L : ℤ)).derivative.eval z|) (x : ℝ) : ∃ R : Polynomial ℂ, R.natDegree ≤ L ∧ (∀ y : ℝ, ‖R.eval ((y : ℂ) * I)‖ = ‖(T ℂ (L : ℤ)).eval ((x : ℂ) + (y : ℂ) * I)‖) ∧ |Q.derivative.eval x| ≤ ‖R.derivative.eval 0‖ := by have hPnat : Q.derivative.natDegree < L := by refine lt_of_le_of_lt ((Polynomial.natDegree_derivative_le Q).trans (Nat.sub_le_sub_right hQ 1)) ?_ exact Nat.sub_lt hL Nat.zero_lt_one have hPdegree : Q.derivative.degree < (L : WithBot ℕ) := by by_cases hP : Q.derivative = 0 · simp [hP] · exact (Polynomial.natDegree_lt_iff_degree_lt hP).mp hPnat have hinterp : Q.derivative = Lagrange.interpolate (range L) (reflectionRoot L) (fun i => Q.derivative.eval (reflectionRoot L i)) := by apply Lagrange.eq_interpolate (reflectionRoot_injOn L) simpa using hPdegree refine ⟨reflectedRootProduct L x, reflectedRootProduct_natDegree_le L x, reflectedRootProduct_vertical_norm L x, ?_⟩ rw [hinterp, Lagrange.interpolate_apply, eval_finsetSum] simp only [eval_mul, eval_C] calc |∑ i ∈ range L, Q.derivative.eval (reflectionRoot L i) * (Lagrange.basis (range L) (reflectionRoot L) i).eval x| ≤ ∑ i ∈ range L, |Q.derivative.eval (reflectionRoot L i) * (Lagrange.basis (range L) (reflectionRoot L) i).eval x| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ i ∈ range L, |(T ℝ (L : ℤ)).derivative.eval (reflectionRoot L i) * (Lagrange.basis (range L) (reflectionRoot L) i).eval x| := by apply Finset.sum_le_sum intro i hi rw [abs_mul, abs_mul] exact mul_le_mul_of_nonneg_right (hroots (reflectionRoot L i) (eval_chebyshev_T_reflectionRoot (Finset.mem_range.mp hi))) (abs_nonneg _) _ = ∑ i ∈ range L, |(T ℝ (L : ℤ)).leadingCoeff| * ∏ j ∈ (range L).erase i, |x - reflectionRoot L j| := by apply Finset.sum_congr rfl intro i hi rw [chebyshev_derivative_mul_lagrangeBasis (Finset.mem_range.mp hi), abs_mul, Finset.abs_prod] _ = |(T ℝ (L : ℤ)).leadingCoeff| * ∑ i ∈ range L, ∏ j ∈ (range L).erase i, |x - reflectionRoot L j| := by rw [Finset.mul_sum] _ = ‖(reflectedRootProduct L x).derivative.eval 0‖ := (reflectedRootProduct_derivative_norm L x).symm

theorem norm_eval_chebyshev_le_endpoint_vertical {L : ℕ} {x : ℝ} (hx : x ∈ Icc (-1) 1) (y : ℝ) : ‖(T ℂ (L : ℤ)).eval ((x : ℂ) + (y : ℂ) * I)‖ ≤ ‖(T ℂ (L : ℤ)).eval ((1 : ℂ) + (y : ℂ) * I)‖ := by by_cases hL : L = 0 · subst L simp have hLpos : 0 < L := Nat.pos_of_ne_zero hL calc ‖(T ℂ (L : ℤ)).eval ((x : ℂ) + (y : ℂ) * I)‖ = ‖(T ℂ (L : ℤ)).leadingCoeff‖ * ∏ k ∈ range L, ‖((x - chebyshevZero L k : ℝ) : ℂ) + (y : ℂ) * Complex.I‖ := norm_eval_chebyshev_eq_leadingCoeff_mul_rootProduct hLpos x y _ ≤ ‖(T ℂ (L : ℤ)).leadingCoeff‖ * ∏ k ∈ range L, ‖((1 - chebyshevZero L k : ℝ) : ℂ) + (y : ℂ) * Complex.I‖ := mul_le_mul_of_nonneg_left (prod_norm_sub_chebyshevZero_le_endpoint hLpos hx y) (norm_nonneg _) _ = ‖(T ℂ (L : ℤ)).eval ((1 : ℂ) + (y : ℂ) * I)‖ := by simpa using (norm_eval_chebyshev_eq_leadingCoeff_mul_rootProduct hLpos (1 : ℝ) y).symm

theorem abs_eval_derivative_le_chebyshev_at_root {L : ℕ} (hL : 0 < L) (Q : Polynomial ℝ) (hQ : Q.natDegree ≤ L) (hnodes : ∀ i, i ≤ L → |Q.eval (Polynomial.Chebyshev.node L i)| ≤ 1) {x : ℝ} (hx : (T ℝ (L : ℤ)).eval x = 0) : |Q.derivative.eval x| ≤ |(T ℝ (L : ℤ)).derivative.eval x| := by classical let s := range (L + 1) let v := Polynomial.Chebyshev.node L let T : ℝ[X] := T ℝ (L : ℤ) let c : ℕ → ℝ := fun i ↦ (Lagrange.basis s v i).derivative.eval x have hQdegree : Q.degree < s.card := by simp only [s, Finset.card_range] exact lt_of_le_of_lt Q.degree_le_natDegree (by exact_mod_cast (Nat.lt_succ_of_le hQ)) have hTdegree : T.degree < s.card := by rw [show T.degree = (L : ℕ) by simp [T], show s.card = L + 1 by simp [s]] exact_mod_cast Nat.lt_succ_self L have hQinterp := Lagrange.eq_interpolate (Polynomial.Chebyshev.strictAntiOn_node L).injOn hQdegree have hTinterp := Lagrange.eq_interpolate (Polynomial.Chebyshev.strictAntiOn_node L).injOn hTdegree have hQder : Q.derivative.eval x = ∑ i ∈ s, Q.eval (v i) * c i := by calc Q.derivative.eval x = (Lagrange.interpolate s v (fun i ↦ Q.eval (v i))).derivative.eval x := by rw [← hQinterp] _ = ∑ i ∈ s, Q.eval (v i) * c i := by simp [Lagrange.interpolate_apply, eval_finsetSum, c] have hTder : T.derivative.eval x = ∑ i ∈ s, (-1 : ℝ) ^ i * c i := by calc T.derivative.eval x = (Lagrange.interpolate s v (fun i ↦ T.eval (v i))).derivative.eval x := by rw [← hTinterp] _ = ∑ i ∈ s, (-1 : ℝ) ^ i * c i := by rw [show (Lagrange.interpolate s v (fun i ↦ T.eval (v i))).derivative.eval x = ∑ i ∈ s, T.eval (v i) * c i by simp [Lagrange.interpolate_apply, eval_finsetSum, c]] apply Finset.sum_congr rfl intro i hi have hiL : i ≤ L := by simpa [s] using hi rw [show T.eval (v i) = (-1 : ℝ) ^ i by exact Polynomial.Chebyshev.eval_T_real_node (Finset.mem_Iic.mpr hiL)] have hsign : ∀ i ∈ s, 0 < (-1 : ℝ) ^ i * c i * T.derivative.eval x := by intro i hi have hiL : i ≤ L := by simpa [s] using hi exact negOnePow_mul_derivative_basis_mul_derivative_T_pos hL hx hiL have hD : T.derivative.eval x ≠ 0 := by intro hzero have := hsign 0 (by simp [s]) rw [hzero, mul_zero] at this exact lt_irrefl 0 this have hmass : ∑ i ∈ s, |c i| = |T.derivative.eval x| := by rcases lt_or_gt_of_ne hD with hneg | hpos · rw [abs_of_neg hneg, hTder, ← Finset.sum_neg_distrib] apply Finset.sum_congr rfl intro i hi have hci : (-1 : ℝ) ^ i * c i < 0 := by have := hsign i hi nlinarith calc |c i| = |(-1 : ℝ) ^ i * c i| := by rw [abs_mul, abs_neg_one_pow, one_mul] _ = -((-1 : ℝ) ^ i * c i) := abs_of_neg hci · rw [abs_of_pos hpos, hTder] apply Finset.sum_congr rfl intro i hi have hci : 0 < (-1 : ℝ) ^ i * c i := by have := hsign i hi nlinarith calc |c i| = |(-1 : ℝ) ^ i * c i| := by rw [abs_mul, abs_neg_one_pow, one_mul] _ = (-1 : ℝ) ^ i * c i := abs_of_pos hci calc |Q.derivative.eval x| = |∑ i ∈ s, Q.eval (v i) * c i| := by rw [hQder] _ ≤ ∑ i ∈ s, |Q.eval (v i) * c i| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ i ∈ s, |c i| := by apply Finset.sum_le_sum intro i hi rw [abs_mul] have hiL : i ≤ L := by simpa [s] using hi calc |Q.eval (v i)| * |c i| ≤ 1 * |c i| := mul_le_mul_of_nonneg_right (by simpa [v] using hnodes i hiL) (abs_nonneg _) _ = |c i| := one_mul _ _ = |T.derivative.eval x| := hmass

theorem duffinSchaeffer_derivative_le (Q : Polynomial ℝ) {L : ℕ} (hL : 0 < L) (hQ : Q.natDegree ≤ L) {C : ℝ} (hC : 0 ≤ C) (hnodes : ∀ i, i ≤ L → |Q.eval (node L i)| ≤ C) {x : ℝ} (hx : x ∈ Icc (-1) 1) : |Q.derivative.eval x| ≤ (L : ℝ) ^ 2 * C := by rw [eval_derivative_eq_sum_chebyshevDerivativeWeight Q hQ x] calc |∑ i ∈ range (L + 1), Q.eval (node L i) * chebyshevDerivativeWeight L x i| ≤ ∑ i ∈ range (L + 1), |Q.eval (node L i) * chebyshevDerivativeWeight L x i| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ i ∈ range (L + 1), C * |chebyshevDerivativeWeight L x i| := by apply Finset.sum_le_sum intro i hi rw [abs_mul] exact mul_le_mul_of_nonneg_right (hnodes i (Nat.le_of_lt_succ (Finset.mem_range.mp hi))) (abs_nonneg _) _ = C * ∑ i ∈ range (L + 1), |chebyshevDerivativeWeight L x i| := by rw [Finset.mul_sum] _ ≤ C * (L : ℝ) ^ 2 := mul_le_mul_of_nonneg_left (sum_abs_chebyshevDerivativeWeight_le_sq hL hx) hC _ = (L : ℝ) ^ 2 * C := by ring

theorem exists_equioscillationWitness {f : ℝ → ℝ} {r s : ℝ} (hrs : r < s) (hf : ContinuousOn f (Icc r s)) (L : ℕ) : Nonempty (EquioscillationWitness f r s L) := by classical obtain ⟨Q, hQdegree, hQbest⟩ := exists_bestPolynomial hrs hf L let g : ℝ → ℝ := fun x ↦ f x - Q.eval x have hg : ContinuousOn g (Icc r s) := hf.sub Q.continuous.continuousOn have hgError : intervalSupNorm g r s = bestUniformApproxError f r s L := by simpa [g, uniformApproxError] using hQbest have hErrorNonneg : 0 ≤ bestUniformApproxError f r s L := bestUniformApproxError_nonneg hrs hf L by_cases hErrorZero : bestUniformApproxError f r s L = 0 · let nodes : Fin (L + 2) → ℝ := fun i ↦ r + (i : ℝ) * (s - r) / (L + 1 : ℝ) have hdenom : 0 < (L + 1 : ℝ) := by positivity have hnodesMono : StrictMono nodes := by intro i j hij have hijReal : (i : ℝ) < (j : ℝ) := by exact_mod_cast hij dsimp [nodes] have hlength : 0 < s - r := sub_pos.mpr hrs simpa [add_comm] using add_lt_add_left (div_lt_div_of_pos_right (mul_lt_mul_of_pos_right hijReal hlength) hdenom) r have hnodesMem : ∀ i, nodes i ∈ Icc r s := by intro i have hi : (i : ℕ) ≤ L + 1 := by omega have hiReal : (i : ℝ) ≤ (L + 1 : ℝ) := by exact_mod_cast hi have hiNonneg : (0 : ℝ) ≤ (i : ℝ) := by positivity have hlength : 0 < s - r := sub_pos.mpr hrs dsimp [nodes] constructor · have : 0 ≤ (i : ℝ) * (s - r) / (L + 1 : ℝ) := by positivity linarith · have hfrac : (i : ℝ) / (L + 1 : ℝ) ≤ 1 := by exact (div_le_one hdenom).2 hiReal calc r + (i : ℝ) * (s - r) / (L + 1 : ℝ) = r + ((i : ℝ) / (L + 1 : ℝ)) * (s - r) := by ring _ ≤ r + 1 * (s - r) := by gcongr _ = s := by ring have hgZero : ∀ x ∈ Icc r s, g x = 0 := by intro x hx have hsup : intervalSupNorm g r s ≤ 0 := by rw [hgError, hErrorZero] have habs := (intervalSupNorm_le_iff hg hrs.le).mp hsup x hx exact abs_eq_zero.mp (le_antisymm habs (abs_nonneg _)) exact ⟨ { approximant := Q approximant_degree := hQdegree approximant_best := hQbest nodes := nodes nodes_strictMono := hnodesMono nodes_mem := hnodesMem orientation := 1 orientation_eq := inl rfl equioscillation := by intro i rw [hErrorZero] simp only [mul_zero] exact hgZero (nodes i) (hnodesMem i) }⟩ · have hErrorPos : 0 < bestUniformApproxError f r s L := lt_of_le_of_ne hErrorNonneg (Ne.symm hErrorZero) have hAlternates : ∃ nodes orientation, IsAlternatingExtrema g r s L nodes orientation := by by_contra hno obtain ⟨P, hPdegree, hPsign⟩ := exists_signPolynomial_of_no_alternatingExtrema hrs hg L (by simpa [hgError] using hErrorPos) hno obtain ⟨t, ht, himprove⟩ := exists_strict_uniformImprovement hrs.le hg (by simpa [hgError] using hErrorPos) hPsign let R : Polynomial ℝ := Q + C t * P have hRdegree : R.natDegree ≤ L := by calc R.natDegree ≤ max Q.natDegree (C t * P).natDegree := by dsimp [R] exact natDegree_add_le _ _ _ ≤ L := by apply max_le hQdegree calc (C t * P).natDegree ≤ (C t).natDegree + P.natDegree := natDegree_mul_le _ ≤ L := by simpa using hPdegree have hResidual : uniformApproxError f r s R = intervalSupNorm (fun x ↦ g x - t * P.eval x) r s := by unfold uniformApproxError congr 2 funext x simp [R, g] ring have hRlower := bestUniformApproxError_le hrs hf hRdegree have hRstrict : uniformApproxError f r s R < bestUniformApproxError f r s L := by rw [hResidual, ← hgError] exact himprove exact (not_lt_of_ge hRlower) hRstrict obtain ⟨nodes, orientation, hmono, hmem, horientation, halternates⟩ := hAlternates exact ⟨ { approximant := Q approximant_degree := hQdegree approximant_best := hQbest nodes := nodes nodes_strictMono := hmono nodes_mem := hmem orientation := orientation orientation_eq := horientation equioscillation := by intro i change g (nodes i) = _ rw [halternates i, hgError] }⟩

theorem exists_strict_uniformImprovement {g : ℝ → ℝ} {r s : ℝ} (hrs : r ≤ s) (hg : ContinuousOn g (Icc r s)) {Q : Polynomial ℝ} (hE : 0 < intervalSupNorm g r s) (hsign : ∀ x ∈ Icc r s, |g x| = intervalSupNorm g r s → 0 < g x * Q.eval x) : ∃ t : ℝ, 0 < t ∧ intervalSupNorm (fun x ↦ g x - t * Q.eval x) r s < intervalSupNorm g r s := by let E := intervalSupNorm g r s let q : ℝ → ℝ := fun x ↦ Q.eval x let p : ℝ → ℝ := fun x ↦ g x * q x have hIcc_ne : (Icc r s).Nonempty := ⟨r, le_rfl, hrs⟩ have hq : Continuous q := Q.continuous have hp : ContinuousOn p (Icc r s) := hg.mul hq.continuousOn have habs_le : ∀ x ∈ Icc r s, |g x| ≤ E := by simpa [E] using (intervalSupNorm_le_iff hg hrs).mp (le_refl (intervalSupNorm g r s)) obtain ⟨xE, hxE, hEmax, -⟩ := isCompact_Icc.exists_sSup_image_eq_and_ge hIcc_ne hg.abs have hxE_eq : |g xE| = E := by simpa [E, intervalSupNorm] using hEmax.symm have hp_xE : 0 < p xE := by exact hsign xE hxE (by simpa [E] using hxE_eq) let B : Set ℝ := {x | x ∈ Icc r s ∧ p x ≤ 0} have hBcompact : IsCompact B := by apply IsCompact.of_isClosed_subset isCompact_Icc (isClosed_Icc.isClosed_le hp continuousOn_const) exact fun _ hx ↦ hx.1 have hc : ∃ c : ℝ, c < E ∧ ∀ x ∈ Icc r s, c ≤ |g x| → 0 < p x := by by_cases hBne : B.Nonempty · obtain ⟨xb, hxb, hxb_max⟩ := hBcompact.exists_isMaxOn hBne (hg.abs.mono (fun _ hx ↦ hx.1)) have hxb_lt : |g xb| < E := by apply lt_of_le_of_ne (habs_le xb hxb.1) intro heq have : 0 < p xb := hsign xb hxb.1 (by simpa [E] using heq) linarith [hxb.2] refine ⟨(|g xb| + E) / 2, by linarith, ?_⟩ intro x hx hcx by_contra hnot have hxB : x ∈ B := ⟨hx, le_of_not_gt hnot⟩ have hmax_le : |g x| ≤ |g xb| := hxb_max hxB linarith · refine ⟨E / 2, by linarith [hE], ?_⟩ intro x hx _ by_contra hnot exact hBne ⟨x, hx, le_of_not_gt hnot⟩ obtain ⟨c, hcE, hc⟩ := hc let A : Set ℝ := {x | x ∈ Icc r s ∧ c ≤ |g x|} have hAcompact : IsCompact A := by apply IsCompact.of_isClosed_subset isCompact_Icc (isClosed_Icc.isClosed_le continuousOn_const hg.abs) exact fun _ hx ↦ hx.1 have hxEA : xE ∈ A := ⟨hxE, by linarith [hxE_eq]⟩ obtain ⟨xm, hxm, hxm_min⟩ := hAcompact.exists_isMinOn ⟨xE, hxEA⟩ (hp.mono (fun _ hx ↦ hx.1)) let m := p xm have hm : 0 < m := by exact hc xm hxm.1 hxm.2 obtain ⟨xM, hxM, hxM_max⟩ := isCompact_Icc.exists_isMaxOn hIcc_ne hq.abs.continuousOn let M := |q xM| have hq_le : ∀ x ∈ Icc r s, |q x| ≤ M := by intro x hx exact hxM_max hx have hM : 0 < M := by have hqE_ne : q xE ≠ 0 := by intro hzero simp [p, hzero] at hp_xE have hqE_pos : 0 < |q xE| := abs_pos.mpr hqE_ne exact lt_of_lt_of_le hqE_pos (hq_le xE hxE) let t := min (m / M ^ 2) ((E - c) / (2 * M)) have ht₁ : 0 < m / M ^ 2 := div_pos hm (sq_pos_of_pos hM) have ht₂ : 0 < (E - c) / (2 * M) := div_pos (sub_pos.mpr hcE) (mul_pos (by norm_num) hM) have ht : 0 < t := lt_min ht₁ ht₂ refine ⟨t, ht, ?_⟩ unfold intervalSupNorm apply (isCompact_Icc.sSup_lt_iff_of_continuous hIcc_ne ((hg.sub (hq.const_mul t).continuousOn).abs) E).2 intro x hx have hgx := habs_le x hx have hqx := hq_le x hx by_cases hhigh : c ≤ |g x| · have hxA : x ∈ A := ⟨hx, hhigh⟩ have hmp : m ≤ p x := hxm_min hxA have htM : t ≤ m / M ^ 2 := min_le_left _ _ have hq_sq : q x ^ 2 ≤ M ^ 2 := by simpa only [sq_abs] using (sq_le_sq₀ (abs_nonneg (q x)) (abs_nonneg M)).2 (by simpa [abs_of_pos hM] using hqx) have hmove : t * q x ^ 2 < 2 * p x := by have hM_sq : 0 < M ^ 2 := sq_pos_of_pos hM have ht_bound : t * M ^ 2 ≤ m := by apply (le_div_iff₀ hM_sq).mp simpa [mul_comm] using htM nlinarith [mul_le_mul_of_nonneg_left hq_sq (le_of_lt ht)] have hsquares : (g x - t * q x) ^ 2 < E ^ 2 := by calc (g x - t * q x) ^ 2 = g x ^ 2 - 2 * t * p x + t ^ 2 * q x ^ 2 := by simp only [p] ring _ < g x ^ 2 := by nlinarith _ ≤ E ^ 2 := by simpa only [sq_abs] using (sq_le_sq₀ (abs_nonneg (g x)) (le_of_lt hE)).2 hgx rw [← sq_abs] at hsquares exact (sq_lt_sq₀ (abs_nonneg _) (le_of_lt hE)).mp hsquares · have htM : t ≤ (E - c) / (2 * M) := min_le_right _ _ have ht_bound : t * M ≤ (E - c) / 2 := by have htwoM : 0 < 2 * M := mul_pos (by norm_num) hM have := (le_div_iff₀ htwoM).mp htM nlinarith calc |g x - t * q x| ≤ |g x| + |t * q x| := abs_sub _ _ _ = |g x| + t * |q x| := by rw [abs_mul, abs_of_pos ht] _ ≤ |g x| + t * M := by gcongr _ < E := by have : |g x| < c := lt_of_not_ge hhigh nlinarith [sub_pos.mpr hcE]

theorem exists_signPolynomial_of_no_alternatingExtrema {g : ℝ → ℝ} {r s : ℝ} (hrs : r < s) (hg : ContinuousOn g (Icc r s)) (L : ℕ) (hE : 0 < intervalSupNorm g r s) (hno : ¬ ∃ nodes orientation, IsAlternatingExtrema g r s L nodes orientation) : ∃ Q : Polynomial ℝ, Q.natDegree ≤ L ∧ ∀ x ∈ Icc r s, |g x| = intervalSupNorm g r s → 0 < g x * Q.eval x := by classical let E := intervalSupNorm g r s let K : Set ℝ := {x | x ∈ Icc r s ∧ |g x| = E} let P : Set ℝ := {x | x ∈ K ∧ g x = E} let N : Set ℝ := {x | x ∈ K ∧ g x = -E} have hKsub : K ⊆ Icc r s := fun _ hx ↦ hx.1 have hKcompact : IsCompact K := by apply isCompact_Icc.of_isClosed_subset · exact isClosed_Icc.isClosed_eq hg.abs continuousOn_const · exact hKsub have hKne : K.Nonempty := by obtain ⟨x, hx, hmax, -⟩ := isCompact_Icc.exists_sSup_image_eq_and_ge (nonempty_Icc.mpr hrs.le) hg.abs exact ⟨x, hx, by simpa [E, intervalSupNorm] using hmax.symm⟩ have hPcompact : IsCompact P := by apply hKcompact.of_isClosed_subset · exact hKcompact.isClosed.isClosed_eq (hg.mono hKsub) continuousOn_const · intro x hx exact hx.1 have hNcompact : IsCompact N := by apply hKcompact.of_isClosed_subset · exact hKcompact.isClosed.isClosed_eq (hg.mono hKsub) continuousOn_const · intro x hx exact hx.1 have hPN : Disjoint P N := by rw [Set.disjoint_left] intro x hxP hxN have : E = -E := hxP.2.symm.trans hxN.2 have : E = 0 := by linarith exact hE.ne' (by simpa [E] using this) have hsignK : ∀ x ∈ K, g x = boolSign (decide (0 < g x)) * E := by intro x hx have hEp : 0 < E := by simpa [E] using hE rcases (abs_eq hEp.le).mp hx.2 with hp | hn · rw [hp] simp [boolSign, hEp] · rw [hn] have hnot : ¬0 < -E := by linarith simp [boolSign, hnot] by_cases hPne : P.Nonempty case neg => refine ⟨C (-1), by simp, ?_⟩ intro x hxI hxE have hxK : x ∈ K := ⟨hxI, by simpa [E] using hxE⟩ have hxsign := hsignK x hxK have hcolor : decide (0 < g x) = false := by by_contra h have ht : decide (0 < g x) = true := Bool.eq_true_of_not_eq_false h have : g x = E := by simpa [boolSign, ht] using hxsign exact hPne ⟨x, hxK, this⟩ have hgx : g x = -E := by simpa [boolSign, hcolor] using hxsign simp only [eval_C] rw [hgx] simpa [E] using hE by_cases hNne : N.Nonempty case neg => refine ⟨C 1, by simp, ?_⟩ intro x hxI hxE have hxK : x ∈ K := ⟨hxI, by simpa [E] using hxE⟩ have hxsign := hsignK x hxK have hcolor : decide (0 < g x) = true := by by_contra h have hf : decide (0 < g x) = false := Bool.eq_false_of_not_eq_true h have : g x = -E := by simpa [boolSign, hf] using hxsign exact hNne ⟨x, hxK, this⟩ have hgx : g x = E := by simpa [boolSign, hcolor] using hxsign simp only [eval_C] rw [hgx] simpa [E] using hE obtain ⟨δ, hδ, hdist⟩ : ∃ δ : ℝ, 0 < δ ∧ ∀ x ∈ P, ∀ y ∈ N, δ < |x - y| := by obtain ⟨d, hd, hd'⟩ := Metric.exists_pos_forall_lt_edist hPcompact hNcompact.isClosed hPN refine ⟨(d : ℝ), by exact_mod_cast hd, ?_⟩ intro x hx y hy simpa [edist_dist, Real.dist_eq] using hd' x hx y hy let ε := δ / 5 have hε : 0 < ε := by dsimp [ε]; positivity obtain ⟨t, ht⟩ := hKcompact.elim_finite_subcover (fun z : K ↦ ball (z : ℝ) ε) (fun _ ↦ Metric.isOpen_ball) (by intro x hx rw [Set.mem_iUnion] exact ⟨⟨x, hx⟩, Metric.mem_ball_self hε⟩) let centers : Finset ℝ := t.map ⟨Subtype.val, Subtype.val_injective⟩ let l : List ℝ := centers.sort let color : ℝ → Bool := fun x ↦ decide (0 < g x) have hlK : ∀ c ∈ l, c ∈ K := by intro c hc have hc' : c ∈ centers := (Finset.mem_sort (· ≤ ·)).mp hc rcases Finset.mem_map.mp hc' with ⟨z, hz, rfl⟩ exact z.2 have hcover : ∀ x ∈ K, ∃ c ∈ l, |x - c| < ε := by intro x hx rcases Set.mem_iUnion₂.mp (ht hx) with ⟨z, hz, hxz⟩ refine ⟨z, ?_, ?_⟩ · apply (Finset.mem_sort (· ≤ ·)).mpr exact Finset.mem_map.mpr ⟨z, hz, rfl⟩ · simpa [Metric.mem_ball, Real.dist_eq] using hxz have hlne : l ≠ [] := by intro hl obtain ⟨x, hx⟩ := hKne obtain ⟨c, hc, -⟩ := hcover x hx simpa [hl] using hc have hlsort : l.Pairwise (· < ·) := by simpa [l] using (Finset.sortedLT_sort centers).pairwise have hlsep : ∀ a ∈ l, ∀ b ∈ l, color a ≠ color b → 4 * ε < |a - b| := by intro a ha b hb hab have haK := hlK a ha have hbK := hlK b hb have hga := hsignK a haK have hgb := hsignK b hbK dsimp [color] at hab ⊢ cases hca : decide (0 < g a) <;> cases hcb : decide (0 < g b) · exfalso apply hab rw [hca, hcb] · have haN : a ∈ N := ⟨haK, by simpa [boolSign, hca] using hga⟩ have hbP : b ∈ P := ⟨hbK, by simpa [boolSign, hcb] using hgb⟩ have hd := hdist b hbP a haN rw [abs_sub_comm] at hd dsimp [ε] linarith · have haP : a ∈ P := ⟨haK, by simpa [boolSign, hca] using hga⟩ have hbN : b ∈ N := ⟨hbK, by simpa [boolSign, hcb] using hgb⟩ have hd := hdist a haP b hbN dsimp [ε] linarith · exfalso apply hab rw [hca, hcb] have hchanges : signChanges color l ≤ L := by by_contra hle have hlt : L < signChanges color l := Nat.lt_of_not_ge hle cases hl : l with | nil => simp [hl, signChanges] at hlt | cons a tail => have hsortCons : (a :: tail).Pairwise (· < ·) := by simpa [hl] using hlsort obtain ⟨w, hwlen, hword, hwchain, hwmem⟩ := exists_alternating_sublist_of_lt_signChanges color hsortCons (by simpa [hl] using hlt) let nodes : Fin (L + 2) → ℝ := fun i ↦ (a :: w).get ⟨i, by simpa [hwlen] using i.isLt⟩ have hnodesK : ∀ i, nodes i ∈ K := by intro i apply hlK _ (by rw [hl]; exact hwmem _ (List.get_mem _ _)) have hnodesMono : StrictMono nodes := by intro i j hij exact hword.rel_get_of_lt hij have hnodeSigns := boolSign_get_eq_of_chain color hwchain apply hno refine ⟨nodes, boolSign (color a), hnodesMono, ?_, ?_, ?_⟩ · intro i exact hKsub (hnodesK i) · cases color a <;> simp [boolSign] · intro i have hgNode := hsignK (nodes i) (hnodesK i) have hsNode := hnodeSigns ⟨i, by simpa [hwlen] using i.isLt⟩ dsimp [nodes] at hgNode ⊢ rw [hgNode] change boolSign (color ((a :: w).get ⟨i, _⟩)) * E = boolSign (color a) * (-1 : ℝ) ^ (i : ℕ) * intervalSupNorm g r s rw [hsNode] cases hl : l with | nil => exact (hlne hl).elim | cons a tail => let Q := listSignPolynomial color (a :: tail) have hchanges' : signChanges color (a :: tail) ≤ L := by simpa [hl] using hchanges have hlsort' : (a :: tail).Pairwise (· < ·) := by simpa [hl] using hlsort have hlsep' : ∀ u ∈ a :: tail, ∀ v ∈ a :: tail, color u ≠ color v → 4 * ε < |u - v| := by simpa [hl] using hlsep refine ⟨Q, (listSignPolynomial_degree color (a :: tail)).trans hchanges', ?_⟩ have hQsign := listSignPolynomial_sign color ε (a :: tail) hε (by simp) hlsort' hlsep' intro x hxI hxE have hxK : x ∈ K := ⟨hxI, by simpa [E] using hxE⟩ obtain ⟨c, hc, hxc⟩ := hcover x hxK have hcK := hlK c hc have hsame : color x = color c := by by_contra hne have hxsign := hsignK x hxK have hcsign := hsignK c hcK dsimp [color] at hne ⊢ cases hcx : decide (0 < g x) <;> cases hcc : decide (0 < g c) · exfalso apply hne rw [hcx, hcc] · have hxN : x ∈ N := ⟨hxK, by simpa [boolSign, hcx] using hxsign⟩ have hcP : c ∈ P := ⟨hcK, by simpa [boolSign, hcc] using hcsign⟩ have hd := hdist c hcP x hxN rw [abs_sub_comm] at hd dsimp [ε] at hxc linarith · have hxP : x ∈ P := ⟨hxK, by simpa [boolSign, hcx] using hxsign⟩ have hcN : c ∈ N := ⟨hcK, by simpa [boolSign, hcc] using hcsign⟩ have hd := hdist x hxP c hcN dsimp [ε] at hxc linarith · exfalso apply hne rw [hcx, hcc] have hc' : c ∈ a :: tail := by simpa [hl] using hc have hpoly := hQsign.2 c hc' x hxc have hxsign := hsignK x hxK dsimp [Q] rw [hxsign] change 0 < boolSign (color x) * E * (listSignPolynomial color (a :: tail)).eval x rw [hsame] have hp := mul_pos (show 0 < E by simpa [E] using hE) hpoly rw [show boolSign (color c) * E * (listSignPolynomial color (a :: tail)).eval x = E * (boolSign (color c) * (listSignPolynomial color (a :: tail)).eval x) by ring] exact hp

theorem norm_eval_derivative_zero_le_chebyshev_endpoint_of_vertical {L : ℕ} (hL : 0 < L) (R : Polynomial ℂ) (hR : R.natDegree ≤ L) (hvertical : ∀ y : ℝ, ‖R.eval ((y : ℂ) * I)‖ ≤ ‖(T ℂ (L : ℤ)).eval ((1 : ℂ) + (y : ℂ) * I)‖) : ‖R.derivative.eval 0‖ ≤ |(T ℝ (L : ℤ)).derivative.eval 1| := by let S : ℂ[X] := (T ℂ (L : ℤ)).comp (X + C 1) have hSnat : S.natDegree = L := by change ((T ℂ (L : ℤ)).comp (X + C 1)).natDegree = L rw [Polynomial.natDegree_comp, Polynomial.Chebyshev.natDegree_T, Int.natAbs_natCast, Polynomial.natDegree_X_add_C, mul_one] have hSdeg : 0 < S.degree := by rw [← Polynomial.natDegree_pos_iff_degree_pos, hSnat] exact hL have hdeg : R.degree ≤ S.degree := by have hSdegree : S.degree = (L : WithBot ℕ) := by rw [Polynomial.degree_eq_natDegree (ne_zero_of_degree_gt hSdeg), hSnat] rw [hSdegree] exact Polynomial.degree_le_of_natDegree_le hR have hSroots : ∀ z : ℂ, S.eval z = 0 → z.re < 0 := by intro z hz have ht : ((1 : ℂ) + z).re < 1 := by apply chebyshev_root_re_lt_one hL simpa [S, add_comm] using hz simpa using ht have hSderiv : S.derivative.eval 0 ≠ 0 := by simp [S, Polynomial.derivative_comp, Polynomial.Chebyshev.derivative_T_eval_one] exact_mod_cast (Nat.ne_of_gt hL) have hbound := norm_eval_derivative_zero_le_of_left_half_plane_roots R S hSdeg hdeg hSroots hSderiv (by simpa [S, add_comm] using hvertical) simpa [S, Polynomial.derivative_comp, Polynomial.Chebyshev.derivative_T_eval_one] using hbound

theorem abs_eval_derivative_le_chebyshev_endpoint_of_root_control {L : ℕ} (hL : 0 < L) (Q : Polynomial ℝ) (hQ : Q.natDegree ≤ L) (hroots : ∀ z : ℝ, (T ℝ (L : ℤ)).eval z = 0 → |Q.derivative.eval z| ≤ |(T ℝ (L : ℤ)).derivative.eval z|) {x : ℝ} (hx : x ∈ Icc (-1) 1) (hvertical : ∀ y : ℝ, ‖(T ℂ (L : ℤ)).eval ((x : ℂ) + (y : ℂ) * I)‖ ≤ ‖(T ℂ (L : ℤ)).eval ((1 : ℂ) + (y : ℂ) * I)‖) : |Q.derivative.eval x| ≤ |(T ℝ (L : ℤ)).derivative.eval 1| := by obtain ⟨R, hRdeg, hRvertical, hQderiv⟩ := exists_chebyshevRootReflection hL Q hQ hroots x refine hQderiv.trans (norm_eval_derivative_zero_le_chebyshev_endpoint_of_vertical hL R hRdeg ?_) intro y rw [hRvertical y] exact hvertical y

theorem sum_normalizedLagrangeWeight_mul_eval_eq_zero {L : ℕ} {nodes : Fin (L + 2) → ℝ} (hnodes : Injective nodes) {Q : Polynomial ℝ} (hQ : Q.natDegree ≤ L) : ∑ i, normalizedLagrangeWeight nodes i * Q.eval (nodes i) = 0 := by classical let Z := ∑ k : Fin (L + 2), |Lagrange.nodalWeight Finset.univ nodes k| have hdegree : Q.degree < (Finset.univ : Finset (Fin (L + 2))).card := by apply lt_of_le_of_lt Q.degree_le_natDegree norm_cast simpa using (show Q.natDegree < L + 2 by omega) have hcoeff := Lagrange.coeff_eq_sum (s := (Finset.univ : Finset (Fin (L + 2)))) (v := nodes) hnodes.injOn (P := Q) hdegree have hcoeffzero : Q.coeff (L + 1) = 0 := Q.coeff_eq_zero_of_natDegree_lt (by omega) have hsum : ∑ i : Fin (L + 2), Lagrange.nodalWeight Finset.univ nodes i * Q.eval (nodes i) = 0 := by simpa [Lagrange.nodalWeight, div_eq_mul_inv, Finset.prod_inv_distrib, mul_comm, hcoeffzero] using hcoeff.symm change ∑ i : Fin (L + 2), (Lagrange.nodalWeight Finset.univ nodes i / Z) * Q.eval (nodes i) = 0 simp_rw [div_mul_eq_mul_div, div_eq_mul_inv] rw [← Finset.sum_mul, hsum, zero_mul]

theorem markov_derivative_Icc (Q : Polynomial ℝ) {r s : ℝ} (hrs : r < s) (L : ℕ) (hQ : Q.natDegree ≤ L) : intervalSupNorm (fun x => Q.derivative.eval x) r s ≤ (2 * (L : ℝ) ^ 2 / (s - r)) * intervalSupNorm (fun x => Q.eval x) r s := by let P := pullbackToUnitInterval Q r s have hP : P.natDegree ≤ L := (natDegree_pullbackToUnitInterval_le Q r s).trans hQ have hunit := markov_derivative_unitInterval P L hP have hden : 0 < s - r := sub_pos.mpr hrs have hhalf : 0 < (s - r) / 2 := by positivity rw [intervalSupNorm_le_iff Q.derivative.continuous.continuousOn hrs.le] intro x hx let t : ℝ := (2 * x - (r + s)) / (s - r) have ht : t ∈ Icc (-1 : ℝ) 1 := by constructor · apply (le_div_iff₀ hden).2 linarith [hx.1] · apply (div_le_iff₀ hden).2 linarith [hx.2] have hmap : ((s - r) / 2) * t + (r + s) / 2 = x := by dsimp [t] field_simp [ne_of_gt hden] ring have hpoint := ((intervalSupNorm_le_iff P.derivative.continuous.continuousOn (by norm_num : (-1 : ℝ) ≤ 1)).mp hunit) t ht have hpull : |((s - r) / 2) * Q.derivative.eval x| ≤ (L : ℝ) ^ 2 * intervalSupNorm (fun x => Q.eval x) r s := by simpa [P, derivative_eval_pullbackToUnitInterval, hmap, intervalSupNorm_pullbackToUnitInterval Q hrs] using hpoint have hscaled : ((s - r) / 2) * |Q.derivative.eval x| ≤ (L : ℝ) ^ 2 * intervalSupNorm (fun x => Q.eval x) r s := by simpa [abs_mul, abs_of_pos hhalf] using hpull calc |Q.derivative.eval x| ≤ ((L : ℝ) ^ 2 * intervalSupNorm (fun x => Q.eval x) r s) / ((s - r) / 2) := (le_div_iff₀ hhalf).2 (by simpa [mul_comm] using hscaled) _ = (2 * (L : ℝ) ^ 2 / (s - r)) * intervalSupNorm (fun x => Q.eval x) r s := by field_simp [ne_of_gt hden]

theorem markov_derivative_unitInterval (Q : Polynomial ℝ) (L : ℕ) (hQ : Q.natDegree ≤ L) : intervalSupNorm (fun x => Q.derivative.eval x) (-1) 1 ≤ (L : ℝ) ^ 2 * intervalSupNorm (fun x => Q.eval x) (-1) 1 := by rw [intervalSupNorm_le_iff Q.derivative.continuous.continuousOn (by norm_num)] intro x hx by_cases hLzero : L = 0 · subst L have hnat : Q.natDegree = 0 := Nat.eq_zero_of_le_zero hQ have hderiv : Q.derivative = 0 := Polynomial.derivative_eq_zero.mpr hnat simp [hderiv] · have hL : 0 < L := Nat.pos_of_ne_zero hLzero have hbound : ∀ y ∈ Icc (-1 : ℝ) 1, |Q.eval y| ≤ intervalSupNorm (fun z => Q.eval z) (-1) 1 := (intervalSupNorm_le_iff Q.continuous.continuousOn (by norm_num)).mp le_rfl have hC : 0 ≤ intervalSupNorm (fun z => Q.eval z) (-1) 1 := (abs_nonneg (Q.eval (node L 0))).trans (hbound _ Polynomial.Chebyshev.node_mem_Icc) exact duffinSchaeffer_derivative_le Q hL hQ hC (fun i _ ↦ hbound _ Polynomial.Chebyshev.node_mem_Icc) hx