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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 811 to 816 of 2,569 results.
DeGiorgi.MemW1pWitness.weakGrad_ae_eq_zero_on_zeroSet
Project documentation
Stampacchia's zero-set theorem for Sobolev witnesses: each weak-gradient component vanishes a.e. on the zero set of the function.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.moser_powerCutoff_memW01p_energy_of_subsolution
Mathematical statement
Analytic core of the Moser pre-estimate: the cutoff-power η · (u_+)^(p/2) belongs to W₀^{1,2} on the outer ball and satisfies the exact energy bound needed for Sobolev. The only remaining nonlinear gap is the construction of the underlying W^{1,2} witness and its energy bound.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.moserDecayRatio_sum_le_half_dim
Mathematical statement
Auxiliary geometric-product bound for the explicit Moser majorant.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.moserRegPow_le_rpow_of_nonneg_le_N
Mathematical 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
Mathematical 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_grad
Mathematical 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.