Lean repositories

• • • DeGiorgi (with Julia Kempe). Formalizes De Giorgi–Nash–Moser theory for uniformly elliptic divergence-form equations with bounded measurable coefficients: local boundedness, weak and strong Harnack inequalities, and Hölder regularity. Includes supporting developments in Sobolev spaces and weak derivatives. This was the first major PDE theorem formalized so I keep this repo in the list for historical reasons, but the code is not pretty and I do not suggest building on top of it.  Github
    • CaffarelliKohnNirenberg (with Vlad Vicol). Formalizes the Caffarelli–Kohn–Nirenberg partial regularity theorem for the three-dimensional incompressible Navier–Stokes equations: the singular set of a suitable weak solution has zero one-dimensional parabolic Hausdorff measure. Includes two -regularity criteria and allows forcing locally in for . An accompanying manuscript presents the proof. Github | Palomar
    • EscauriazaSereginSverak. Formalizes the Escauriaza-Seregin-Šverák and Ladyzhenskaya-Prodi-Serrin regularity theorems for the three-dimensional incompressible Navier–Stokes equations: Leray–Hopf solutions satisfying the critical space-time integrability conditions are smooth at positive times and unique. Includes the supporting Carleman inequalities, unique continuation and backward uniqueness. An accompanying manuscript presents the proofs. Github | Palomar
    • CIVAxisymmetric (with Vlad Vicol). A formalization of the paper by Constantin, Ignatova and Vicol on the regularity of asymptotically axisymmetric solutions to the 3D Navier-Stokes equations with analytic forcing. This paper shows that the blow-up solution with smooth forcing term constructed by OpenAI cannot be improved to an analytic forcing term. Github | Palomar  
    • AVAnomalousDiffusion (with Vlad Vicol). A formalization of our paper on anomalous diffusion by iterative quantitative homogenization. Github | Palomar 
    • CoarseGraining (with Tuomo Kuusi). A formalization, based on this paper, of coarse-graining theory for elliptic equations, including quenched homogenization estimates for isotropic random media. (There is also a decent amount of elliptic regularity theory formalized in this repo: Schauder & Calderon-Zygmund estimates, etc). Github | Palomar
    • Superdiffusion (with Tuomo Kuusi). A complete formalization of our paper (joint with Ahmed Bou-Rabee) on power-law superdiffusion and anomalous elliptic regularity for a diffusion process in a random, multiscale divergence-free drift. Github | Palomar
    • SuperdiffusionCLT. A complete formalization of our paper (joint with Tuomo Kuusi and Ahmed Bou-Rabee) proving a -type superdiffusion and superdiffusive central limit theorem for a Brownian motion in a critically-correlated random divergence-free drift. Github | Palomar
    • HighContrastHomogenization (with Tuomo Kuusi and Amélie Loher). A formalization of our paper proving that the scale at which homogenization occurs is at most a power of the ellipticity ratio for stationary random coefficient fields with a finite range of dependence. Github | Palomar
    • MarkovProcess. Constructs continuous-path strong Markov processes from conservative Feller semigroups satisfying a Kolmogorov moment condition, with existence and uniqueness for every starting point. Includes killed processes, exit laws, Dynkin’s formula, optional stopping, and Feynman–Kac semigroups for bounded potentials.  Github | Palomar
    • BKARForestFormula. Formalizes the Brydges–Kennedy–Abdesselam–Rivasseau forest interpolation formula for smooth functions, expressing a fully coupled quantity as a sum of integrals indexed by forests, as stated for example in Abdesselam and Rivasseau. This is a fundamental tool for cluster expansions used in constructive field theory. Github | Palomar