Mixed second weak derivatives commute #
EllipticPdes.Regularity.differentiated_weakForm_wkInfty produces an equation whose principal
unknown is the vector (∂_ℓ∂ᵢu)ᵢ, one derivative in the differentiation direction of every
first derivative of the solution. The induction of Guo, Partial Differential Equations (Course
Lecture Notes), Theorem VIII.3.2 (p. 65) consumes it as an equation for ∂_ℓu,
whose gradient is (∂ᵢ∂_ℓu)ᵢ. Those two vectors agree only because mixed weak derivatives
commute, and HasIteratedWeakDerivOn is deliberately built without presuming it.
Absence of local integrability #
Testing shows only that the difference of the two second derivatives annihilates every test
function supported in the region, and the fundamental lemma of the calculus of variations turns
that into vanishing almost everywhere on an open set. Reaching for it here would drag in local
integrability of an L² class, which is a detour.
A cutoff is shorter and is the form every consumer below takes anyway. For a test function χ
supported in
the region, χ·ρ is admissible for every whole-space test function ρ, so the whole-space
class of χ·w annihilates every test class and
EllipticPdes.Regularity.annihilates_of_forall_testCls kills it outright. Every term the
induction rewrites has a factor of the middle cutoff or one of its derivatives, and the outer
cutoff of the tower is identically 1 on a neighbourhood of that support, so the cut-off
identity is all that is ever asked for.
Main declarations #
partialD_comm: classical partial derivatives of a smooth function commute.mulTest_eq_zero_of_forall_testFn: a class annihilating every test function is killed by any cutoff supported in the region.mulTest_weakDerivOn_unique: two weak derivatives of one class agree after a cutoff.mulTest_mixed_weakDeriv_comm: the two mixed second weak derivatives agree after a cutoff.
Classical partial derivatives commute #
Schwarz for partialD. The i-th partial of the ℓ-th partial of a smooth function is
the ℓ-th partial of its i-th partial.
partialD ℓ φ is fun y => fderiv ℝ φ y (eℓ), an application of a differentiable
map into continuous linear maps against a constant, so fderiv_clm_apply reads its derivative
off fderiv ℝ (fderiv ℝ φ) with the two arguments flipped. Symmetry of the second Fréchet
derivative then swaps them back.
Vanishing of a class orthogonal to every test function #
Test-annihilation kills the cut-off class. If w ∈ L²(V) integrates to zero against
every test function supported in V, then χ·w = 0 for any test function χ supported in
V.
For a whole-space test function ρ, the product χ·ρ is supported in tsupport χ ⊆ V, so it
is one of the functions the hypothesis covers. The whole-space extension of χ·w therefore
annihilates every test class, and annihilates_of_forall_testCls makes it zero. Extension by
zero preserves the norm, so χ·w itself is zero.
Uniqueness of the weak derivative on a region after a cutoff. Two weak ℓ-derivatives of
the same class pair identically with every test function supported in the region, so their
difference is killed by any cutoff supported there.
The region is not asked to be open, which is why the conclusion has the cutoff. A weak derivative on a set with empty interior is constrained by nothing, and the consumers multiply by a cutoff regardless.
Mixed second weak derivatives commute #
Mixed second weak derivatives commute after a cutoff. Where uᵢ and u_ℓ are weak
first derivatives of u on V, and u_{ℓi} is a weak ℓ-derivative of uᵢ while u_{iℓ}
is a weak i-derivative of u_ℓ, the two agree once multiplied by any test function supported
in V.
Two integrations by parts move each of them onto u: ∫ u_{ℓi} φ = ∫ u ∂ᵢ∂_ℓφ and
∫ u_{iℓ} φ = ∫ u ∂_ℓ∂ᵢφ, admissibly, since a partial derivative of a test function supported
in V is again one. partialD_comm identifies the two right-hand sides, so the difference
annihilates every test function supported in V.