The Caccioppoli inequality for weak solutions

Let u ∈ H¹(Ω) be a weak solution of the divergence-form equation

-∂ⱼ(aⁱʲ ∂ᵢu) = f in Ω, with f ∈ L²(Ω),

meaning ∫_Ω ⟨a ∇u, ∇v⟩ = ∫_Ω f v for every v ∈ H¹₀(Ω); no boundary condition is imposed on u. If the coefficient a is measurable and uniformly elliptic with constants 0 < λ ≤ Λ, then for every smooth cutoff ζ compactly supported in Ω,

∫_Ω ζ² ‖∇u‖² ≤ (2Λ/λ)² ∫_Ω ‖∇ζ‖² u² + (2/λ) ∫_Ω ζ² f u.

This is the Caccioppoli inequality (the reverse Poincaré, or interior energy, inequality): the gradient of a solution on the region where ζ = 1 is controlled by the solution itself on the support of ζ. The constants depend only on the ellipticity constants λ and Λ, and not on Ω, on the dimension, or on any regularity of the coefficients beyond measurability. It is the basic interior estimate of elliptic regularity theory: it is an ingredient in difference-quotient proofs of interior H² regularity under additional coefficient regularity, and its variant for the truncations (u - k)⁺ of subsolutions, not proved here, is the starting point of De Giorgi's iteration.

The proof tests the equation against ζ² u, which lies in H¹₀(Ω) because ζ is compactly supported in Ω, and whose gradient is ζ² ∇u + 2ζu ∇ζ. Ellipticity bounds the first term of ⟨a ∇u, ∇(ζ² u)⟩ below by λζ²‖∇u‖², and Young's inequality absorbs half of it into the cross term 2ζu ⟨a ∇u, ∇ζ⟩.

Main declarations

• TauCeti.PDE.W1p.setIntegral_sq_mul_norm_gradient_sq_le_of_pointwise: the common integration and absorption step for Caccioppoli inequalities.
• TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_sq_le: the Caccioppoli inequality.

References

• L. C. Evans, Partial Differential Equations, §6.3.1 (the energy estimate in the proof of Theorem 1, interior H² regularity).
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, §8.2 and §8.6.
• M. Giaquinta, L. Martinazzi, An Introduction to the Regularity Theory for Elliptic Systems, Harmonic Maps and Minimal Graphs, Theorem 4.4.

theorem TauCeti.PDE.W1p.setIntegral_sq_mul_norm_gradient_sq_le_of_pointwise {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {lam Lam : ℝ} (hlam : 0 < lam) (w : ↥(W1p mu Omega 2)) {ψ : EuclideanSpace ℝ ι → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {M : ℝ} (hψM : ∀ (x : EuclideanSpace ℝ ι), |ψ x| ≤ M) (hgradM : ∀ (x : EuclideanSpace ℝ ι), ‖gradient ψ x‖ ≤ M) {e force : EuclideanSpace ℝ ι → ℝ} (he : MeasureTheory.Integrable e (mu.restrict ↑Omega)) (hpointwise : ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, lam * (ψ x ^ 2 * ‖↑↑(W1p.gradient w) x‖ ^ 2) ≤ e x + lam / 2 * (ψ x ^ 2 * ‖↑↑(W1p.gradient w) x‖ ^ 2) + 2 * Lam ^ 2 / lam * (‖gradient ψ x‖ ^ 2 * ↑↑(W1p.value w) x ^ 2)) (hforce : ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, e x ∂mu ≤ ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, force x ∂mu) : ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ψ x ^ 2 * ‖↑↑(W1p.gradient w) x‖ ^ 2 ∂mu ≤ (2 * Lam / lam) ^ 2 * ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ‖gradient ψ x‖ ^ 2 * ↑↑(W1p.value w) x ^ 2 ∂mu + 2 / lam * ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, force x ∂mu

Integrate a pointwise Caccioppoli estimate and absorb half of its energy term. This is the common measure-theoretic step for the solution and subsolution forms of the inequality; the caller supplies the energy density and its comparison with the forcing term.

theorem TauCeti.PDE.W1p.setIntegral_norm_gradient_sq_mul_value_sq_le {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} (w : ↥(W1p mu Omega 2)) {ψ : EuclideanSpace ℝ ι → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {G : ℝ} (hG : ∀ (x : EuclideanSpace ℝ ι), ‖gradient ψ x‖ ≤ G) {S : Set (EuclideanSpace ℝ ι)} (hS : MeasurableSet S) (hts : tsupport ψ ⊆ S) {g : EuclideanSpace ℝ ι → ℝ} (hg : MeasureTheory.Integrable g (mu.restrict ↑Omega)) (hwg : ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, ↑↑(W1p.value w) x ^ 2 ≤ g x) : ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ‖gradient ψ x‖ ^ 2 * ↑↑(W1p.value w) x ^ 2 ∂mu ≤ G ^ 2 * ∫ (x : EuclideanSpace ℝ ι) in ↑Omega ∩ S, g x ∂mu

Bound the cutoff-gradient term by the squared gradient bound and an integral over a set containing the support of the cutoff. The comparison function may dominate the Sobolev value only almost everywhere.

theorem TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_sq_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {lam Lam : ℝ} (h : UniformlyEllipticOn (↑Omega) a lam Lam) (ha : MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega)) {f : ↥(MeasureTheory.Lp ℝ 2 (mu.restrict ↑Omega))} {u : ↥(W1p mu Omega 2)} (hu : ∀ (v : ↥(W1p0 mu Omega 2)), energyFormH1 a 0 0 u ↑v = ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ↑↑f x * ↑↑(W1p.value ↑v) x ∂mu) {ψ : EuclideanSpace ℝ ι → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hcpt : HasCompactSupport ψ) (hts : tsupport ψ ⊆ ↑Omega) : ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ψ x ^ 2 * ‖↑↑(W1p.gradient u) x‖ ^ 2 ∂mu ≤ (2 * Lam / lam) ^ 2 * ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ‖gradient ψ x‖ ^ 2 * ↑↑(W1p.value u) x ^ 2 ∂mu + 2 / lam * ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ψ x ^ 2 * ↑↑f x * ↑↑(W1p.value u) x ∂mu

The Caccioppoli inequality. Let a be measurable and uniformly elliptic on Ω with constants 0 < λ ≤ Λ, and let u ∈ H¹(Ω) be a weak solution of -∂ⱼ(aⁱʲ ∂ᵢu) = f in Ω, in the sense that a(u, v) = ∫_Ω f v for every v ∈ H¹₀(Ω), with no boundary condition on u. Then for every smooth ψ compactly supported in Ω,

∫_Ω ψ² ‖∇u‖² ≤ (2Λ/λ)² ∫_Ω ‖∇ψ‖² u² + (2/λ) ∫_Ω ψ² f u.

For f = 0 the last term vanishes, and the gradient of u where ψ = 1 is bounded by u itself on the support of ψ.