Hölder continuity of weak solutions (De Giorgi)

Let a be measurable and uniformly elliptic on an open set Ω ⊆ ℝⁿ, n ≥ 3, with constants 0 < λ ≤ Λ, and let u ∈ H¹(Ω) be a weak solution of -∂ⱼ(aⁱʲ ∂ᵢu) = 0. This file proves De Giorgi's theorem: u has a representative which is locally Hölder continuous in Ω, with an exponent α ∈ (0, 1] depending only on λ, Λ, the dimension and the normalization of the Haar measure. No regularity of the coefficients beyond measurability is assumed.

The representative is the precise representative TauCeti.MeasureTheory.preciseRepresentative of u, the limit of its averages over shrinking balls. It agrees with u almost everywhere on Ω by the Lebesgue differentiation theorem (TauCeti.W1p.ae_eq_preciseRepresentative). The Hölder estimate on a set K whose closed R-thickening lies in Ω combines two a-priori estimates on the balls B(x, R), x ∈ K: De Giorgi's interior oscillation estimate, which bounds the oscillation of u on B(x, r) by C r^α, and local boundedness, which bounds |u| on B(x, R/2). Both constants are controlled by the L² norm of u on Ω, and TauCeti.MeasureTheory.holderOnWith_preciseRepresentative turns them into a Hölder bound for the precise representative, with constant C R^(-α - n/2) ‖u‖_{L²(Ω)}.

Main declarations

• TauCeti.PDE.exists_holderOnWith_preciseRepresentative: De Giorgi's theorem; the precise representative of a weak solution is Hölder continuous on every set at positive distance from ∂Ω, with an explicit constant and a uniform exponent.
• TauCeti.PDE.exists_holderOnWith_preciseRepresentative_of_isCompact: the precise representative of a weak solution is Hölder continuous on every compact subset of Ω, with a uniform exponent.
• TauCeti.PDE.continuousOn_preciseRepresentative: the precise representative of a weak solution is continuous on Ω.

References

• E. De Giorgi, Sulla differenziabilità e l'analiticità delle estremali degli integrali multipli regolari, Mem. Accad. Sci. Torino (1957).
• Q. Han, F. Lin, Elliptic Partial Differential Equations, Chapter 4.
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Theorem 8.22 and Theorem 8.24.

theorem TauCeti.PDE.exists_holderOnWith_preciseRepresentative {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {lam Lam : ℝ} {pstar : ENNReal} (hpstar : pstar ≠ ⊤) (hexp : pstar⁻¹ + (↑(Fintype.card ι))⁻¹ = 2⁻¹) : ∃ (α : NNReal) (C : ℝ), 0 < α ∧ α ≤ 1 ∧ 0 < C ∧ ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {u : ↥(W1p mu Omega 2)} {K : Set (EuclideanSpace ℝ ι)} {R : ℝ}, UniformlyEllipticOn (↑Omega) a lam Lam → MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega) → (∀ (v : ↥(W1p0 mu Omega 2)), energyFormH1 a 0 0 u ↑v = 0) → 0 < R → Metric.cthickening R K ⊆ ↑Omega → HolderOnWith (C * R ^ (-↑α) * (R ^ (-↑(Fintype.card ι) / 2) * √(∫ (y : EuclideanSpace ℝ ι) in ↑Omega, ↑↑(W1p.value u) y ^ 2 ∂mu))).toNNReal α (MeasureTheory.preciseRepresentative mu ↑↑(W1p.value u)) K

De Giorgi's theorem: Hölder continuity of weak solutions. Let 2* be the Sobolev exponent of W^{1,2} in dimension n, so that 1/2* + 1/n = 1/2 and 2* < ∞ (this forces n ≥ 3). There are α ∈ (0, 1] and C > 0, depending only on λ, Λ, the dimension and the normalization of the additive Haar measure mu, such that the following holds. Let a be measurable and uniformly elliptic on Ω with constants λ, Λ, and let u ∈ H¹(Ω) be a weak solution of -∂ⱼ(aⁱʲ ∂ᵢu) = 0. If the closed R-thickening of a set K lies in Ω, then the precise representative of u is Hölder continuous on K with exponent α and constant C R^(-α - n/2) ‖u‖_{L²(Ω)}.

The precise representative agrees with u almost everywhere on Ω (TauCeti.W1p.ae_eq_preciseRepresentative). No regularity of the coefficients beyond measurability is assumed.

theorem TauCeti.PDE.exists_holderOnWith_preciseRepresentative_of_isCompact {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {lam Lam : ℝ} {pstar : ENNReal} (hpstar : pstar ≠ ⊤) (hexp : pstar⁻¹ + (↑(Fintype.card ι))⁻¹ = 2⁻¹) : ∃ (α : NNReal), 0 < α ∧ α ≤ 1 ∧ ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {u : ↥(W1p mu Omega 2)} {K : Set (EuclideanSpace ℝ ι)}, UniformlyEllipticOn (↑Omega) a lam Lam → MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega) → (∀ (v : ↥(W1p0 mu Omega 2)), energyFormH1 a 0 0 u ↑v = 0) → IsCompact K → K ⊆ ↑Omega → ∃ (C : NNReal), HolderOnWith C α (MeasureTheory.preciseRepresentative mu ↑↑(W1p.value u)) K

De Giorgi's theorem on compact sets. Let 2* be the Sobolev exponent of W^{1,2} in dimension n, so that 1/2* + 1/n = 1/2 and 2* < ∞ (this forces n ≥ 3). There is α ∈ (0, 1], depending only on λ, Λ, the dimension and the normalization of the additive Haar measure mu, such that the following holds. Let a be measurable and uniformly elliptic on Ω with constants λ, Λ, and let u ∈ H¹(Ω) be a weak solution of -∂ⱼ(aⁱʲ ∂ᵢu) = 0. Then the precise representative of u is Hölder continuous with exponent α on every compact K ⊆ Ω.

theorem TauCeti.PDE.continuousOn_preciseRepresentative {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {lam Lam : ℝ} {pstar : ENNReal} (hpstar : pstar ≠ ⊤) (hexp : pstar⁻¹ + (↑(Fintype.card ι))⁻¹ = 2⁻¹) {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {u : ↥(W1p mu Omega 2)} (h : UniformlyEllipticOn (↑Omega) a lam Lam) (ha : MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega)) (hu : ∀ (v : ↥(W1p0 mu Omega 2)), energyFormH1 a 0 0 u ↑v = 0) : ContinuousOn (MeasureTheory.preciseRepresentative mu ↑↑(W1p.value u)) ↑Omega

Continuity of weak solutions. Let 2* be the Sobolev exponent of W^{1,2} in dimension n, so that 1/2* + 1/n = 1/2 and 2* < ∞ (this forces n ≥ 3). Let a be measurable and uniformly elliptic on Ω, and let u ∈ H¹(Ω) be a weak solution of -∂ⱼ(aⁱʲ ∂ᵢu) = 0. Then the precise representative of u, which agrees with u almost everywhere on Ω, is continuous on Ω.