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.integrable_bilinFormIntegrandOfCoeff
Plain-language statement
The bilinear-form integrand is integrable on Ω.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.integrable_bounded_mul_bilinFormIntegrand
Project documentation
Integrability of a bounded scalar times the bilinear-form integrand. If |f(x)| ≤ C everywhere and the bilinear-form integrand ⟪A∇u,∇u⟫ is integrable (which it always is for u ∈ W^{1,2}), then f · ⟪A∇u,∇u⟫ is integrable. This is a key API lemma for the Caccioppoli/Moser absorption argument. Proved in a standalone context to keep elaboration managea...
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.integrable_divergenceRHSIntegrandOfField
Plain-language statement
The divergence-form RHS integrand is integrable on Ω.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.isWeakSolution_subDatum_of_dirichletProblem
Plain-language statement
A Dirichlet solution lifts to a zero-boundary weak solution for the shifted unknown u - u₀.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.JNBall.fivefold_subset_sixBall
Plain-language statement
The five-fold enlargement of a JNBall stays inside the five-fold enlargement of the ambient ball.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.john_nirenberg
Plain-language statement
John-Nirenberg exponential decay from a one-step decay hypothesis on pointwise level sets.
Source project: DeGiorgi
Person-level attribution pending.