OAI/Geometry/EinsteinFour/SineLogPolynomial.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

An explicit comparison function for the lower-volume sine remainder.

  1. def OAI.PositiveEinsteinFour.Jacobi.sineLogPolynomial line 12
  2. def OAI.PositiveEinsteinFour.Jacobi.sineCotPolynomial line 13
  3. def OAI.PositiveEinsteinFour.Jacobi.sineLogRate line 14
  4. def OAI.PositiveEinsteinFour.Jacobi.sineLogResidual line 15
  5. def OAI.PositiveEinsteinFour.Jacobi.sineLogWronskian line 16
  6. theorem OAI.PositiveEinsteinFour.Jacobi.sineLogPolynomial_hasDerivAt line 19
  7. theorem OAI.PositiveEinsteinFour.Jacobi.sineCotPolynomial_hasDerivAt line 26
  8. theorem OAI.PositiveEinsteinFour.Jacobi.sineLogWronskian_hasDerivAt line 34
  9. theorem OAI.PositiveEinsteinFour.Jacobi.sineLogWronskian_nonneg line 45