OAI/Analysis/KadisonKastler/AmplificationRowLimits.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual randomized recovery rows have drift at most 70δ

The finitely many power estimates are combined with scalar-phase orthogonality and coordinate normalization. The resulting statements concern precisely the rows used in the scalar recovery average.

  1. theorem OAI.KadisonKastler.randomized_recovery_forward_row_limit line 57

    Source documentation

    The actual forward recovery rows have eventual drift 70δ on a unit vector.

    theorem randomized_recovery_forward_row_limit
    (hs : ∀ j, let T := hilbertMatrix (diagonalAmplification (n := Fin n) h)
…

    Mentions: OAI.KadisonKastler.hilbertMatrix, OAI.KadisonKastler.diagonalAmplification

  2. theorem OAI.KadisonKastler.randomized_recovery_backward_row_limit line 94

    Source documentation

    The adjoint recovery rows satisfy the matching actual 70δ drift bound.

    theorem randomized_recovery_backward_row_limit
    (ξ : Generator.FiniteHilbert (Fin n) H) (hξ : ‖ξ‖ = 1) :
    ∀ ε > 0, ∀ᶠ j in (ω : Filter ℕ),
      let T := hilbertMatrix (diagonalAmplification (n := Fin n) h)
…

    Mentions: OAI.Generator.FiniteHilbert, OAI.KadisonKastler.hilbertMatrix, OAI.KadisonKastler.diagonalAmplification