strongConcaveOn_iff_convex — Mathlib

English

If hf: UniformConcaveOn s φ f and hg: UniformConvexOn s ψ g, then UniformConcaveOn s (φ+ψ) (f−g).

Русский

Если hf: UniformConcaveOn s φ f и hg: UniformConvexOn s ψ g, то UniformConcaveOn s (φ+ψ) (f−g).

LaTeX

$$$$ \text{UniformConcaveOn}(s,\phi,f) \land \text{UniformConvexOn}(s,\psi,g) \Rightarrow \text{UniformConcaveOn}(s,\phi+\psi,f-g). $$$$

Lean4

theorem strongConcaveOn_iff_convex : StrongConcaveOn s m f ↔ ConcaveOn ℝ s fun x ↦ f x + m / (2 : ℝ) * ‖x‖ ^ 2 :=
  by
  refine and_congr_right fun _ ↦ forall₄_congr fun x _ y _ ↦ forall₅_congr fun a b ha hb hab ↦ ?_
  simp_rw [← sub_le_iff_le_add, smul_eq_mul, aux_add ha hb hab, mul_assoc, mul_left_comm]

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