Hahn–Banach theorem

TheoremOne-step Hahn–Banach extension#✓fully proved

Let \(E\) be a seminormed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \(M\) be a subspace of \(E\), let \(C \ge 0\) be a real number, and let \(f \colon M \to \mathbb{K}\) be a continuous linear functional with \(\|f(m)\| \le C\|m\|\) for all \(m \in M\). If \(x_0 \in E\) does not lie in \(M\), then \(M\) is strictly contained in \(M' = M + \mathbb{K} x_0\), and there is a continuous linear functional \(g \colon M' \to \mathbb{K}\) that agrees with \(f\) on \(M\) and satisfies \(\|g(v)\| \le C\|v\|\) for all \(v \in M'\).

theorem hahn_banach_one_step_extension_bound
    (M : Subspace 𝕜 E) (f : ↥M →L[𝕜] 𝕜) (C : ℝ) (hC : 0 ≤ C)
    (hf_bound : ∀ m : M, ‖f m‖ ≤ C * ‖(m : E)‖)
    (x₀ : E) (hx₀ : x₀ ∉ M) :
    ∃ g : ↥(M ⊔ 𝕜 ∙ x₀) →L[𝕜] 𝕜,
      (∀ m : M, g ⟨↑m, mem_sup_left m.2⟩ = f m) ∧
      (∀ v : ↥(M ⊔ 𝕜 ∙ x₀), ‖g v‖ ≤ C * ‖(v : E)‖) ∧
      M < M ⊔ 𝕜 ∙ x₀

TheoremQuotient seminorm equals distance to the subspace#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), let \(S\) be a linear subspace of \(E\), and give \(E/S\) the quotient seminorm. Then for every \(x \in E\) the class \(q(x)\) of \(x\) under the quotient map \(q \colon E \to E/S\) satisfies \(\|q(x)\| = d(x, S)\), where \(d(x, S) = \inf_{s \in S} \|x - s\|\) is the distance from \(x\) to \(S\).

theorem norm_mkQL_apply (S : Submodule 𝕜 E) (x : E) :
    ‖S.mkQL x‖ = Metric.infDist x (S : Set E)

Used by 2

Used byHahn–Banach distance formula, attainment form · The quotient map has norm at most one

TheoremThe quotient map has norm at most one#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), let \(S\) be a linear subspace of \(E\), and give \(E/S\) the quotient seminorm. Then the quotient map \(q \colon E \to E/S\), a continuous linear map, has operator norm \(\|q\| \le 1\).

theorem norm_mkQL_le (S : Submodule 𝕜 E) : ‖S.mkQL‖ ≤ 1

Uses 1 · Used by 1

Proof usesQuotient seminorm equals distance to the subspace

Used byHahn–Banach distance formula, attainment form

TheoremHahn–Banach distance formula, attainment form#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), let \(S\) be a linear subspace of \(E\), not necessarily closed, and let \(x \in E\). Then there is a continuous linear functional \(f \colon E \to \mathbb{K}\) with \(\|f\| \le 1\) that vanishes on \(S\) and satisfies \(f(x) = d(x, S)\), where \(d(x, S) = \inf_{s \in S} \|x - s\|\) is the distance from \(x\) to \(S\).

theorem exists_annihilating_apply_eq_infDist (S : Submodule 𝕜 E) (x : E) :
    ∃ f : E →L[𝕜] 𝕜, (∀ s ∈ S, f s = 0) ∧ ‖f‖ ≤ 1 ∧
      f x = (Metric.infDist x (S : Set E) : 𝕜)

Uses 2 · Used by 3

Proof usesQuotient seminorm equals distance to the subspace · The quotient map has norm at most one

Used bySeparation · Norm-one annihilating functional at positive distance · Hahn–Banach distance formula

TheoremNorm-one annihilating functional at positive distance#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), let \(S\) be a linear subspace of \(E\), and let \(x \in E\) have positive distance \(d(x, S) = \inf_{s \in S} \|x - s\| > 0\) from \(S\). Then there is a continuous linear functional \(f \colon E \to \mathbb{K}\) with \(\|f\| = 1\) that vanishes on \(S\) and satisfies \(f(x) = d(x, S)\).

A functional with \(\|f\| \le 1\) that vanishes on \(S\) and satisfies \(f(x) = d(x, S)\) has norm exactly \(1\): for \(s \in S\) we have \(d(x, S) = |f(x - s)| \le \|f\| \, \|x - s\|\), and \(s\) can be chosen with \(\|x - s\|\) arbitrarily close to \(d(x, S) > 0\).

theorem exists_annihilating_norm_one (S : Submodule 𝕜 E) {x : E}
    (hx : 0 < Metric.infDist x (S : Set E)) :
    ∃ f : E →L[𝕜] 𝕜, (∀ s ∈ S, f s = 0) ∧ ‖f‖ = 1 ∧
      f x = (Metric.infDist x (S : Set E) : 𝕜)

Uses 1 · Used by 2

Proof usesHahn–Banach distance formula, attainment form

Used byNorm-one annihilating functional outside a closed subspace · Birkhoff–James orthogonality gives an annihilating norming functional

TheoremNorm-one annihilating functional outside a closed subspace#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), let \(S\) be a closed linear subspace of \(E\) and let \(x \in E\) with \(x \notin S\). Then there is a continuous linear functional \(f \colon E \to \mathbb{K}\) with \(\|f\| = 1\) that vanishes on \(S\) and satisfies \(f(x) = d(x, S)\), where \(d(x, S) = \inf_{s \in S} \|x - s\|\) is the distance from \(x\) to \(S\).

Since \(S\) is closed and \(x \notin S\), the distance \(d(x, S)\) is positive.

theorem exists_annihilating_of_notMem (S : Submodule 𝕜 E) (hS : IsClosed (S : Set E))
    {x : E} (hx : x ∉ S) :
    ∃ f : E →L[𝕜] 𝕜, (∀ s ∈ S, f s = 0) ∧ ‖f‖ = 1 ∧
      f x = (Metric.infDist x (S : Set E) : 𝕜)

Uses 1

Proof usesNorm-one annihilating functional at positive distance

TheoremHahn–Banach distance formula#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), let \(S\) be a linear subspace of \(E\), not necessarily closed, and let \(x \in E\). Then the distance \(d(x, S) = \inf_{s \in S} \|x - s\|\) from \(x\) to \(S\) equals the supremum of \(|f(x)|\) over all continuous linear functionals \(f \colon E \to \mathbb{K}\) with \(\|f\| \le 1\) that vanish on \(S\).

The supremum is attained, by the attainment form of the distance formula.

theorem infDist_eq_sSup_norm_apply (S : Submodule 𝕜 E) (x : E) :
    Metric.infDist x (S : Set E) =
      sSup { r : ℝ | ∃ f : E →L[𝕜] 𝕜, ‖f‖ ≤ 1 ∧ (∀ s ∈ S, f s = 0) ∧ ‖f x‖ = r }

Uses 1

Proof usesHahn–Banach distance formula, attainment form

TheoremSeparation of convex bodies at positive distance#●ready to prove

Let \(E\) be a real Banach space and let \(A, B \subseteq E\) be convex bodies, that is, convex, closed and bounded sets with nonempty interior. If there is \(\varepsilon > 0\) with \(\operatorname{dist}(a, b) \ge \varepsilon\) for all \(a \in A\) and \(b \in B\), then there are a nonzero continuous linear functional \(F : E \to \mathbb{R}\) and a constant \(c \in \mathbb{R}\) with \(F(a) \le c\) for all \(a \in A\) and \(c \le F(b)\) for all \(b \in B\).

theorem_wanted convexBodiesSeparatedByHyperplane :
    ∀ (E : Type) [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
      (A B : Set E),
      Convex ℝ A → IsClosed A → (interior A).Nonempty →
      (∃ R : ℝ, ∀ a ∈ A, ‖a‖ ≤ R) →
      Convex ℝ B → IsClosed B → (interior B).Nonempty →
      (∃ R : ℝ, ∀ b ∈ B, ‖b‖ ≤ R) →
      (∃ ε : ℝ, 0 < ε ∧ ∀ a ∈ A, ∀ b ∈ B, ε ≤ dist a b) →
      ∃ (F : E →L[ℝ] ℝ) (c : ℝ), F ≠ 0 ∧
        (∀ a ∈ A, F a ≤ c) ∧ (∀ b ∈ B, c ≤ F b)

Sources

• S. Mazur, Problem 64 of the Scottish Book; the theorem is true, as recorded in the typescript Ad 64 (Eidelheit, January 11, 1936), which gives the stronger statement that separation holds even for non-disjoint bodies with no common interior points. The positive-distance case follows from standard Hahn–Banach separation.

7 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.