OAI/Geometry/EinsteinFour/ScalarGreenLimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The scalar flat-kernel determinant converges to sin(theta)/theta.

  1. theorem OAI.PositiveEinsteinFour.Jacobi.tendsto_of_cube_tendsto line 11
  2. theorem OAI.PositiveEinsteinFour.Jacobi.scalarGreen_reference_factorization line 23
  3. theorem OAI.PositiveEinsteinFour.Jacobi.scalarGreen_reference_det line 33
  4. theorem OAI.PositiveEinsteinFour.Jacobi.scalarGreen_determinant_tendsto line 40