PhaseCoefficientLimits.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Coefficient limits for the actual randomized matrix partition

theorem OAI.KadisonKastler.amplificationPhaseCoefficients_support line 37
Source documentation
The supports of both signs of the actual phase coefficients match exactly the support projections in the clipped-column estimate.
```
theorem amplificationPhaseCoefficients_support
    (E : Generator.MatrixUnitSystem (Fin k) (Algebra M))
    (w : BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M)))
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.amplificationPhaseCoefficients_contract line 67
Source documentation
The actual two coefficient columns remain contractions in the original representation.
```
theorem amplificationPhaseCoefficients_contract
    (E : Generator.MatrixUnitSystem (Fin k) (Algebra M))
    (w : unitary (BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M))))
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.matrixVonNeumann

theorem OAI.KadisonKastler.amplificationPhaseCoefficients_quotient_bounds line 98

Source documentation

The free-word bound specialized to the concrete matrix partition.

theorem amplificationPhaseCoefficients_quotient_bounds
    (hFock : PublishedDiagonalFockRepresentation.{v})
    (htrace : ∀ a, τ.toLinearMap (amplificationPartition E a) = ((n * k : ℕ) : ℂ)⁻¹)
    (hfree : FreeHaarMoments σ R.constant.range
      (Unitary.map (StarMonoidHom.ofClass R.quotient) w))
    (r : ℕ) (hword : freeWordThreshold (r + 1) ≤ n * k) :
    (∀ s : Sym (Fin (n * k)) (r + 1),
      ‖R.quotient (positivePhaseCoefficientSequence (amplificationPartition E)
        (w : BoundedSequence _) (r + 1) s)‖ ≤
          projectionWordWeight (freeWordC (r + 1)) s) ∧
    (∀ s : Sym (Fin (n * k)) (r + 1),
      ‖R.quotient (negativePhaseCoefficientSequence (amplificationPartition E)
…

Mentions: OAI.KadisonKastler.amplificationPartition, OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.freeWordThreshold, OAI.KadisonKastler.positivePhaseCoefficientSequence, OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.projectionWordWeight, OAI.KadisonKastler.freeWordC, OAI.KadisonKastler.negativePhaseCoefficientSequence

theorem OAI.KadisonKastler.negative_amplification_coefficient_limit_of_bounds line 128
Source documentation
Specialization of the fixed-vector clipping limit to negative coefficients.
```
theorem negative_amplification_coefficient_limit_of_bounds
    (hbound : ∀ s : Sym (Fin (n * k)) (r + 1),
      ‖R.quotient (negativePhaseCoefficientSequence (amplificationPartition E)
        (w : BoundedSequence _) (r + 1) s)‖ ≤
          projectionWordWeight (freeWordC (r + 1)) s)
    (z : Generator.FiniteHilbert (Fin n) H) :
    ∀ ε > 0, ∀ᶠ j in (ω : Filter ℕ),
      let T := hilbertMatrix (diagonalAmplification (n := Fin n) h)
…
```
Mentions: OAI.KadisonKastler.negativePhaseCoefficientSequence, OAI.KadisonKastler.amplificationPartition, OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.projectionWordWeight, OAI.KadisonKastler.freeWordC, OAI.Generator.FiniteHilbert, OAI.KadisonKastler.hilbertMatrix, OAI.KadisonKastler.diagonalAmplification

theorem OAI.KadisonKastler.negative_amplification_coefficient_limit line 171

Source documentation

The negative coefficients have restored drift at most 66δ on every fixed vector, before phase averaging.

theorem negative_amplification_coefficient_limit
    (hFock : PublishedDiagonalFockRepresentation.{v})
    (htrace : ∀ a, τ.toLinearMap (amplificationPartition E a) = ((n * k : ℕ) : ℂ)⁻¹)
    (hfree : FreeHaarMoments σ R.constant.range
      (Unitary.map (StarMonoidHom.ofClass R.quotient) w))
    (hword : freeWordThreshold (r + 1) ≤ n * k)
    (z : Generator.FiniteHilbert (Fin n) H) :
    ∀ ε > 0, ∀ᶠ j in (ω : Filter ℕ),
      let T := hilbertMatrix (diagonalAmplification (n := Fin n) h)
…

Mentions: OAI.KadisonKastler.amplificationPartition, OAI.KadisonKastler.FreeHaarMoments, OAI.KadisonKastler.freeWordThreshold, OAI.Generator.FiniteHilbert, OAI.KadisonKastler.hilbertMatrix, OAI.KadisonKastler.diagonalAmplification

theorem OAI.KadisonKastler.positive_amplification_coefficient_limit_of_bounds line 191
Source documentation
The positive coefficient column has drift 68δ on vectors moved by the controlled unitary lift.
```
theorem positive_amplification_coefficient_limit_of_bounds
    (hbound : ∀ s : Sym (Fin (n * k)) (r + 1),
      ‖R.quotient (positivePhaseCoefficientSequence (amplificationPartition E)
        (w : BoundedSequence _) (r + 1) s)‖ ≤
          projectionWordWeight (freeWordC (r + 1)) s)
    (s : unitary (BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M))))
…
```
Mentions: OAI.KadisonKastler.positivePhaseCoefficientSequence, OAI.KadisonKastler.amplificationPartition, OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.projectionWordWeight, OAI.KadisonKastler.freeWordC, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann