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.moserRegPowerCutoffWitness_grad
Plain-language statement
The gradient of moserRegPowerCutoffWitness decomposes as η · (chain rule) + (product rule). This is the analogue of deGiorgiCutoffTestWitnessWeighted_grad from Chapter 05.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.moserRegTestCutoff_memH01
Plain-language statement
The regularized Moser test function belongs to H₀¹(B_s).
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.moserRegTestPow_nonneg_of_nonneg
Plain-language statement
The moserRegTestPow is nonneg on nonneg inputs: since smoothClip(t) ≥ 0 for t ≥ 0, we have (ε + smoothClip(t))^{p-1} ≥ ε^{p-1}.
Source project: DeGiorgi
Person-level attribution pending.