Theorems · Theorem · special functions

Polynomial.Chebyshev.isLocalExtr_T_real

∀ {n k : ℕ},
  n ≠ 0 →
    0 < k →
      k < n → IsLocalExtr (fun x => Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n)) (Real.cos (↑k * Real.pi / ↑n))

Defined in: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Cited by: 1 results in Mathlib
Foundations: Depth 218 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement · cited by 25,697
Real.pistatement · cited by 1,774
Polynomial.evalstatement · cited by 796
Evenproof · cited by 444
Real.cosstatement · cited by 424
Oddproof · cited by 364
Polynomial.Chebyshev.Tstatement · cited by 108
Nat.even_or_oddproof · cited by 28
IsLocalExtrstatement · cited by 28
Polynomial.Chebyshev.isLocalMax_T_realproof · cited by 1
Polynomial.Chebyshev.isLocalMin_T_realproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

Polynomial.Chebyshev.isLocalExtr_T_real_iffproof · cited by 0