OAI/Geometry/EinsteinFour/JacobiCompressionLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Positivity of the actual first-mode compression survives the mesh limit.

  1. theorem OAI.PositiveEinsteinFour.Jacobi.reference_compression_posSemidef line 15
  2. theorem OAI.PositiveEinsteinFour.Jacobi.continuous_radial_compression_posSemidef line 52