{"id":"palomar/PALOMAR-2026-10-11-000001","url":"https://github.com/amelieloher/hypoelliptic-aleksandrov/tree/d7e0125892d7bbd013c86c9c5d6a04e39e0168a6","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-11-000001-v1.json","repo":"https://github.com/amelieloher/hypoelliptic-aleksandrov","tags":["math.AP","math.PR","msc:35K70","msc:35B50","msc:35B65","msc:35Q84","msc:35H10","kinetic-equations","pde","maximum-principle"],"score":0,"title":"Kinetic Aleksandrov estimates","trust":"high","domain":"math.AP","source":"palomar","authors":["Amélie Loher"],"reviews":0,"subject":"math.AP","summary":"A Lean 4 / Mathlib formalisation of Aleksandrov maximum principles for kinetic equations d_t u + v.grad_x u - A : D_v^2 u = f in non-divergence form, with measurable, uniformly elliptic diffusion acting only in the velocity. For coefficients A(t,v) the estimate holds for every source exponent p > 2d+1; for autonomous coefficients a(x,v) in one space dimension for every p above a threshold 1 + beta_*(Lambda/lambda) = 1 + 128 d^2 (Lambda/lambda)^2 / 3. In each case the estimate implies interior Hölder continuity of solutions; for coefficients A(t,x,v) this is the kinetic Krylov–Safonov…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-11","reactions":{},"formalized":true,"formalizes":[{"title":"From Döblin to Aleksandrov","identifier":"","relationship":"formalizes"},{"title":"Döblin–Fourier cancellation and kinetic Aleksandrov estimates","identifier":"","relationship":"formalizes"},{"title":"We need ABP","identifier":"","relationship":"formalizes"},{"title":"Sequences of convex functions and estimates of the maximum of the solution of a parabolic equation","identifier":"","relationship":"formalizes"},{"title":"A certain property of solutions of parabolic equations with measurable coefficients","identifier":"","relationship":"formalizes"}]}