Supporting Direction at the Nearest Frontier

This formalizes the supporting half-space estimate for a bounded open convex set.

Let $E$ be a nontrivial finite-dimensional real inner-product space, let $\Omega\subseteq E$ be open, convex, and bounded, and let $x_0\in\Omega$. Then there exists a unit vector $e\in E$ such that every $x\in\Omega$ satisfies

The declaration is exists_unit_inner_le_infDist_frontier_readable. Here infDist is the distance from $x_0$ to the frontier, and the conclusion is existential rather than a uniqueness statement about the supporting direction.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem exists_unit_inner_le_infDist_frontier {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {Ω : Set E} (hΩ : IsOpen Ω)
    (hc : Convex ℝ Ω) (hb : Bornology.IsBounded Ω) {x₀ : E} (hx₀ : x₀ ∈ Ω) :
    ∃ e : E, ‖e‖ = 1 ∧ ∀ x ∈ Ω, ⟪x - x₀, e⟫ ≤ infDist x₀ (frontier Ω)

Module navigation

Module: Analysis/Convex/Alexandrov.

Previous: mem_subgradientImage_of_affine_le_of_nonneg_frontier · Next: exists_pos_volume_convexHull_closedBall_union_singleton_ge.

Source excerpt, lines 624–627 · Frozen source 408915f.