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.indicator_bmo_bound
Plain-language statement
On balls staying inside Metric.ball x₀ r, the zero extension agrees with u.
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.
DeGiorgi.john_nirenberg_iteration
Plain-language statement
Iteration of level-set decay to exponential decay.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.john_nirenberg_iteration_decay_iterate
Plain-language statement
Iterating one-step level-set decay gives a geometric bound.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.john_nirenberg_iteration_rpow_bound
Plain-language statement
Exponential domination for the discrete John-Nirenberg iteration.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.simple_iteration_lemma
Plain-language 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.