Classical representatives of constant-coefficient weak solutions

A C² representative of a weak solution of -div(A ∇u) = f, with constant matrix A and continuous f, satisfies this equation at every point of the open domain. No boundary condition or symmetry of A is needed. For uniformly elliptic A, a weak solution of the homogeneous equation has a smooth representative whose classical gradient agrees almost everywhere with its weak gradient. This allows classical interior estimates to be applied to weak solutions of the frozen coefficient equation.

The operator is the existing TauCeti.PDE.divMatrixGradient, with the sign convention -divMatrixGradient (fun _ => A) u = f. The coordinate formula divMatrixGradient_eq_sum_fderiv_fderiv_apply identifies it with the contraction of A against the Hessian, including nonsymmetric matrices.

References

• L. C. Evans, Partial Differential Equations, 2nd ed., §6.3.1.
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, §6.1 (freezing coefficients) and §8.1 (weak solutions).

theorem TauCeti.PDE.energyFormH1_ofTestFunctionₗ_eq_neg_setIntegral_divMatrixGradient {ι : Type u_1} [Fintype ι] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {A : Matrix ι ι ℝ} {g : EuclideanSpace ℝ ι → ℝ} (hg : ContDiffOn ℝ 2 g ↑Omega) {u : ↥(W1p mu Omega 2)} (hug : ↑↑(W1p.value u) =ᵐ[mu.restrict ↑Omega] g) (φ : TestFunction Omega ℝ ⊤) : energyFormH1 (fun (x : EuclideanSpace ℝ ι) => A) 0 0 u ((W1p.ofTestFunctionₗ mu Omega 2) φ) = -∫ (x : EuclideanSpace ℝ ι) in ↑Omega, φ x * divMatrixGradient (fun (x : EuclideanSpace ℝ ι) => A) g x ∂mu

Green's identity for a C² representative of a Sobolev function, tested against a compactly supported smooth function. No ellipticity, boundary condition, or global Hessian bound is used.

theorem TauCeti.PDE.divMatrixGradient_eq_neg_of_forall_energyFormH1_eq {ι : Type u_1} [Fintype ι] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {A : Matrix ι ι ℝ} {g f : EuclideanSpace ℝ ι → ℝ} (hg : ContDiffOn ℝ 2 g ↑Omega) (hf : ContinuousOn f ↑Omega) {u : ↥(W1p mu Omega 2)} (hug : ↑↑(W1p.value u) =ᵐ[mu.restrict ↑Omega] g) (hu : ∀ (φ : TestFunction Omega ℝ ⊤), energyFormH1 (fun (x : EuclideanSpace ℝ ι) => A) 0 0 u ((W1p.ofTestFunctionₗ mu Omega 2) φ) = ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, f x * φ x ∂mu) (x : EuclideanSpace ℝ ι) : x ∈ Omega → divMatrixGradient (fun (x : EuclideanSpace ℝ ι) => A) g x = -f x

A C² representative of a weak solution with continuous forcing satisfies -div(A ∇g) = f pointwise. Only compactly supported test functions are required in the weak formulation, and the matrix need not be elliptic or symmetric.

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

Every weak solution of a homogeneous, constant, uniformly elliptic equation has a smooth classical representative. Its classical gradient is the weak gradient almost everywhere. There is no boundary condition on the solution or regularity assumption on the boundary.