Moving a derivative onto the solution under Guo's coefficient hypothesis #
EllipticPdes.Regularity.principal_move, transport_move and zeroth_move move ∂_ℓ from
the test function onto the solution in the three terms of the equation, each by one application
of the Leibniz rule for a C¹ weight. Guo, Partial Differential Equations (Course
Lecture Notes), Theorem VIII.3.2 (p. 65) asks only for W^{k,∞} coefficients, which have no
classical derivative, and this file repeats the three with HasWeakDerivOn.mul_isWkInfty_left
in place of HasWeakDerivOn.mul_contDiff_left.
The statements differ from their C¹ counterparts in one place: where those write partialD ℓ (fun y => A.a y i j) for the derivative of a coefficient, these write the chosen representative
hA.D [ℓ] i j that IsWkInftyCoeff supplies. Everything else is unchanged, so a consumer that
reaches for the commutator by name sees the same shape.
Main declarations #
principal_move_wkInfty: the principal term, fora ∈ W^{1,∞}.transport_move_wkInfty: the transport term, forb_i ∈ W^{1,∞}.zeroth_move_wkInfty: the zeroth-order term, forc ∈ W^{1,∞}.commutator_move_wkInfty: the principal commutator, fora ∈ W^{2,∞}.differentiated_weakForm_div_wkInfty: the four moves assembled, divergence-datum form.differentiated_weakForm_wkInfty: Evans's equation (34), strong-datum form.
Reading the order-one data off a W^{k,∞} bundle #
The coefficient entry is measurable, read off the order-zero member of the family.
The order-one member of the family is a weak partial derivative of the coefficient entry.
The order-one member of the family is measurable.
The order-one member of the family is essentially bounded by bound 1.
The order-two member of the family is a weak partial derivative of the order-one member.
The order-two member of the family is measurable.
The order-two member of the family is essentially bounded by bound 2.
The function is measurable, read off the order-zero member of the family.
The order-one member of the family is a weak partial derivative of the function.
The order-one member of the family is measurable.
Three terms #
Principal term for a W^{1,∞} coefficient. For every direction pair the weighted first
derivative a_{ij}·∂ᵢu has weak ℓ-derivative (∂_ℓ a_{ij})·∂ᵢu + a_{ij}·∂_ℓ∂ᵢu, with the
coefficient derivative read off the family rather than taken classically. Testing against ∂ⱼφ
and summing gives
∑ ∫_V a_{ij}(∂ᵢu) ∂_ℓ∂ⱼφ = -∑ ∫_V [(∂_ℓ a_{ij})(∂ᵢu) + a_{ij}(∂ₗ∂ᵢu)] ∂ⱼφ.
Transport term for a W^{1,∞} coefficient.
∫_V b_i(∂ᵢu) ∂_ℓφ = -∫_V [(∂_ℓ b_i)(∂ᵢu) + b_i(∂ₗ∂ᵢu)] φ, with the coefficient derivative read
off the family.
Zeroth-order term for a W^{1,∞} coefficient.
∫_V c·u·∂_ℓφ = -∫_V [(∂_ℓ c)·u + c·(∂ₗu)] φ, with the coefficient derivative read off the
family.
Principal commutator #
Moving ∂ⱼ off the principal commutator for a W^{2,∞} coefficient. The coefficient
derivative ∂_ℓ a_{ij} is itself a W^{1,∞} 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 order of the coefficient hypothesis is used only here: it supplies the mixed member
hA.D [j, ℓ] of the family. The C² version commutator_move spends most of its length
turning the Hessian bound into a bound on the mixed partial through two operator-norm steps, and
the W^{2,∞} bundle has that bound outright.
Differentiated identity #
Differentiated weak formulation (divergence-datum form) for W^{1,∞} coefficients.
Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2, with every classical
coefficient derivative replaced by the chosen representative the W^{k,∞} bundles supply. Given
the localised weak identity hLoc for u on V together with the first and second weak
derivatives, for a fixed direction ℓ and every test function φ with tsupport φ ⊆ V, ∑ ∫_V a_{ij}(∂ₗ∂ᵢu) ∂ⱼφ + ∑ ∫_V (∂_ℓ a_{ij})(∂ᵢu) ∂ⱼφ = ∫_V (∂_ℓf) φ - ∑ ∫_V [(∂_ℓ b_i)(∂ᵢu)+b_i(∂ₗ∂ᵢu)] φ - ∫_V [(∂_ℓ c)u + c(∂_ℓu)] φ.
Where differentiated_weakForm_div asks for a ∈ C² and b, c ∈ C¹, this asks for one weak
derivative of each, which is Guo's hypothesis at the first order.
Differentiated weak formulation (Evans strong-datum form), for W^{2,∞} principal and
W^{1,∞} lower-order coefficients. Moving ∂ⱼ off the principal commutator with
commutator_move_wkInfty merges the second block of the left-hand side into the datum, leaving
∑ ∫_V a_{ij}(∂ₗ∂ᵢu) ∂ⱼφ = ∫_V f_ℓ · φ with
f_ℓ = ∂_ℓf - ∑_i [(∂_ℓ b_i)(∂ᵢu)+b_i(∂ₗ∂ᵢu)] - [(∂_ℓ c)u + c(∂_ℓu)] + ∑_{i,j}[(∂ⱼ∂_ℓ a_{ij})(∂ᵢu)+(∂_ℓ a_{ij})(∂ⱼ∂ᵢu)]
delivered as an explicit sum of integrals. Every derivative of a coefficient is read off the
bundle, so nothing here asks a coefficient to be differentiable.