Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 3 research declarations. Search 10,000 more complete Mathlib declarations.
3 results
Clear filtersDeGiorgi.moserRegPow_le_rpow_of_nonneg_le_N
Plain-language statement
moserRegPow ε N p t ≤ (ε + t) ^ (p / 2) for 0 ≤ t ≤ N, since moserRegPow t = (ε + clip(t))^{p/2} - ε^{p/2} and ε^{p/2} ≥ 0.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.moserRegPow_sq_le_rpow_of_nonneg_le_N
Plain-language statement
moserRegPow ε N p t ^ 2 ≤ (ε + t) ^ p for 0 ≤ t ≤ N and 1 < p. Since 0 ≤ moserRegPow ≤ (ε + t)^{p/2}, squaring gives ≤ ((ε + t)^{p/2})^2 = (ε + t)^p.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.moserRegPowerCutoffWitness_norm_sq_le
Project documentation
Pointwise gradient norm bound for the regularized powered cutoff. Extracted as a standalone lemma to keep the surrounding proof context small.
Source project: DeGiorgi
Person-level attribution pending.