SpectralRoundingDischarge.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The one-half spectral rounding inequality

The cutoff is the support of the positive part of 2a-1. Its polynomial order inequality implies the required L² inequality for every positive functional on a concrete von Neumann algebra.

def OAI.KadisonSimilarity.halfSpectralProjection line 20
Source documentation
The actual half-threshold spectral projection.
```
def halfSpectralProjection (a : H →L[ℂ] H) : H →L[ℂ] H :=
…
```
theorem OAI.KadisonSimilarity.halfSpectralProjection_isStarProjection line 23
theorem OAI.KadisonSimilarity.halfSpectralProjection_mem line 26
theorem OAI.KadisonSimilarity.halfSpectralProjection_commutes line 31
theorem OAI.KadisonSimilarity.halfSpectralProjection_square_le line 42
Source documentation
Pure operator order form of the scalar cutoff estimate.
```
theorem halfSpectralProjection_square_le (a : H →L[ℂ] H) (ha : IsSelfAdjoint a) :
    (halfSpectralProjection a - a) ^ 2 ≤ 4 * (a * a - a) ^ 2 := by
…
```
Mentions: OAI.KadisonSimilarity.halfSpectralProjection
instance OAI.KadisonSimilarity.vonNeumann_closed line 90

theorem OAI.KadisonSimilarity.preGNS_rounding_norm_le line 97

Source documentation

Passing the polynomial order estimate through a positive functional.

theorem preGNS_rounding_norm_le {A : Type*} [CStarAlgebra A] [PartialOrder A]
    [StarOrderedRing A] (τ : A →ₚ[ℂ] ℂ) (a p : A)
    (ha : IsSelfAdjoint a) (hp : IsSelfAdjoint p)
    (horder : (p - a) ^ 2 ≤ 4 * (a * a - a) ^ 2) :
    ‖τ.toPreGNS (p - a)‖ ≤ 2 * ‖τ.toPreGNS (a * a - a)‖ := by
…

theorem OAI.KadisonSimilarity.isStarProjection_subtype_of_coe line 124
theorem OAI.KadisonSimilarity.isStarProjection_subtype_mk line 131
def OAI.KadisonSimilarity.halfSpectralProjectionElement line 140
Source documentation
The spectral projection as an element of the von Neumann algebra.
```
def halfSpectralProjectionElement (a : P.toStarSubalgebra) : P.toStarSubalgebra :=
…
```
theorem OAI.KadisonSimilarity.halfSpectralProjectionElement_isStarProjection line 143
theorem OAI.KadisonSimilarity.halfSpectralProjectionElement_square_le line 151
theorem OAI.KadisonSimilarity.halfSpectralProjectionElement_norm_le line 173
theorem OAI.KadisonSimilarity.spectralProjectionRoundingInput line 183
Source documentation
The tracial-ultrapower rounding input follows from the concrete spectral projection. In fact positivity of the functional is enough for this step.
```
theorem spectralProjectionRoundingInput :
    @SpectralProjectionRoundingInput P.toStarSubalgebra (roundingCStar P)
      (roundingOrder P) (roundingStarOrder P) τ :=
…
```
Mentions: OAI.KadisonSimilarity.SpectralProjectionRoundingInput