The exact Rumin coefficient

The real coefficient obtained after inserting the three-dimensional low-momentum volume is the real value of the coefficient.

Exact equality between the coefficient emitted by scalar Rumin integration and the extended nonnegative coefficient.

theorem LiebThirring.ruminCoefficient_real_eq (q : ℕ) (hq : 1 ≤ q) : 9 / 35 * (↑q * (1 / (6 * Real.pi ^ 2))) ^ (-2 / 3) = ↑ruminConstant * ↑q ^ (-2 / 3)

The real coefficient obtained after inserting the three-dimensional low-momentum volume is the real value of the coefficient.

theorem LiebThirring.ofReal_ruminCoefficient_eq (q : ℕ) (hq : 1 ≤ q) : ENNReal.ofReal (9 / 35 * (↑q * (1 / (6 * Real.pi ^ 2))) ^ (-2 / 3)) = ↑ruminConstant * ↑q ^ (-2 / 3)

Exact equality between the coefficient emitted by scalar Rumin integration and the extended nonnegative coefficient.