Decay of upper level sets of weak subsolutions (De Giorgi)

Let a be measurable and uniformly elliptic on Ω ⊆ ℝⁿ with constants 0 < λ ≤ Λ, and let u ∈ H¹(Ω) be a weak subsolution of -∂ⱼ(aⁱʲ ∂ᵢu) ≤ 0. Suppose that on a ball B(x₀, 2R) ⊆ Ω we have u ≤ M, and that on the concentric ball B_R = B(x₀, R) the sublevel set {u ≤ k} occupies at least a fixed proportion θ > 0 of B_R, for some level k < M. Along the levels kⱼ = M - (M - k)/2ʲ, which rise from k to M, this file proves De Giorgi's decay estimate for upper level sets

√j · |{u ≥ kⱼ} ∩ B_R| ≤ C |B_R|,

with C depending only on λ, Λ, θ and the dimension. In particular {u ≥ kⱼ} occupies an arbitrarily small proportion of B_R once j is large.

The proof combines three estimates for the truncations (u - kⱼ)⁺: the Caccioppoli inequality on the pair of balls B_R ⊆ B_{2R} (TauCeti.PDE.exists_setIntegral_ball_norm_gradient_posPartAbove_sq_le), which bounds ∫_{B_R} |∇(u - kⱼ)⁺|² by R⁻² (M - kⱼ)² |B_{2R}|; De Giorgi's isoperimetric inequality on B_R between the levels kⱼ and kⱼ₊₁, followed by the Cauchy–Schwarz inequality on the strip {kⱼ < u < kⱼ₊₁} (TauCeti.W1p.sq_sub_mul_measureReal_mul_measureReal_le_of_ball_subset). Together they give |{u ≥ kⱼ₊₁} ∩ B_R|² ≤ C² |B_R| |{kⱼ < u < kⱼ₊₁} ∩ B_R|, and the strips are disjoint.

Combined with local boundedness (TauCeti.PDE.exists_ae_value_le_mul_rpow_mul_sqrt_setIntegral), which turns smallness of {u ≥ kⱼ} into a pointwise bound on a smaller ball, this is the step of De Giorgi's proof of Hölder continuity that makes the oscillation of a weak solution decay from one ball to the next.

Main declarations

• TauCeti.PDE.exists_sqrt_mul_measureReal_le_mul_measureReal_ball: the decay estimate.

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_sqrt_mul_measureReal_le_mul_measureReal_ball {ι : Type u_1} [Fintype ι] [DecidableEq ι] {lam Lam θ : ℝ} (hθ : 0 < θ) : ∃ (C : ℝ), 0 < C ∧ ∀ {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [inst : mu.IsAddHaarMeasure] {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 → MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ ι) => max (↑↑(W1p.value u) x - k) 0) 2 (mu.restrict ↑Omega) → (∀ᵐ (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} → ∀ (j : ℕ), √↑j * (mu.restrict (Metric.ball x₀ R)).real {x : EuclideanSpace ℝ ι | M - (M - k) / 2 ^ j ≤ ↑↑(W1p.value u) x} ≤ C * mu.real (Metric.ball x₀ R)

Decay of upper level sets of weak subsolutions (De Giorgi). Fix ellipticity constants λ, Λ and a proportion θ > 0. There is C > 0, depending only on these and the dimension, 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 - k)⁺ ∈ L²(Ω), u ≤ M almost everywhere on B(x₀, 2R), and |{u ≤ k} ∩ B(x₀, R)| ≥ θ |B(x₀, R)|. Then for every j,

√j · |{u ≥ M - (M - k)/2ʲ} ∩ B(x₀, R)| ≤ C |B(x₀, R)|.

The constant is independent of R and of the additive Haar measure μ. No regularity of the coefficients beyond measurability is assumed.