Oscillation decay for weak solutions (De Giorgi)

Let a be measurable and uniformly elliptic on Ω ⊆ ℝⁿ, n ≥ 3, with constants 0 < λ ≤ Λ. This file proves the two steps of De Giorgi's proof of Hölder continuity that turn the measure estimates for level sets into a pointwise gain on a smaller ball.

• Reduction of the supremum. Let u ∈ H¹(Ω) be a weak subsolution of -∂ⱼ(aⁱʲ ∂ᵢu) ≤ 0 with u ≤ M on B(x₀, 2R) ⊆ Ω, and suppose the sublevel set {u ≤ k} occupies at least a proportion θ > 0 of B(x₀, R). Then u ≤ M - δ (M - k) on B(x₀, R/2), where δ ∈ (0, 1) depends only on λ, Λ, θ, the dimension and the normalization of the Haar measure.
• Oscillation decay. If u is a weak solution of -∂ⱼ(aⁱʲ ∂ᵢu) = 0 with m ≤ u ≤ M on B(x₀, 2R), then on B(x₀, R/2) either u ≤ M - δ (M - m) or u ≥ m + δ (M - m). Either way the oscillation of u drops from M - m to at most (1 - δ)(M - m).
• Power-law decay. Iterating over the balls B(x₀, R / 4ʲ), the oscillation of a weak solution on B(x₀, R / 4ʲ) is at most (1 - δ)ʲ times its oscillation on B(x₀, R), hence at most C (r / R)^α times it on B(x₀, r) for every 0 < r ≤ R, with 0 < α ≤ 1 and C depending only on λ, Λ, the dimension and the Haar normalization.
• Interior oscillation estimate. Combined with De Giorgi's local boundedness theorem, the oscillation of a weak solution on B(x₀, r), r ≤ R/2, is at most C (r / R)^α R^{-n/2} ‖u‖_{L²(B(x₀, R))} whenever B(x₀, R) ⊆ Ω.

The reduction of the supremum combines De Giorgi's decay of upper level sets (TauCeti.PDE.exists_sqrt_mul_measureReal_le_mul_measureReal_ball) with local boundedness above a level (TauCeti.PDE.exists_ae_value_le_add_mul_rpow_mul_sqrt_setIntegral_of_inv_add_eq_inv): along the levels kⱼ = M - (M - k)/2ʲ, the set {u ≥ kⱼ} occupies a proportion O(j^{-1/2}) of B(x₀, R), so the L² mass of (u - kⱼ)⁺ there is O((M - kⱼ)² j^{-1/2} Rⁿ), and local boundedness gives u ≤ kⱼ + (M - kⱼ)/2 on B(x₀, R/2) once j is large. Oscillation decay applies this to u or to -u at the mid level (m + M)/2, whichever sublevel set fills at least half of B(x₀, R). The power-law decay is the a-priori estimate behind the interior Hölder continuity of weak solutions: a function whose essential oscillation on balls decays like a power of the radius agrees almost everywhere with a Hölder continuous function.

Oscillation is tracked through explicit a.e. bounds: u takes values in an interval [m', m' + L] almost everywhere on a ball, rather than through an essential oscillation functional.

Main declarations

• TauCeti.PDE.exists_ae_value_le_sub_mul_sub: the reduction of the supremum.
• TauCeti.PDE.exists_ae_value_le_sub_mul_sub_or_add_mul_sub_le: oscillation decay.
• TauCeti.PDE.exists_ae_value_mem_Icc_add_pow_mul_sub: geometric decay of the oscillation along the balls B(x₀, R / 4ʲ).
• TauCeti.PDE.exists_ae_value_mem_Icc_add_mul_rpow_mul_sub: the power law osc(B(x₀, r)) ≤ C (r / R)^α osc(B(x₀, R)).
• TauCeti.PDE.exists_ae_value_mem_Icc_add_mul_rpow_mul_rpow_mul_sqrt_setIntegral: the interior oscillation estimate in terms of the L² norm.

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.
• L. Caffarelli, A. Vasseur, The De Giorgi method for regularity of solutions of elliptic equations and its applications to fluid dynamics, Discrete Contin. Dyn. Syst. Ser. S (2010).

