Weak gradient of a W^{1,infinity} coefficient #
IsLipCoeff is the hypothesis the interior estimate reads, and the cutoff reduction that
takes the estimate from H_0^1(Omega) to H^1(Omega) reads one thing more: a weak gradient
of each coefficient entry, essentially bounded, which CoeffWeakGrad bundles. A C^1
coefficient supplies it through its classical partials (IsC1Coeff.coeffWeakGrad) and a
W^{k+1,infinity} family through its first order (IsWkInftyCoeff.coeffWeakGrad). This file
supplies it from the Lipschitz estimate alone, which is what Guo, Partial Differential
Equations I and II (Course Lecture Notes), Theorem VIII.2.2 (p. 63) and Gilbarg-Trudinger,
Elliptic Partial Differential Equations of Second Order, Theorem 8.8 (p. 179) ask of the
leading coefficients.
The argument #
Rademacher's theorem (LipschitzWith.ae_differentiableAt) gives a derivative almost
everywhere, and fderiv names it: the total fderiv of Mathlib is the derivative where one
exists and zero elsewhere, so coeffDa A l i j below is measurable (measurable_fderiv) and
bounded by the Lipschitz constant wherever the derivative exists
(norm_fderiv_le_of_lipschitz).
That it is the weak derivative is the difference quotient identity
∫ a(x) (φ(x - h e_l) - φ(x))/h = ∫ ((a(x + h e_l) - a(x))/h) φ(x),
exact for every h ≠ 0 by translation invariance of the volume, taken to the limit along
h = 1/(n+1). On the left the quotient of φ converges uniformly to -∂_l φ and is
supported in one compact set for every h ≤ 1; on the right the quotient of a is bounded
by A₁ and converges almost everywhere by Rademacher. Dominated convergence on each side
gives ∫ a ∂_l φ = -∫ (da) φ.
Main declarations #
IsLipCoeff.lipschitzWith: the estimate as aLipschitzWithstatement.coeffDa: the chosen representative of∂_l a_{ij}.measurable_coeffDa,IsLipCoeff.abs_da_le: its measurability and its bound, the bound being pointwise rather than essential, sincefderivis zero off the differentiability set.
What this file does not yet supply #
HasWeakPartial l (fun x => A.a x i j) (coeffDa A l i j), and with it
IsLipCoeff.coeffWeakGrad. The route is the one described above: the difference quotient
identity by measurePreserving_translate and MeasurePreserving.integral_comp, then
tendsto_integral_of_dominated_convergence on each side, the almost-everywhere convergence
of the quotient of a coming from LipschitzWith.ae_differentiableAt through
hasDerivAt_iff_tendsto_slope. Until it is proved, the cutoff reduction of
interior_H2_estimate_W12 reads a C¹ bundle and the H^1 statements of the interior
theory ask C¹ of the principal coefficients where Guo VIII.2.2 and Gilbarg-Trudinger 8.8
ask W^{1,∞}.
The Lipschitz estimate of IsLipCoeff as a LipschitzWith statement, which is what
Rademacher's theorem and the bound on the derivative are stated for.
The chosen representative of the weak partial ∂_l a_{ij}: the total fderiv applied to
the l-th basis vector, which is the classical partial wherever the entry is differentiable
and zero on the null set where it is not. It is written for the coefficient rather than for a
bundle over it, no hypothesis being needed to name it.
Equations
- EllipticPdes.Regularity.coeffDa A l i j x = (fderiv ℝ (fun (y : EuclideanSpace ℝ (Fin d)) => A.a y i j) x) (EuclideanSpace.single l 1)
Instances For
coeffDa is measurable, the total fderiv being measurable and evaluation at a vector
continuous. No regularity of the entry enters.
coeffDa is bounded by the Lipschitz constant everywhere: where the entry is differentiable
this is the converse mean value inequality, and elsewhere fderiv is zero.