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.
    • CoarseGraining (with Tuomo Kuusi). Formalizes coarse-graining theory for elliptic equations, including quenched homogenization estimates for isotropic random media. Based on this paper.
    • Superdiffusion (with Tuomo Kuusi). A complete formalization of this paper (joint with Ahmed Bou-Rabee and Tuomo Kuusi) which proves power-law superdiffusion and anomalous elliptic regularity for a diffusion process in a random, multiscale divergence-free drift. Builds on the CoarseGraining and MarkovProcess libraries.
    • 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. Provides the probabilistic infrastructure used in the Superdiffusion repository.
    • 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. This is a fundamental tool for cluster expansions used in constructive field theory. See Abdesselam and Rivasseau.