OAI/Geometry/EinsteinFour/JacobiExpectedLog.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The averaged logarithmic determinant estimate from the finite moments.

  1. theorem OAI.PositiveEinsteinFour.Jacobi.expected_log_det_lower line 14