Uniformly convex spaces

TheoremStrict convexity implies uniform convexity in finite dimensions#✓fully proved

In a finite-dimensional real normed space, strict convexity implies uniform convexity. The proof maximizes ‖x + y‖ over the compact set of pairs of unit vectors at distance at least ε; strict convexity says the maximum is < 2, and the gap is the required δ.

theorem uniformConvexSpace_of_finiteDimensional_strictConvexSpace
    [FiniteDimensional ℝ E] [StrictConvexSpace ℝ E] : UniformConvexSpace E

Used by 3

Used byUnique nearest point from a minimizing sequence in finite dimensions · Minimizing sequences converge to the unique nearest point · Strict and uniform convexity agree in finite dimensions

TheoremStrict and uniform convexity agree in finite dimensions#✓fully proved

In finite dimensions, strict convexity and uniform convexity are equivalent.

theorem strictConvexSpace_iff_uniformConvexSpace_of_finiteDimensional
    [FiniteDimensional ℝ E] :
    StrictConvexSpace ℝ E ↔ UniformConvexSpace E

Uses 1

Proof usesStrict convexity implies uniform convexity in finite dimensions

TheoremConvergence of minimizing sequences in uniformly convex spaces#✓fully proved

In a complete uniformly convex space, a minimizing sequence for the distance from a point x to a closed convex set K converges to a point of K attaining that distance. The argument is the usual one: if the sequence were not Cauchy, two far-apart almost-minimizing terms would have normalized displacements far apart on the unit sphere, and uniform convexity would force their midpoint to beat the infimum, contradicting convexity of K.

theorem exists_tendsto_of_minimizingSequence {K : Set E} (hKconv : Convex ℝ K)
    (hKclosed : IsClosed K) {x : E} (u : ℕ → E) (hu : ∀ n, u n ∈ K)
    (hmin : Tendsto (fun n => ‖u n - x‖) atTop (𝓝 (infDist x K))) :
    ∃ y ∈ K, ‖y - x‖ = infDist x K ∧ Tendsto u atTop (𝓝 y)

Used by 2

Used byUnique nearest point from a minimizing sequence in finite dimensions · Minimizing sequences converge to the unique nearest point

TheoremUnique nearest point from a minimizing sequence in finite dimensions#✓fully proved

In a finite-dimensional strictly convex space, a minimizing sequence for the distance to a closed convex set supplies a unique nearest point. The uniqueness clause only assumes that a second point belongs to the set and attains the distance; it does not assume that the minimizing sequence converges to that point.

theorem exists_unique_nearestPoint_of_minimizingSequence_of_finiteDimensional
    [FiniteDimensional ℝ E] [StrictConvexSpace ℝ E] {K : Set E} (hKconv : Convex ℝ K)
    (hKclosed : IsClosed K) {x : E} (u : ℕ → E) (hu : ∀ n, u n ∈ K)
    (hmin : Tendsto (fun n => ‖u n - x‖) atTop (𝓝 (infDist x K))) :
    ∃! y, y ∈ K ∧ ‖y - x‖ = infDist x K

Uses 2 · Used by 1

Proof usesConvergence of minimizing sequences in uniformly convex spaces · Strict convexity implies uniform convexity in finite dimensions

Used byMinimizing sequences converge to the unique nearest point

TheoremMinimizing sequences converge to the unique nearest point#✓fully proved

In a finite-dimensional strictly convex space, a minimizing sequence for the distance to a closed convex set converges to the unique point of the set attaining that distance. This preserves the original combined API as a corollary of nearest-point uniqueness and minimizing-sequence convergence.

theorem exists_unique_tendsto_of_minimizingSequence_of_finiteDimensional
    [FiniteDimensional ℝ E] [StrictConvexSpace ℝ E] {K : Set E} (hKconv : Convex ℝ K)
    (hKclosed : IsClosed K) {x : E} (u : ℕ → E) (hu : ∀ n, u n ∈ K)
    (hmin : Tendsto (fun n => ‖u n - x‖) atTop (𝓝 (infDist x K))) :
    ∃! y, y ∈ K ∧ ‖y - x‖ = infDist x K ∧ Tendsto u atTop (𝓝 y)

Uses 3

Proof usesConvergence of minimizing sequences in uniformly convex spaces · Unique nearest point from a minimizing sequence in finite dimensions · Strict convexity implies uniform convexity in finite dimensions

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.