RowPairing.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The weak operator pairing represented by the randomized rows

def OAI.KadisonKastler.averageRowProduct line 18
theorem OAI.KadisonKastler.averageRowProduct_inner line 23
Source documentation
Testing the averaged row product against two vectors gives exactly the scalar pairing used in the error estimate.
```
theorem averageRowProduct_inner (F G : Ω → K →L[ℂ] H)
    (x : Ω → H →L[ℂ] H) (ξ η : K) :
    inner ℂ (averageRowProduct F G x ξ) η =
      meanPairing x (fun i => F i ξ) (fun i => G i η) := by
…
```
Mentions: OAI.KadisonKastler.averageRowProduct, OAI.KadisonKastler.meanPairing
def OAI.KadisonKastler.WeakOperatorConverges line 32
Source documentation
Weak operator convergence, in the only form needed for scalar recovery. It records all vector pairings of the actual operators.
```
def WeakOperatorConverges (l : Filter J) (T : J → K →L[ℂ] K) (T₀ : K →L[ℂ] K) : Prop :=
…
```

theorem OAI.KadisonKastler.WeakOperatorConverges.row_pairing_sub line 37

Source documentation

A scalar weak limit of the row product supplies the limit of the pairing difference in the randomized commutator argument.

theorem WeakOperatorConverges.row_pairing_sub
    {l : Filter J} (F G : J → Ω → K →L[ℂ] H) (x : J → Ω → H →L[ℂ] H)
    {c : ℝ} (hlim : WeakOperatorConverges l
      (fun j => averageRowProduct (F j) (G j) (x j)) ((c : ℂ) • ContinuousLinearMap.id ℂ K))
    (ξ η ζ : K) :
    Tendsto (fun j => meanPairing (x j) (fun i => F j i ξ) (fun i => G j i η) -
      meanPairing (x j) (fun i => F j i ζ) (fun i => G j i ξ)) l
      (𝓝 ((c : ℂ) * (inner ℂ ξ η - inner ℂ ζ ξ))) := by
…

Mentions: OAI.KadisonKastler.WeakOperatorConverges, OAI.KadisonKastler.averageRowProduct, OAI.KadisonKastler.meanPairing