mrdouglasnySpectralPositivity0.1.0

Perron-Frobenius, Jentzsch theorem, and matrix/operator positivity in Lean 4
#math
Displaying 1-2 of 2 packages depending on mrdouglasny/SpectralPositivity
Sort by

  1. mrdouglasny/MarkovSemigroupsuses073f4af

    Markov semigroups, functional inequalities, and convergence to equilibrium in Lean 4

  2. mrdouglasny/pphi2uses073f4af

    Construction of phi^4_2 quantum field theory in Lean 4