Moser's crossover estimate for positive supersolutions

Let a be measurable and uniformly elliptic on Ω ⊆ ℝⁿ, n ≥ 1, with constants 0 < λ ≤ Λ, and let u ∈ H¹(Ω) be a weak supersolution of the divergence-form equation

-∂ᵢ(aⁱʲ ∂ⱼu) ≥ 0 in Ω,

meaning a(u, v) ≥ 0 for every nonnegative v ∈ H¹₀(Ω), with u ≥ ε almost everywhere for some ε > 0. This file proves Moser's crossover estimate: there are constants c > 0 and K, depending only on the dimension, such that for every exponent |p| ≤ c λ/Λ and every ball with B(x₀, 4√n r) ⊆ Ω,

⨍_{B(x₀, r)} u^p · ⨍_{B(x₀, r)} u^{-p} ≤ K.

Neither factor is controlled on its own, but their product is, uniformly in u, ε and the ball. In Moser's proof of the weak Harnack inequality this links the bound on negative powers of a positive supersolution to a bound on its positive powers: lower bounds on u are stated in terms of ⨍ u^{-p}, and the crossover estimate turns them into lower bounds in terms of ⨍ u^p.

The proof combines two results. The logarithm log u has mean oscillation at most C Λ/λ on every ball B with 2B ⊆ Ω (TauCeti.PDE.exists_setAverage_abs_log_sub_setAverage_le), and the crossover form of the John–Nirenberg inequality on Euclidean balls (TauCeti.exists_setLIntegral_exp_mul_mul_setLIntegral_exp_neg_mul_ball_le) bounds ∫_B exp (p log u) · ∫_B exp (-p log u) by K |B|² once |p| Λ/λ is small. On B the integrands are u^p and u^{-p}.

Main declarations

• TauCeti.PDE.exists_setAverage_rpow_mul_setAverage_rpow_neg_le: the crossover estimate.

References

• J. Moser, On Harnack's theorem for elliptic differential equations, Comm. Pure Appl. Math. 14 (1961), 577–591.
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, §8.6 (the proof of Theorem 8.18).

theorem TauCeti.PDE.exists_setAverage_rpow_mul_setAverage_rpow_neg_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] : ∃ (c : ℝ), 0 < c ∧ ∃ (K : ℝ), ∀ (mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)) [inst : mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {lam Lam : ℝ} {u : ↥(W1p mu Omega 2)} {ε : ℝ} {x₀ : EuclideanSpace ℝ ι} {r p : ℝ}, 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) → 0 ≤ energyFormH1 a 0 0 u ↑v) → 0 < ε → (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, ε ≤ ↑↑(W1p.value u) x) → Metric.ball x₀ (4 * √↑(Fintype.card ι) * r) ⊆ ↑Omega → |p| ≤ c * (lam / Lam) → (⨍ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ r, ↑↑(W1p.value u) x ^ p ∂mu) * ⨍ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ r, ↑↑(W1p.value u) x ^ (-p) ∂mu ≤ K

Moser's crossover estimate. There are constants c > 0 and K, depending only on the dimension n ≥ 1, with the following property. Let a be measurable and uniformly elliptic on Ω with constants 0 < λ ≤ Λ, and let u ∈ H¹(Ω) be a weak supersolution of -∂ᵢ(aⁱʲ ∂ⱼu) ≥ 0 with u ≥ ε almost everywhere for some ε > 0. Then for every ball with B(x₀, 4√n r) ⊆ Ω and every exponent |p| ≤ c λ/Λ,

⨍_{B(x₀, r)} u^p · ⨍_{B(x₀, r)} u^{-p} ≤ K.

The bound is independent of u, ε, λ, Λ and the ball.