GeneratedGNSRecovery.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Recovery through an intermediate generated algebra. The free-corner argument is carried out on that algebra's own GNS space; its compression still recovers the original operator with no change in the bound.

theorem OAI.KadisonSimilarity.restrictedHom_preserves_trace line 21
def OAI.KadisonSimilarity.generatedGNSInclusion line 25
Source documentation
The source embeds in the intermediate algebra's GNS space.
```
def generatedGNSInclusion : τA.GNS →ₗᵢ[ℂ] (restrictedPositiveTrace τP L).GNS :=
…
```
Mentions: OAI.KadisonSimilarity.restrictedPositiveTrace
theorem OAI.KadisonSimilarity.generatedGNSInclusion_vector line 29
theorem OAI.KadisonSimilarity.generatedGNSInclusion_comp line 37
Source documentation
The intermediate GNS embedding followed by its inclusion is the original GNS embedding, on all completed vectors.
```
theorem generatedGNSInclusion_comp :
    (restrictedTracialGNSInclusion τP L).toContinuousLinearMap.comp
      (generatedGNSInclusion τA τP L φ hmem hφ).toContinuousLinearMap =
    (gnsTracialHomIsometry τA τP φ hφ).toContinuousLinearMap := by
…
```
Mentions: OAI.KadisonSimilarity.restrictedTracialGNSInclusion, OAI.KadisonSimilarity.generatedGNSInclusion, OAI.KadisonSimilarity.gnsTracialHomIsometry
def OAI.KadisonSimilarity.generatedGNSCompression line 54
Source documentation
Compress an ambient operator to the intermediate generated algebra.
```
def generatedGNSCompression (S : τP.GNS →L[ℂ] τP.GNS) :
    (restrictedPositiveTrace τP L).GNS →L[ℂ] (restrictedPositiveTrace τP L).GNS :=
…
```
Mentions: OAI.KadisonSimilarity.restrictedPositiveTrace

theorem OAI.KadisonSimilarity.norm_generatedGNSCompression_commutator_le line 60

Source documentation

The GNS restriction preserves every ambient commutator bound.

theorem norm_generatedGNSCompression_commutator_le
    (S : τP.GNS →L[ℂ] τP.GNS) (a : L) {c : ℝ}
    (hbound : ‖commutator S (τP.gnsStarAlgHom (a : P))‖ ≤ c) :
    ‖commutator (generatedGNSCompression τP L S)
      ((restrictedPositiveTrace τP L).gnsStarAlgHom a)‖ ≤ c := by
…

Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.generatedGNSCompression, OAI.KadisonSimilarity.restrictedPositiveTrace

theorem OAI.KadisonSimilarity.generatedGNSCompression_traceCornerBound line 76

Source documentation

Small-corner bounds restrict to the generated algebra's GNS model.

theorem generatedGNSCompression_traceCornerBound
    (trP : ∀ a b : P, τP (a * b) = τP (b * a))
    (D : StarSubalgebra ℂ P) (S : τP.GNS →L[ℂ] τP.GNS) {t ε : ℝ}
    (hbound : (gnsTracialGeometry τP trP).TraceCornerBound D S t ε) :
    (gnsTracialGeometry (restrictedPositiveTrace τP L)
      (restrictedPositiveTrace_tracial τP L trP)).TraceCornerBound
      (D.comap L.subtype) (generatedGNSCompression τP L S) t ε := by
…

Mentions: OAI.KadisonSimilarity.gnsTracialGeometry, OAI.KadisonSimilarity.restrictedPositiveTrace, OAI.KadisonSimilarity.restrictedPositiveTrace_tracial, OAI.KadisonSimilarity.generatedGNSCompression

theorem OAI.KadisonSimilarity.generatedGNSCompression_commutes line 89

Source documentation

Commutation with the free subfactor also survives the restriction.

theorem generatedGNSCompression_commutes
    (D : StarSubalgebra ℂ P) (S : τP.GNS →L[ℂ] τP.GNS)
    (hcomm : ∀ a : D, S.comp (τP.gnsStarAlgHom (a : P)) =
      (τP.gnsStarAlgHom (a : P)).comp S) :
    ∀ a : D.comap L.subtype,
      (generatedGNSCompression τP L S).comp
        ((restrictedPositiveTrace τP L).gnsStarAlgHom (a : L)) =
      ((restrictedPositiveTrace τP L).gnsStarAlgHom (a : L)).comp
        (generatedGNSCompression τP L S) := by
…

Mentions: OAI.KadisonSimilarity.generatedGNSCompression, OAI.KadisonSimilarity.restrictedPositiveTrace

theorem OAI.KadisonSimilarity.generatedGNSCompression_recover line 107

Source documentation

The original compression identity survives insertion of the generated algebra between the two Hilbert spaces.

theorem generatedGNSCompression_recover
    (T : τA.GNS →L[ℂ] τA.GNS) (S : τP.GNS →L[ℂ] τP.GNS)
    (hT : (gnsTracialHomIsometry τA τP φ hφ).toContinuousLinearMap.adjoint.comp
      (S.comp (gnsTracialHomIsometry τA τP φ hφ).toContinuousLinearMap) = T) :
    (generatedGNSInclusion τA τP L φ hmem hφ).toContinuousLinearMap.adjoint.comp
      ((generatedGNSCompression τP L S).comp
        (generatedGNSInclusion τA τP L φ hmem hφ).toContinuousLinearMap) = T := by
…

Mentions: OAI.KadisonSimilarity.gnsTracialHomIsometry, OAI.KadisonSimilarity.generatedGNSInclusion, OAI.KadisonSimilarity.generatedGNSCompression

theorem OAI.KadisonSimilarity.norm_commutator_le_generated_GNS_compression line 119

Source documentation

A free-corner bound on the intermediate algebra bounds the original commutator, using the same constant.

theorem norm_commutator_le_generated_GNS_compression
    (trP : ∀ a b : P, τP (a * b) = τP (b * a))
    (T : τA.GNS →L[ℂ] τA.GNS) (S : τP.GNS →L[ℂ] τP.GNS)
    (hT : (gnsTracialHomIsometry τA τP φ hφ).toContinuousLinearMap.adjoint.comp
      (S.comp (gnsTracialHomIsometry τA τP φ hφ).toContinuousLinearMap) = T)
    (a : A) :
    ‖commutator T (τA.gnsStarAlgHom a)‖ ≤
      ‖(gnsTracialGeometry (restrictedPositiveTrace τP L)
          (restrictedPositiveTrace_tracial τP L trP)).baseOperator
        (φ.codRestrict L hmem).range
        (commutator (generatedGNSCompression τP L S)
          ((restrictedPositiveTrace τP L).gnsStarAlgHom (φ.codRestrict L hmem a)))‖ :=
…

Mentions: OAI.KadisonSimilarity.gnsTracialHomIsometry, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.gnsTracialGeometry, OAI.KadisonSimilarity.restrictedPositiveTrace, OAI.KadisonSimilarity.restrictedPositiveTrace_tracial, OAI.KadisonSimilarity.generatedGNSCompression