Project-declaredLean 4.29.0-rc6
Weak harnack
DeGiorgi.weak_harnack
Plain-language statement
Weak Harnack inequality for positive supersolutions on Bā. For u > 0 with -āĀ·(Aāu) ā„ 0 on Bā, and 0 < q < 1: āuā_{L^{q*}(B_{1/4})} ⤠(C(d)/(1-q)^{d/c'})^{Ī^{1/2}} Ā· essInf_{B_{1/4}} u The estimate is stated on B_{1/4}, the ball naturally produced by the forward and inverse Moser steps together with the crossover estimate.
partial differential equationsregularity theoryanalysis
Source project: DeGiorgi
Person-level attribution pending.