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 7 research declarations. Search 10,000 more complete Mathlib declarations.
7 results
Clear filtersDeGiorgi.abs_ballAverage_sub_sixBallAverage_le
Plain-language statement
The average shift estimate: |(u)_B - (u)_{6B}| ≤ 6^d * M.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.abs_sub_const_bmo_le_two
Plain-language statement
The absolute value function |u - c| has BMO seminorm at most 2M whenever u has BMO seminorm at most M. Uses the reverse triangle inequality ||a| - |b|| ≤ |a - b|.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.abs_subballAverage_sub_ballAverage_le
Plain-language statement
The average on a sub-ball differs from the average on a larger ball by at most the volume ratio times the mean oscillation on the larger ball.
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_from_base
Plain-language statement
John-Nirenberg iteration from a base level. This is a variant of john_nirenberg (and john_nirenberg_iteration) where the one-step decay hypothesis h_decay is only assumed for lam ≥ A (instead of for all lam > 0). The exponential decay conclusion holds for all t > 0, with a slightly larger constant prefactor 1/θ² to absorb the base case `...
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.john_nirenberg_level_set_decay
Plain-language statement
Geometric decay of selected John-Nirenberg bad-ball unions from the local half-measure step.
Source project: DeGiorgi
Person-level attribution pending.