OAI/Geometry/EinsteinFour/DirichletVectorSequence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The block Dirichlet operator on an actual vector sequence.

  1. theorem OAI.PositiveEinsteinFour.Jacobi.scalarLift_mulVec line 10
  2. theorem OAI.PositiveEinsteinFour.Jacobi.blockDiagonal_mulVec line 16
  3. theorem OAI.PositiveEinsteinFour.Jacobi.dirichletMatrix_eq_scalarLift line 21
  4. theorem OAI.PositiveEinsteinFour.Jacobi.dirichlet_mulVec_sequence line 28