Research proof index

Moser L^p → L∞ estimate for subsolutions on the unit ball, in the honest essential/a.e. form available before the continuity upgrade. This is the normalized-coefficient unit-ball form of the Moser local maximum estimate.

Moser L^p → L∞ estimate on an arbitrary ball, in the same a.e.-power format as the unit-ball Chapter 06 theorem.

The p = 2 anchor for Chapter 06 is already available from Chapter 05. This is the exact normalized De Giorgi unit-ball estimate rewritten in the Chapter 06 a.e. power-bound format. It is the base case that the later Moser iteration should strictly improve from p = 2 to arbitrary p > 1.

Regularized logarithmic gradient bound: for fixed ε > 0, ∫_Ω φ²|∇u|²/(u+ε)² ≤ 4Λ ∫_Ω |∇φ|². This is the ε-level estimate that feeds into log_gradient_bound_of_supersolution via ε → 0.

Logarithmic gradient bound for positive supersolutions. If u > 0 satisfies -∇·(A∇u) ≥ 0 on Ω, then for every smooth cutoff φ supported in Ω: ∫_Ω φ² |∇u|²/u² ≤ 4Λ ∫_Ω |∇φ|². Equivalently, setting v = -log u: ∫_Ω φ² |∇v|² ≤ 4Λ ∫_Ω |∇φ|². Proof: apply log_gradient_bound_eps for each ε > 0 to get ∫ φ²|∇u|²/(u+ε)² ≤ 4Λ ∫ |∇φ|², then send...

A smooth compactly supported function belongs to W₀^{1,p}(ℝ^d).