Perron's extremal solutions of the Bernoulli one-phase problem: viscosity, inner variational and one-sided minimizing solutions, and free boundary structure in the plane
A Lean 4 formalization of the main results of Abedin, Feldman and Stinson on Perron's extremal solutions of the one-phase Bernoulli free boundary problem Δu = 0 in {u > 0} ∩ U, |∇u| = Q on ∂{u > 0} ∩ U. Let U ⊂ ℝᵈ, d ≥ 2, be open, bounded and connected with C² boundary, and let Q be Lipschitz on the closure of U with 0 0 on ∂U is (i) a viscosity solution in U, (ii) an inner variational solution in U for some χ (the first domain variation of the Alt–Caffarelli energy ∫ |∇u|² + Q² χ vanishes), and (iii) a downward minimizer of that energy on a ball around each free boundary point; the largest…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-27-000028
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-27-000028/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-27-000028/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'