OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/OrthogonalBlockDecomposition.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Block coordinates on an orthogonal subspace and its actual complement. The high space may retain an unused copy of the low coordinates, since the physical vectors and trial vectors lie in the kernel of the restriction.

  1. def OAI.ContinuumCoulomb.Perturbation.orthogonalHighPart line 15
  2. theorem OAI.ContinuumCoulomb.Perturbation.orthogonalHighPart_kernel line 17
  3. theorem OAI.ContinuumCoulomb.Perturbation.orthogonal_assemble line 21
  4. theorem OAI.ContinuumCoulomb.Perturbation.orthogonalInclusion_norm line 26
  5. theorem OAI.ContinuumCoulomb.Perturbation.orthogonalParts_norm line 32
  6. theorem OAI.ContinuumCoulomb.Perturbation.orthogonalAssemble_norm line 40
  7. theorem OAI.ContinuumCoulomb.Perturbation.orthogonalBlock_energy line 46
  8. theorem OAI.ContinuumCoulomb.Perturbation.orthogonalBlock_full_energy line 66