convexOn_descPochhammer_eval — Mathlib

English

The function x ↦ (descPochhammer ℝ n).eval (x) is convex on [n-1, ∞).

Русский

Функция x ↦ (descPochhammer ℝ n).eval(x) выпукла на отрезке [n-1, ∞).

LaTeX

$$$$ \operatorname{ConvexOn}\; \mathbb{R}\; (\mathrm{Set.Ici}(n-1))\; (\mathrm{descPochhammer} \mathbb{R} n).\mathrm{eval}. $$$$

Lean4

/-- `descPochhammer ℝ n` is convex on `[n-1, ∞)`. -/
theorem convexOn_descPochhammer_eval (n : ℕ) : ConvexOn ℝ (Set.Ici (n - 1 : ℝ)) (descPochhammer ℝ n).eval :=
  by
  rcases n.eq_zero_or_pos with h_eq | _
  · simp [h_eq, convexOn_const, convex_Ici]
  · apply
      MonotoneOn.convexOn_of_deriv (convex_Ici (n - 1 : ℝ)) continuous_descPochhammer_eval.continuousOn
        differentiable_descPochhammer_eval.differentiableOn
    rw [interior_Ici]
    exact monotoneOn_deriv_descPochhammer_eval n

Похожие утверждения