RecoveryRowDrift.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Recovery-row drift from the actual errors of the unitary powers

theorem OAI.KadisonKastler.diagonalAmplification_coordinate_compatibility line 20
Source documentation
The diagonal amplification applies the original operator in each coordinate.
```
theorem diagonalAmplification_coordinate_compatibility (h : H →L[ℂ] H)
    (x : Generator.FiniteHilbert (Fin n) H) (a : Fin n) :
    h (x a) = (hilbertMatrix (diagonalAmplification (n := Fin n) h) x) a := by
…
```
Mentions: OAI.Generator.FiniteHilbert, OAI.KadisonKastler.hilbertMatrix, OAI.KadisonKastler.diagonalAmplification

theorem OAI.KadisonKastler.normalized_phase_row_error line 36

Source documentation

Coordinate compatibility transports a phase sum of power errors to the error of the corresponding normalized row.

theorem normalized_phase_row_error
    (h : H →L[ℂ] H)
    (T : Generator.FiniteHilbert (Fin n) H →L[ℂ] Generator.FiniteHilbert (Fin n) H)
    (hcoord : ∀ x : Generator.FiniteHilbert (Fin n) H, ∀ a, h (x a) = (T x) a)
    (χ : I → Ω → ℂ) (X Y : I → Generator.FiniteHilbert (Fin n) H)
    (s t : ℝ) (z : Ω) (a : Fin n) :
    h (s • (t • finitePhaseSum χ X z) a) - s • (t • finitePhaseSum χ Y z) a =
      s • (t • finitePhaseSum χ (fun r => T (X r) - Y r) z) a := by
…

Mentions: OAI.Generator.FiniteHilbert, OAI.KadisonKastler.finitePhaseSum

theorem OAI.KadisonKastler.recoveryForwardRows_drift_le line 51

Source documentation

A uniform power-error bound in RMS gives the same bound for the actual forward recovery rows after the independent scalar phase and coordinate choice.

theorem recoveryForwardRows_drift_le (M : VonNeumannAlgebra H)
    (h : H →L[ℂ] H)
    (T : Generator.FiniteHilbert (Fin n) H →L[ℂ] Generator.FiniteHilbert (Fin n) H)
    (hcoord : ∀ x : Generator.FiniteHilbert (Fin n) H, ∀ a, h (x a) = (T x) a)
    (v : Θ → unitary (Algebra (matrixVonNeumann (ι := Fin n) M)))
…

Mentions: OAI.Generator.FiniteHilbert, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann

theorem OAI.KadisonKastler.recoveryBackwardRows_drift_le line 79

Source documentation

The adjoint power errors control the backward rows, with comparison vector T ξ as needed in the scalar quadratic estimate.

theorem recoveryBackwardRows_drift_le (M : VonNeumannAlgebra H)
    (h : H →L[ℂ] H)
    (T : Generator.FiniteHilbert (Fin n) H →L[ℂ] Generator.FiniteHilbert (Fin n) H)
    (hcoord : ∀ x : Generator.FiniteHilbert (Fin n) H, ∀ a, h (x a) = (T x) a)
    (v : Θ → unitary (Algebra (matrixVonNeumann (ι := Fin n) M)))
…

Mentions: OAI.Generator.FiniteHilbert, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann

theorem OAI.KadisonKastler.eventually_recoveryForwardRows_drift_le line 110

Source documentation

Finitely many eventual power bounds give the eventual forward-row bound with the same arbitrary error tolerance.

theorem eventually_recoveryForwardRows_drift_le (M : VonNeumannAlgebra H)
    (l : Filter J) (h : H →L[ℂ] H)
    (T : Generator.FiniteHilbert (Fin n) H →L[ℂ] Generator.FiniteHilbert (Fin n) H)
    (hcoord : ∀ x : Generator.FiniteHilbert (Fin n) H, ∀ a, h (x a) = (T x) a)
    (v : J → Θ → unitary (Algebra (matrixVonNeumann (ι := Fin n) M)))
…

Mentions: OAI.Generator.FiniteHilbert, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann

theorem OAI.KadisonKastler.eventually_recoveryBackwardRows_drift_le line 136

Source documentation

The same finite intersection of eventual events controls the backward rows.

theorem eventually_recoveryBackwardRows_drift_le (M : VonNeumannAlgebra H)
    (l : Filter J) (h : H →L[ℂ] H)
    (T : Generator.FiniteHilbert (Fin n) H →L[ℂ] Generator.FiniteHilbert (Fin n) H)
    (hcoord : ∀ x : Generator.FiniteHilbert (Fin n) H, ∀ a, h (x a) = (T x) a)
    (v : J → Θ → unitary (Algebra (matrixVonNeumann (ι := Fin n) M)))
…

Mentions: OAI.Generator.FiniteHilbert, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann