Research proof index

Integrability of a bounded scalar times the bilinear-form integrand. If |f(x)| ≤ C everywhere and the bilinear-form integrand ⟪A∇u,∇u⟫ is integrable (which it always is for u ∈ W^{1,2}), then f · ⟪A∇u,∇u⟫ is integrable. This is a key API lemma for the Caccioppoli/Moser absorption argument. Proved in a standalone context to keep elaboration managea...

The divergence-form RHS integrand is integrable on Ω.

A Dirichlet solution lifts to a zero-boundary weak solution for the shifted unknown u - u₀.

The five-fold enlargement of a JNBall stays inside the five-fold enlargement of the ambient ball.

John-Nirenberg exponential decay from a one-step decay hypothesis on pointwise level sets.

John-Nirenberg iteration from a base level. This is a variant of john_nirenberg (and john_nirenberg_iteration) where the one-step decay hypothesis h_decay is only assumed for lam ≥ A (instead of for all lam > 0). The exponential decay conclusion holds for all t > 0, with a slightly larger constant prefactor 1/θ² to absorb the base case `...