strictConvexOn — Mathlib

English

If a function is uniformly convex on s with a modulus φ, and φ(r) > 0 for all r ≠ 0, then f is strictly convex on s.

Русский

Если функция выпукла униформно на s с модулем φ и φ(r) > 0 для всех r ≠ 0, то f строго выпукла на s.

LaTeX

$$$$ \text{UniformConvexOn}(s,\phi,f) \land (\forall r\, (r \neq 0 \Rightarrow \phi(r) > 0)) \Rightarrow \text{StrictConvexOn}(\mathbb{R},s,f). $$$$

Lean4

theorem strictConvexOn (hf : UniformConvexOn s φ f) (hφ : ∀ r, r ≠ 0 → 0 < φ r) : StrictConvexOn ℝ s f :=
  by
  refine ⟨hf.1, fun x hx y hy hxy a b ha hb hab ↦ (hf.2 hx hy ha.le hb.le hab).trans_lt <| sub_lt_self _ ?_⟩
  rw [← sub_ne_zero, ← norm_pos_iff] at hxy
  have := hφ _ hxy.ne'
  positivity

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