TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

The closure Hölder spaces are Banach spaces

Statement

Assume Countable Choice. Let $n \geq 1$ , let $k \geq 0$ be an integer, $0 < α < 1$ , $K \in {R, C}$ and let $Ω \subseteq R^{n}$ be open and nonempty. Then $C_{b}^{k, α} (Ω; K)$ with the norm of Hölder spaces $C^{k, α}$ , closure and interior scaled norms, and $C^{k, α}$ domains is a Banach space over $K$ : every Cauchy sequence in $∥ \cdot ∥_{C^{k, α} (Ω)}$ converges in that norm to a limit whose $k$ -th partial derivatives are $α$ -Hölder on $Ω$ . If in addition $Ω$ is a bounded $C^{k, α}$ domain with nonempty boundary, then the subspace $X_{0} : = {u \in C_{b}^{k, α} (Ω) : u extends continuously to \overset{ˉ}{Ω} with u ∣_{\partial Ω} = 0}$ is closed in $C_{b}^{k, α} (Ω)$ and hence is a Banach space. For every bounded open nonempty $Ω$ , the boundary-extension class $C^{k, α} (\overset{ˉ}{Ω}; K)$ is also a closed subspace of $C_{b}^{k, α} (Ω; K)$ and hence a Banach space, as is its zero-boundary subspace. Completeness here is for the full finite Hölder norm. A boundary Hölder seminorm alone does not define a norm on this function space, since it vanishes on nonzero constant functions.

Facts & Assumptions

Given: ${A C}_{ω}$ , $n \geq 1$ , integers $k \geq 0$ , $0 < α < 1$ , $K \in {R, C}$ , an open nonempty $Ω \subseteq R^{n}$ , and a Cauchy sequence $(u_{j})$ in $C_{b}^{k, α} (Ω; K)$ .

[A1]

The only choice assumption is Countable Choice ${A C}_{ω}$ , used through the sequential completeness of $R$ and $C$ and the cited metric-space completeness conventions. No full Axiom of Choice is used. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F1]

The norm is $∥ u ∥_{C^{k, α} (Ω)} = \sum_{j = 0}^{k} \sup_{Ω} \max_{∣ β ∣ = j} ∣ D^{β} u ∣ + [u]_{k, α; Ω}$ with $[u]_{k, α; Ω} = \sum_{∣ β ∣ = k} [D^{β} u]_{0, α; Ω}$ , and $C_{b}^{k, α}$ consists of the $C^{k}$ functions with finite norm; $D^{β}$ are the canonical-order derivatives. (Hölder spaces $C^{k, α}$ , closure and interior scaled norms, and $C^{k, α}$ domains, $C^{k}$ maps and multi-index derivative notation in Euclidean space)

[F2]

