ProjectionCommutators.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The orthogonal block estimate used before the spectral step approximation.

theorem OAI.KadisonSimilarity.norm_commutator_projection_le line 16
Source documentation
For a projection, the two off-diagonal blocks control its commutator by their maximum. The proof uses orthogonal input and output decompositions.
```
theorem norm_commutator_projection_le (T e : H →L[ℂ] H)
    (hstar : star e = e) (hsq : e * e = e) {a : ℝ}
    (hleft : ‖(1 - e) * T * e‖ ≤ a) (hright : ‖e * T * (1 - e)‖ ≤ a) :
    ‖commutator T e‖ ≤ a := by
…
```
Mentions: OAI.KadisonSimilarity.commutator
def OAI.KadisonSimilarity.complementProjection line 71
Source documentation
Complement of a commutant projection, as a commutant projection.
```
def complementProjection {M : VonNeumannAlgebra H} (e : CommutantProjection M) :
    CommutantProjection M :=
…
```
Mentions: OAI.KadisonSimilarity.CommutantProjection
theorem OAI.KadisonSimilarity.offDiagonalValue_le_norm line 79
theorem OAI.KadisonSimilarity.norm_offDiagonal_le line 94
Source documentation
Each defining off-diagonal block is bounded by the distance seminorm.
```
theorem norm_offDiagonal_le (M : VonNeumannAlgebra H) (T : H →L[ℂ] H)
    (e : CommutantProjection M) :
    ‖(1 - e.val) * T * e.val‖ ≤ offDiagonalSeminorm M T := by
…
```
Mentions: OAI.KadisonSimilarity.CommutantProjection, OAI.KadisonSimilarity.offDiagonalSeminorm
theorem OAI.KadisonSimilarity.offDiagonalSeminorm_nonneg line 104
Source documentation
The off-diagonal distance seminorm is nonnegative.
```
theorem offDiagonalSeminorm_nonneg (M : VonNeumannAlgebra H) (T : H →L[ℂ] H) :
    0 ≤ offDiagonalSeminorm M T := by
…
```
Mentions: OAI.KadisonSimilarity.offDiagonalSeminorm
theorem OAI.KadisonSimilarity.norm_commutator_projection_le_offDiagonal line 110
Source documentation
The first estimate in the manuscript's hyperreflexivity proof.
```
theorem norm_commutator_projection_le_offDiagonal (M : VonNeumannAlgebra H)
    (T : H →L[ℂ] H) (e : CommutantProjection M) :
    ‖commutator T e.val‖ ≤ offDiagonalSeminorm M T := by
…
```
Mentions: OAI.KadisonSimilarity.CommutantProjection, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.offDiagonalSeminorm

theorem OAI.KadisonSimilarity.scalarCommutatorNorm_le_four_of_selfAdjoint line 120

Source documentation

Real/imaginary decomposition reduces the scalar estimate to a bound on selfadjoint elements.

theorem scalarCommutatorNorm_le_four_of_selfAdjoint (M : VonNeumannAlgebra H)
    (T : H →L[ℂ] H)
    (selfAdjointBound : ∀ A : H →L[ℂ] H, A ∈ M.commutant → star A = A →
      ‖commutator T A‖ ≤ 2 * offDiagonalSeminorm M T * ‖A‖) :
    scalarCommutatorNorm M.commutant T ≤ 4 * offDiagonalSeminorm M T := by
…

Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.offDiagonalSeminorm, OAI.KadisonSimilarity.scalarCommutatorNorm