Mathlib.Analysis.Bernstein­Szego­Trig

theorem szegoInterp_hasDerivAt (β : ℕ) (hβ : 1 ≤ β) (Q₀ Q₁ t₀ : ℝ) : HasDerivAt (fun t => szegoInterp β Q₀ Q₁ t₀ t) Q₁ t₀ := by let c : ℝ := β have hc : c ≠ 0 := by have hβne : β ≠ 0 := Nat.one_le_iff_ne_zero.mp hβ have hβneR : (β : ℝ) ≠ 0 := by exact_mod_cast hβne simpa [c] using hβneR have hu : HasDerivAt (fun t : ℝ => c * (t - t₀)) c t₀ := by simpa [c] using (((hasDerivAt_id t₀).sub_const t₀).const_mul c) have hcos : HasDerivAt (fun t : ℝ => cos (c * (t - t₀))) 0 t₀ := by have h0 := (Real.hasDerivAt_cos (c * (t₀ - t₀))).comp t₀ hu have h : HasDerivAt (fun t : ℝ => cos (c * (t - t₀))) (-sin (c * (t₀ - t₀)) * c) t₀ := h0 simpa using h have hsin : HasDerivAt (fun t : ℝ => sin (c * (t - t₀))) c t₀ := by have h0 := (Real.hasDerivAt_sin (c * (t₀ - t₀))).comp t₀ hu have h : HasDerivAt (fun t : ℝ => sin (c * (t - t₀))) (cos (c * (t₀ - t₀)) * c) t₀ := h0 simpa using h have hsum : HasDerivAt (fun t : ℝ => Q₀ * cos (c * (t - t₀)) + (Q₁ / c) * sin (c * (t - t₀))) Q₁ t₀ := by have h : HasDerivAt (fun t : ℝ => Q₀ * cos (c * (t - t₀)) + (Q₁ / c) * sin (c * (t - t₀))) _ t₀ := (hcos.const_mul Q₀).fun_add (hsin.const_mul (Q₁ / c)) simpa [hc] using h simpa [szegoInterp, c] using hsum

theorem szegoInterp_amplitude (β : ℕ) (Q₀ Q₁ t₀ : ℝ) : ∃ φ : ℝ, ∀ t, szegoInterp β Q₀ Q₁ t₀ t = sqrt (Q₀ ^ 2 + (Q₁ / (β : ℝ)) ^ 2) * cos ((β : ℝ) * (t - t₀) - φ) := by simpa [szegoInterp] using szegoInterp_amplitude_core (β : ℝ) Q₀ (Q₁ / (β : ℝ)) t₀

theorem szegoInterp_abs_le (β : ℕ) (Q₀ Q₁ t₀ t : ℝ) : |szegoInterp β Q₀ Q₁ t₀ t| ≤ sqrt (Q₀ ^ 2 + (Q₁ / (β : ℝ)) ^ 2) := by obtain ⟨φ, hφ⟩ := szegoInterp_amplitude β Q₀ Q₁ t₀ rw [hφ t, abs_mul] have hA : 0 ≤ sqrt (Q₀ ^ 2 + (Q₁ / (β : ℝ)) ^ 2) := Real.sqrt_nonneg _ calc |sqrt (Q₀ ^ 2 + (Q₁ / (β : ℝ)) ^ 2)| * |cos ((β : ℝ) * (t - t₀) - φ)| ≤ |sqrt (Q₀ ^ 2 + (Q₁ / (β : ℝ)) ^ 2)| * 1 := by apply mul_le_mul_of_nonneg_left (abs_cos_le_one _) (abs_nonneg _) _ = sqrt (Q₀ ^ 2 + (Q₁ / (β : ℝ)) ^ 2) := by rw [mul_one, abs_of_nonneg hA]

