Uniform interior C^{1,α} estimates for infinity-harmonic functions in dimensions d ≥ 3
A complete Lean 4 / Mathlib formalization of the main results of the preprint "Uniform Interior C^{1,α} Estimates for Infinity-Harmonic Functions" (OpenAI, 2026). For every dimension d ≥ 3 there are α ∈ (0, 1/3] and C < ∞ such that every bounded viscosity solution u of the infinity-Laplace equation Δ_∞u = Σ u_i u_j u_ij = 0 on the unit ball of ℝ^d is differentiable on the half ball, with sup |∇u| + [∇u]_{C^{0,α}} ≤ C · osc u (Theorem 1.1). Consequently every infinity-harmonic function on a connected open subset of ℝ^d, d ≥ 3, is C¹ (Corollary 1.2). The proof rests on a Liouville theorem for…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-29-000040
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-29-000040/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-29-000040/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'