{"id":"palomar/PALOMAR-2026-11-01-000009","url":"https://github.com/MColbrook/Affine-reverse-Faber-Krahn-problem/tree/8da3a495c1e4ca178ae216c01ae44826fbe1a7cc","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-01-000009-v1.json","repo":"https://github.com/MColbrook/Affine-reverse-Faber-Krahn-problem","tags":["math.SP","math.MG","msc:35P15","msc:52A23"],"score":0,"title":"A formal proof of an affine reverse Faber-Krahn inequality","trust":"high","domain":"math.SP","source":"palomar","authors":["Matthew J. Colbrook","George Stepaniants"],"reviews":0,"subject":"math.SP","summary":"The three principal manuscript results M01, M02 and M03, with their original domains and quantifier order. M01: one finite C>0 before every n>0 and compact convex Euclidean body K with nonempty interior; there exists a literal real special-linear matrix S with finite actual H0 Rayleigh infimum on interior(S K) and lambda_1(interior(S K))*volume(K)^(2/n) 0 before every n>0 and origin-symmetric compact convex volume-one K with nonempty interior in maximal Gaussian measure position; its actual H0 Rayleigh infimum is at most C*n. M03: for each real P>=2 one finite C(P)>0 precedes every n>0,…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-01","reactions":{},"formalized":true,"formalizes":[{"title":"An affine reverse Faber--Krahn inequality via information decay","identifier":"sha256:1d30574bf6a09012c0492449d6860884c993b191837c9c0d2a9bd17080a3d0bc","relationship":"adapts"},{"title":"P. Bizeul: Entropy and information jump for log-concave vectors","identifier":"https://doi.org/10.5802/crmath.390","relationship":"adapts"},{"title":"Jonathan Ho: isoperimetric Lean proofs","identifier":"https://github.com/hojonathanho/isoperimetric/tree/29768f8beeaf17295cdf3853d37da35d7e2b0a5f","relationship":"adapts"},{"title":"Scott Armstrong and Amelie Loher: Gaussian closure under L2 convergence","identifier":"https://github.com/scottnarmstrong/DOZZ/tree/5d770d1a6d69fac6dbb63060e8a89861bf3ee330","relationship":"adapts"},{"title":"Djalil Chafai: complete Brascamp--Lieb Lean proof","identifier":"https://github.com/djalilchafai/ginibre-poincare/tree/a1b2ba84e7dad8ba11b5c49a18b986a762a00a41","relationship":"adapts"}]}