Best approximation in normed spaces

TheoremExistence of best approximations in finite-dimensional subspaces#✓fully proved

Every point of a normed space has a nearest point in a finite-dimensional subspace (proximinality). No completeness hypothesis on the ambient space is needed: completeness enters only through the finite-dimensional subspace, whose closed balls are compact.

theorem exists_bestApproximation_of_finiteDimensional {𝕜 : Type*} [RCLike 𝕜]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    {F : Submodule 𝕜 E} [FiniteDimensional 𝕜 F] (x : E) :
    ∃ y ∈ F, ∀ z ∈ F, ‖x - y‖ ≤ ‖x - z‖

Used by 1

Used byUnique best approximation in finite-dimensional subspaces

TheoremUniqueness of best approximation in strictly convex spaces#✓fully proved

In a strictly convex real normed space, a convex set contains at most one point nearest to a given point: the midpoint of two distinct nearest points would be strictly closer, by norm_midpoint_lt_iff.

theorem eq_of_isBestApproximation_of_strictConvexSpace {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E] [StrictConvexSpace ℝ E]
    {K : Set E} (hK : Convex ℝ K) {x y₁ y₂ : E} (hy₁ : y₁ ∈ K) (hy₂ : y₂ ∈ K)
    (h₁ : ∀ z ∈ K, ‖x - y₁‖ ≤ ‖x - z‖) (h₂ : ∀ z ∈ K, ‖x - y₂‖ ≤ ‖x - z‖) :
    y₁ = y₂

Used by 1

Used byUnique best approximation in finite-dimensional subspaces

TheoremUnique best approximation in finite-dimensional subspaces#✓fully proved

Existence plus uniqueness: a finite-dimensional subspace of a strictly convex real normed space admits a unique best approximation to every point.

theorem exists_unique_bestApproximation_of_finiteDimensional {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E] [StrictConvexSpace ℝ E]
    {F : Submodule ℝ E} [FiniteDimensional ℝ F] (x : E) :
    ∃ y ∈ F, (∀ z ∈ F, ‖x - y‖ ≤ ‖x - z‖) ∧
      ∀ y' ∈ F, (∀ z ∈ F, ‖x - y'‖ ≤ ‖x - z‖) → y' = y

Uses 2

Proof usesUniqueness of best approximation in strictly convex spaces · Existence of best approximations in finite-dimensional subspaces

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.