English
Right translation preserves strict convexity.
Русский
Правый перенос сохраняет строгую выпуклость.
LaTeX
$$$StrictConvexOn\ 𝕜\ s\ f \Rightarrow \forall c\, StrictConvexOn\ 𝕜\ ((fun z => c + z)^{-1}\' s) (f \circ (fun z => z + c))$$$
Lean4
theorem strictConvexOn_iff_div {f : E → β} :
StrictConvexOn 𝕜 s f ↔
Convex 𝕜 s ∧
∀ ⦃x⦄,
x ∈ s →
∀ ⦃y⦄,
y ∈ s →
x ≠ y →
∀ ⦃a b : 𝕜⦄,
0 < a →
0 < b → f ((a / (a + b)) • x + (b / (a + b)) • y) < (a / (a + b)) • f x + (b / (a + b)) • f y :=
and_congr Iff.rfl
⟨by
intro h x hx y hy hxy a b ha hb
have hab := add_pos ha hb
apply h hx hy hxy (div_pos ha hab) (div_pos hb hab)
rw [← add_div, div_self hab.ne'], by
intro h x hx y hy hxy a b ha hb hab
simpa [hab, zero_lt_one] using h hx hy hxy ha hb⟩