theorem TauCeti.PDE.exists_ae_value_le_sub_mul_sub {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {lam Lam : ℝ} {pstar : ENNReal} (hpstar : pstar ≠ ⊤) (hexp : pstar⁻¹ + (↑(Fintype.card ι))⁻¹ = 2⁻¹) {θ : ℝ} (hθ : 0 < θ) : ∃ (δ : ℝ), 0 < δ ∧ δ < 1 ∧ ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {u : ↥(W1p mu Omega 2)} {x₀ : EuclideanSpace ℝ ι} {R k M : ℝ}, UniformlyEllipticOn (↑Omega) a lam Lam → MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega) → (∀ (v : ↥(W1p0 mu Omega 2)), (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, 0 ≤ ↑↑(W1p.value ↑v) x) → energyFormH1 a 0 0 u ↑v ≤ 0) → 0 < R → Metric.ball x₀ (2 * R) ⊆ ↑Omega → k ≤ M → (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ (2 * R)), ↑↑(W1p.value u) x ≤ M) → θ * mu.real (Metric.ball x₀ R) ≤ (mu.restrict (Metric.ball x₀ R)).real {x : EuclideanSpace ℝ ι | ↑↑(W1p.value u) x ≤ k} → ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ (R / 2)), ↑↑(W1p.value u) x ≤ M - δ * (M - k)

Reduction of the supremum (De Giorgi). 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), and fix a proportion θ > 0. 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 subsolution of -∂ⱼ(aⁱʲ ∂ᵢu) ≤ 0, that is a(u, v) ≤ 0 for every nonnegative v ∈ H¹₀(Ω). Let B(x₀, 2R) ⊆ Ω and levels k ≤ M be such that u ≤ M almost everywhere on B(x₀, 2R) and |{u ≤ k} ∩ B(x₀, R)| ≥ θ |B(x₀, R)|. Then

u ≤ M - δ (M - k) almost everywhere on B(x₀, R/2).

No regularity of the coefficients beyond measurability is assumed.

theorem TauCeti.PDE.exists_ae_value_le_sub_mul_sub_or_add_mul_sub_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {lam Lam : ℝ} {pstar : ENNReal} (hpstar : pstar ≠ ⊤) (hexp : pstar⁻¹ + (↑(Fintype.card ι))⁻¹ = 2⁻¹) : ∃ (δ : ℝ), 0 < δ ∧ δ < 1 ∧ ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {u : ↥(W1p mu Omega 2)} {x₀ : EuclideanSpace ℝ ι} {R m M : ℝ}, 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.ball x₀ (2 * R) ⊆ ↑Omega → (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ (2 * R)), m ≤ ↑↑(W1p.value u) x ∧ ↑↑(W1p.value u) x ≤ M) → (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ (R / 2)), ↑↑(W1p.value u) x ≤ M - δ * (M - m)) ∨ ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ (R / 2)), m + δ * (M - m) ≤ ↑↑(W1p.value u) x

Oscillation decay for weak solutions (De Giorgi). 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, that is a(u, v) = 0 for every v ∈ H¹₀(Ω). Let B(x₀, 2R) ⊆ Ω and m, M be such that m ≤ u ≤ M almost everywhere on B(x₀, 2R). Then almost everywhere on B(x₀, R/2), either

u ≤ M - δ (M - m) throughout, or m + δ (M - m) ≤ u throughout.

In particular the essential oscillation of u on B(x₀, R/2) is at most (1 - δ)(M - m).

