Star-convex sets: dilates and complements of closed half-subspaces

The dilates of a set s star-convex about 0 increase with the factor: p • s ⊆ q • s for 0 ≤ p ≤ q (StarConvex.smul_mono), and in particular for a convex set containing 0 (Convex.smul_mono_of_zero_mem). Thresholds defined by dilates, such as successive minima, are monotone because of this.

For a subspace W of a vector space E over a linearly ordered field and a linear functional φ on E, the set {x ∈ W | φ x ≤ 0} is a closed half of W. Its complement in E is star-convex about any v ∈ W with 0 < φ v (TauCeti.starConvex_compl_setOf_mem_and_nonpos): a segment from v that ends outside W leaves W at once, and one that ends in W stays where φ is positive. This is the subspace analogue of Mathlib's starConvex_compl_Iic.

References

Convex.smul_mono_of_zero_mem follows the lemma of the same name in the successive-minima proposal for Mathlib by Kevin H. Wilson, Mathlib/Analysis/Convex/Basic.lean at https://github.com/khwilson/mathlib4/blob/8423d1c878e50d8504a230ffd9b6ec76ce6a08eb/Mathlib/Analysis/Convex/Basic.lean (Apache 2.0).

theorem TauCeti.starConvex_compl_setOf_mem_and_nonpos {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {W : Submodule 𝕜 E} {φ : E →ₗ[𝕜] 𝕜} {v : E} (hv : v ∈ W) (hφv : 0 < φ v) : StarConvex 𝕜 v {x : E | x ∈ W ∧ φ x ≤ 0}ᶜ

The complement of the closed half-subspace {x ∈ W | φ x ≤ 0} is star-convex about any v ∈ W with 0 < φ v.

theorem StarConvex.smul_mono {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {p q : 𝕜} (hs : StarConvex 𝕜 0 s) (hp : 0 ≤ p) (hpq : p ≤ q) : p • s ⊆ q • s

The dilates of a set star-convex about 0 increase with the factor: p • s ⊆ q • s whenever 0 ≤ p ≤ q.

theorem Convex.smul_mono_of_zero_mem {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {p q : 𝕜} (hs : Convex 𝕜 s) (h₀ : 0 ∈ s) (hp : 0 ≤ p) (hpq : p ≤ q) : p • s ⊆ q • s

The dilates of a convex set containing 0 increase with the factor: p • s ⊆ q • s whenever 0 ≤ p ≤ q.