Super sq le of le rpow half mul
DeGiorgi.super_sq_le_of_le_rpow_half_mul
Plain-language statement
Squaring a bound of the form c ≤ a^(1/2) * b^(1/2) gives c² ≤ a * b.
Source project: DeGiorgi
Person-level attribution pending.
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.super_sq_le_of_le_rpow_half_mul
Plain-language statement
Squaring a bound of the form c ≤ a^(1/2) * b^(1/2) gives c² ≤ a * b.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.superlevel_measureReal_le_integral_posPart
Plain-language statement
Chebyshev bound for the superlevel set {u > λ} using (u-θ)₊.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.supersolution_ae_closeout_inv
Plain-language statement
Closeout: pass from iterated L^{pₙ}(B_{rₙ}) bounds to an a.e. L^∞ bound on u⁻¹ over B_{1/2}. Since rₙ > 1/2 for all n and pₙ → ∞, the L^{pₙ} norms converge to the L^∞ norm. The uniform bound from the iteration + geometric majorant gives the pointwise bound.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.supersolution_iteration_inverse
Plain-language statement
Iteration of the inverse-power one-step bound by induction. At each step, supersolution_preMoser_inverse provides the Lᵖⁿ → Lᵖⁿ⁺¹ gain, and we accumulate the product of step constants.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.superStepConstInv_le
Plain-language statement
Each inverse-power step constant is bounded by a simpler expression. The key simplification: pₙ/(1+pₙ) ≤ pₙ (since pₙ > 0), and gap_n = 2^{-(n+2)}, so 1/gap_n² = 4^{n+2} = 16 · 4^n.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.vitali_covering_lemma
Project documentation
Vitali covering lemma (5r-covering): from any family of balls, one can extract a disjoint subfamily such that the 5× enlargements cover the union, and every original ball meets a selected ball of at least half its radius.
Source project: DeGiorgi
Person-level attribution pending.