English
If convex on S and interior x with left-derivative equal to zero, then x is a minimum on S.
Русский
Если f выпукла на S и interior x, а левая производная равна нулю, то x — точка минимума на S.
LaTeX
$$$$ \ derivWithin f( Iio x) x = 0 \Rightarrow IsMinOn\ f\ S\ x $$$$
Lean4
theorem isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg (hf : ConvexOn ℝ S f) (hx : x ∈ interior S)
(hf_ld : derivWithin f (Iio x) x ≤ 0) (hf_rd : 0 ≤ derivWithin f (Ioi x) x) : IsMinOn f S x :=
by
intro y hy
rcases lt_trichotomy x y with hxy | h_eq | hyx
· suffices 0 ≤ slope f x y
by
simp only [slope_def_field, div_nonneg_iff, sub_nonneg, tsub_le_iff_right, zero_add, not_le.mpr hxy, and_false,
or_false] at this
exact this.1
exact hf_rd.trans <| rightDeriv_le_slope_of_mem_interior hf hx hy hxy
· simp [h_eq]
· suffices slope f x y ≤ 0
by
simp only [slope_def_field, div_nonpos_iff, sub_nonneg, tsub_le_iff_right, zero_add, not_le.mpr hyx, and_false,
or_false] at this
exact this.1
rw [slope_comm]
exact (slope_le_leftDeriv_of_mem_interior hf hy hx hyx).trans hf_ld
