SpectralStepDischarge.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

Concrete spectral cut projections

We construct the spectral cuts from the closed range of the positive part. The construction takes place in the represented Hilbert space; bicommutant closure proves membership in the given von Neumann algebra.

def OAI.KadisonSimilarity.operatorRangeClosure line 23
Source documentation
Closed range used to construct the support projection of an operator.
```
def operatorRangeClosure (B : H →L[ℂ] H) : Submodule ℂ H :=
…
```
instance OAI.KadisonSimilarity.operatorRangeClosure_complete line 26
def OAI.KadisonSimilarity.rangeSupport line 31
Source documentation
The orthogonal projection onto the closed operator range.
```
def rangeSupport (B : H →L[ℂ] H) : H →L[ℂ] H :=
…
```
theorem OAI.KadisonSimilarity.rangeSupport_isStarProjection line 34
theorem OAI.KadisonSimilarity.rangeSupport_mul line 38
theorem OAI.KadisonSimilarity.mul_rangeSupport line 43
theorem OAI.KadisonSimilarity.operatorRangeClosure_invariant line 50
theorem OAI.KadisonSimilarity.rangeSupport_commutes line 62
theorem OAI.KadisonSimilarity.rangeSupport_mem line 68
theorem OAI.KadisonSimilarity.mul_rangeSupport_eq_zero line 79
Source documentation
Annihilating the range also annihilates its orthogonal support.
```
theorem mul_rangeSupport_eq_zero (B C : H →L[ℂ] H) (h : C * B = 0) :
    C * rangeSupport B = 0 := by
…
```
Mentions: OAI.KadisonSimilarity.rangeSupport
def OAI.KadisonSimilarity.upperSpectralCut line 90
Source documentation
The open upper spectral cut (t,∞) of a selfadjoint operator.
```
def upperSpectralCut (A : H →L[ℂ] H) (t : ℝ) : H →L[ℂ] H :=
…
```
theorem OAI.KadisonSimilarity.upperSpectralCut_isStarProjection line 93
theorem OAI.KadisonSimilarity.upperSpectralCut_mem line 96
theorem OAI.KadisonSimilarity.shifted_mul_upperSpectralCut line 109
Source documentation
Multiplication by a cut removes the negative part of the shifted operator.
```
theorem shifted_mul_upperSpectralCut (A : H →L[ℂ] H) (hA : IsSelfAdjoint A) (t : ℝ) :
    (A - t • 1) * upperSpectralCut A t = (A - t • 1)⁺ := by
…
```
Mentions: OAI.KadisonSimilarity.upperSpectralCut
theorem OAI.KadisonSimilarity.shifted_mul_complement_upperSpectralCut line 121
theorem OAI.KadisonSimilarity.nonneg_le_norm_smul_support line 133
Source documentation
A positive operator supported by a projection is bounded by its norm times that projection.
```
theorem nonneg_le_norm_smul_support (B p : H →L[ℂ] H)
    (hB : 0 ≤ B) (hp : IsStarProjection p) (hpB : p * B = B) (hBp : B * p = B) :
    B ≤ ‖B‖ • p := by
…
```
def OAI.KadisonSimilarity.binarySpectralCorrection line 140
Source documentation
One binary spectral correction.
```
def binarySpectralCorrection (B : H →L[ℂ] H) (r : ℝ) : H →L[ℂ] H :=
…
```
theorem OAI.KadisonSimilarity.norm_sub_binarySpectralCorrection_le line 144
Source documentation
Binary rounding halves the norm bound without changing the algebra.
```
theorem norm_sub_binarySpectralCorrection_le (B : H →L[ℂ] H)
    (hB : IsSelfAdjoint B) {r : ℝ} (hr : 0 ≤ r) (hBr : ‖B‖ ≤ r) :
    ‖B - binarySpectralCorrection B r‖ ≤ r / 2 := by
…
```
Mentions: OAI.KadisonSimilarity.binarySpectralCorrection
def OAI.KadisonSimilarity.binarySpectralRadius line 197
Source documentation
The prescribed geometric error radius.
```
def binarySpectralRadius (A : H →L[ℂ] H) (k : ℕ) : ℝ := ‖A‖ * (1 / 2 : ℝ) ^ k
…
```
theorem OAI.KadisonSimilarity.binarySpectralRadius_nonneg line 200
theorem OAI.KadisonSimilarity.binarySpectralRadius_succ line 204
def OAI.KadisonSimilarity.binarySpectralResidual line 210
Source documentation
Repeated binary rounding, performed inside the given operator algebra.
```
def binarySpectralResidual (A : H →L[ℂ] H) : ℕ → H →L[ℂ] H
  | 0 => A
  | k + 1 => binarySpectralResidual A k -
      binarySpectralCorrection (binarySpectralResidual A k) (binarySpectralRadius A k)
```
Mentions: OAI.KadisonSimilarity.binarySpectralCorrection, OAI.KadisonSimilarity.binarySpectralRadius
theorem OAI.KadisonSimilarity.binarySpectralResidual_selfAdjoint line 215
theorem OAI.KadisonSimilarity.binarySpectralResidual_norm_le line 224
theorem OAI.KadisonSimilarity.real_smul_mem_vonNeumann line 233
theorem OAI.KadisonSimilarity.positive_rangeSupport_mem line 238
theorem OAI.KadisonSimilarity.binarySpectralResidual_mem line 242
theorem OAI.KadisonSimilarity.binarySpectralResidual_eq_sub_sum line 251
theorem OAI.KadisonSimilarity.sum_binarySpectralRadius_le line 265
theorem OAI.KadisonSimilarity.binarySpectralRadius_tendsto_zero line 274
theorem OAI.KadisonSimilarity.spectralStep_binary_eq_sum line 283
Source documentation
The accumulated binary corrections have exactly the required scalar offset and projection coefficients.
```
theorem spectralStep_binary_eq_sum (A : H →L[ℂ] H) (n : ℕ) :
    spectralStep (-(∑ i : Fin n, binarySpectralRadius A i / 2))
      (fun i : Fin n => binarySpectralRadius A i)
      (fun i : Fin n => rangeSupport (binarySpectralResidual A i)⁺) =
      ∑ k ∈ Finset.range n,
        binarySpectralCorrection (binarySpectralResidual A k) (binarySpectralRadius A k) := by
…
```
Mentions: OAI.KadisonSimilarity.spectralStep, OAI.KadisonSimilarity.binarySpectralRadius, OAI.KadisonSimilarity.rangeSupport, OAI.KadisonSimilarity.binarySpectralResidual, OAI.KadisonSimilarity.binarySpectralCorrection
theorem OAI.KadisonSimilarity.spectralStepApproximation line 298
Source documentation
The required published spectral approximation is constructed directly: each binary correction halves the residual norm, while all coefficients together cost at most twice the original norm.
```
theorem spectralStepApproximation (P : VonNeumannAlgebra H) : SpectralStepApproximation P := by
…
```
Mentions: OAI.KadisonSimilarity.SpectralStepApproximation