Localising the bilinear pairing to plain integrals #
The weak formulation a solution satisfies pairs H1amb Ω vectors through the bounded bilinear
form Op.fullBilin. Every localised step of interior regularity instead works with plain
integrals over a compact V ⊆ Ω against a test function supported in V, on
Lp ℝ 2 (volume.restrict V) classes. This file is the bridge between the two.
The derivation is mechanical. A test function supported in V has its graph in H₀¹(Ω), so the
weak formulation applies to it; EllipticCoeff.bilin_apply and
FullEllipticOp.lowerBilin_apply expand the pairing into inner products; inner_actL_eq and
inner_mulCoeffL_eq turn each of those into an integral over Ω; each integrand has a factor
vanishing off tsupport v ⊆ V, so the integral shrinks to V; and the restriction of the
whole-space extension of each coordinate agrees with that coordinate on V.
The localised identity is the hypothesis hLoc of differentiated_weakForm and
differentiated_weakForm_div, which nothing discharged before. Discharging it makes the
differentiated-equation identity of Evans, Partial Differential Equations (2nd ed.),
§6.3.1, Theorem 2, reachable from the weak formulation itself.
Main declarations #
localWeakForm_of_fullBilin: the localised plain-integral weak identity onV.differentiated_weakForm_of_weakSolution: the differentiated-equation identity, with every hypothesis except the weakℓ-derivative of the datum discharged from the weak formulation and the interiorH²estimate.
Localised plain-integral weak identity #
Localised weak formulation (Evans, Partial Differential Equations (2nd ed.), §6.3.1,
Theorem 2). A weak solution u ∈ H₀¹(Ω) of L u = f, stated through the bilinear pairing
Op.fullBilin over all of Ω, satisfies the plain-integral identity ∑_{i,j} ∫_V a_{ij}(∂ᵢu) ∂ⱼv + ∑_i ∫_V b_i (∂ᵢu) v + ∫_V c u v = ∫_V f v on any measurable V ⊆ Ω, for every test
function v with tsupport v ⊆ V, with each coordinate read as the V-restriction of its
whole-space extension by zero. This is the shape the differentiated-equation identity takes as
its hypothesis hLoc.
Differentiated-equation identity from the weak formulation #
Differentiated-equation identity for a weak solution (Evans, Partial Differential
Equations (2nd ed.), §6.3.1, Theorem 2). For a weak solution u ∈ H₀¹(Ω) of L u = f with
C² principal coefficients and C¹ lower-order coefficients, and any compact V ⋐ Ω, the
second weak derivatives of u on V exist and are bounded by the data, and for every direction
ℓ in which the datum has a weak derivative Df, the pair (∂_ℓ∂ᵢu, Df) satisfies Evans'
equation (34) against every test function supported in V.
Every hypothesis of differentiated_weakForm other than the weak ℓ-derivative of f is
discharged here: the second derivatives come from interior_H2_estimate, the first
derivatives from hasWeakDeriv_extendL2_of_mem_H01, and the localised weak identity from
localWeakForm_of_fullBilin. The weak derivative of f cannot be dropped, since Evans (26)
assumes f ∈ H^m(U) and his datum (36) contains D^α f.