Differentiated identity for a weak solution under Guo's coefficient hypothesis

EllipticPdes.Regularity.differentiated_weakForm_of_weakSolution discharges every hypothesis of the differentiated identity except the weak ℓ-derivative of the datum, and asks for C² principal and C¹ lower-order coefficients. Guo, Partial Differential Equations (Course Lecture Notes), Theorem VIII.3.2 (p. 65) asks instead for W^{k+2,∞} and W^{k+1,∞}, and this file repeats the bridge under that hypothesis.

One hypothesis on the principal part remains beyond the bundles. The interior H² estimate is proved by difference quotients, which asks the Lipschitz estimate of IsLipCoeff, exactly as higher_interior_regularity asks for it in its base case. What the W^{k,∞} bundles remove is the second classical derivative of the principal part and the first of the lower-order coefficients.

Main declarations

• differentiated_weakForm_of_weakSolution_wkInfty: Evans's equation (34) for a weak solution, with every coefficient derivative read off a W^{k,∞} bundle.

theorem EllipticPdes.Regularity.differentiated_weakForm_of_weakSolution_wkInfty {n : ℕ} (Op : Sobolev.FullEllipticOp (n + 1)) {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩm : MeasurableSet Ω) (hΩo : IsOpen Ω) (hA1 : IsLipCoeff Op.toEllipticCoeff) {k m : ℕ} (hA : IsWkInftyCoeff Op.toEllipticCoeff (k + 2)) (hbc : IsWkInftyLower Op (m + 1)) (ℓ : Fin (n + 1)) {V : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hVc : IsCompact V) (hVΩ : V ⊆ Ω) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (u : ↥(Sobolev.H01 Ω)) (f : Sobolev.L2D Ω) (Df : Sobolev.L2D V), HasWeakDerivOn V ℓ (restrictL2 ((extendL2 hΩm) f)) Df → (∀ (w : ↥(Sobolev.H01 Ω)), ((Op.fullBilin Ω) u) w = ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in Ω, ↑↑f x * ↑↑((↑w).ofLp 0) x) → ∃ (D2 : Fin (n + 1) → Fin (n + 1) → Sobolev.L2D V), (∀ (p i : Fin (n + 1)), HasWeakDerivOn V p (restrictL2 ((extendL2 hΩm) ((↑u).ofLp i.succ))) (D2 p i)) ∧ (∀ (p i : Fin (n + 1)), ‖D2 p i‖ + ‖restrictL2 ((extendL2 hΩm) ((↑u).ofLp i.succ))‖ + ‖restrictL2 ((extendL2 hΩm) ((↑u).ofLp 0))‖ ≤ C * (‖f‖ + ‖(↑u).ofLp 0‖)) ∧ ∀ (φ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ V → ∑ i : Fin (n + 1), ∑ j : Fin (n + 1), ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in V, Op.a x i j * ↑↑(D2 ℓ i) x * Sobolev.partialD j φ x = (((∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in V, ↑↑Df x * φ x) - ∑ i : Fin (n + 1), ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in V, ((hbc.bReg i).D [ℓ] x * ↑↑(restrictL2 ((extendL2 hΩm) ((↑u).ofLp i.succ))) x + Op.b x i * ↑↑(D2 ℓ i) x) * φ x) - ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in V, (hbc.cReg.D [ℓ] x * ↑↑(restrictL2 ((extendL2 hΩm) ((↑u).ofLp 0))) x + Op.c x * ↑↑(restrictL2 ((extendL2 hΩm) ((↑u).ofLp ℓ.succ))) x) * φ x) + ∑ i : Fin (n + 1), ∑ j : Fin (n + 1), ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in V, (hA.D [j, ℓ] i j x * ↑↑(restrictL2 ((extendL2 hΩm) ((↑u).ofLp i.succ))) x + hA.D [ℓ] i j x * ↑↑(D2 j i) x) * φ x

Differentiated-equation identity for a weak solution with W^{k,∞} coefficients. For a weak solution u ∈ H₀¹(Ω) of L u = f 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's equation (34) against every test function supported in V, with each coefficient derivative read off its bundle.

The H² estimate supplies the second derivatives and their bound, hasWeakDeriv_extendL2_of_mem_H01 the first derivatives, and localWeakForm_of_fullBilin the localised weak identity. Only the weak derivative of f is left as a hypothesis, since Evans's datum (36) contains D^α f.