Theorems · Theorem · special functions

Polynomial.Chebyshev.isLocalMax_T_real

∀ {n k : ℕ},
  n ≠ 0 →
    0 < k →
      k < n →
        Even k → IsLocalMax (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 217 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.

Cites29

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

Realstatement and proof · cited by 25,697
le_reflproof · cited by 2,061
Real.pistatement and proof · cited by 1,774
Set.Iooproof · cited by 1,214
le_of_ltproof · cited by 1,175
Polynomial.evalstatement and proof · cited by 796
Evenstatement and proof · cited by 444
Real.cosstatement and proof · cited by 424
zero_leproof · cited by 382
mul_posproof · cited by 374
div_posproof · cited by 337
Nat.cast_pos'proof · cited by 219

Cited by1

Results whose statement or proof uses this declaration.

Polynomial.Chebyshev.isLocalExtr_T_realproof · cited by 1