RandomizedQuadratic.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.KadisonKastler.hilbertMatrix_diagonalAmplification_eq line 19
Source documentation
The matrix and direct-sum definitions of diagonal amplification agree.
```
theorem hilbertMatrix_diagonalAmplification_eq (h : H →L[ℂ] H) :
    hilbertMatrix (diagonalAmplification (n := Fin n) h) =
…
```
Mentions: OAI.KadisonKastler.hilbertMatrix, OAI.KadisonKastler.diagonalAmplification
theorem OAI.KadisonKastler.diagonalAmplification_isSelfAdjoint line 26
Source documentation
A symmetric operator remains selfadjoint after diagonal amplification.
```
theorem diagonalAmplification_isSelfAdjoint (h : H →L[ℂ] H) (hh : h.IsSymmetric) :
    IsSelfAdjoint (hilbertMatrix (diagonalAmplification (n := Fin n) h)) := by
…
```
Mentions: OAI.KadisonKastler.hilbertMatrix, OAI.KadisonKastler.diagonalAmplification
theorem OAI.KadisonKastler.randomized_recovery_quadratic_bound line 40
Source documentation
The two actual eventual row-error estimates, the scalar derivation bound, and the constructed recovery family imply the 282δ quadratic estimate. The row-error hypotheses are the only analytic assembly premises here.
```
theorem randomized_recovery_quadratic_bound
    (D : TraceQuotientMap (matrixVonNeumannTrace (ι := Fin n) M τ) σ ω)
…
```
Mentions: OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.matrixVonNeumannTrace