strictConcaveOn — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem strictConcaveOn (hf : UniformConcaveOn s φ f) (hφ : ∀ r, r ≠ 0 → 0 < φ r) : StrictConcaveOn ℝ 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' <| lt_add_of_pos_right _ ?_⟩
  rw [← sub_ne_zero, ← norm_pos_iff] at hxy
  have := hφ _ hxy.ne'
  positivity

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