Bounded C^{1,α} maps #
This file constructs the normed space of bounded continuously differentiable maps whose Fréchet
derivative is bounded and globally Hölder continuous, and proves that it is Banach when the
codomain is Banach. Its norm is the maximum of the supremum norm of the function and the
HolderSpace norm of its derivative. This is an equivalent form of the usual C^{1,α} norm
‖f‖_∞ + ‖Df‖_∞ + [Df]_α.
An element is represented by a bounded continuous function and a Hölder-space derivative, subject
to the condition that the latter is the Fréchet derivative of the former. The derivative field is
therefore uniquely determined, and C1HolderSpace.ext only asks for equality of the functions.
This is the first positive-order member of the bounded global C^{k,α} scale used in Schauder
estimates. It extends TauCeti.HolderSpace, which supplies the order-zero member and the complete
space in which the derivative fields converge. The file also proves the closed derivative-graph
lemma shared by the higher-order constructions.
Main declarations #
TauCeti.C1HolderSpace: boundedC¹maps with bounded globallyα-Hölder derivative.TauCeti.C1HolderSpace.valueL: the continuous linear map forgetting the derivative.TauCeti.C1HolderSpace.fderivL: the continuous linear map returning the Hölder derivative.TauCeti.C1HolderSpace.instCompleteSpace: the Banach-space structure.TauCeti.isClosed_setOf_hasFDerivAt: closedness of the bounded-continuous derivative graph.
References #
L. C. Evans, Partial Differential Equations, Section 6.3; D. Gilbarg and N. Trudinger, Elliptic Partial Differential Equations of Second Order, Section 4.1.
The set of bounded continuous fields satisfying the Fréchet derivative identity is closed.
The space of bounded C¹ maps whose Fréchet derivative is bounded and globally
α-Hölder. Its inherited product norm is
max ‖f‖_∞ (‖Df‖_∞ + [Df]_α).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A bounded C^{1,α} element coerces to its underlying function from E to F.
Equations
- TauCeti.C1HolderSpace.instCoeFun = { coe := fun (f : TauCeti.C1HolderSpace α E F) => ⇑(↑f).1 }
The underlying bounded continuous function of a bounded C^{1,α} map.
Equations
- f.toBoundedContinuousFunction = (↑f).1
Instances For
The Fréchet derivative, as a bounded globally Hölder function with values in continuous linear maps.
Instances For
Construct a bounded C^{1,α} map from a function, its Hölder derivative, and the derivative
identity.
Instances For
The constant map as a bounded C^{1,α} map.
Equations
Instances For
A constant bounded C^{1,α} map has zero derivative.
The recorded derivative is the Fréchet derivative of the underlying function.
The derivative accessor agrees with Mathlib's fderiv.
A bounded C^{1,α} map is differentiable.
A bounded C^{1,α} map is continuously differentiable.
The derivative field of a bounded C^{1,α} map is globally α-Hölder.
Two bounded C^{1,α} maps are equal when their underlying functions agree pointwise.
Forgetting the derivative defines a continuous linear map to bounded continuous functions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returning the derivative defines a continuous linear map to the global Hölder space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The C^{1,α} norm is the maximum of the supremum norm of the function and the
supremum-plus-Hölder norm of its derivative.
The supremum norm of the function is controlled by the C^{1,α} norm.
The Hölder-space norm of the derivative is controlled by the C^{1,α} norm.
Bounded C^{1,α} maps into a Banach space form a Banach space.