ConcreteCoefficientLimits.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The restored 66- and 68-delta coefficient estimates

The concrete support estimate and the trace quotient give the two coefficient bounds used in phase averaging. In the moving-vector estimate, the only extra term is the 2δ commutator of the free lift.

theorem OAI.KadisonKastler.concrete_coefficient_drift_fixed line 59
Source documentation
Restoring the finite coefficient column on a fixed vector retains its 66δ estimate in the ultrafilter limit.
```
theorem concrete_coefficient_drift_fixed (z : Generator.FiniteHilbert (Fin n) H) :
    ∀ ε > 0, ∀ᶠ j in (ω : Filter ℕ),
      let T := hilbertMatrix (diagonalAmplification (n := Fin n) h)
…
```
Mentions: OAI.Generator.FiniteHilbert, OAI.KadisonKastler.hilbertMatrix, OAI.KadisonKastler.diagonalAmplification
theorem OAI.KadisonKastler.concrete_coefficient_drift_moving line 72
Source documentation
A unitary lift with coordinate commutator bound 2δ gives the 68δ estimate on its moving vectors.
```
theorem concrete_coefficient_drift_moving
    (s : unitary (BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M))))
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann