OAI/Geometry/EinsteinFour/FlatDirichletNormalizer.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual square-root normalizer for the flat Green kernel.

  1. theorem OAI.PositiveEinsteinFour.Jacobi.flatDirichlet_posDef line 12
  2. theorem OAI.PositiveEinsteinFour.Jacobi.flatGreen_eq_inverse line 23
  3. theorem OAI.PositiveEinsteinFour.Jacobi.flatGreen_posDef line 26
  4. theorem OAI.PositiveEinsteinFour.Jacobi.scaledFlatGreen_posSemidef line 30
  5. def OAI.PositiveEinsteinFour.Jacobi.flatGreenRoot line 33
  6. theorem OAI.PositiveEinsteinFour.Jacobi.flatGreenRoot_square line 36
  7. theorem OAI.PositiveEinsteinFour.Jacobi.flatGreenRoot_transpose line 42