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 823 to 828 of 2,569 results.
DeGiorgi.rescaleToUnitBall_isSupersolution
Mathematical statement
Transport supersolutions on B(x₀, R) to the unit ball via affine pullback.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.simple_iteration_lemma
Mathematical statement
Simple Iteration Lemma (AKM, Appendix C, Lemma C.6, specialized to ξ = 2). Suppose ρ : ℝ → ℝ satisfies: 1. ρ ≥ 0 on [1/2, 1), 2. sup_{t ∈ [1/2,1)} (1-t)² ρ(t) < ∞ (finiteness of weighted supremum), 3. For all 1/2 ≤ s < t < 1: ρ(s) ≤ (1/2) ρ(t) + A_iter · (t - s)⁻² Then ρ(1/2) ≤ C_iter · A_iter. Proof sketch (following AKM): - Let `M...
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.smooth_input_unitBallExtension_smoothing
Mathematical statement
Smooth-input interface smoothing for the explicit extension operator. For smooth compactly supported input ψ, the piecewise extension unitBallExtension ψ can itself be approximated globally in full W^{1,p} by smooth compactly supported functions. The gradient side is expressed against some global field Gψ attached to the exact extension. The surro...
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.sobolev_of_approx
Mathematical statement
The main whole-space Sobolev inequality for functions approximated by smooth compactly supported functions.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.sobolev_of_memW01p_univ
Mathematical statement
Whole-space Sobolev inequality specialized to the MemW₀^{1,p} data already stored in the MemW₀^{1,p} witness predicate.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.sobolev_poincare_smooth_unitBall
Mathematical statement
Sobolev-Poincare for smooth functions on the unit ball.
Source project: DeGiorgi
Person-level attribution pending.