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 787 to 792 of 2,569 results.
DeGiorgi.john_nirenberg_iteration
Mathematical statement
Iteration of level-set decay to exponential decay.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.john_nirenberg_iteration_decay_iterate
Mathematical statement
Iterating one-step level-set decay gives a geometric bound.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.john_nirenberg_iteration_rpow_bound
Mathematical statement
Exponential domination for the discrete John-Nirenberg iteration.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.john_nirenberg_level_set_decay
Mathematical statement
Geometric decay of selected John-Nirenberg bad-ball unions from the local half-measure step.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.le_essInf_halfBall_of_ae_bound
Mathematical statement
An a.e. lower bound on the half ball upgrades to an essential-infimum bound on the half ball.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.level_set_family_from_base
Project documentation
A set-family John-Nirenberg tail decay theorem from a base-level one-step decay hypothesis. This is the reusable set-family analogue of john_nirenberg_from_base. It iterates one-step decay starting from the base level A for an arbitrary antitone measurable family E_lam, and is useful when the Calderon-Zygmund / stopping-time work has already been pa...
Source project: DeGiorgi
Person-level attribution pending.