Higher interior regularity for a weak solution in H¹

Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2 (p. 332): for a^{ij}, b^i, c ∈ C^{m+1}(U), f ∈ H^m(U) and a weak solution u ∈ H¹(U) of L u = f, u ∈ H^{m+2}_loc(U) with ‖u‖_{H^{m+2}(V)} ≤ C (‖f‖_{H^m(U)} + ‖u‖_{L²(U)}) for V ⋐ U.

The statement here is for a local weak solution U ∈ W12 Ω with no boundary condition. It is read off higher_interior_regularity, stated for H₀¹ solutions, through the cutoff reduction, by induction on the order.

• Order k at V. Take η = 1 near V, supported in Ω. η U ∈ H₀¹(Ω) solves an equation whose datum pairs f and the coordinates of U against weights supported in tsupport η (reduction_testFn). If every coordinate of U has k weak derivatives on tsupport η, the datum has k weak derivatives on Ω (exists_reductionDatum), the H₀¹ theorem at order k gives η U₀ in H^{k+2}(V), and η = 1 on V (restrictL2_extendL2_cutoffMul) makes that U₀.
• The hypothesis at order k + 1 on a compact W is the conclusion at order k on tsupport θ for θ = 1 near W: U₀ has k + 2 weak derivatives there, and on W the first of them are the gradient coordinates of U by uniqueness of the weak derivative after the cutoff θ (exists_collarFamily_of_weakDerivOn). At order 0 the hypothesis asks for the L² norms of the coordinates on W, which the Caccioppoli estimate exists_norm_mulTest_grad_le bounds by ‖f‖ + ‖U₀‖.

The bound has ‖U₀‖_{L²(Ω)} on the right, as in Evans.

Main declarations

• LocalRegularityAt: the order-k conclusion for local weak solutions.
• LocalFamiliesAt: the order-k hypothesis on the coordinates of the solution.
• localRegularityAt_of_localFamiliesAt, localFamiliesAt_zero, localFamiliesAt_succ.
• higher_interior_regularity_W12: the theorem, with a^{ij} ∈ W^{k+1,∞} and C¹, and b^i, c ∈ W^{k,∞}.
• localRegularityAt_zero_of_isC1Coeff: order zero from C¹ principal coefficients alone.

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

Order-k interior conclusion for local weak solutions. 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 M + ‖U₀‖, for a datum with k weak derivatives bounded by M.

Equations

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

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

Order-k hypothesis on the coordinates. For every compact W ⊆ Ω every coordinate of a local weak solution, the function and its gradient alike, has k weak derivatives on W, bounded by M + ‖U₀‖ with a constant quantified before the solution and the datum.

Equations

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

theorem EllipticPdes.Regularity.restrictL2_extendL2_mulTest_of_eqOn {n : ℕ} {Ω W : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩm : MeasurableSet Ω) (hWm : MeasurableSet W) (hWΩ : W ⊆ Ω) {ζ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} (hζ : Sobolev.IsTestFn Ω ζ) (hζW : Set.EqOn ζ 1 W) (g : Sobolev.L2D Ω) : restrictL2 ((extendL2 hΩm) ((mulTest hζ) g)) = restrictL2 ((extendL2 hΩm) g)

Invisibility of a cutoff on a set where it is one. For ζ = 1 on W ⊆ Ω, cutting ζ g down to W is cutting g down to W.

theorem EllipticPdes.Regularity.localFamiliesAt_zero {n : ℕ} (Op : Sobolev.FullEllipticOp (n + 1)) {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩm : MeasurableSet Ω) (hΩo : IsOpen Ω) : LocalFamiliesAt Op hΩm 0

Hypothesis at order zero. At order zero the hypothesis on the coordinates asks only for their L² norms on W. ‖U₀‖ bounds the function, and the gradient, cut off by ζ = 1 near W, is bounded by ‖f‖ + ‖U₀‖ through the Caccioppoli estimate.

theorem EllipticPdes.Regularity.localFamiliesAt_succ {n : ℕ} (Op : Sobolev.FullEllipticOp (n + 1)) {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩm : MeasurableSet Ω) (hΩo : IsOpen Ω) {k : ℕ} (hk : LocalRegularityAt Op hΩm k) : LocalFamiliesAt Op hΩm (k + 1)

Hypothesis at k + 1 from the conclusion at k. For a compact W, the conclusion at order k on tsupport θ, with θ = 1 near W, gives U₀ its k + 2 weak derivatives on W, whose first entries are the gradient coordinates of U by exists_collarFamily_of_weakDerivOn. Each coordinate then has k + 1.

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

Conclusion at order k from the hypothesis at order k. The step that reads the H₀¹ theorem higher_interior_regularity off the cutoff reduction: for η = 1 near V, the datum of η U has k weak derivatives once the coordinates of U have them on tsupport η, and the conclusion for η U on V is the conclusion for U.

def EllipticPdes.Regularity.isWkInftyZero {n : ℕ} {f : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} (hf : Measurable f) {M : ℝ} (hM0 : 0 ≤ M) (hM : ∀ᵐ (x : EuclideanSpace ℝ (Fin (n + 1))), |f x| ≤ M) : IsWkInfty f 0

An essentially bounded measurable function is in W^{0,∞}: the family is constant and no weak derivative is asked.

Equations

• EllipticPdes.Regularity.isWkInftyZero hf hM0 hM = { D := fun (x : List (Fin (n + 1))) => f, D_nil := ⋯, D_meas := ⋯, D_step := ⋯, bound := fun (x : ℕ) => M, bound_nonneg := ⋯, ess_bdd := ⋯ }

def EllipticPdes.Regularity.isWkInftyLowerZero {n : ℕ} (Op : Sobolev.FullEllipticOp (n + 1)) : IsWkInftyLower Op 0

The lower-order coefficients of every FullEllipticOp are in W^{0,∞}.

Equations

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

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

Higher interior regularity for a weak solution in H¹ (Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2, p. 332). A local weak solution U ∈ W12 Ω of L U = f, with no boundary condition, W^{k+1,∞} principal coefficients of class C¹, W^{k,∞} lower-order coefficients and a datum with k weak derivatives bounded by M, has weak derivatives of every order up to k + 2 on each compact V ⊆ Ω, bounded by C (M + ‖U₀‖) with C quantified before the solution and the datum.

theorem EllipticPdes.Regularity.localRegularityAt_zero_of_isC1Coeff {n : ℕ} (Op : Sobolev.FullEllipticOp (n + 1)) {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩm : MeasurableSet Ω) (hΩo : IsOpen Ω) (hA1 : IsC1Coeff Op.toEllipticCoeff) : LocalRegularityAt Op hΩm 0

Order zero with C¹ principal coefficients alone. The interior H² conclusion for a local weak solution asks nothing of the lower-order coefficients beyond FullEllipticOp, and nothing of the principal part beyond a bounded derivative (Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 1, p. 327).