Differentiated-equation integral identity #
For u ∈ H₀¹(Ω) weakly solving Lu = f with C² principal coefficients, this file builds
towards the differentiated-equation integral identity of Evans, Partial Differential
Equations (2nd ed.), §6.3.1, Theorem 2: for a fixed direction ℓ and every smooth
compactly-supported test φ with tsupport φ ⊆ V,
∑_{i,j} ∫_V a_{ij} (∂_ℓ∂ᵢu) ∂ⱼφ + ∑_{i,j} ∫_V (∂_ℓ a_{ij})(∂ᵢu) ∂ⱼφ = ∫_V f_ℓ · φ
with f_ℓ an explicit lower-order datum. The identity is stated in HasWeakDerivOn-style
integration by parts on plain Lp ℝ 2 (volume.restrict V) classes.
This file starts with the small calculus facts used repeatedly throughout this file: the partial
derivative of a smooth (resp. compactly supported) test function is again smooth (resp.
compactly supported), so ∂ⱼφ is again an admissible HasWeakDerivOn test function, and the
pointwise Leibniz rule for partialD against a product.
Test-function calculus #
The partial derivative of a C^∞ function is C^∞.
The partial derivative of a compactly-supported function has compact support.
∂ⱼφ is again an admissible HasWeakDerivOn test function on V when φ is.
Coefficient mollification #
Weighted weak-derivative product rule #
Weak-derivative Leibniz with a C¹ weight. If g has weak ℓ-derivative g' on V,
and a is C¹ with a, ∂_ℓ a bounded almost everywhere (so the products below are L²(V)
classes), then a·g has weak ℓ-derivative (∂_ℓ a)·g + a·g' on V. Proved by mollifying the
globally defined coefficient a, which keeps the test function C^∞ and needs no support margin
at ∂V.
Moving ∂_ℓ onto u in the principal term #
Moving ∂_ℓ from the test function onto u in the principal term. For every direction
pair the coefficient-weighted first derivative a_{ij}·∂ᵢu has weak ℓ-derivative
(∂_ℓ a_{ij})·∂ᵢu + a_{ij}·∂_ℓ∂ᵢu; testing against ∂ⱼφ yields, summed over i,j,
∑ ∫_V a_{ij}(∂ᵢu) ∂_ℓ∂ⱼφ = -∑ ∫_V [(∂_ℓ a_{ij})(∂ᵢu) + a_{ij}(∂ₗ∂ᵢu)] ∂ⱼφ.
Transport, zeroth-order and datum terms #
Transport term. Moving ∂_ℓ from the test function onto ∂ᵢu weighted by the transport
coefficient b_i: ∫_V b_i(∂ᵢu) ∂_ℓφ = -∫_V [(∂_ℓ b_i)(∂ᵢu) + b_i(∂ₗ∂ᵢu)] φ. A direct
specialisation of HasWeakDerivOn.mul_contDiff_left at weight b_i and g := ∂ᵢu, tested
against φ itself, which is already C^∞, compactly supported, with tsupport φ ⊆ V.
Zeroth-order term. Moving ∂_ℓ from the test function onto u weighted by the
zeroth-order coefficient c: ∫_V c·u·∂_ℓφ = -∫_V [(∂_ℓ c)·u + c·(∂ₗu)] φ. The same
specialisation of HasWeakDerivOn.mul_contDiff_left at weight c and g := u.
Datum term. Given that f has weak ℓ-derivative Df on V, moving ∂_ℓ off the
test function is literally the defining property of HasWeakDerivOn: ∫_V f·∂_ℓφ = -∫_V (∂_ℓf)·φ. This is where the development assumes f ∈ H¹_loc(V), strictly stronger than the f ∈ L² already available from interior_H2_estimate, and is what makes ∂_ℓ f an L²(V) class
feeding the datum f_ℓ.
Assembly of the differentiated identity #
Mixed-partial symmetry for test functions. For a C^∞ function the two classical
second partials agree: ∂_ℓ ∂ⱼφ = ∂ⱼ ∂_ℓφ. This is mathlib's symmetry of the second Fréchet
derivative (second_derivative_symmetric), transported through the partialD-as-directional-
fderiv notation via fderiv_clm_apply.
Differentiated weak formulation (divergence-datum form), Evans, Partial Differential
Equations (2nd ed.), §6.3.1, Theorem 2. Given the local weak identity hLoc for u on V
together with the first/second weak-derivative data, for a fixed direction ℓ and every
admissible test φ with tsupport φ ⊆ V, the difference quotient ∂_ℓu satisfies ∑ ∫_V a_{ij}(∂ₗ∂ᵢu) ∂ⱼφ + ∑ ∫_V (∂_ℓ a_{ij})(∂ᵢu) ∂ⱼφ = ∫_V (∂_ℓf) φ - ∑ ∫_V [(∂_ℓ b_i)(∂ᵢu)+b_i(∂ₗ∂ᵢu)] φ - ∫_V [(∂_ℓ c)u + c(∂_ℓu)] φ. The local weak formulation hLoc on
plain integrals is a hypothesis: deriving it from the divergence-form bilinear pairing is the
repackaging deferred to a later step.
Principal commutator in strong-datum form (needs C²) #
Moving ∂ⱼ off the principal commutator (needs a ∈ C²). For a fixed direction pair
i, j the coefficient gradient ∂_ℓ a_{ij} is a C¹ weight, so the product (∂_ℓ a_{ij})·∂ᵢu
has a weak j-derivative and testing against φ moves ∂ⱼ onto the product: ∫_V (∂_ℓ a_{ij})(∂ᵢu) ∂ⱼφ = -∫_V [(∂ⱼ∂_ℓ a_{ij})(∂ᵢu) + (∂_ℓ a_{ij})(∂ⱼ∂ᵢu)] φ. The second-derivative
bound A2/hess_bdd is used only here: it controls the mixed partial ∂ⱼ∂_ℓ a_{ij} appearing
in the commutator datum.
Evans strong-datum differentiated weak formulation #
Differentiated weak formulation (Evans strong-datum form), Evans, Partial Differential
Equations (2nd ed.), §6.3.1, Theorem 2. Starting from the divergence-datum identity
differentiated_weakForm_div and moving ∂ⱼ off the principal commutator with commutator_move
(which needs a ∈ C²), the second block of the left-hand side merges into the datum, leaving the
Evans strong form
∑ ∫_V a_{ij}(∂ₗ∂ᵢu) ∂ⱼφ = ∫_V f_ℓ · φ.
The datum f_ℓ is delivered as an explicit sum of L²(V) integrals on the right,
f_ℓ = ∂_ℓf - ∑_i [(∂_ℓ b_i)(∂ᵢu)+b_i(∂ₗ∂ᵢu)] - [(∂_ℓ c)u + c(∂_ℓu)] + ∑_{i,j}[(∂ⱼ∂_ℓ a_{ij})(∂ᵢu)+(∂_ℓ a_{ij})(∂ⱼ∂ᵢu)];
packaging it into a single L²(V) class is a trivial-but-verbose follow-up left undone. The full
second-derivative family hD2_j (the j-derivative of every ∂ᵢu) is what the commutator needs
beyond the single direction used in the divergence-datum form.