concaveOn_iff_div — Mathlib

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 (β := βᵒᵈ)

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