theorem TauCeti.PDE.exists_ae_value_mem_Icc_add_pow_mul_sub {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {lam Lam : ℝ} {pstar : ENNReal} (hpstar : pstar ≠ ⊤) (hexp : pstar⁻¹ + (↑(Fintype.card ι))⁻¹ = 2⁻¹) : ∃ (δ : ℝ), 0 < δ ∧ δ < 1 ∧ ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {u : ↥(W1p mu Omega 2)} {x₀ : EuclideanSpace ℝ ι} {R m M : ℝ}, 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.ball x₀ R ⊆ ↑Omega → (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ R), ↑↑(W1p.value u) x ∈ Set.Icc m M) → ∀ (j : ℕ), ∃ (m' : ℝ), ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ (R / 4 ^ j)), ↑↑(W1p.value u) x ∈ Set.Icc m' (m' + (1 - δ) ^ j * (M - m))

Iterated oscillation decay (De Giorgi). 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. If B(x₀, R) ⊆ Ω and u ∈ [m, M] almost everywhere on B(x₀, R), then for every j, almost everywhere on B(x₀, R / 4ʲ) the function u takes values in an interval of length (1 - δ)ʲ (M - m).

theorem TauCeti.PDE.exists_ae_value_mem_Icc_add_mul_rpow_mul_sub {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {lam Lam : ℝ} {pstar : ENNReal} (hpstar : pstar ≠ ⊤) (hexp : pstar⁻¹ + (↑(Fintype.card ι))⁻¹ = 2⁻¹) : ∃ (α : ℝ) (C : ℝ), 0 < α ∧ α ≤ 1 ∧ 0 < C ∧ ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {u : ↥(W1p mu Omega 2)} {x₀ : EuclideanSpace ℝ ι} {R r m M : ℝ}, 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 → r ≤ R → Metric.ball x₀ R ⊆ ↑Omega → (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ R), ↑↑(W1p.value u) x ∈ Set.Icc m M) → ∃ (m' : ℝ), ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ r), ↑↑(W1p.value u) x ∈ Set.Icc m' (m' + C * (r / R) ^ α * (M - m))

Power-law oscillation decay (De Giorgi). 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 B(x₀, R) ⊆ Ω and u ∈ [m, M] almost everywhere on B(x₀, R), then for every radius 0 < r ≤ R, almost everywhere on B(x₀, r) the function u takes values in an interval of length C (r / R)^α (M - m).

The exponent is α = min (log(1/(1 - δ)) / log 4) 1, where δ is the constant of TauCeti.PDE.exists_ae_value_mem_Icc_add_pow_mul_sub, and C = 4^α; the cap at 1 is the range in which the estimate yields Hölder continuity.

theorem TauCeti.PDE.exists_ae_value_mem_Icc_add_mul_rpow_mul_rpow_mul_sqrt_setIntegral {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {lam Lam : ℝ} {pstar : ENNReal} (hpstar : pstar ≠ ⊤) (hexp : pstar⁻¹ + (↑(Fintype.card ι))⁻¹ = 2⁻¹) : ∃ (α : ℝ) (C : ℝ), 0 < α ∧ α ≤ 1 ∧ 0 < C ∧ ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {u : ↥(W1p mu Omega 2)} {x₀ : EuclideanSpace ℝ ι} {R 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 → r ≤ R / 2 → Metric.ball x₀ R ⊆ ↑Omega → ∃ (m' : ℝ), ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ r), ↑↑(W1p.value u) x ∈ Set.Icc m' (m' + C * (r / R) ^ α * (R ^ (-↑(Fintype.card ι) / 2) * √(∫ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ R, ↑↑(W1p.value u) x ^ 2 ∂mu)))

De Giorgi's interior oscillation estimate. 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 B(x₀, R) ⊆ Ω and 0 < r ≤ R/2, then almost everywhere on B(x₀, r) the function u takes values in an interval of length

C (r / R)^α R^{-n/2} ‖u‖_{L²(B(x₀, R))}.

No bound on u is assumed: the oscillation of u on B(x₀, R/2) is controlled by its L² norm through De Giorgi's local boundedness theorem, and the power law TauCeti.PDE.exists_ae_value_mem_Icc_add_mul_rpow_mul_sub propagates it to smaller balls. This is the a-priori estimate behind the interior Hölder continuity of weak solutions.