Slopes of affine functions that are nonpositive on a set

For a point x₀ and a height a ≤ 0, the admissible slopes on a set s are the vectors p with a + ⟪x - x₀, p⟫ ≤ 0 for all x ∈ s, that is, those for which the affine function through (x₀, a) with slope p is nonpositive on s. This file shows that the admissible slopes on a set form a convex set, that for s inside the closure of a bounded set Ω containing x₀ every slope of norm below -a / diam Ω is admissible, and that for an open convex set Ω with a point of the complement and s ⊆ closure Ω there is an admissible slope of norm -a / dist (x₀, Ωᶜ).

Main results

• TauCeti.convex_setOf_forall_add_inner_le: the slopes which are nonpositive on a set form a convex set.
• TauCeti.ball_subset_setOf_forall_add_inner_le: a ball of admissible slopes.
• TauCeti.exists_mem_setOf_forall_add_inner_le_dist_eq: an admissible slope of norm -a / dist (x₀, Ωᶜ).

theorem TauCeti.convex_setOf_forall_add_inner_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Set E) (a : ℝ) (x₀ : E) : Convex ℝ {p : E | ∀ x ∈ s, a + inner ℝ (x - x₀) p ≤ 0}

The set of slopes p with a + ⟪x - x₀, p⟫ ≤ 0 for all x in a set s is convex.

theorem TauCeti.ball_subset_setOf_forall_add_inner_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {Ω s : Set E} {a : ℝ} {x₀ : E} (hΩ : Bornology.IsBounded Ω) (hx₀ : x₀ ∈ Ω) (hs : s ⊆ closure Ω) : Metric.ball 0 (-a / Metric.diam Ω) ⊆ {p : E | ∀ x ∈ s, a + inner ℝ (x - x₀) p ≤ 0}

For a bounded set Ω containing x₀, a set s ⊆ closure Ω and a height a, every slope of norm below -a / diam Ω makes the affine function through (x₀, a) nonpositive on s.

theorem TauCeti.exists_mem_setOf_forall_add_inner_le_dist_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {Ω s : Set E} {a : ℝ} {x₀ : E} [FiniteDimensional ℝ E] (hΩo : IsOpen Ω) (hconv : Convex ℝ Ω) (hx₀ : x₀ ∈ Ω) (hs : s ⊆ closure Ω) (hh : 0 ≤ -a) (hΩc : Ωᶜ.Nonempty) : ∃ q ∈ {p : E | ∀ x ∈ s, a + inner ℝ (x - x₀) p ≤ 0}, dist q 0 = -a / Metric.infDist x₀ Ωᶜ

If Ω is open and convex with x₀ ∈ Ω, the complement of Ω is nonempty, s ⊆ closure Ω and a ≤ 0, there is a slope q of norm -a / dist(x₀, Ωᶜ) with a + ⟪x - x₀, q⟫ ≤ 0 on s.