English
Right translation preserves strict concavity.
Русский
Правый перенос сохраняет строгую конкавность.
LaTeX
$$$StrictConcaveOn\ 𝕜\ s\ f \Rightarrow \forall c\, StrictConcaveOn\ 𝕜\ ((fun z => c + z)^{-1}\' s) (f \circ (fun z => z + c))$$$
Lean4
theorem concaveOn_iff_div {f : E → β} :
ConcaveOn 𝕜 s f ↔
Convex 𝕜 s ∧
∀ ⦃x⦄,
x ∈ s →
∀ ⦃y⦄,
y ∈ s →
∀ ⦃a b : 𝕜⦄,
0 ≤ a →
0 ≤ b →
0 < a + b →
(a / (a + b)) • f x + (b / (a + b)) • f y ≤ f ((a / (a + b)) • x + (b / (a + b)) • y) :=
convexOn_iff_div (β := βᵒᵈ)