Popular repositories Loading

1. cencov-petz cencov-petz Public

   Lean 4 proof of the finite Čencov–Petz uniqueness theorem: continuous monotone metrics on finite probability simplexes are scalar multiples of Fisher information.

   Lean

2. compact-spectral compact-spectral Public

   Lean 4 proof of the spectral theorem for compact self-adjoint operators: a Hilbert basis of eigenvectors exists.

   Lean

3. rellich-kondrachov rellich-kondrachov Public

   Lean 4 proof of Rellich–Kondrachov: the H¹ to L² Sobolev embedding is compact on compact Riemannian manifolds.

   Lean

4. abenenson.github.io abenenson.github.io Public

   Personal site — writing, papers, projects

   HTML

5. channel-capacity channel-capacity Public

   Lean 4 formalization of uniqueness of capacity-achieving priors for Markov kernels

   Lean