{"id":"palomar/PALOMAR-2026-10-19-000019","url":"https://github.com/CoolRmal/bergman-weak-type/tree/600df3646a6070299e831b565a3be0585483ee2c","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-19-000019-v1.json","repo":"https://github.com/CoolRmal/bergman-weak-type","tags":["math.CV","math.FA","msc:30H20","msc:42B35","msc:47B38","complex-analysis","bergman-projection","formalization"],"score":0,"title":"Bergman projection weak type constants","trust":"high","domain":"math.CV","source":"palomar","authors":["Yongxi Lin"],"reviews":0,"subject":"math.CV","summary":"A Lean formalization of weak type (1,1) constants for the Bergman projection and its positive-kernel counterpart on the unit disk. The proved results are the sharp unweighted constants, weighted positive-kernel constants, and upper and lower weighted bounds for the complex projection. A further theorem characterizes Euclidean disks among bounded simply connected open regions using their reproducing Bergman kernels, without boundary regularity assumptions. All seven main comparison targets are proved using only the standard permitted Lean axioms.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-19","reactions":{},"formalized":true,"formalizes":[{"title":"Research notes on sharp and weighted Bergman weak type estimates","identifier":"","relationship":"formalizes"},{"title":"Domain rigidity questions for the positive Bergman operator","identifier":"","relationship":"formalizes"}]}