theorem IsTrigPolyLE.card_zeros_le {n : ℕ} {f : ℝ → ℝ} (hf : IsTrigPolyLE n f) (hne : ∃ t, f t ≠ 0) {c : ℝ} {S : Finset ℝ} (hS : ↑S ⊆ Ico c (c + 2 * pi)) (hzero : ∀ t ∈ S, f t = 0) : S.card ≤ 2 * n := by rcases hf with ⟨a, b, hf⟩ let P := trigPolyComplexPoly n a b let e : ℝ → ℂ := fun t => exp ((t : ℂ) * I) have hPne : P ≠ 0 := by rcases hne with ⟨t₀, ht₀⟩ intro hP have hprod : e t₀ ^ n * ((f t₀ : ℝ) : ℂ) = 0 := by simpa [P, e, hP] using (trigPolyComplexPoly_eval n a b f hf t₀).symm have hfzeroC : ((f t₀ : ℝ) : ℂ) = 0 := by exact (mul_eq_zero.mp hprod).resolve_left (pow_ne_zero _ (Complex.exp_ne_zero _)) exact ht₀ (Complex.ofReal_eq_zero.mp hfzeroC) have hinj : InjOn e (S : Set ℝ) := by intro s hs t ht hst exact exp_mul_I_injOn_Ico (hS hs) (hS ht) hst have hsubset : S.image e ⊆ P.roots.toFinset := by intro z hz rcases Finset.mem_image.mp hz with ⟨t, htS, rfl⟩ rw [Multiset.mem_toFinset] rw [Polynomial.mem_roots'] refine ⟨hPne, ?_⟩ rw [Polynomial.IsRoot.def] have heval := trigPolyComplexPoly_eval n a b f hf t have hft : ((f t : ℝ) : ℂ) = 0 := by rw [hzero t htS] norm_num simpa [P, e, hft] using heval calc S.card = (S.image e).card := (Finset.card_image_of_injOn hinj).symm _ ≤ P.roots.toFinset.card := Finset.card_le_card hsubset _ ≤ P.roots.card := Multiset.toFinset_card_le _ _ ≤ P.natDegree := Polynomial.card_roots' P _ ≤ 2 * n := trigPolyComplexPoly_natDegree_le n a b

theorem IsTrigPolyLE.card_simple_add_double_le {n : ℕ} {f : ℝ → ℝ} (hf : IsTrigPolyLE n f) (hne : ∃ t, f t ≠ 0) {c : ℝ} {S : Finset ℝ} (hS : ↑S ⊆ Ico c (c + 2 * pi)) (hzero : ∀ t ∈ S, f t = 0) {t₀ : ℝ} (ht₀mem : t₀ ∈ Ico c (c + 2 * pi)) (ht₀S : t₀ ∉ S) (hf0 : f t₀ = 0) (hderiv : HasDerivAt f 0 t₀) : S.card + 2 ≤ 2 * n := by classical rcases hf with ⟨a, b, hf⟩ let P := trigPolyComplexPoly n a b let e : ℝ → ℂ := fun t => exp ((t : ℂ) * Complex.I) have hPne : P ≠ 0 := by rcases hne with ⟨t, ht⟩ intro hP have hprod : e t ^ n * ((f t : ℝ) : ℂ) = 0 := by simpa [P, e, hP] using (trigPolyComplexPoly_eval n a b f hf t).symm have hfzeroC : ((f t : ℝ) : ℂ) = 0 := by exact (mul_eq_zero.mp hprod).resolve_left (pow_ne_zero _ (Complex.exp_ne_zero _)) exact ht (Complex.ofReal_eq_zero.mp hfzeroC) have hroot0 : P.IsRoot (e t₀) := by rw [Polynomial.IsRoot.def] have heval := trigPolyComplexPoly_eval n a b f hf t₀ have hf0C : ((f t₀ : ℝ) : ℂ) = 0 := by rw [hf0] norm_num simpa [P, e, hf0C] using heval have hder0 : P.derivative.IsRoot (e t₀) := by have hcoerce : HasDerivAt (fun t : ℝ => ((t : ℝ) : ℂ)) (1 : ℂ) t₀ := by have h0 := (hasDerivAt_id' (x := t₀)).ofReal_comp have h1 : HasDerivAt (fun t : ℝ => ((t : ℝ) : ℂ)) _ t₀ := h0 simpa using h1 have hinner : HasDerivAt (fun t : ℝ => (t : ℂ) * Complex.I) Complex.I t₀ := by simpa using hcoerce.mul_const Complex.I have he : HasDerivAt e (e t₀ * Complex.I) t₀ := by simpa [e] using hinner.cexp have hpoly : HasDerivAt (fun t : ℝ => P.eval (e t)) (P.derivative.eval (e t₀) * (e t₀ * Complex.I)) t₀ := by have h0 := (P.hasDerivAt (e t₀)).comp t₀ he have h1 : HasDerivAt (fun t : ℝ => P.eval (e t)) _ t₀ := h0 simpa using h1 have hfC : HasDerivAt (fun t : ℝ => ((f t : ℝ) : ℂ)) (0 : ℂ) t₀ := by simpa using hderiv.ofReal_comp have hprod : HasDerivAt (fun t : ℝ => (e t) ^ n * ((f t : ℝ) : ℂ)) 0 t₀ := by have hraw : HasDerivAt (fun t : ℝ => (e t) ^ n * ((f t : ℝ) : ℂ)) _ t₀ := (he.fun_pow n).fun_mul hfC simpa [hf0] using hraw have hsame : HasDerivAt (fun t : ℝ => P.eval (e t)) 0 t₀ := by refine hprod.congr_of_eventuallyEq (Filter.Eventually.of_forall ?_) intro t simpa [P, e] using trigPolyComplexPoly_eval n a b f hf t have hmul : P.derivative.eval (e t₀) * (e t₀ * Complex.I) = 0 := hpoly.unique hsame have hne : e t₀ * Complex.I ≠ 0 := by exact mul_ne_zero (Complex.exp_ne_zero _) Complex.I_ne_zero rw [Polynomial.IsRoot.def] exact (mul_eq_zero.mp hmul).resolve_right hne have hmult2 : 2 ≤ P.rootMultiplicity (e t₀) := by have hlt : 1 < P.rootMultiplicity (e t₀) := (Polynomial.one_lt_rootMultiplicity_iff_isRoot hPne).2 ⟨hroot0, hder0⟩ omega have hinj : InjOn e ((S : Set ℝ) ∪ {t₀}) := by intro s hs t ht hst have hsI : s ∈ Ico c (c + 2 * pi) := by rcases hs with hsS | rfl · exact hS hsS · exact ht₀mem have htI : t ∈ Ico c (c + 2 * pi) := by rcases ht with htS | rfl · exact hS htS · exact ht₀mem exact exp_mul_I_injOn_Ico hsI htI hst let A : Finset ℂ := S.image e have hcardA : A.card = S.card := by have hinjS : InjOn e (S : Set ℝ) := by intro s hs t ht hst exact hinj (inl hs) (inl ht) hst simpa [A] using Finset.card_image_of_injOn hinjS have he0_not_mem_A : e t₀ ∉ A := by intro hmem rcases Finset.mem_image.mp hmem with ⟨t, htS, ht⟩ have ht_eq : t = t₀ := hinj (inl htS) (inr rfl) ht exact ht₀S (ht_eq ▸ htS) have hAroots : A ⊆ P.roots.toFinset := by intro z hz rcases Finset.mem_image.mp hz with ⟨t, htS, rfl⟩ rw [Multiset.mem_toFinset] rw [Polynomial.mem_roots'] refine ⟨hPne, ?_⟩ rw [Polynomial.IsRoot.def] have heval := trigPolyComplexPoly_eval n a b f hf t have hft : ((f t : ℝ) : ℂ) = 0 := by rw [hzero t htS] norm_num simpa [P, e, hft] using heval let T : Multiset ℂ := A.val + Multiset.replicate 2 (e t₀) have hTroots : T ≤ P.roots := by rw [Multiset.le_iff_count] intro z by_cases hz0 : z = e t₀ · subst hz0 have hAcount : A.val.count (e t₀) = 0 := by rw [Multiset.count_eq_zero] simpa using he0_not_mem_A have hrootcount : 2 ≤ P.roots.count (e t₀) := by simpa [Polynomial.count_roots] using hmult2 change (A.val + Multiset.replicate 2 (e t₀)).count (e t₀) ≤ P.roots.count (e t₀) rw [Multiset.count_add, hAcount] simpa using hrootcount · by_cases hzA : z ∈ A · have hAcount : A.val.count z = 1 := by exact Multiset.count_eq_one_of_mem A.nodup hzA have hrepcount : (Multiset.replicate 2 (e t₀)).count z = 0 := by rw [Multiset.count_replicate] simp [show ¬ e t₀ = z by exact fun h => hz0 h.symm] have hrootmem : z ∈ P.roots := by exact Multiset.mem_toFinset.mp (hAroots hzA) have hrootcount : 1 ≤ P.roots.count z := by exact Multiset.count_pos.mpr hrootmem change (A.val + Multiset.replicate 2 (e t₀)).count z ≤ P.roots.count z rw [Multiset.count_add, hAcount, hrepcount] simpa using hrootcount · have hAcount : A.val.count z = 0 := by rw [Multiset.count_eq_zero] simpa using hzA have hrepcount : (Multiset.replicate 2 (e t₀)).count z = 0 := by rw [Multiset.count_replicate] simp [show ¬ e t₀ = z by exact fun h => hz0 h.symm] change (A.val + Multiset.replicate 2 (e t₀)).count z ≤ P.roots.count z rw [Multiset.count_add, hAcount, hrepcount] simp have hTcard : T.card = S.card + 2 := by simp [T, hcardA] calc S.card + 2 = T.card := hTcard.symm _ ≤ P.roots.card := Multiset.card_le_card hTroots _ ≤ P.natDegree := Polynomial.card_roots' P _ ≤ 2 * n := trigPolyComplexPoly_natDegree_le n a b

theorem hasDerivAt_cosComp (R : Polynomial ℝ) (t : ℝ) : HasDerivAt (fun s => R.eval (cos s)) (R.derivative.eval (cos t) * (-sin t)) t := by have h1 : HasDerivAt (fun x => eval x R) (R.derivative.eval (cos t)) (cos t) := R.hasDerivAt (cos t) have h2 : HasDerivAt cos (-sin t) t := Real.hasDerivAt_cos t exact h1.comp t h2

theorem szegoInterp_isTrigPolyLE (β : ℕ) (Q₀ Q₁ t₀ : ℝ) : IsTrigPolyLE β (szegoInterp β Q₀ Q₁ t₀) := by let A : ℝ := Q₀ * cos ((β : ℝ) * t₀) - (Q₁ / (β : ℝ)) * sin ((β : ℝ) * t₀) let B : ℝ := Q₀ * sin ((β : ℝ) * t₀) + (Q₁ / (β : ℝ)) * cos ((β : ℝ) * t₀) refine ⟨fun k => if k = β then A else 0, fun k => if k = β then B else 0, ?_⟩ intro t rw [Finset.sum_eq_single β] · simp only [szegoInterp, A, B, ↓reduceIte] have harg : (β : ℝ) * (t - t₀) = (β : ℝ) * t - (β : ℝ) * t₀ := by ring rw [harg, Real.cos_sub, Real.sin_sub] ring · intro k _ hne simp only [hne, ↓reduceIte, zero_mul, zero_add] · intro hnot exact elim (hnot (Finset.mem_range.mpr (Nat.lt_succ_self β)))

theorem cosComp_isTrigPolyLE (R : Polynomial ℝ) (β : ℕ) (hβ : R.natDegree ≤ β) : IsTrigPolyLE β (fun t => R.eval (cos t)) := by classical revert R induction β with | zero => intro R hR obtain ⟨c, rfl⟩ := Polynomial.natDegree_eq_zero.mp (Nat.le_zero.mp hR) simpa using isTrigPolyLE_const 0 c | succ β ih => intro R hRβ by_cases hR : R.natDegree ≤ β · exact (ih R hR).mono (Nat.le_succ β) · have hRdeg : R.natDegree = β + 1 := by exact le_antisymm hRβ (Nat.succ_le_of_lt (Nat.lt_of_not_ge hR)) let T : Polynomial ℝ := Polynomial.Chebyshev.T ℝ (((β + 1 : ℕ) : ℤ)) let P : Polynomial ℝ := T.cancelLeads R have hTdeg : T.natDegree = β + 1 := by dsimp [T] rw [Polynomial.Chebyshev.natDegree_T] apply Nat.cast_injective (R := ℤ) rw [Int.natCast_natAbs] have hnonneg : 0 ≤ ((β : ℤ) + 1) := by omega rw [abs_of_nonneg hnonneg] norm_num have hPdeg : P.natDegree ≤ β := by have hlt : P.natDegree < R.natDegree := by exact Polynomial.natDegree_cancelLeads_lt_of_natDegree_le_natDegree (by simp [hTdeg, hRdeg]) (by simp [hRdeg]) omega have hPtrig : IsTrigPolyLE (β + 1) (fun t => P.eval (cos t)) := (ih P hPdeg).mono (Nat.le_succ β) have hcostrig : IsTrigPolyLE (β + 1) (fun t => R.leadingCoeff * cos (((β + 1 : ℕ) : ℝ) * t)) := IsTrigPolyLE.const_mul R.leadingCoeff (cos_nat_mul_isTrigPolyLE (β + 1)) have hsum : IsTrigPolyLE (β + 1) (fun t => P.eval (cos t) + R.leadingCoeff * cos (((β + 1 : ℕ) : ℝ) * t)) := hPtrig.add hcostrig have hTlc_ne : T.leadingCoeff ≠ 0 := by simp [T] have hscaled : IsTrigPolyLE (β + 1) (fun t => (T.leadingCoeff)⁻¹ * (P.eval (cos t) + R.leadingCoeff * cos (((β + 1 : ℕ) : ℝ) * t))) := IsTrigPolyLE.const_mul (T.leadingCoeff)⁻¹ hsum refine hscaled.congr ?_ intro t have hTeval : T.eval (cos t) = cos (((β + 1 : ℕ) : ℝ) * t) := by simp [T] have hPeval : P.eval (cos t) = T.leadingCoeff * R.eval (cos t) - R.leadingCoeff * T.eval (cos t) := by simp [P, Polynomial.cancelLeads, hTdeg, hRdeg] rw [hPeval, hTeval] field_simp [hTlc_ne] ring

theorem szego_deriv_sq_bound (R : Polynomial ℝ) (β : ℕ) (hβ : R.natDegree ≤ β) (M : ℝ) (hM : ∀ t, |R.eval (cos t)| ≤ M) : ∀ t, (deriv (fun s => R.eval (cos s)) t) ^ 2 + (β : ℝ) ^ 2 * (R.eval (cos t)) ^ 2 ≤ (β : ℝ) ^ 2 * M ^ 2 := by intro t₀ by_cases hβ0 : β = 0 · subst β obtain ⟨c, hRc⟩ := Polynomial.natDegree_eq_zero.mp (Nat.le_zero.mp hβ) subst R have hderiv0 : deriv (fun s => eval (cos s) (Polynomial.C c)) t₀ = 0 := by rw [deriv_cosComp] simp rw [hderiv0] simp · have hβ1 : 1 ≤ β := Nat.succ_le_of_lt (Nat.pos_of_ne_zero hβ0) let Q : ℝ → ℝ := fun t => R.eval (cos t) let Q₀ : ℝ := Q t₀ let Q₁ : ℝ := deriv Q t₀ let A : ℝ := sqrt (Q₀ ^ 2 + (Q₁ / (β : ℝ)) ^ 2) have hM_nonneg : 0 ≤ M := by exact (abs_nonneg (Q t₀)).trans (hM t₀) have hβR_ne : (β : ℝ) ≠ 0 := by exact_mod_cast hβ0 have hA_nonneg : 0 ≤ A := Real.sqrt_nonneg _ have hrad_nonneg : 0 ≤ Q₀ ^ 2 + (Q₁ / (β : ℝ)) ^ 2 := by nlinarith [sq_nonneg Q₀, sq_nonneg (Q₁ / (β : ℝ))] have hamp_sq : A ^ 2 = Q₀ ^ 2 + (Q₁ / (β : ℝ)) ^ 2 := by dsimp [A] rw [Real.sq_sqrt hrad_nonneg] have hAmpBound : A ^ 2 ≤ M ^ 2 := by by_contra hnot have hgt : M ^ 2 < A ^ 2 := lt_of_not_ge hnot have hA_gt_M : M < A := by nlinarith [sq_lt_sq.mp hgt, hA_nonneg, hM_nonneg] let Sfun : ℝ → ℝ := szegoInterp β Q₀ Q₁ t₀ let g : ℝ → ℝ := fun t => Q t - Sfun t have hg_trig : IsTrigPolyLE β g := by exact (cosComp_isTrigPolyLE R β hβ).sub (szegoInterp_isTrigPolyLE β Q₀ Q₁ t₀) have hg_t₀ : g t₀ = 0 := by dsimp [g, Sfun, Q₀, Q] rw [szegoInterp_self] ring have hQ_hasDeriv : HasDerivAt Q Q₁ t₀ := by dsimp [Q₁, Q] simpa [deriv_cosComp] using (hasDerivAt_cosComp R t₀) have hS_hasDeriv : HasDerivAt Sfun Q₁ t₀ := by dsimp [Sfun] exact szegoInterp_hasDerivAt β hβ1 Q₀ Q₁ t₀ have hg_deriv : HasDerivAt g 0 t₀ := by have h := hQ_hasDeriv.fun_sub hS_hasDeriv rw [sub_self] at h exact h have hg_nonzero : ∃ t, g t ≠ 0 := by obtain ⟨φ, hφ⟩ := szegoInterp_amplitude β Q₀ Q₁ t₀ let u : ℝ := t₀ + φ / (β : ℝ) refine ⟨u, ?_⟩ have hS_u : Sfun u = A := by dsimp [Sfun] rw [hφ u] have harg : (β : ℝ) * (u - t₀) - φ = 0 := by dsimp [u] field_simp [hβR_ne] ring rw [harg, Real.cos_zero, mul_one] have hQ_le : |Q u| ≤ M := hM u intro hg0 have hQu_eq : Q u = A := by have := congrArg (fun x => x + Sfun u) hg0 simpa [g, hS_u] using this have : A ≤ M := by rw [← hQu_eq] exact le_trans (le_abs_self _) hQ_le linarith -- The remaining classical Szegő step: the interpolant `Sfun` has amplitude -- `A` (`szegoInterp_amplitude`, phase `φ`), attaining `±A` at the extrema -- `u_k = t₀ + (φ + kπ)/β`, where `Sfun (u_k) = A·(-1)^k`. Since `A > M ≥ |Q|` -- the continuous degree-≤`β` trig polynomial `g = Q − Sfun` has strictly -- alternating sign `g(u_k)·(-1)^k < 0` at the `2β + 1` consecutive extrema -- `u_m, …, u_{m+2β}` (with `m` the integer such that `t₀ ∈ (u_m, u_{m+1})`), -- so by the IVT it has a zero in each of the `2β` open gaps `(u_j, u_{j+1})`. -- Dropping the first gap (the only one containing the double zero `t₀`) -- leaves `2β − 1` distinct zeros counted once and all `≠ t₀`, packaged as a -- finset `S ⊆ [u_m, u_m + 2π)` with `card = 2β − 1`. Applying the generalized -- multiplicity count `IsTrigPolyLE.card_simple_add_double_le` (period -- `[c, c+2π)`, `c = u_m`; `hg_trig`, `hg_nonzero`, `hg_t₀`, `hg_deriv`) gives -- `(2β − 1) + 2 ≤ 2β`, whence `omega` derives the contradiction. have hcount : (2 * β - 1) + 2 ≤ 2 * β := by classical obtain ⟨φ, hφ⟩ := szegoInterp_amplitude β Q₀ Q₁ t₀ have hβR_pos : 0 < (β : ℝ) := by exact_mod_cast hβ1 let u : ℤ → ℝ := fun k => t₀ + φ / (β : ℝ) + (k : ℝ) * (pi / (β : ℝ)) let m : ℤ := ⌊(-φ) / Real.pi⌋ have hu_mono : StrictMono u := by simpa [u] using szegoExtrema_strictMono hβR_pos t₀ φ have hgap_pos : ∀ k : ℤ, u k < u (k + 1) := fun k => hu_mono (by omega) have hS_ext : ∀ k : ℤ, Sfun (u k) = A * ((-1 : ℝ) ^ k) := by intro k dsimp [Sfun] rw [hφ (u k)] rw [szegoExtrema_arg hβR_ne t₀ φ k] rw [Real.cos_int_mul_pi] have hg_cont : Continuous g := by have hQ_cont : Continuous Q := by dsimp [Q] fun_prop have hS_cont : Continuous Sfun := by dsimp [Sfun] exact szegoInterp_continuous β Q₀ Q₁ t₀ dsimp [g] exact hQ_cont.sub hS_cont have hsign : ∀ k : ℤ, g (u k) * ((-1 : ℝ) ^ k) < 0 := by intro k let s : ℝ := (-1 : ℝ) ^ k have hs_abs : |s| = 1 := by simp [s] have hs_sq : s * s = 1 := by have hs_sq_abs : |s| ^ 2 = 1 := by rw [hs_abs] norm_num rw [sq_abs] at hs_sq_abs nlinarith [hs_sq_abs] have hQs_le : Q (u k) * s ≤ M := by calc Q (u k) * s ≤ |Q (u k) * s| := le_abs_self _ _ = |Q (u k)| * |s| := by rw [abs_mul] _ = |Q (u k)| := by rw [hs_abs, mul_one] _ ≤ M := hM (u k) have hS := hS_ext k calc g (u k) * s = (Q (u k) - A * s) * s := by dsimp [g] rw [hS] _ = Q (u k) * s - A := by rw [show (Q (u k) - A * s) * s = Q (u k) * s - A * (s * s) by ring] rw [hs_sq, mul_one] _ < 0 := by linarith have hzero_exists : ∀ k : ℤ, ∃ x, x ∈ Ioo (u k) (u (k + 1)) ∧ g x = 0 := by intro k let s : ℝ := (-1 : ℝ) ^ k let F : ℝ → ℝ := fun x => g x * s have hs_ne : s ≠ 0 := by have hs_abs : |s| = 1 := by simp [s] intro hs0 rw [hs0, abs_zero] at hs_abs norm_num at hs_abs have hleft : F (u k) < 0 := by simpa [F, s] using hsign k have hright : 0 < F (u (k + 1)) := by have hnext := hsign (k + 1) have hs_next : ((-1 : ℝ) ^ (k + 1) : ℝ) = -s := by rw [zpow_add₀] · norm_num [s] · norm_num rw [hs_next] at hnext dsimp [F] nlinarith have hF_cont : ContinuousOn F (Icc (u k) (u (k + 1))) := by exact (hg_cont.mul continuous_const).continuousOn have hzero_mem : (0 : ℝ) ∈ Ioo (F (u k)) (F (u (k + 1))) := ⟨hleft, hright⟩ rcases intermediate_value_Ioo (le_of_lt (hgap_pos k)) hF_cont hzero_mem with ⟨x, hx, hFx⟩ refine ⟨x, hx, ?_⟩ have hgxs : g x * s = 0 := by simpa [F] using hFx exact (mul_eq_zero.mp hgxs).resolve_right hs_ne let v : ℤ → ℝ := fun k => choose (hzero_exists k) have hv_mem : ∀ k : ℤ, v k ∈ Ioo (u k) (u (k + 1)) := by intro k exact (Classical.choose_spec (hzero_exists k)).1 have hv_zero : ∀ k : ℤ, g (v k) = 0 := by intro k exact (Classical.choose_spec (hzero_exists k)).2 have hv_mono : StrictMono v := by intro k l hkl have hk1le : k + 1 ≤ l := by omega exact (lt_of_lt_of_le (hv_mem k).2 (hu_mono.monotone hk1le)).trans (hv_mem l).1 let N : ℕ := 2 * β - 1 let w : Fin N → ℝ := fun j => v (m + 1 + (j : ℤ)) let S : Finset ℝ := (Finset.univ : Finset (Fin N)).image w have hS_zero : ∀ x ∈ S, g x = 0 := by intro x hx rcases Finset.mem_image.mp hx with ⟨j, _hj, hjx⟩ rw [← hjx] dsimp [w] exact hv_zero (m + 1 + (j : ℤ)) have hS_sub : ↑S ⊆ Ico (u m) (u m + 2 * pi) := by intro x hx rcases Finset.mem_image.mp hx with ⟨j, _hj, hjx⟩ rw [← hjx] dsimp [w] constructor · have hm_lt : m < m + 1 + (j : ℤ) := by omega exact ((hu_mono hm_lt).trans (hv_mem (m + 1 + (j : ℤ))).1).le · have hidx : m + 1 + (j : ℤ) + 1 ≤ m + (2 * β : ℤ) := by have hjlt : (j : ℕ) < N := j.isLt dsimp [N] at hjlt omega have hu_le : u (m + 1 + (j : ℤ) + 1) ≤ u (m + (2 * β : ℤ)) := hu_mono.monotone hidx have hper : u (m + (2 * β : ℤ)) = u m + 2 * pi := by simpa [u] using szegoExtrema_period hβR_ne t₀ φ m exact (hv_mem (m + 1 + (j : ℤ))).2.trans_le (hu_le.trans (le_of_eq hper)) have ht₀_gap : t₀ ∈ Ico (u m) (u (m + 1)) := by simpa [u, m] using szegoExtrema_floor_mem hβR_pos t₀ φ have ht₀_mem : t₀ ∈ Ico (u m) (u m + 2 * pi) := by constructor · exact ht₀_gap.1 · have hidx : m + 1 < m + (2 * β : ℤ) := by omega have hper : u (m + (2 * β : ℤ)) = u m + 2 * pi := by simpa [u] using szegoExtrema_period hβR_ne t₀ φ m exact ht₀_gap.2.trans (by simpa [hper] using hu_mono hidx) have ht₀_not_mem : t₀ ∉ S := by intro ht₀S rcases Finset.mem_image.mp ht₀S with ⟨j, _hj, hj⟩ have hidx : m + 1 ≤ m + 1 + (j : ℤ) := by omega have hut : u (m + 1) ≤ u (m + 1 + (j : ℤ)) := hu_mono.monotone hidx have ht_lt : t₀ < w j := by dsimp [w] exact ht₀_gap.2.trans_le -- … truncated; follow the source link for the rest …