LocalLogarithmicLaplacian.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Local logarithmic calculus for a bounded-gradient weak Laplacian

Only a positive lower bound on the region of interest is needed. The constructed global Sobolev function agrees there with the logarithm; its global L² source comes from a smooth scalar extension.

theorem OAI.RegularPointCoordinates.exists_local_logarithmic_laplacian line 21