AmplificationPowerLimits.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The randomized power errors from the coefficient word estimates

The positive power restores the controlled final factor, costing 2δ. The negative power is already the negative word. Thus both actual powers satisfy the 70δ bound used in the recovery rows.

theorem OAI.KadisonKastler.sequenceUnitaryEval_mul_constant line 26
Source documentation
Evaluation commutes with appending a constant unitary.
```
theorem sequenceUnitaryEval_mul_constant
    (s : unitary (BoundedSequence A)) (U : unitary A) (j : ℕ) :
    sequenceUnitaryEval
      (s * Unitary.map (StarMonoidHom.ofClass (boundedSequenceConst (B := A))) U) j =
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.sequenceUnitaryEval, OAI.KadisonKastler.boundedSequenceConst

theorem OAI.KadisonKastler.negative_amplification_power_limit line 68

Source documentation

Actual adjoint powers have eventual root-mean-square error at most 70δ.

theorem negative_amplification_power_limit (ξ : Generator.FiniteHilbert (Fin n) H) :
    ∀ ε > 0, ∀ᶠ j in (ω : Filter ℕ),
      let T : Generator.FiniteHilbert (Fin n) H →L[ℂ] Generator.FiniteHilbert (Fin n) H :=
…

Mentions: OAI.Generator.FiniteHilbert

theorem OAI.KadisonKastler.positive_amplification_power_limit line 112
Source documentation
Restoring the controlled final unitary turns the 68δ word estimate into the actual positive-power estimate 70δ.
```
theorem positive_amplification_power_limit
    (hs : ∀ j, let T := hilbertMatrix (diagonalAmplification (n := Fin n) h)
…
```
Mentions: OAI.KadisonKastler.hilbertMatrix, OAI.KadisonKastler.diagonalAmplification