Stampacchia's lemma #
Let φ be nonnegative and nonincreasing on [k₀, ∞), and suppose that
φ h ≤ (M / (h - k)) ^ α * φ k ^ β whenever k₀ ≤ k < h,
with M > 0, α > 0 and β > 1. Then φ vanishes at the finite level
k₀ + d, where d = M * φ k₀ ^ ((β - 1) / α) * 2 ^ (β / (β - 1)).
This is the numerical lemma behind Stampacchia's proof of global boundedness for weak solutions
of elliptic equations. There φ h is the measure of the superlevel set {u > h} of a weak
subsolution u, and testing the equation against (u - k)⁺, combined with the Sobolev and
Chebyshev inequalities, gives the recursive inequality. The conclusion φ (k₀ + d) = 0 says that
u ≤ k₀ + d almost everywhere.
The proof evaluates φ along the levels kⱼ = k₀ + d (1 - 2⁻ʲ), which increase to k₀ + d. The
values φ kⱼ satisfy the superlinear recurrence of TauCeti.le_geom_of_le_mul_pow_mul_rpow, with
the choice of d making the starting value exactly small enough, so they decay geometrically; since
φ (k₀ + d) ≤ φ kⱼ for every j, it vanishes.
Main declarations #
TauCeti.apply_add_eq_zero_of_le_div_sub_rpow_mul_rpow: Stampacchia's lemma.
References #
- G. Stampacchia, Le problème de Dirichlet pour les équations elliptiques du second ordre à coefficients discontinus, Ann. Inst. Fourier 15 (1965).
- D. Kinderlehrer, G. Stampacchia, An Introduction to Variational Inequalities and Their Applications, Chapter II, Appendix B, Lemma B.1.
Stampacchia's lemma. Let φ be nonnegative and antitone on [k₀, ∞), with
φ h ≤ (M / (h - k)) ^ α * φ k ^ β whenever k₀ ≤ k < h,
for constants M > 0, α > 0 and β > 1. Then φ (k₀ + d) = 0, where
d = M * φ k₀ ^ ((β - 1) / α) * 2 ^ (β / (β - 1)).