ReducingRepresentationTransfer.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact transfer from a reducing representation to a larger one. Extension by zero preserves scalar and matrix commutator norms, so a standard-form embedding costs no constant in the finite-factor estimate.

theorem OAI.KadisonSimilarity.adjoint_intertwines_representations line 24
Source documentation
A star intertwiner also intertwines in the reverse direction through its Hilbert adjoint.
```
theorem adjoint_intertwines_representations (a : A) :
    I.toContinuousLinearMap.adjoint.comp (ρ a) =
      (σ a).comp I.toContinuousLinearMap.adjoint := by
…
```
def OAI.KadisonSimilarity.reducingExtension line 32
Source documentation
Extension by zero of the operator under study.
```
def reducingExtension (Y : H →L[ℂ] H) : K →L[ℂ] K :=
…
```
theorem OAI.KadisonSimilarity.norm_reducingExtension_commutator line 37
Source documentation
The scalar commutator has exactly its original norm.
```
theorem norm_reducingExtension_commutator (Y : H →L[ℂ] H) (a : A) :
    ‖commutator (reducingExtension I Y) (ρ a)‖ = ‖commutator Y (σ a)‖ := by
…
```
Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.reducingExtension
theorem OAI.KadisonSimilarity.norm_reducingExtension_matrix_commutator line 47
Source documentation
The same exact identity holds at every finite matrix level.
```
theorem norm_reducingExtension_matrix_commutator
    (Y : H →L[ℂ] H) (n : ℕ) (X : Matrix (Fin n) (Fin n) A) :
    ‖commutator (amplify (reducingExtension I Y) n)
      (matrixOperator (X.map ρ))‖ =
    ‖commutator (amplify Y n) (matrixOperator (X.map σ))‖ := by
…
```
Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.reducingExtension, OAI.KadisonSimilarity.matrixOperator
theorem OAI.KadisonSimilarity.norm_representedMatrix_of_injective line 78
Source documentation
A faithful star representation preserves the norm of every actual C-star matrix, including the zero-size case.
```
theorem norm_representedMatrix_of_injective
    (hσ : Function.Injective σ) (n : ℕ) (X : CStarMatrix (Fin n) (Fin n) A) :
    ‖representedMatrix σ X‖ = ‖X‖ := by
…
```
Mentions: OAI.KadisonSimilarity.representedMatrix

theorem OAI.KadisonSimilarity.finite_estimate_of_reducing_representation line 94

Source documentation

Any complete commutator bound for the larger representation restricts to its reducing subrepresentation without loss. The scalar premise uses the actual C-star norm of the represented algebra's source.

theorem finite_estimate_of_reducing_representation {C : ℝ}
    (estimate : ∀ (Z : K →L[ℂ] K) (δ : ℝ), 0 ≤ δ →
      (∀ a, ‖commutator Z (ρ a)‖ ≤ δ * ‖a‖) →
      ∀ (n : ℕ) (X : CStarMatrix (Fin n) (Fin n) A),
        ‖commutator (amplify Z n) (representedMatrix ρ X)‖ ≤ C * δ * ‖X‖)
    (Y : H →L[ℂ] H) {δ : ℝ} (hδ : 0 ≤ δ)
    (hscalar : ∀ a, ‖commutator Y (σ a)‖ ≤ δ * ‖a‖)
    (n : ℕ) (X : CStarMatrix (Fin n) (Fin n) A) :
    ‖commutator (amplify Y n) (representedMatrix σ X)‖ ≤ C * δ * ‖X‖ := by
…

Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.representedMatrix

theorem OAI.KadisonSimilarity.commutatorEstimate_of_subtype_bound line 115

Source documentation

For the faithful concrete subtype representation, the C-star matrix estimate is exactly the paper's operator-matrix CommutatorEstimate.

theorem commutatorEstimate_of_subtype_bound (P : VonNeumannAlgebra H)
    [IsClosed (P.toStarSubalgebra : Set (H →L[ℂ] H))] {C : ℝ}
    (estimate : ∀ (Y : H →L[ℂ] H) (δ : ℝ), 0 ≤ δ →
      (∀ a : P.toStarSubalgebra,
        ‖commutator Y (a : H →L[ℂ] H)‖ ≤ δ * ‖a‖) →
      ∀ (n : ℕ) (X : CStarMatrix (Fin n) (Fin n) P.toStarSubalgebra),
        ‖commutator (amplify Y n) (representedMatrix P.toStarSubalgebra.subtype X)‖ ≤
          C * δ * ‖X‖) : CommutatorEstimate P C := by
…

Mentions: OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.representedMatrix, OAI.KadisonSimilarity.CommutatorEstimate