markov_inequality_interval

import Mathlib.Algebra.Polynomial.Basic
import Mathlib.Algebra.Polynomial.Degree.Defs
import Mathlib.Algebra.Polynomial.Derivative
import Mathlib.Algebra.Polynomial.Eval.Defs
import Mathlib.Data.Real.Basic

/-!
# Markov's brothers inequality on a continuous interval

Classical inequality (A. A. Markov, 1889): for univariate real polynomial
`Q` of degree `≤ d` absolutely bounded by `M` on a closed interval
`[a, b]` with `a < b`, the derivative is uniformly bounded by `2 d² M /
(b - a)` on the same interval. The constant `2 d² / (b - a)` is sharp,
achieved by the appropriately scaled Chebyshev polynomial `T_d`.

This is one of the foundational classical results in the theory of
polynomial inequalities, but is *not* present in Mathlib at the
inside-the-interval level (Mathlib has the outside-the-interval extremal
property `Polynomial.Chebyshev.eval_iterate_derivative_le_of_forall_abs_le_one`
for `x ≥ 1`, but the inside-the-interval Markov bound requires a separate
argument via Chebyshev expansion + sign analysis).

Left as a platform leaf — DEFERRED. Sub-leaf of `markov_polya_grid`.
Estimated 300-500 lines.
-/

/-- **Markov's brothers inequality on `[a, b]`.**

For real polynomial `Q` of degree `≤ d` with `|Q(x)| ≤ M` for every
`x ∈ [a, b]` (with `a < b`), the derivative satisfies the sharp bound
`|Q'(c)| ≤ 2 d² M / (b - a)` for every `c ∈ [a, b]`. -/

theorem markov_inequality_interval
    (a b : ℝ) (hab : a < b) (Q : Polynomial ℝ) {d : ℕ} (M : ℝ)
    (h_deg : Q.natDegree ≤ d)
    (h_bound : ∀ x : ℝ, a ≤ x → x ≤ b → |Q.eval x| ≤ M) :
    ∀ c : ℝ, a ≤ c → c ≤ b →
      |Q.derivative.eval c| ≤ 2 * (d : ℝ)^2 * M / (b - a) := by sorry