Hyperreflexivity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The Arveson commutant-distance formula reduces hyperreflexivity to uniform matrix commutator bounds and the scalar spectral estimate. The formula is recorded in Christensen, Sinclair, Smith and White, Perturbations of C-algebraic invariants*, Geom. Funct. Anal. 20 (2010), 368–397, Equation (2.1).

def OAI.KadisonSimilarity.completeCommutatorNorm line 25
Source documentation
Completely bounded norm of the inner derivation restricted to P. The extended nonnegative real value permits this norm to be infinite before an estimate has been proved. Matrix norms are the concrete Hilbert norms.
```
def completeCommutatorNorm (P : VonNeumannAlgebra H) (Y : H →L[ℂ] H) : ℝ≥0∞ :=
…
```
def OAI.KadisonSimilarity.ArvesonDistanceFormula line 32
Source documentation
The specialization of CSSW (2010), Equation (2.1), used for this operator. M is already equal to its double commutant by its VonNeumannAlgebra structure.
```
def ArvesonDistanceFormula (M : VonNeumannAlgebra H) (T : H →L[ℂ] H) : Prop :=
…
```
theorem OAI.KadisonSimilarity.completeCommutatorNorm_le line 37
Source documentation
A uniform concrete matrix estimate controls the completely bounded norm.
```
theorem completeCommutatorNorm_le (P : VonNeumannAlgebra H) (Y : H →L[ℂ] H)
    {C : ℝ} (hC : 0 ≤ C) (estimate : CommutatorEstimate P C) :
    completeCommutatorNorm P Y ≤ ENNReal.ofReal (C * scalarCommutatorNorm P Y) := by
…
```
Mentions: OAI.KadisonSimilarity.CommutatorEstimate, OAI.KadisonSimilarity.completeCommutatorNorm, OAI.KadisonSimilarity.scalarCommutatorNorm
theorem OAI.KadisonSimilarity.twice_distance_le_of_arveson line 50
Source documentation
Application of the published distance formula. This deduction contains no additional analytic hypothesis beyond the stated matrix estimate.
```
theorem twice_distance_le_of_arveson (M : VonNeumannAlgebra H) (T : H →L[ℂ] H)
    {C : ℝ} (hC : 0 ≤ C) (arveson : ArvesonDistanceFormula M T)
    (estimate : CommutatorEstimate M.commutant C) :
    2 * Metric.infDist T (M : Set (H →L[ℂ] H)) ≤
      C * scalarCommutatorNorm M.commutant T := by
…
```
Mentions: OAI.KadisonSimilarity.ArvesonDistanceFormula, OAI.KadisonSimilarity.CommutatorEstimate, OAI.KadisonSimilarity.scalarCommutatorNorm
theorem OAI.KadisonSimilarity.hyperreflexivity_bound_of_arveson line 62
Source documentation
The quantitative hyperreflexivity bound from the commutant-distance formula, a uniform matrix estimate, and the scalar spectral bound.
```
theorem hyperreflexivity_bound_of_arveson (M : VonNeumannAlgebra H) (T : H →L[ℂ] H)
    {C : ℝ} (hC : 0 ≤ C) (arveson : ArvesonDistanceFormula M T)
    (estimate : CommutatorEstimate M.commutant C)
    (scalarBound : scalarCommutatorNorm M.commutant T ≤ 4 * offDiagonalSeminorm M T) :
    Metric.infDist T (M : Set (H →L[ℂ] H)) ≤ 2 * C * offDiagonalSeminorm M T := by
…
```
Mentions: OAI.KadisonSimilarity.ArvesonDistanceFormula, OAI.KadisonSimilarity.CommutatorEstimate, OAI.KadisonSimilarity.scalarCommutatorNorm, OAI.KadisonSimilarity.offDiagonalSeminorm