strictConvexOn_pow — Mathlib

English

For n ≥ 2, the map x ↦ x^n is strictly convex on [0, ∞).

Русский

Для n ≥ 2 отображение x^n строго выпукло на [0, ∞).

LaTeX

$$2 ≤ n ⇒ StrictConvexOn ℝ (Ici 0) (fun x : ℝ => x^n)$$

Lean4

/-- `x^n`, `n : ℕ` is strictly convex on `[0, +∞)` for all `n` greater than `2`. -/
theorem strictConvexOn_pow {n : ℕ} (hn : 2 ≤ n) : StrictConvexOn ℝ (Ici 0) fun x : ℝ => x ^ n :=
  by
  apply StrictMonoOn.strictConvexOn_of_deriv (convex_Ici _) (continuousOn_pow _)
  eta_expand
  simp_rw [deriv_pow_field, interior_Ici]
  exact fun x (hx : 0 < x) y _ hxy =>
    mul_lt_mul_of_pos_left (pow_lt_pow_left₀ hxy hx.le <| Nat.sub_ne_zero_of_lt hn) (by positivity)

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