Higher interior regularity for H₀¹ weak solutions

James Guo, Partial Differential Equations (Course Lecture Notes), Theorem VIII.3.2 (Higher Interior Regularity, p. 65) gives the weak-coefficient version. The formalization below treats H₀¹ weak solutions u of L u = f, with globally defined coefficients and a separate globally Lipschitz hypothesis on the principal-coefficient representatives. With a_{ij} ∈ W^{k+1,∞}, b_i, c ∈ W^{k,∞} and f ∈ H^k, the solution lies in H^{k+2}_loc with

‖u‖_{H^{k+2}(V)} ≤ C (‖f‖_{H^k(Ω)} + ‖u‖_{L²(Ω)}) for every V ⋐ Ω,

the constant depending on the data and the pair V ⋐ Ω and on neither u nor f. Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2 (p. 332) is the same statement with C^{k+1} coefficients, which IsCkCoeff.toIsWkInftyCoeff shows to be the stronger hypothesis. The theorem below asks Guo's weak-derivative orders together with the separate pointwise IsLipCoeff bundle for the base case.

Shape of the induction

InteriorRegularityAt Op Ω k packages the conclusion at order k, and the theorem is an induction on k over that predicate.

• Order 0 is interior_H2_estimate with its (k, i)-indexed second derivatives assembled into a HasIteratedWeakDerivOn family of order 2.
• The step differentiates the equation once. Where u solves L u = f, the derivative ∂_l u solves L (∂_l u) = ∂_l f + R_l, with R_l collecting the terms in which the differentiation lands on a coefficient rather than on u. Those terms pair one derivative of a coefficient against derivatives of u of order at most two, so R_l sits in H^{k-1} once the order-k-1 conclusion is available for u itself. Applying the induction hypothesis to ∂_l u on an intermediate V ⋐ W ⋐ Ω gives ∂_l u ∈ H^{k+1}(V), which is u ∈ H^{k+2}(V).

The differentiated equation is already available as EllipticPdes.Regularity.differentiated_weakForm_div, and the admissibility of the test function it needs as interior_cutoffGrad_mem_H01.

Main declarations

• InteriorRegularityAt: the order-k conclusion, as a predicate, so that the induction has something to be an induction over.
• interiorRegularityAt_zero: the base case.
• exists_cutoffDeriv_weakForm: the differentiated equation, as a weak formulation for the cutoff derivative, which is what the induction hypothesis consumes.
• interiorRegularityAt_succ: the induction step.
• higher_interior_regularity: the theorem.

def EllipticPdes.Regularity.InteriorRegularityAt {n : ℕ} (Op : Sobolev.FullEllipticOp (n + 1)) {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩm : MeasurableSet Ω) (k : ℕ) : Prop

Order-k interior conclusion. For every compact V ⋐ Ω there is a constant, quantified before the solution and the datum, bounding every weak derivative of u of order at most k + 2 on V by ‖f‖_{H^k} + ‖u‖_{L²}. The datum's H^k norm enters through a bound M on its own iterated family, which IteratedL2Bound.norm_le shows to dominate ‖f‖.

Equations

• One or more equations did not get rendered due to their size.

theorem EllipticPdes.Regularity.interiorRegularityAt_zero {n : ℕ} (Op : Sobolev.FullEllipticOp (n + 1)) {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩm : MeasurableSet Ω) (hΩo : IsOpen Ω) (hA : IsLipCoeff Op.toEllipticCoeff) : InteriorRegularityAt Op hΩm 0

Base case: order zero is the interior H² estimate. The estimate interior_H2_estimate returns, for each direction pair (k, i), a weak k-derivative of ∂ᵢu on V together with its bound. Assembling those into a HasIteratedWeakDerivOn family of order 2 is a matter of naming: the empty list is u, a singleton [i] is ∂ᵢu, a pair [k, i] is the returned wki, and longer lists are unconstrained because D_step is asked only of lists shorter than 2.

The first-order step, which the H² estimate does not itself provide, is hasWeakDeriv_extendL2_of_mem_H01: the ambient encoding's coordinate i.succ is the weak i-derivative of coordinate 0 on the whole space, and hasWeakDerivOn_of_hasWeakDeriv localises it to V.

No constant is spent. The H² estimate bounds the sum of the three norms, so each of them is bounded on its own, and IteratedL2Bound.norm_le supplies ‖f‖ ≤ M.

theorem EllipticPdes.Regularity.exists_cutoffDeriv_weakForm {n : ℕ} (Op : Sobolev.FullEllipticOp (n + 1)) {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩm : MeasurableSet Ω) (hΩo : IsOpen Ω) (hA1 : IsLipCoeff Op.toEllipticCoeff) {k : ℕ} (hA : IsWkInftyCoeff Op.toEllipticCoeff (k + 2)) (hbc : IsWkInftyLower Op (k + 1)) (hk : InteriorRegularityAt Op hΩm k) {V : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hVc : IsCompact V) (hVΩ : V ⊆ Ω) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (u : ↥(Sobolev.H01 Ω)) (f : Sobolev.L2D Ω) (M : ℝ) (hfk : HasIteratedWeakDerivOn Ω (k + 1) f), IteratedL2Bound hfk M → (∀ (w : ↥(Sobolev.H01 Ω)), ((Op.fullBilin Ω) u) w = ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in Ω, ↑↑f x * ↑↑((↑w).ofLp 0) x) → ∀ (ℓ : Fin (n + 1)), ∃ (U : ↥(Sobolev.H01 Ω)) (F : Sobolev.L2D Ω) (hFk : HasIteratedWeakDerivOn Ω k F), restrictL2 ((extendL2 hΩm) ((↑U).ofLp 0)) = restrictL2 ((extendL2 hΩm) ((↑u).ofLp ℓ.succ)) ∧ (∀ (w : ↥(Sobolev.H01 Ω)), ((Op.fullBilin Ω) U) w = ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in Ω, ↑↑F x * ↑↑((↑w).ofLp 0) x) ∧ IteratedL2Bound hFk (C * (M + ‖(↑u).ofLp 0‖)) ∧ ‖(↑U).ofLp 0‖ ≤ C * (M + ‖(↑u).ofLp 0‖)

