Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generated
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A bounded complex linear functional on a subspace of a complex normed space extends with the same norm

Statement

Assume the Axiom of Choice. Let X be a complex normed space, let M⊆X be a linear subspace, and let f0:M→C be a bounded complex linear functional. Then there exists a bounded complex linear functional F:X→C such that F∣M=f0 and ∥F∥=∥f0∥.

Facts & Assumptions

Given: The Axiom of Choice, A complex normed space X, a linear subspace M⊆X, and a bounded complex linear functional f0:M→C.

[A1]

AC is used through the real extension supplier [L1] in step 2.1.

[L1]

A bounded real linear functional on a real normed subspace extends with the same norm (A bounded real linear functional on a subspace of a real normed space extends with the same norm).

[L2]

A complex linear functional is recovered from its real part by f(x)=u(x)−iu(ix), and conversely every such formula defines a complex linear functional (A complex linear functional is recovered from its real part by f(x)=u(x)-iu(ix)).

[L3]

The complex norm axioms are those of Complex norm and complex normed space. The same norm is a real norm on realification (Realification preserves a complex norm and its metric); a complex-linear subspace carries its restricted complex norm (A complex normed linear subspace) and realifies to a real normed subspace with the same norm and restricted metric (A complex normed subspace and its finite basis realify).

Proof

technique · direct
1.1L2givenalgebra

Let u:=Re⁡f0. By [L2], u is real linear on the underlying real subspace M. Also ∣u(m)∣≤∣f0(m)∣≤∥f0∥ ∥m∥(m∈M), so u is bounded with ∥u∥≤∥f0∥.

2.1L1L2L3step 1.1construct

Apply [L1] to the underlying real normed spaces. This yields a bounded real linear functional U:X→R extending u and satisfying ∥U∥=∥u∥. Define F(x):=U(x)−iU(ix)(x∈X). By [L2], F is complex linear and Re⁡F=U.

3.1L2step 2.1

For m∈M, the equality U∣M=u and [L2] give F(m)=u(m)−iu(im)=f0(m). So F extends f0.

3.2L2L3step 1.1step 2.1choosealgebra

Fix x∈X. Choose θ∈R so that eiθF(x)=∣F(x)∣ is a nonnegative real number. Since Re⁡F=U and F is complex linear, ∣F(x)∣=Re⁡(eiθF(x))=Re⁡F(eiθx)=U(eiθx). Therefore ∣F(x)∣≤∥U∥ ∥eiθx∥=∥U∥ ∥x∥≤∥f0∥ ∥x∥, where the last inequality uses step 1.1 and ∥U∥=∥u∥. Hence ∥F∥≤∥f0∥.

4.1step 3.1step 3.2algebra∎

Since F∣M=f0, every m∈M with ∥m∥≤1 satisfies ∣f0(m)∣=∣F(m)∣≤∥F∥. Taking the supremum over the unit ball of M gives ∥f0∥≤∥F∥. Combined with step 3.2, this yields ∥F∥=∥f0∥.

Depends on

Used by

Dependency tree · two levels

26 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources