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 187 research declarations. Search 10,000 more complete Mathlib declarations.
187 results
Clear filtersDeGiorgi.MemW1pWitness.ae_eq_p
Plain-language statement
Weak gradients of the same W^{1,p} function agree a.e. on the source open set.
Source project: DeGiorgi
Person-level attribution pending.
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
Plain-language 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
Plain-language 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
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.