Differentiated equation as a weak formulation for a cutoff derivative. For a weak solution u of L u = f and each direction ℓ, there is an element U ∈ H₀¹(Ω) agreeing with ∂_ℓ u on V, a datum F ∈ L²(Ω) with k weak derivatives, and a weak formulation B[U, w] = ⟪F, w⟫ for every w ∈ H₀¹(Ω), with both ‖U‖ and the H^k bound on F controlled by the data.

This is Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2, step 3 in the shape the induction consumes, and it is where the analytic content of the step sits.

U is ξ · ∂_ℓ u for the middle cutoff of a tower for V ⋐ Ω, which EllipticPdes.Regularity.interior_cutoffGrad_mem_H01 places in H₀¹(Ω) and EllipticPdes.Regularity.restrictL2_extendL2_mulTest_xi makes invisible on V. F collects ∂_ℓ f, the terms of EllipticPdes.Regularity.differentiated_weakForm_wkInfty in which the differentiation lands on a coefficient, and the commutator with ξ. Each of those is a W^{k,∞} weight against a derivative of u of order at most two, so EllipticPdes.Regularity.exists_iteratedWeakDeriv_mul and EllipticPdes.Regularity.HasIteratedWeakDerivOn.sum assemble the family and its bound, and EllipticPdes.Regularity.weakForm_of_testFn extends the identity from test functions to H₀¹(Ω).

Order-k conclusion as a hypothesis

F pairs second derivatives of u against first derivatives of the coefficients, so F ∈ H^k asks for u ∈ H^{k+2} on a neighbourhood of tsupport ξ, which is the order-k conclusion at that compact set. Evans reaches for it at the same point: the datum (36) of §6.3.1, Theorem 2 contains D²u, and its H^k bound is read off the inductive hypothesis rather than off the solution's membership of H₀¹(Ω). Passing hk here rather than deriving it is what keeps the step an induction.

theorem EllipticPdes.Regularity.interiorRegularityAt_succ {n : ℕ} (Op : Sobolev.FullEllipticOp (n + 1)) {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩm : MeasurableSet Ω) (hΩo : IsOpen Ω) (hA1 : IsLipCoeff Op.toEllipticCoeff) {k : ℕ} (hA : IsWkInftyCoeff Op.toEllipticCoeff (k + 2)) (hbc : IsWkInftyLower Op (k + 1)) (hk : InteriorRegularityAt Op hΩm k) : InteriorRegularityAt Op hΩm (k + 1)

Induction step. Differentiating the equation once raises the order-k conclusion to order k + 1, under one more order of regularity on every coefficient.

∂_ℓ u lies outside H₀¹(Ω): it is a first derivative of an H₀¹ function and lies only in H¹_loc, so InteriorRegularityAt, which quantifies over H01 Ω, cannot be applied to it. exists_cutoffDeriv_weakForm supplies the cutoff that can be, together with its datum, and this step is what remains once that is in hand.

The induction hypothesis returns k + 2 weak derivatives of the cutoff derivative on V, which HasIteratedWeakDerivOn.congr reads as k + 2 weak derivatives of ∂_ℓ u itself, the cutoff being 1 there. Reassembling over ℓ through HasIteratedWeakDerivOn.ofDeriv gives u ∈ H^{k + 3}(V).

The constant is 2 C₁ C₀ + 1, with C₀ from the datum and C₁ from the induction hypothesis. The two summands of C₀ (M + ‖u‖) + ‖U‖ are each at most C₀ (M + ‖u‖), which is where the factor of two comes from, and the + 1 covers ‖u‖ itself, which the order-zero entry of the assembled family needs and which no derivative bound supplies.

theorem EllipticPdes.Regularity.higher_interior_regularity {n : ℕ} (Op : Sobolev.FullEllipticOp (n + 1)) {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩm : MeasurableSet Ω) (hΩo : IsOpen Ω) (hA1 : IsLipCoeff Op.toEllipticCoeff) (k : ℕ) (hA : IsWkInftyCoeff Op.toEllipticCoeff (k + 1)) (hbc : IsWkInftyLower Op k) : InteriorRegularityAt Op hΩm k

Higher interior regularity (Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2, p. 332; a variant of James Guo, Partial Differential Equations (Course Lecture Notes), Theorem VIII.3.2, p. 65). Evans states the result for C^{m+1} coefficients; the weak coefficient derivative hypotheses follow Guo's statement. This formalization additionally requires the specified principal-coefficient representatives to be globally Lipschitz for the base case, and quantifies over H₀¹ weak solutions. The pointwise Lipschitz hypothesis is retained separately from the weak-derivative bundles.

With W^{k+1,∞} principal coefficients, W^{k,∞} lower-order coefficients and an H^k datum, weak derivatives of every order up to k + 2 exist on each compact V ⋐ Ω. Their L² bounds use a constant quantified before the solution, datum and datum bound.

At k = 0, interiorRegularityAt_zero uses the pointwise IsLipCoeff hypothesis alone. The step to order k + 1 differentiates the equation once: its datum pairs second derivatives of each a_{ij} and first derivatives of b_i, c against derivatives of u of order at most two, so an H^k datum asks a_{ij} ∈ W^{k+2,∞} and b_i, c ∈ W^{k+1,∞} (exists_cutoffDatum), and the induction hypothesis at order k asks no more.