SpectralSteps.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The spectral-step part of the hyperreflexivity deduction

SpectralStepApproximation isolates exactly the norm approximation by spectral projections that the manuscript uses. It is the step-function specialization of Blackadar, Operator Algebras (2006; revised manuscript February 8, 2017), I.6.1.3--4, with membership of spectral projections from I.9.2.1(iv). The scalar offset is essential: summation by parts gives a total variation of the remaining coefficients at most twice the operator norm.

The spectral approximation and the uniform commutator estimate together imply the hyperreflexivity bound.

def OAI.KadisonSimilarity.spectralStep line 27

Source documentation

A scalar offset plus a finite linear combination of spectral projections.

def spectralStep {n : ℕ} (r : ℝ) (c : Fin n → ℝ) (e : Fin n → H →L[ℂ] H) :
    H →L[ℂ] H := (r : ℂ) • 1 + ∑ i, (c i : ℂ) • e i

def OAI.KadisonSimilarity.SpectralStepApproximation line 31
Source documentation
Spectral approximation with a bound on the sum of absolute coefficients.
```
def SpectralStepApproximation (P : VonNeumannAlgebra H) : Prop :=
…
```
theorem OAI.KadisonSimilarity.commutator_spectralStep line 39
Source documentation
The scalar term has zero commutator; the other terms retain their coefficients.
```
theorem commutator_spectralStep (T : H →L[ℂ] H) {n : ℕ}
    (r : ℝ) (c : Fin n → ℝ) (e : Fin n → H →L[ℂ] H) :
    commutator T (spectralStep r c e) = ∑ i, (c i : ℂ) • commutator T (e i) := by
…
```
Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.spectralStep

theorem OAI.KadisonSimilarity.norm_commutator_spectralStep_le line 46

Source documentation

A finite spectral sum is controlled by the total variation of its coefficients.

theorem norm_commutator_spectralStep_le (M : VonNeumannAlgebra H) (T : H →L[ℂ] H)
    {n : ℕ} (r : ℝ) (c : Fin n → ℝ) (e : Fin n → H →L[ℂ] H)
    (he : ∀ i, e i ∈ M.commutant ∧ star (e i) = e i ∧ e i * e i = e i) :
    ‖commutator T (spectralStep r c e)‖ ≤
      (∑ i, |c i|) * offDiagonalSeminorm M T := by
…

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

theorem OAI.KadisonSimilarity.norm_commutator_selfAdjoint_of_spectralSteps line 65
Source documentation
The projection approximation yields the claimed sharp scalar-level factor 2 for a selfadjoint input.
```
theorem norm_commutator_selfAdjoint_of_spectralSteps (M : VonNeumannAlgebra H)
    (approximation : SpectralStepApproximation M.commutant) (T A : H →L[ℂ] H)
    (hA : A ∈ M.commutant) (hAstar : star A = A) :
    ‖commutator T A‖ ≤ 2 * offDiagonalSeminorm M T * ‖A‖ := by
…
```
Mentions: OAI.KadisonSimilarity.SpectralStepApproximation, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.offDiagonalSeminorm
theorem OAI.KadisonSimilarity.scalarCommutatorNorm_le_four_of_spectralSteps line 97
Source documentation
The real/imaginary decomposition now yields the scalar factor 4.
```
theorem scalarCommutatorNorm_le_four_of_spectralSteps (M : VonNeumannAlgebra H)
    (approximation : SpectralStepApproximation M.commutant) (T : H →L[ℂ] H) :
    scalarCommutatorNorm M.commutant T ≤ 4 * offDiagonalSeminorm M T := by
…
```
Mentions: OAI.KadisonSimilarity.SpectralStepApproximation, OAI.KadisonSimilarity.scalarCommutatorNorm, OAI.KadisonSimilarity.offDiagonalSeminorm
theorem OAI.KadisonSimilarity.hyperreflexivity_of_spectralSteps_and_arveson line 106
Source documentation
Spectral approximation and the uniform commutator estimate imply the hyperreflexivity bound with constant 2 * C.
```
theorem hyperreflexivity_of_spectralSteps_and_arveson (M : VonNeumannAlgebra H)
    (approximation : SpectralStepApproximation M.commutant) (T : H →L[ℂ] H)
    {C : ℝ} (hC : 0 ≤ C) (arveson : ArvesonDistanceFormula M T)
    (estimate : CommutatorEstimate M.commutant C) :
    Metric.infDist T (M : Set (H →L[ℂ] H)) ≤ 2 * C * offDiagonalSeminorm M T :=
…
```
Mentions: OAI.KadisonSimilarity.SpectralStepApproximation, OAI.KadisonSimilarity.ArvesonDistanceFormula, OAI.KadisonSimilarity.CommutatorEstimate, OAI.KadisonSimilarity.offDiagonalSeminorm