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.
Under Dependent Choice, a bounded operator between Banach spaces is bounded below exactly when it is injective with closed range
Statement
Assume the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain).
Let and be Banach spaces over the same scalar field, and let be a bounded linear operator. Then is bounded below if and only if it is injective and has closed range.
Facts & Assumptions
Given: Banach spaces and , and a bounded linear operator .
Dependent Choice is assumed (The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain).
Being bounded below means that some satisfies for every (A bounded operator that is bounded below).
A Banach space is complete, and a closed subspace of a Banach space is Banach (Banach space, A closed subspace of a Banach space is Banach).
In a nonempty complete metric space, a countable union of closed sets with empty interior cannot be the whole space (Under Dependent Choice, a nonempty complete metric space is not a countable union of closed sets with empty interior).
A map is injective when equal outputs force equal inputs (Injection, surjection, bijection).
Proof
Assume is bounded below, with constant from [L1]. If , then , so and . Thus is injective.
Let be a sequence in converging to . Then by [L1], so is Cauchy in and hence converges to some by [L2]. If is any bound for , then , so . Since limits are unique in normed spaces, . Therefore is closed.
Conversely, assume is injective and is closed. Then is Banach by [L2], and is a bounded linear bijection.
Let . Since , [L0] and [L3] yield an integer such that has nonempty interior in . So there exist and with . Because as well, subtraction gives .
We claim that every with has a preimage with and . Start with . If , then , so step 1.4 gives with . Put and . Then and . Inductively this constructs with for every . The series is absolutely convergent because , so [L2] gives with . Also , hence .
Now let with . Put , so . Step 2.1 gives with and . Then satisfies and . The same inequality is trivial at , so the inverse is bounded by .
Applying step 3.1 to gives for every , that is, . Therefore is bounded below.
Step 1.2 proves that bounded below implies injective with closed range, and steps 1.3 through 4.1 prove the converse.
Depends on
- A bounded operator that is bounded below
- Banach space
- The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain
- A closed subspace of a Banach space is Banach
- Under Dependent Choice, a nonempty complete metric space is not a countable union of closed sets with empty interior
- Injection, surjection, bijection
Used by
- Under Dependent Choice, a surjective bounded operator between Banach spaces has a bounded right inverse exactly when its kernel is complemented Theorem
- Under Dependent Choice, an injective bounded operator between Banach spaces has a bounded left inverse exactly when its range is closed and complemented Theorem
Dependency tree · two levels
19 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
- Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (standard reference, not scraped)
- Gerald Teschl, Topics in Real and Functional Analysis (standard reference, not scraped)