The absorption lemma for estimates between nested radii

Let f be bounded above on an interval [r₀, r₁] and satisfy

f s ≤ θ f t + A (t - s)^{-β} + B whenever r₀ ≤ s < t ≤ r₁,

with 0 ≤ θ < 1 and A, B ≥ 0. Then f r₀ ≤ C (A (r₁ - r₀)^{-β} + B), where C depends only on θ and β. The term θ f t is absorbed: iterating the inequality along the radii sᵢ = r₁ - τⁱ (r₁ - r₀), for a ratio τ ∈ (0, 1) with θ < τ^β, produces a convergent geometric series, while the bounded remainder θᵏ f(sₖ) tends to zero.

This is the standard device for removing a fraction of the quantity being estimated from the right-hand side of an estimate on concentric balls, where f r is a norm of the unknown on the ball of radius r. In De Giorgi–Nash–Moser theory it turns an L² bound for the supremum of a subsolution into an Lᵖ bound with p < 2.

Main declarations

• TauCeti.exists_le_mul_mul_rpow_add_of_le_mul_add: the absorption lemma.
• TauCeti.sq_mul_le_of_forall_le: a coupled form for two quantities k and h on concentric balls, where k is bounded by h and h by an arbitrarily small multiple of k. It absorbs the weighted suprema sup (R - σ) h(σ) and sup (R - σ)² k(σ), as in the interior W^{2,p} estimate.
• TauCeti.le_add_mul_of_le_add_of_le_add_mul_add_mul: absorbs bounded lower-order terms of a step estimate between concentric balls into the (t - s)⁻¹ and (t - s)⁻² terms, so that TauCeti.sq_mul_le_of_forall_le applies.

References

• M. Giaquinta, Multiple Integrals in the Calculus of Variations and Nonlinear Elliptic Systems, Chapter V, Lemma 3.1.
• Q. Han, F. Lin, Elliptic Partial Differential Equations, Lemma 4.3.
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, proof of Theorem 9.11 (the weighted interior seminorms).

theorem TauCeti.exists_le_mul_mul_rpow_add_of_le_mul_add {θ : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : θ < 1) (β : ℝ) : ∃ (C : ℝ), 0 < C ∧ ∀ {f : ℝ → ℝ} {r₀ r₁ A B : ℝ}, r₀ < r₁ → 0 ≤ A → 0 ≤ B → BddAbove (f '' Set.Icc r₀ r₁) → (∀ (s t : ℝ), r₀ ≤ s → s < t → t ≤ r₁ → f s ≤ θ * f t + A * (t - s) ^ (-β) + B) → f r₀ ≤ C * (A * (r₁ - r₀) ^ (-β) + B)

The absorption lemma. Fix 0 ≤ θ < 1 and an exponent β. There is C > 0, depending only on θ and β, such that the following holds. Let f be bounded above on [r₀, r₁], with r₀ < r₁, and suppose that

f s ≤ θ f t + A (t - s)^{-β} + B whenever r₀ ≤ s < t ≤ r₁,

for some A, B ≥ 0. Then f r₀ ≤ C (A (r₁ - r₀)^{-β} + B).

theorem TauCeti.sq_mul_le_of_forall_le {R z a₀ K cA cB N : ℝ} {k h y : ℝ → ℝ} (hR0 : 0 < R) (ha₀ : 0 ≤ a₀) (hK1 : 1 ≤ K) (hcA : 0 ≤ cA) (hcB : 0 ≤ cB) (hN : 0 ≤ N) (hk0 : ∀ (σ : ℝ), 0 ≤ k σ) (hh0 : ∀ (σ : ℝ), 0 ≤ h σ) (hkR : ∀ σ ∈ Set.Ioo 0 R, k σ ≤ k R) (hhR : ∀ σ ∈ Set.Ioo 0 R, h σ ≤ h R) (hyz : ∀ σ ∈ Set.Ioo 0 R, y σ ≤ z) (hA : ∀ {s t : ℝ}, 0 < s → s < t → t ≤ R → k s ≤ a₀ + K * (cA / (t - s) * h t + cA / (t - s) ^ 2 * z)) (hB : ∀ {s t : ℝ}, 0 < s → s < t → t ≤ R → ∀ {η : ℝ}, 0 < η → h s ≤ η * (k t + cB / (t - s) * h t + cB / (t - s) ^ 2 * y t) + N / η * y t) {r : ℝ} (hr : 0 < r) (hrR : r < R) : (R - r) ^ 2 * k r ≤ 2 * (R ^ 2 * a₀) + (8 * cA + 256 * cA ^ 2 * N + 16 * cA * N * (4 * cB + 1)) * K ^ 2 * z

Absorption over concentric balls. Let 0 < r < R, and let k, h, y be nonnegative functions of the radius, thought of as the norms of D²u, ∇u and u on B_σ, with k and h bounded on (0, R) by their values at R and y ≤ z there. Suppose that for 0 < s < t ≤ R

k(s) ≤ a₀ + K (c_A (t - s)⁻¹ h(t) + c_A (t - s)⁻² z) and h(s) ≤ η (k(t) + c_B (t - s)⁻¹ h(t) + c_B (t - s)⁻² y(t)) + (N / η) y(t) for all η > 0.

Then (R - r)² k(r) is bounded by R² a₀ and z alone. The proof absorbs the weighted suprema sup (R - σ) h(σ) and sup (R - σ)² k(σ) over 0 < σ < R, applying both inequalities at σ and the midpoint (σ + R) / 2.

theorem TauCeti.le_add_mul_of_le_add_of_le_add_mul_add_mul {k G F h z a K cA β γ R s t : ℝ} (ha : 0 ≤ a) (hK : 0 ≤ K) (hcA : 0 ≤ cA) (hβ : 0 ≤ β) (hγ : 0 ≤ γ) (hh : 0 ≤ h) (hz : 0 ≤ z) (hs : 0 < s) (hst : s < t) (htR : t ≤ R) (hk : k ≤ a * G + K * (cA / (t - s) * h + cA / (t - s) ^ 2 * z)) (hG : G ≤ F + β * h + γ * z) : k ≤ a * F + (K + a * (β * R + γ * R ^ 2)) * ((cA + 1) / (t - s) * h + (cA + 1) / (t - s) ^ 2 * z)

Absorbing bounded lower-order terms in the step between concentric balls. Let 0 < s < t ≤ R. If the step between B_s and B_t bounds k by a G plus terms in (t - s)⁻¹ h and (t - s)⁻² z, and G ≤ F + β h + γ z, then since t - s ≤ R the terms β h and γ z are absorbed into the last two terms: their coefficient K becomes K + a (β R + γ R²) and the constant cA becomes cA + 1. This puts a step estimate with lower-order terms into the form required by TauCeti.sq_mul_le_of_forall_le, as in the interior W^{2,p} estimate with lower-order terms.