Bounded C^{k,α} maps of every order #
This file constructs, for every k : ℕ, the normed space C_b^{k,α}(E, F) of C^k maps whose
iterated Fréchet derivatives through order k are bounded and whose k-th iterated derivative is
globally α-Hölder, and proves that it is Banach when the codomain is Banach. Its norm is
‖f‖ = ∑_{i ≤ k} ‖D^i f‖_∞ + [D^k f]_α,
where D^i f = iteratedFDeriv ℝ i f and the suprema use the operator norm of continuous
multilinear maps. These are the spatial trace spaces of parabolic Schauder theory, and the
targets of Schauder estimates of arbitrary order.
An element is represented by its family of iterated derivative fields: bounded continuous fields
E →ᵇ (E [×i]→L[ℝ] F) for i < k and a bounded Hölder field of order k, subject to the
condition that each field is the Fréchet derivative of the previous one, curried on the left.
This is exactly the condition that the family is a Taylor series up to order k for its
order-zero field, so the fields are the iterated derivatives of the underlying function. The
conditions are closed under uniform convergence, which gives completeness.
Main declarations #
TauCeti.CkHolderSpace k α E F: boundedC^kmaps with bounded derivatives through orderkand globallyα-Hölderk-th derivative.TauCeti.CkHolderSpace.iteratedFDeriv: the bounded continuousi-th derivative field fori ≤ k;TauCeti.CkHolderSpace.coe_iteratedFDerividentifies it with Mathlib'siteratedFDeriv.TauCeti.CkHolderSpace.contDiffandTauCeti.CkHolderSpace.memHolder_iteratedFDeriv: the regularity of an element;TauCeti.CkHolderSpace.ofContDiffis the converse constructor.TauCeti.CkHolderSpace.norm_eq: the norm is the sum of the supremum norms of the derivatives through orderkand theα-Hölder seminorm of thek-th derivative.TauCeti.CkHolderSpace.norm_fderiv_le_iteratedFDeriv_one,TauCeti.CkHolderSpace.norm_fderiv_fderiv_le_iteratedFDeriv_twoandTauCeti.CkHolderSpace.holderWith_fderiv_fderiv: bounds on the curried derivativesDfandD(Df)by the derivative fields, and the Hölder bound onD(Df)fork = 2.TauCeti.CkHolderSpace.iteratedFDerivLandTauCeti.CkHolderSpace.iteratedFDerivHolderL: the derivative fields as continuous linear maps; the second has operator norm at most one.TauCeti.CkHolderSpace.instCompleteSpace: completeness when the codomain is complete.
References #
D. Gilbarg and N. Trudinger, Elliptic Partial Differential Equations of Second Order, Section 4.1; A. Lunardi, Analytic Semigroups and Optimal Regularity in Parabolic Problems, Chapter 0.
Shortcut instance for bounded continuous fields of n-multilinear maps. Without it, instance
search for the module structure of ℓ¹ products of these fields indexed by the order n exceeds
the default synthesis depth. It is local so that the instance path for these fields is unchanged
outside this file, and no public statement below mentions it: only definition bodies and proofs
use it.
Instances For
Shortcut instance for bounded continuous fields of n-multilinear maps, needed for operator
norms of continuous linear maps into these fields indexed by the order n. It is local for the
same reason.
Instances For
The space of bounded C^k maps whose iterated Fréchet derivatives through order k are
bounded and whose k-th iterated derivative is globally α-Hölder. Its norm is
∑_{i ≤ k} ‖D^i f‖_∞ + [D^k f]_α.
Instances For
The bounded continuous i-th derivative field of a bounded C^{k,α} map, for i ≤ k. It
agrees with Mathlib's iteratedFDeriv by CkHolderSpace.iteratedFDeriv_eq.
Instances For
The k-th derivative field of a bounded C^{k,α} map, as an element of the bounded
Hölder space.
Instances For
The underlying function of a bounded C^{k,α} map: its order-zero derivative field, evaluated
on the empty tuple. Use the coercion ⇑f instead.
Instances For
A bounded C^{k,α} map is determined by its underlying function.
Two bounded C^{k,α} maps are equal when their underlying functions agree pointwise.
The recorded derivative fields are the iterated Fréchet derivatives of the underlying function.
The i-th derivative field is Mathlib's iteratedFDeriv of the underlying function.
A bounded C^{k,α} map is k times continuously differentiable.
The Hölder field, as a bounded continuous field, is the derivative field of order k.
The Hölder field records the k-th iterated Fréchet derivative.
The Hölder field is Mathlib's k-th iteratedFDeriv of the underlying function.
The k-th iterated Fréchet derivative of a bounded C^{k,α} map is globally α-Hölder.
The C^{k,α} norm is the sum of the supremum norms of the iterated derivatives through
order k and the α-Hölder seminorm of the k-th iterated derivative.
The supremum norm of each iterated derivative field is controlled by the C^{k,α} norm.
Each iterated derivative through order k is pointwise controlled by the C^{k,α} norm.
The values of a bounded C^{k,α} map are controlled by its C^{k,α} norm.
The α-Hölder seminorm of the k-th iterated derivative is controlled by the C^{k,α}
norm.
The values of a bounded C^{k,α} map are controlled by the supremum norm of its order-zero
field.
The first derivative of a bounded C^{k+1,α} map is controlled by the supremum norm of its
first derivative field.
The curried second derivative of a bounded C^{k+2,α} map is controlled by the supremum norm
of its second derivative field.
The derivative of a bounded C^{k+1,α} map is k times continuously differentiable.
The curried second derivative of a bounded C^{2,α} map is α-Hölder with the Hölder
seminorm of D²f.
The i-th derivative field, as a continuous linear map to bounded continuous fields. It is
bounded by the C^{k,α} norm pointwise, by CkHolderSpace.norm_iteratedFDeriv_le.
Instances For
The k-th derivative field, as a continuous linear map to the bounded Hölder space.
Instances For
The Hölder-space norm of the k-th derivative field is controlled by the C^{k,α} norm.
The k-th derivative map to the bounded Hölder space has operator norm at most one.
Build a bounded C^{k,α} map from a C^k function whose iterated derivatives through order
k are bounded and whose k-th iterated derivative is globally α-Hölder.
Instances For
Bounded C^{k,α} maps into a Banach space form a Banach space.
Bounded finite-order Hölder maps vanishing outside a prescribed set, as a submodule of the native derivative-graph space.
Instances For
Membership in the supported submodule means vanishing outside its defining set.
The support of an element of the supported Hölder submodule lies in its defining set.