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 146 research declarations. Search 10,000 more complete Mathlib declarations.
146 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.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.
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.
DeGiorgi.norm_smoothFunToLp_eq
Plain-language statement
Norm of the L² class carried by a smooth test function.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.rescaleToUnitBall_isHomogeneousWeakSolution
Plain-language statement
Transport homogeneous weak solutions on B(x₀, R) to the unit ball via affine pullback.
Source project: DeGiorgi
Person-level attribution pending.