OAI/Geometry/EinsteinFour/VarianceCorrection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The variance correction in equation (17). Equal second moments remove the mean of the difference with the exact deficit weight.

  1. theorem OAI.PositiveEinsteinFour.Variance.variance_correction_nonneg line 18