Rumin’s constant

The explicit three-dimensional coefficient in the kinetic Lieb–Thirring inequality.

noncomputable def LiebThirring.ruminConstant : NNReal

The explicit three-dimensional kinetic coefficient obtained from Rumin’s argument.

Equations

• LiebThirring.ruminConstant = (9 / 35 * (6 * Real.pi ^ 2) ^ (2 / 3)).toNNReal