Infinite differentiability in the interior with classical hypotheses

Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 3 (p. 334): "Assume a^{ij}, b^i, c ∈ C^∞(U) and f ∈ C^∞(U). Suppose u ∈ H¹(U) is a weak solution of the elliptic PDE Lu = f in U. Then u ∈ C^∞(U)." The standing assumptions are those of §6.3.1 (U ⊂ ℝⁿ bounded and open, the uniform ellipticity of §6.1.1) and of §6.1.1 (a^{ij} = a^{ji}).

This file states the theorem on plain functions. The coefficients are smooth and uniformly elliptic on the open set U with no bound (SmoothOpOn), the datum is smooth on U, and the solution is a function u square-integrable on each compact subset of U with a weak gradient G, square-integrable on each compact subset, satisfying the weak formulation against every test function supported in U (LocalWeakSol). That is Evans's u ∈ H¹_loc(U), which u ∈ H¹(U) implies.

Weak formulation

Evans defines a weak solution in §6.1.2 for coefficients in L^∞(U), by B[u, v] = (f, v) for every v ∈ H₀¹(U), and in Remark (ii) after Theorem 1 of §6.3.1 he reads the same identity against every v ∈ C_c^∞(U). Coefficients smooth on U need not be bounded on U, and then B[u, v] need not be defined for v ∈ H₀¹(U), while it is defined for every v ∈ C_c^∞(U), since a smooth coefficient is bounded on the support of v. The statements here take the identity against C_c^∞(U), the weaker hypothesis of the two: an H₀¹(U) weak solution is one.

Proof

The proof is local. For each closed ball B ⊆ U, localise supplies an open W ⊇ B with compact closure in U, a global operator agreeing with the given one on W and meeting every regularity mixin, and a smooth compactly supported datum agreeing with f on W; the restriction of u to W is then a local weak solution in W12 W (isLocalWeakSolution_of_localWeakSol), interior_smooth_global_W12 gives a representative smooth on W, and exists_contDiffOn_of_closedBall_ae glues the balls. In dimension zero the space is a point and every function is smooth.

Main declarations

• exists_contDiffOn_of_localWeakSol: Theorem 3 on an open set, for every dimension.
• exists_contDiffOn_of_weakSolution_evans: Theorem 3 with the unnecessary boundedness and symmetry assumptions omitted.

theorem EllipticPdes.Regularity.exists_contDiffOn_of_localWeakSol_succ {n : ℕ} {U : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hU : IsOpen U) (P : SmoothOpOn (n + 1) U) {f u : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} {G : Fin (n + 1) → EuclideanSpace ℝ (Fin (n + 1)) → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) (hu : ∀ (K : Set (EuclideanSpace ℝ (Fin (n + 1)))), IsCompact K → K ⊆ U → MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict K)) (hG : ∀ (i : Fin (n + 1)) (K : Set (EuclideanSpace ℝ (Fin (n + 1)))), IsCompact K → K ⊆ U → MeasureTheory.MemLp (G i) 2 (MeasureTheory.volume.restrict K)) (hgrad : Embedding.HasWeakGradOn U u G) (hsol : LocalWeakSol U P.a P.b P.c f u G) : ∃ (u' : EuclideanSpace ℝ (Fin (n + 1)) → ℝ), ContDiffOn ℝ (↑⊤) u' U ∧ u' =ᵐ[MeasureTheory.volume.restrict U] u

Theorem 3 in positive dimension, where the Sobolev ladder applies.

theorem EllipticPdes.Regularity.exists_contDiffOn_of_localWeakSol {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) (P : SmoothOpOn d U) {f u : EuclideanSpace ℝ (Fin d) → ℝ} {G : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) (hu : ∀ (K : Set (EuclideanSpace ℝ (Fin d))), IsCompact K → K ⊆ U → MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict K)) (hG : ∀ (i : Fin d) (K : Set (EuclideanSpace ℝ (Fin d))), IsCompact K → K ⊆ U → MeasureTheory.MemLp (G i) 2 (MeasureTheory.volume.restrict K)) (hgrad : Embedding.HasWeakGradOn U u G) (hsol : LocalWeakSol U P.a P.b P.c f u G) : ∃ (u' : EuclideanSpace ℝ (Fin d) → ℝ), ContDiffOn ℝ (↑⊤) u' U ∧ u' =ᵐ[MeasureTheory.volume.restrict U] u

Infinite differentiability in the interior (Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 3, p. 334). Let U be open, the coefficients a^{ij}, b^i, c smooth and uniformly elliptic on U (P : SmoothOpOn), and f smooth on U. If u is square-integrable on every compact subset of U, with a weak gradient G on U square-integrable on every compact subset, and u solves L u = f weakly against every test function supported in U, then u agrees almost everywhere on U with a function smooth on U. Every dimension is covered; in dimension zero the space is a point.

theorem EllipticPdes.Regularity.exists_contDiffOn_of_weakSolution_evans {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {c f u : EuclideanSpace ℝ (Fin d) → ℝ} {G : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (ha : ∀ (i j : Fin d), ContDiffOn ℝ (↑⊤) (fun (x : EuclideanSpace ℝ (Fin d)) => a x i j) U) (hb : ∀ (i : Fin d), ContDiffOn ℝ (↑⊤) (fun (x : EuclideanSpace ℝ (Fin d)) => b x i) U) (hc : ContDiffOn ℝ (↑⊤) c U) (hf : ContDiffOn ℝ (↑⊤) f U) {θ : ℝ} (hθ : 0 < θ) (hell : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict U, ∀ (ξ : Fin d → ℝ), θ * ∑ i : Fin d, ξ i ^ 2 ≤ ∑ i : Fin d, ∑ j : Fin d, a x i j * ξ i * ξ j) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict U)) (hG : ∀ (i : Fin d), MeasureTheory.MemLp (G i) 2 (MeasureTheory.volume.restrict U)) (hgrad : Embedding.HasWeakGradOn U u G) (hsol : LocalWeakSol U a b c f u G) : ∃ (u' : EuclideanSpace ℝ (Fin d) → ℝ), ContDiffOn ℝ (↑⊤) u' U ∧ u' =ᵐ[MeasureTheory.volume.restrict U] u

Infinite differentiability in the interior, Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 3 (p. 334), generalized to open domains and nonsymmetric principal coefficients. U ⊆ ℝᵈ is open, a^{ij}, b^i, c, f ∈ C^∞(U), the operator is uniformly elliptic with a constant θ > 0 for almost every x ∈ U (§6.1.1, (4)), u ∈ H¹(U): u and its weak gradient G lie in L²(U). If u is a weak solution of L u = f in U, tested against every v ∈ C_c^∞(U) as in Remark (ii) after Theorem 1, then u agrees almost everywhere on U with a function in C^∞(U).

Boundedness of U and symmetry of a^{ij} are unnecessary for this interior conclusion.