SourceLocalQuantization.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Relative local quantization for the actual source in the constructed finite-factor presentation. Every small projection lies in that source.

theorem OAI.KadisonSimilarity.FiniteFactorPresentation.exists_small_source_compression line 39

Source documentation

Centered ambient coefficients admit a nonzero, arbitrarily small source projection on which all compressions have arbitrarily small trace norm.

theorem exists_small_source_compression {I : Type*} [Fintype I]
    (x : I → F.N.toStarSubalgebra) (hx : ∀ i, F.representation.trace (x i) = 0)
    {δ η : ℝ} (hδ : 0 < δ) (hη : 0 < η) :
    ∃ q : (FiniteMatrixStage.generatedVonNeumann F.source.stages).toStarSubalgebra,
      IsStarProjection q ∧ q ≠ 0 ∧
      (F.representation.trace
        (coordinateInclusion (FiniteMatrixStage.generatedVonNeumann_le F.source.stages) q)).re < η ∧
      ∀ i, ‖(vectorPositiveFunctional F.N F.representation.vector).toPreGNS
        (coordinateInclusion (FiniteMatrixStage.generatedVonNeumann_le F.source.stages) q * x i *
          coordinateInclusion (FiniteMatrixStage.generatedVonNeumann_le F.source.stages) q)‖ ^ 2 <
        δ * (F.representation.trace
          (coordinateInclusion (FiniteMatrixStage.generatedVonNeumann_le F.source.stages) q)).re := by
…

Mentions: OAI.KadisonSimilarity.vectorPositiveFunctional