ProjectionTrace.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Traces of actual orthogonal projections

The trace calculation uses the algebraic theorem for a projection onto a submodule. In particular, no spectral decomposition or matrix norm instance is needed. Matrix transport is valid in every basis, and hence in the orthonormal basis used for the weighted grading.

theorem OAI.LeanBlast.GotsmanLinial.starProjection_isProj line 27
Source documentation
The actual orthogonal projection is algebraically a projection onto its specified submodule.
```
theorem starProjection_isProj (K : Submodule 𝕜 E) :
    LinearMap.IsProj K K.starProjection.toLinearMap where
…
```
theorem OAI.LeanBlast.GotsmanLinial.trace_starProjection line 33
Source documentation
The trace of the actual orthogonal projection is the dimension of its range.
```
theorem trace_starProjection (K : Submodule 𝕜 E) :
    LinearMap.trace 𝕜 E K.starProjection.toLinearMap = (Module.finrank 𝕜 K : 𝕜) :=
…
```

theorem OAI.LeanBlast.GotsmanLinial.trace_toMatrix_starProjection line 40

Source documentation

The matrix trace of an orthogonal projection is independent of the chosen basis.

theorem trace_toMatrix_starProjection (b : Module.Basis ι 𝕜 E) (K : Submodule 𝕜 E) :
    Matrix.trace (LinearMap.toMatrix b b K.starProjection.toLinearMap) =
      (Module.finrank 𝕜 K : 𝕜) := by
…

theorem OAI.LeanBlast.GotsmanLinial.trace_toMatrixOrthonormal_starProjection line 46

Source documentation

The orthonormal matrix representation used by the grading has the correct trace.

theorem trace_toMatrixOrthonormal_starProjection (b : OrthonormalBasis ι 𝕜 E)
    (K : Submodule 𝕜 E) :
    Matrix.trace (LinearMap.toMatrixOrthonormal b K.starProjection.toLinearMap) =
      (Module.finrank 𝕜 K : 𝕜) :=
…

theorem OAI.LeanBlast.GotsmanLinial.re_trace_toMatrixOrthonormal_starProjection line 60

Source documentation

The real trace required by Hilbert--Schmidt block-mass computations.

theorem re_trace_toMatrixOrthonormal_starProjection (b : OrthonormalBasis ι ℂ E)
    (K : Submodule ℂ E) :
    (Matrix.trace (LinearMap.toMatrixOrthonormal b K.starProjection.toLinearMap)).re =
      (Module.finrank ℂ K : ℝ) := by
…