English
For a convexOn function on C, if C is open and nonempty, then f is locally Lipschitz on C.
Русский
Для функции выпуклой на открытом непустом C функция локально липшицева на C.
LaTeX
$$$\\LocallyLipschitzOn C f$$$
Lean4
protected theorem locallyLipschitzOn (hC : IsOpen C) (hf : ConvexOn ℝ C f) : LocallyLipschitzOn C f :=
by
obtain rfl | ⟨x₀, hx₀⟩ := C.eq_empty_or_nonempty
· simp
· obtain ⟨b, hx₀b, hbC⟩ := exists_mem_interior_convexHull_affineBasis (hC.mem_nhds hx₀)
refine ((hf.continuousOn_tfae hC ⟨x₀, hx₀⟩).out 3 0).mp ?_
refine ⟨x₀, hx₀, BddAbove.isBoundedUnder (IsOpen.mem_nhds isOpen_interior hx₀b) ?_⟩
exact
(hf.bddAbove_convexHull ((subset_convexHull ..).trans hbC) ((finite_range _).image _).bddAbove).mono
(by gcongr; exact interior_subset)
