bddBelow_slope_lt_of_mem_interior

English

For a convex set S and a function f that is differentiable on interior S, the derivative inside at Ioi x has slope equal to the infimum of the slopes f at x.

Русский

Для выпуклого множества S и функции f, дифференцируемой на interior(S), производная внутри Ioi x совпадает с инфимином slope.

LaTeX

$$$\\forall S, f, x \\; (\\text{ConvexOn } \\mathbb{R} \\, S \\, f) \\Rightarrow x\\in \\mathrm{intr}(S) \\Rightarrow HasDerivWithinAt f (\\sInf (\\text{image } (\\text{slope } f x) (\\{y\\in S \\mid x

Lean4

theorem bddBelow_slope_lt_of_mem_interior (hfc : ConvexOn 𝕜 s f) (hxs : x ∈ interior s) :
    BddBelow (slope f x '' {y ∈ s | x < y}) :=
  by
  obtain ⟨y, hyx, hys⟩ : ∃ y, y < x ∧ y ∈ s := Eventually.exists_lt (mem_interior_iff_mem_nhds.mp hxs)
  refine bddBelow_iff_subset_Ici.mpr ⟨slope f x y, fun y' ⟨z, hz, hz'⟩ ↦ ?_⟩
  simp_rw [mem_Ici, ← hz']
  refine hfc.slope_mono (interior_subset hxs) ?_ ?_ (hyx.trans hz.2).le
  · simp [hys, hyx.ne]
  · simp [hz.2.ne', hz.1]

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