RecoveryRowAverages.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The actual finite recovery-row average

The coordinate row sandwich identifies the random row product with the sequence-level recovery observable. The constructed trace expectation and scalar recovery bound therefore give its weak scalar limit.

theorem OAI.KadisonKastler.finiteAverage_repeat_snd line 22

Source documentation

Repeating a finite average along an independent nonempty finite index leaves it unchanged.

theorem finiteAverage_repeat_snd {I A V : Type*} [Fintype I] [Nonempty I] [Fintype A]
    [NormedAddCommGroup V] [NormedSpace ℂ V] (f : A → V) :
    finiteAverage (fun ia : I × A => f ia.2) = finiteAverage f := by
…

Mentions: OAI.KadisonKastler.finiteAverage

def OAI.KadisonKastler.recoverySequenceForwardRows line 36
Source documentation
Forward polynomial rows for the unitary at a sequence coordinate.
```
def recoverySequenceForwardRows (M : VonNeumannAlgebra H) (N : ℕ)
    (v : I → unitary (BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M))))
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
def OAI.KadisonKastler.recoverySequenceBackwardRows line 42
Source documentation
Backward polynomial rows at the same sequence coordinate.
```
def recoverySequenceBackwardRows (M : VonNeumannAlgebra H) (N : ℕ)
    (v : I → unitary (BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M))))
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
def OAI.KadisonKastler.recoverySequenceContractions line 48
Source documentation
The corner entries are actual elements of the original algebra.
```
def recoverySequenceContractions (M : VonNeumannAlgebra H) (N : ℕ)
    (v : I → unitary (BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M))))
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.recoverySequenceContractions_norm_le line 54
theorem OAI.KadisonKastler.recoveryRows_average_eq line 62
Source documentation
The row product is the actual finite average of the recovery observable, not merely a scalar trace identity.
```
theorem recoveryRows_average_eq (M : VonNeumannAlgebra H) (hn : 0 < n) (N : ℕ)
    (v : I → unitary (BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M))))
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.finiteAverage_repeated_matrixDiagonalProjection line 84
Source documentation
The repeated outer coordinate partition has normalized scalar average.
```
theorem finiteAverage_repeated_matrixDiagonalProjection (M : VonNeumannAlgebra H) :
    finiteAverage (fun ia : I × Fin n => matrixDiagonalProjection M ia.2) =
      (((n : ℝ)⁻¹ : ℝ) : ℂ) • (1 : Algebra (matrixVonNeumann (ι := Fin n) M)) := by
…
```
Mentions: OAI.KadisonKastler.finiteAverage, OAI.KadisonKastler.matrixDiagonalProjection, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.TraceQuotientMap.exists_recoveryRows_weak_scalar line 98
Source documentation
The actual recovery rows have a scalar weak limit with real part at least one half, using only the free quotient unitaries and the finite trace formulas.
```
theorem TraceQuotientMap.exists_recoveryRows_weak_scalar
    (D : TraceQuotientMap (matrixVonNeumannTrace (ι := Fin n) M τ) σ ω)
…
```
Mentions: OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.matrixVonNeumannTrace