Lower bounds from small negative powers of supersolutions

A positive weak supersolution of -div(a ∇u) ≥ 0 satisfies the local estimate

u⁻¹ ≤ D R^{-n/p} (∫_{B(x₀, R)} u⁻ᵖ)^{1/p} on B(x₀, R/2), for every 0 < p ≤ 2.

The constant depends on the ellipticity constants, the dimension, the exponent and the normalization of Haar measure, but not on the positive lower bound assumed for u. This is the negative-power input to the weak Harnack inequality: a crossover estimate for positive and negative powers can combine this lower bound with reverse Hölder estimates.

The more general Sobolev-inequality form is also provided. Both results use local boundedness of subsolutions and the convex reciprocal approximations from TauCeti.PDE.UniformlyEllipticOn.ae_inv_value_le_mul_setIntegral_rpow.

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_ae_inv_value_le_mul_rpow_mul_setIntegral_rpow_of_forall_eLpNorm_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {lam Lam : ℝ} {q : ENNReal} (hq : 2 < q) (S : NNReal) {p : ℝ} (hp : 0 < p) (hp2 : p ≤ 2) : ∃ (D : ℝ), 0 < D ∧ ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {u : ↥(W1p mu Omega 2)} {m : ℝ} {x₀ : EuclideanSpace ℝ ι} {R : ℝ}, UniformlyEllipticOn (↑Omega) a lam Lam → MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega) → (∀ (y : EuclideanSpace ℝ ι) (s : ℝ), Metric.ball y s ⊆ ↑Omega → ∀ v ∈ w1p0Submodule mu { carrier := Metric.ball y s, is_open' := ⋯ } 2, MeasureTheory.eLpNorm (↑↑(W1p.value v)) q (mu.restrict (Metric.ball y s)) ≤ ↑S * ‖W1p.gradient v‖ₑ) → (∀ (v : ↥(W1p0 mu Omega 2)), (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, 0 ≤ ↑↑(W1p.value ↑v) x) → 0 ≤ energyFormH1 a 0 0 u ↑v) → 0 < m → (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, m ≤ ↑↑(W1p.value u) x) → 0 < R → Metric.ball x₀ R ⊆ ↑Omega → ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ (R / 2)), (↑↑(W1p.value u) x)⁻¹ ≤ D * R ^ (-(2 * (1 - 2 / q.toReal)⁻¹ / p)) * (∫ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ R, (↑↑(W1p.value u) x)⁻¹ ^ p ∂mu) ^ p⁻¹

Lower bound from negative powers under a Sobolev inequality. Suppose every ball in Ω satisfies ‖v‖_q ≤ S ‖∇v‖₂ for v ∈ W^{1,2}_0, where q > 2. For 0 < p ≤ 2, a positive weak supersolution satisfies u⁻¹ ≤ D R^{-2/(αp)} (∫_{B(x₀, R)} u⁻ᵖ)^{1/p} on the half ball, with α = 1 - 2/q. The constant is independent of the domain, the solution and its positive lower bound.

theorem TauCeti.PDE.exists_ae_inv_value_le_mul_rpow_mul_setIntegral_rpow {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {lam Lam : ℝ} [Nonempty ι] {p : ℝ} (hp : 0 < p) (hp2 : p ≤ 2) : ∃ (D : ℝ), 0 < D ∧ ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {u : ↥(W1p mu Omega 2)} {m : ℝ} {x₀ : EuclideanSpace ℝ ι} {R : ℝ}, 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 < m → (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, m ≤ ↑↑(W1p.value u) x) → 0 < R → Metric.ball x₀ R ⊆ ↑Omega → ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ (R / 2)), (↑↑(W1p.value u) x)⁻¹ ≤ D * R ^ (-↑(Fintype.card ι) / p) * (∫ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ R, (↑↑(W1p.value u) x)⁻¹ ^ p ∂mu) ^ p⁻¹

Moser's lower bound from small negative powers. For every 0 < p ≤ 2 and every positive weak supersolution in any dimension n ≥ 1, u⁻¹ ≤ D R^{-n/p} (∫_{B(x₀, R)} u⁻ᵖ)^{1/p} almost everywhere on B(x₀, R/2). The constant depends only on λ, Λ, p, the dimension and Haar normalization, not on the positive lower bound for u. No boundary regularity is required.