SpectralCutBounds.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Quantitative high spectral cuts. The discarded part has small operator norm, and positivity bounds the trace of the retained projection.

theorem OAI.KadisonSimilarity.upperSpectralCut_commutes_self line 15
theorem OAI.KadisonSimilarity.smul_upperSpectralCut_le line 26
Source documentation
The high cut of a positive operator is bounded in order by that operator.
```
theorem smul_upperSpectralCut_le (A : H →L[ℂ] H) (hA : 0 ≤ A) (t : ℝ) :
    t • upperSpectralCut A t ≤ A := by
…
```
Mentions: OAI.KadisonSimilarity.upperSpectralCut
theorem OAI.KadisonSimilarity.norm_complement_upperSpectralCut_mul_le line 46
Source documentation
Removing the high cut of x x* leaves operator norm at most ε.
```
theorem norm_complement_upperSpectralCut_mul_le (x : H →L[ℂ] H)
    (ε : ℝ) (hε : 0 ≤ ε) :
    ‖(1 - upperSpectralCut (x * star x) (ε ^ 2)) * x‖ ≤ ε := by
…
```
Mentions: OAI.KadisonSimilarity.upperSpectralCut
def OAI.KadisonSimilarity.leftSpectralCut line 95
Source documentation
The high left spectral cut of an element of the normal algebra.
```
def leftSpectralCut (M : VonNeumannAlgebra H) (x : M.toStarSubalgebra) (ε : ℝ) :
    M.toStarSubalgebra :=
…
```
theorem OAI.KadisonSimilarity.leftSpectralCut_isStarProjection line 101
theorem OAI.KadisonSimilarity.norm_complement_leftSpectralCut_mul_le line 109

theorem OAI.KadisonSimilarity.leftSpectralCut_trace_bound line 115

Source documentation

Chebyshev's trace bound for the left spectral cut.

theorem leftSpectralCut_trace_bound (M : VonNeumannAlgebra H)
    (τ : M.toStarSubalgebra →ₚ[ℂ] ℂ)
    (htr : ∀ a b, τ (a * b) = τ (b * a))
    (x : M.toStarSubalgebra) (ε : ℝ) :
    ε ^ 2 * (τ (leftSpectralCut M x ε)).re ≤ ‖gnsTracialVector τ x‖ ^ 2 := by
…

Mentions: OAI.KadisonSimilarity.leftSpectralCut, OAI.KadisonSimilarity.gnsTracialVector

theorem OAI.KadisonSimilarity.leftSpectralCut_trace_tendsto_zero line 141

Source documentation

Algebra vectors tending to zero have high spectral cuts of vanishing trace at every fixed positive threshold.

theorem leftSpectralCut_trace_tendsto_zero (M : VonNeumannAlgebra H)
    (τ : M.toStarSubalgebra →ₚ[ℂ] ℂ)
    (htr : ∀ a b, τ (a * b) = τ (b * a))
    (x : ℕ → M.toStarSubalgebra)
    (hx : Tendsto (fun n => gnsTracialVector τ (x n)) atTop (𝓝 0))
    (ε : ℝ) (hε : 0 < ε) :
    Tendsto (fun n => (τ (leftSpectralCut M (x n) ε)).re) atTop (𝓝 0) := by
…

Mentions: OAI.KadisonSimilarity.gnsTracialVector, OAI.KadisonSimilarity.leftSpectralCut