Smoothness of weak solutions for smooth coefficients

Let a be a uniformly elliptic coefficient field on Ω whose entries are smooth on Ω, and let u ∈ H¹(Ω) be a weak solution of the divergence-form equation

-∂ᵢ(aⁱʲ ∂ⱼu) = f in Ω,

meaning ∫_Ω ⟨∇v, a ∇u⟩ = ∫_Ω f v for every v ∈ H¹₀(Ω), with no boundary condition on u. If, near every point of Ω, f lies in W^{k,2} for every k (as it does when f is smooth on Ω), then u agrees almost everywhere on Ω with a function that is smooth on Ω. So a weak solution with smooth coefficients and data is, after modification on a null set, a classical solution in the interior. No regularity of ∂Ω, no global bound on the derivatives of a, and no global integrability of the derivatives of f is assumed.

The proof is local. Near a point of Ω, the restriction of u to a small ball W solves the equation on W (TauCeti.PDE.energyFormH1_restrictL_eq_setIntegral), with data in every W^{k,2}(W). Interior H^{k+2} regularity (TauCeti.PDE.UniformlyEllipticOn.exists_value_eq_value_restrictL_of_contDiffOn) then puts u in every W^{m,2}(B) for the concentric ball B of half the radius, and the interior Sobolev embedding (TauCeti.exists_contDiffOn_ae_eq_of_forall_wkp) makes u smooth on B. The smooth representatives on these balls glue to one on Ω (TauCeti.exists_contDiffOn_ae_eq_of_locally).

A weak solution of the Dirichlet problem (TauCeti.PDE.IsWeakSolutionDirichlet) satisfies the hypothesis by TauCeti.PDE.isWeakSolutionDirichlet_iff. With a = 1 this covers the Poisson problem -Δu = f, whose weak solution on a domain contained in a ball exists and is unique by TauCeti.PDE.existsUnique_isWeakSolutionDirichlet_laplacian_of_subset_ball.

The statements are for Lebesgue measure volume, the measure of the Sobolev embedding.

Main results

• TauCeti.PDE.UniformlyEllipticOn.exists_contDiffOn_ae_eq_of_contDiffOn: for smooth coefficients, a weak solution whose data lies locally in every W^{k,2} has a representative smooth on Ω.
• TauCeti.PDE.UniformlyEllipticOn.exists_contDiffOn_ae_eq: its constant-coefficient case.

References

• L. C. Evans, Partial Differential Equations, 2nd ed., §6.3.1, Theorem 3 (infinite differentiability in the interior).
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Corollary 8.11.

theorem TauCeti.PDE.UniformlyEllipticOn.exists_contDiffOn_ae_eq_of_contDiffOn {ι : Type u_1} [Fintype ι] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} [DecidableEq ι] {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {lam Lam : ℝ} (ha : UniformlyEllipticOn (↑Omega) a lam Lam) (hsmooth : ∀ (i j : ι), ContDiffOn ℝ (↑⊤) (fun (x : EuclideanSpace ℝ ι) => a x i j) ↑Omega) {f : EuclideanSpace ℝ ι → ℝ} (hf : ∀ x ∈ Omega, ∃ (V : TopologicalSpace.Opens (EuclideanSpace ℝ ι)), x ∈ V ∧ ∀ (k : ℕ), ∃ (F : Wkp MeasureTheory.volume V 2 k), ↑↑(Wkp.value k F) =ᵐ[MeasureTheory.volume.restrict ↑V] f) {u : ↥(W1p MeasureTheory.volume Omega 2)} (hu : ∀ (v : ↥(W1p0 MeasureTheory.volume Omega 2)), energyFormH1 a 0 0 u ↑v = ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, f x * ↑↑(W1p.value ↑v) x) : ∃ (g : EuclideanSpace ℝ ι → ℝ), ContDiffOn ℝ (↑⊤) g ↑Omega ∧ ↑↑(W1p.value u) =ᵐ[MeasureTheory.volume.restrict ↑Omega] g

Interior smoothness for smooth coefficients. Let a be uniformly elliptic on Ω, with entries smooth on Ω, let f lie in W^{k,2} of a neighbourhood of each point of Ω for every k, and let u ∈ H¹(Ω) be a weak solution of

-∂ᵢ(aⁱʲ ∂ⱼu) = f in Ω,

in the sense that ∫_Ω ⟨∇v, a ∇u⟩ = ∫_Ω f v for every v ∈ H¹₀(Ω), with no boundary condition on u. Then u agrees almost everywhere on Ω with a function smooth on Ω.

No regularity of ∂Ω is assumed.

theorem TauCeti.PDE.UniformlyEllipticOn.exists_contDiffOn_ae_eq {ι : Type u_1} [Fintype ι] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {A : Matrix ι ι ℝ} {lam : ℝ} (hlam : 0 < lam) (hA : ∀ (ξ : EuclideanSpace ℝ ι), lam * ‖ξ‖ ^ 2 ≤ ξ.ofLp ⬝ᵥ A.mulVec ξ.ofLp) {f : EuclideanSpace ℝ ι → ℝ} (hf : ∀ x ∈ Omega, ∃ (V : TopologicalSpace.Opens (EuclideanSpace ℝ ι)), x ∈ V ∧ ∀ (k : ℕ), ∃ (F : Wkp MeasureTheory.volume V 2 k), ↑↑(Wkp.value k F) =ᵐ[MeasureTheory.volume.restrict ↑V] f) {u : ↥(W1p MeasureTheory.volume Omega 2)} (hu : ∀ (v : ↥(W1p0 MeasureTheory.volume Omega 2)), energyFormH1 (fun (x : EuclideanSpace ℝ ι) => A) 0 0 u ↑v = ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, f x * ↑↑(W1p.value ↑v) x) : ∃ (g : EuclideanSpace ℝ ι → ℝ), ContDiffOn ℝ (↑⊤) g ↑Omega ∧ ↑↑(W1p.value u) =ᵐ[MeasureTheory.volume.restrict ↑Omega] g

Interior smoothness for a constant principal coefficient. Let A be a constant, uniformly elliptic matrix, let f lie in W^{k,2} of a neighbourhood of each point of Ω for every k, and let u ∈ H¹(Ω) be a weak solution of

-∂ᵢ(Aⁱʲ ∂ⱼu) = f in Ω,

in the sense that ∫_Ω ⟨∇v, A ∇u⟩ = ∫_Ω f v for every v ∈ H¹₀(Ω), with no boundary condition on u. Then u agrees almost everywhere on Ω with a function smooth on Ω. This is the constant case of TauCeti.PDE.UniformlyEllipticOn.exists_contDiffOn_ae_eq_of_contDiffOn.