Uniformly Cauchy sequences of real- (or complex-) valued functions converge uniformly; a uniform limit of continuous functions is continuous; and if $g_{m} \to g$ uniformly on an interval and the derivatives $g_{m}^{'}$ converge uniformly with $g_{m} (t_{0}) \to g (t_{0})$ at one point, then $g^{'} = \lim_{m} g_{m}^{'}$ . (A sequence of real-valued functions converges uniformly if and only if it is uniformly Cauchy, The uniform limit of continuous real-valued functions on a metric space is continuous, A uniform limit of continuous complex-valued functions is continuous, If continuously differentiable functions converge at one point and their derivatives converge uniformly on a closed interval, then the functions converge uniformly to a differentiable function whose derivative is the derivative limit)

[F3]

A Banach space is a complete normed space; a subspace of a complete metric space is complete if and only if it is closed, under Countable Choice. (Banach space, Complete metric space: every Cauchy sequence converges in the space, Closed subspaces of complete metric spaces are complete; the converse under countable choice)

[F4]

The real mean value theorem bounds the increment of a differentiable function on a segment by the supremum of its derivative times the length of the segment. (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ )

Proof

technique · direct

1.1givenF1F2algebraA1

Uniform limits of the derivative fields. Since $(u_{j})$ is Cauchy in $∥ \cdot ∥_{C^{k, α} (Ω)}$ , for every multi-index $β$ with $∣ β ∣ \leq k$ the sequence $(D^{β} u_{j})$ is uniformly Cauchy on $Ω$ : for $j, l$ and every $x \in Ω$ , $∣ D^{β} u_{j} (x) - D^{β} u_{l} (x) ∣ \leq ∥ u_{j} - u_{l} ∥_{C^{k, α} (Ω)}$ . By [F2] there is a bounded function $v_{β}$ with $D^{β} u_{j} \to v_{β}$ uniformly on $Ω$ , and $v_{β}$ is continuous. Moreover $\sup_{Ω} ∣ v_{β} ∣ = \lim_{j} \sup_{Ω} ∣ D^{β} u_{j} ∣ \leq {lim inf}_{j} ∥ u_{j} ∥_{C^{k, α} (Ω)} < \infty$ , the last bound holding because a Cauchy sequence is bounded.

2.1step 1.1F1algebra

The limits are Hölder. For $∣ β ∣ = k$ and $x \neq y$ in $Ω$ , $∣ v_{β} (x) - v_{β} (y) ∣ = \lim_{j} ∣ D^{β} u_{j} (x) - D^{β} u_{j} (y) ∣ \leq {lim inf}_{j} [D^{β} u_{j}]_{0, α; Ω} ∣ x - y ∣^{α}$ ; hence $[v_{β}]_{0, α; Ω} \leq {lim inf}_{j} [D^{β} u_{j}]_{0, α; Ω} \leq {lim inf}_{j} ∥ u_{j} ∥_{C^{k, α} (Ω)} < \infty$ and $v_{β}$ is $α$ -Hölder on $Ω$ . Consequently $v_{0}$ (whose finiteness and continuity is step 1.1, including $k = 0$ , where no derivative is involved) satisfies $∥ v_{0} ∥_{C^{k, α} (Ω)} \leq {lim inf}_{j} ∥ u_{j} ∥_{C^{k, α} (Ω)} < \infty$ as soon as $v_{β} = D^{β} v_{0}$ for all $∣ β ∣ \leq k$ , which is proved next.

2.2step 1.1F1F2algebraF4

Identification of the limits with the derivatives of $v_{0}$ . Proceed by induction on $∣ β ∣$ . For $β = 0$ , $v_{0}$ is the limit. Suppose $v_{β} = D^{β} v_{0}$ is known on $Ω$ for some $∣ β ∣ < k$ ; fix $i$ and a ball $B ⋐ Ω$ (every point of $Ω$ lies in such a ball). On $B$ , all $u_{j}$ are $C^{k}$ ; for orders at least two, Continuous mixed partials of order $k$ are invariant under permutations identifies their derivative words with the canonical-order fields. Thus $D^{β} u_{j} \to v_{β}$ uniformly while $D^{β + e_{i}} u_{j} \to v_{β + e_{i}}$ uniformly; by [F2] applied to the restrictions to each coordinate segment inside $B$ (as in the one-variable theorem on a closed interval, at a fixed base point where $D^{β} u_{j}$ converges), the limit $v_{β}$ is differentiable in direction $e_{i}$ with $\partial_{i} v_{β} = v_{β + e_{i}}$ on $B$ ; Since every point lies in such a ball, this gives $\partial_{i} D^{β} v_{0} = D^{β + e_{i}} v_{0} = v_{β + e_{i}}$ on $Ω$ .

3.1step 2.1step 2.2F1F2F3algebra

Convergence in the Hölder norm. Let $ε > 0$ and choose $J$ with $∥ u_{j} - u_{l} ∥_{C^{k, α} (Ω)} \leq ε$ for $j, l \geq J$ . Fixing $l \geq J$ and passing to the limit in the componentwise bounds of steps 1.1 and 2.1 gives $\sup_{Ω} ∣ v_{β} - D^{β} u_{l} ∣ \leq ε$ for all $∣ β ∣ \leq k$ and $[v_{β} - D^{β} u_{l}]_{0, α; Ω} \leq ε$ for $∣ β ∣ = k$ ; hence $∥ v_{0} - u_{l} ∥_{C^{k, α} (Ω)} \leq C_{k} ε$ for every $l \geq J$ with a dimensional factor $C_{k}$ . So the Cauchy sequence converges in the norm to $v_{0} \in C_{b}^{k, α} (Ω)$ , and $C_{b}^{k, α} (Ω; K)$ is complete: it is a Banach space over $K$ (the vector-space operations are the pointwise ones and the norm is by [F1]). The complex case follows from the real case applied to real and imaginary parts, using [F2]'s complex uniform limit statement.

4.1step 3.1F1F2F3algebra

The boundary-condition subspace. Assume now $Ω$ is a bounded $C^{k, α}$ domain with nonempty boundary, and let $(u_{j})$ be a sequence in $X_{0}$ converging to $u$ in $C_{b}^{k, α} (Ω)$ . Each $u_{j}$ has a continuous extension ${\overset{ˉ}{u}}_{j}$ to $\overset{ˉ}{Ω}$ with ${\overset{ˉ}{u}}_{j} = 0$ on $\partial Ω$ . Since $\overset{ˉ}{Ω}$ is compact and the extensions are uniformly Cauchy on the dense set $Ω$ , they are uniformly Cauchy on $\overset{ˉ}{Ω}$ (for $x \in \overset{ˉ}{Ω}$ and $y \in Ω$ near $x$ , $∣ {\overset{ˉ}{u}}_{j} (x) - {\overset{ˉ}{u}}_{l} (x) ∣ = \lim_{y \to x} ∣ {\overset{ˉ}{u}}_{j} (y) - {\overset{ˉ}{u}}_{l} (y) ∣ \leq \sup_{Ω} ∣ u_{j} - u_{l} ∣$ ); hence ${\overset{ˉ}{u}}_{j}$ converges uniformly on $\overset{ˉ}{Ω}$ to a continuous $\overset{ˉ}{u}$ with $\overset{ˉ}{u} ∣_{Ω} = u$ and $\overset{ˉ}{u} = 0$ on the closed set $\partial Ω$ , so $u \in X_{0}$ . Thus $X_{0}$ is closed in the Banach space $C_{b}^{k, α} (Ω)$ , and [F3] makes it complete, hence a Banach space.

5.1step 3.1F1F2F3algebra∎

The closure class. Let $Ω$ be any bounded open nonempty set and let $u_{j} \in C^{k, α} (\overset{ˉ}{Ω}; K)$ converge to $u$ in $C_{b}^{k, α} (Ω; K)$ . For every $∣ β ∣ \leq k$ , let $w_{j, β}$ be the continuous extension of $D^{β} u_{j}$ . Density gives $\sup_{\overset{ˉ}{Ω}} ∣ w_{j, β} - w_{l, β} ∣ = \sup_{Ω} ∣ D^{β} u_{j} - D^{β} u_{l} ∣$ , so [F2] yields a continuous uniform limit $w_{β}$ on $\overset{ˉ}{Ω}$ . Its restriction is $D^{β} u$ , by convergence in the full norm. Thus $u$ belongs to the boundary-extension class, which is a closed linear subspace of $C_{b}^{k, α} (Ω; K)$ and is Banach by step 3.1 and [F3], with the same norm by [F1]. Its zero-boundary subspace is closed because the uniform limit $w_{0}$ of extensions vanishing on $\partial Ω$ also vanishes there, hence is Banach as well. No identification of the closure class with all of $C_{b}^{k, α} (Ω)$ is required.

Remarks

The interior completeness assertion holds for arbitrary open nonempty $Ω$ . The closure-class assertion assumes boundedness to match its definition; its proof and the closedness of the zero-boundary subspace require no boundary regularity. On an arbitrary bounded open set the closure class can be a proper closed subspace of $C_{b}^{k, α} (Ω)$ when $k \geq 1$ .
The local class $C_{l o c}^{k, α} (Ω)$ may contain functions with infinite full-domain norm; the displayed norm defines a Banach space on its finite-norm class $C^{k, α} (Ω) = C_{b}^{k, α} (Ω)$ . No assertion about completeness for a boundary pseudometric is made.

Depends on

Used by

Global Schauder estimate and classical Dirichlet solvability by the continuity method Theorem

Dependency tree · two levels

64 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

Leon Simon, Lectures on Partial Differential Equations (Stanford University; complete 118-page author notes, Chapter 12 Schauder Theory) (standard reference, not scraped)
Armin Schikorra, Partial Differential Equations I & II (version October 1, 2025; complete 281-page graduate lecture notes) (standard reference, not scraped)
John Villavert, Elementary Theory and Methods for Elliptic Partial Differential Equations (2017; complete 220-page lecture notes) (standard reference, not scraped)