OAI/Geometry/EinsteinFour/FlatDirichletGreenTrace.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Trace and mesh limit of the flat Green matrix.

  1. theorem OAI.PositiveEinsteinFour.Jacobi.sum_nodes line 12
  2. theorem OAI.PositiveEinsteinFour.Jacobi.sum_nodes_sq line 21
  3. theorem OAI.PositiveEinsteinFour.Jacobi.flatGreen_trace line 30
  4. def OAI.PositiveEinsteinFour.Jacobi.scaledFlatGreen line 42
  5. theorem OAI.PositiveEinsteinFour.Jacobi.scaledFlatGreen_trace line 45
  6. theorem OAI.PositiveEinsteinFour.Jacobi.scaledFlatGreen_trace_tendsto line 51
  7. theorem OAI.PositiveEinsteinFour.Jacobi.scaledFlatGreen_nonneg line 58