Interpolation inequalities for derivatives #

This file proves the supremum-norm interpolation inequalities that control an intermediate derivative by a small multiple of a higher one plus a large multiple of the function. They are used to absorb lower-order terms in Schauder estimates, elliptic and parabolic.

The basic estimate is a first-order Taylor bound: if g has derivative g' and g' is α-Hölder with constant H on a segment from x to x + w, then ‖g (x + w) - g x - g' x w‖ ≤ H ‖w‖^(1 + α). Hence

‖g' x w‖ ≤ ‖g (x + w)‖ + ‖g x‖ + H ‖w‖^(1 + α).

Choosing ‖w‖ = ε in every direction gives, on the whole space,

‖D^(k+1) f‖_∞ ≤ 2 ε⁻¹ ‖D^k f‖_∞ + ε^α [D^(k+1) f]_α

for every ε > 0. For α = 1 this is the Landau-type inequality ‖D^(k+1) f‖_∞ ≤ 2 ε⁻¹ ‖D^k f‖_∞ + ε ‖D^(k+2) f‖_∞. Combining the two and absorbing the supremum of D^(k+2) f, which must be finite a priori, gives

‖D^(k+2) f‖_∞ ≤ 32 ε⁻² ‖D^k f‖_∞ + 2 ε^α [D^(k+2) f]_α.

All constants are absolute: they depend neither on the dimension nor on α.

Interior estimates need local bounds, which use the second derivative. If g'' is α-Hölder with constant H on s, the second-order Taylor remainder of g along a segment in s is at most H ‖w‖^(2 + α). In the symmetric difference g (x + w) - g (x - w) the second-order terms cancel, so at the centre x of a closed ball of radius ε in s, with ‖g‖ ≤ M there,

‖g' x‖ ≤ M / ε + H ε^(1 + α),

and at the centre of a closed ball of radius 2 ε in s, ‖g'' x‖ ≤ 2 M / ε² + 3 H ε^α. Only the values of g and the Hölder constant of g'' on s enter. For a function which is C² on an open set containing s, with D²u α-Hölder on s, these are bounds on ‖Du‖ and ‖D²u‖.

On a closed interval [a, b] the same argument applies to one-sided derivatives within [a, b], for steps h with 2 h ≤ b - a, since from each point of [a, b] a step of length h in one of the two directions stays in the interval. With temporal Hölder exponent α / 2 and h = ε², this is the estimate for time derivatives on a slab used in parabolic Hölder spaces.

For a function u (x, t) of space and time, the same Taylor bound at the spatial scale h = √|t - s|, applied to the difference u (·, t) - u (·, s), gives

‖D_x u (x, t) - D_x u (x, s)‖ ≤ (C₂ + Cₜ) |t - s|^((1 + α) / 2),

where C₂ is the α / 2-Hölder constant in time of D_x² u and Cₜ is the α-Hölder constant in space of ∂ₜ u. The increment of the difference over a spatial step of length h is controlled by the mean value inequality in time and the spatial Hölder bound on ∂ₜ u, and its linear approximation error by the difference of the Hessians.

Main declarations #

HolderOnWith.norm_image_sub_sub_le_of_hasFDerivWithinAt: the first-order Taylor bound for a Hölder derivative.
HolderOnWith.norm_sub_fderiv_le_of_mem_ball: the Taylor remainder on a ball for the derivative of a differentiable function.
HolderOnWith.norm_apply_le_of_hasFDerivWithinAt: the resulting bound on a directional derivative.
HolderOnWith.norm_le_of_hasFDerivWithinAt_ball: the local interpolation inequality on a ball, also applicable to differences of two functions.
HolderOnWith.norm_fderiv_sub_fderiv_le_of_norm_sub_le_ball: comparison of two derivatives from uniform function error and possibly different Hölder constants.
HolderWith.norm_le_of_hasFDerivAt, HolderWith.norm_fderiv_le_of_norm_le and HolderWith.norm_iteratedFDeriv_succ_le_of_norm_le: the interpolation inequality on the whole space.
ContDiff.norm_iteratedFDeriv_succ_le_of_norm_iteratedFDeriv_le: the Landau-type inequality.
HolderWith.norm_iteratedFDeriv_add_two_le_of_norm_le and HolderWith.norm_iteratedFDeriv_succ_le_of_norm_le_of_bddAbove: the absorbed bounds on the two derivatives above D^k f, and HolderWith.norm_iteratedFDeriv_succ_le_and_norm_iteratedFDeriv_add_two_le: both bounds with one constant, for scales ε ≤ 1, and HolderWith.norm_fderiv_le_and_norm_iteratedFDeriv_two_le: its specialisation to k = 0, stated for a function bounded in norm.
HolderOnWith.norm_image_sub_sub_sub_le_of_hasFDerivWithinAt: the second-order Taylor bound for a Hölder second derivative.
HolderOnWith.norm_le_of_hasFDerivWithinAt_of_closedBall_subset and HolderOnWith.norm_le_of_hasFDerivWithinAt_of_closedBall_two_mul_subset: the local interpolation inequalities for the first and second derivatives on a ball.
HolderOnWith.norm_fderiv_le_of_contDiffOn and HolderOnWith.norm_iteratedFDeriv_two_le_of_contDiffOn: the same for a C² function.
HolderOnWith.norm_le_of_hasDerivWithinAt_Icc: the interpolation inequality for derivatives within a closed interval.
TauCeti.holderOnWith_Icc_of_hasFDerivAt_of_hasDerivWithinAt: the temporal (1 + α) / 2-Hölder continuity of the spatial derivative.

References #

D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Section 6.8 (interpolation inequalities).
A. Lunardi, Analytic Semigroups and Optimal Regularity in Parabolic Problems, Chapter 0.
O. A. Ladyzhenskaya, V. A. Solonnikov, N. N. Ural'tseva, Linear and Quasi-linear Equations of Parabolic Type, Chapter II (parabolic Hölder spaces).