CountableAmplification.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Finite standard multiplicities exhaust the countable standard representation. The first-coordinate projections and all intertwining identities below are constructed on the actual Hilbert direct sum.

abbrev OAI.KadisonSimilarity.CountableCopies line 23
Source documentation
The countable Hilbert direct sum of a fixed Hilbert space.
```
abbrev CountableCopies (H : Type*) [NormedAddCommGroup H] := lp (fun _ : ℕ => H) 2
```
def OAI.KadisonSimilarity.countableOperatorValue line 25
theorem OAI.KadisonSimilarity.countableOperatorValue_norm line 30
def OAI.KadisonSimilarity.countableAmplify line 40
Source documentation
The actual coordinatewise countable amplification of an operator.
```
def countableAmplify (T : H →L[ℂ] H) : CountableCopies H →L[ℂ] CountableCopies H :=
…
```
Mentions: OAI.KadisonSimilarity.CountableCopies
theorem OAI.KadisonSimilarity.countableAmplify_apply line 47
theorem OAI.KadisonSimilarity.norm_countableAmplify_le line 50
theorem OAI.KadisonSimilarity.countableAmplify_adjoint line 55
def OAI.KadisonSimilarity.firstCopiesInclusion line 63
Source documentation
Insert the first n coordinates, with zero in every later coordinate.
```
def firstCopiesInclusion (n : ℕ) : HilbertCopies H n →L[ℂ] CountableCopies H :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.CountableCopies
theorem OAI.KadisonSimilarity.firstCopiesInclusion_apply line 67
theorem OAI.KadisonSimilarity.firstCopiesInclusion_adjoint_apply line 71
theorem OAI.KadisonSimilarity.firstCopiesInclusion_adjoint_self line 79
def OAI.KadisonSimilarity.firstCopiesIsometry line 89
Source documentation
The coordinate insertion preserves the Hilbert norm.
```
def firstCopiesIsometry (n : ℕ) : HilbertCopies H n →ₗᵢ[ℂ] CountableCopies H where
…
```
Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.CountableCopies
theorem OAI.KadisonSimilarity.norm_firstCopiesInclusion_le line 94
def OAI.KadisonSimilarity.firstCopiesProjection line 98
Source documentation
The orthogonal projection onto the first n copies.
```
def firstCopiesProjection (n : ℕ) : CountableCopies H →L[ℂ] CountableCopies H :=
…
```
Mentions: OAI.KadisonSimilarity.CountableCopies
theorem OAI.KadisonSimilarity.firstCopiesProjection_adjoint line 101
theorem OAI.KadisonSimilarity.firstCopiesProjection_tendsto line 105
theorem OAI.KadisonSimilarity.countableAmplify_firstCopiesInclusion line 115
theorem OAI.KadisonSimilarity.firstCopiesInclusion_adjoint_countableAmplify line 123
theorem OAI.KadisonSimilarity.norm_firstCopies_compression_commutator_le line 131
Source documentation
Scalar commutators can only decrease on the first finite block.
```
theorem norm_firstCopies_compression_commutator_le
    (Y : CountableCopies H →L[ℂ] CountableCopies H) (T : H →L[ℂ] H) (r : ℕ)
    {c : ℝ} (h : ‖commutator Y (countableAmplify T)‖ ≤ c) :
    ‖commutator ((firstCopiesInclusion r).adjoint.comp
      (Y.comp (firstCopiesInclusion r))) (amplify T r)‖ ≤ c := by
…
```
Mentions: OAI.KadisonSimilarity.CountableCopies, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.countableAmplify, OAI.KadisonSimilarity.firstCopiesInclusion, OAI.KadisonSimilarity.amplify
theorem OAI.KadisonSimilarity.matrix_firstCopies_intertwines line 146
theorem OAI.KadisonSimilarity.matrix_firstCopies_adjoint_intertwines line 157

theorem OAI.KadisonSimilarity.norm_firstCopies_matrix_compression line 169

Source documentation

Extending the compressed matrix commutator by zero preserves its norm.

theorem norm_firstCopies_matrix_compression (r n : ℕ)
    (Y : CountableCopies H →L[ℂ] CountableCopies H)
    (X : Matrix (Fin n) (Fin n) (H →L[ℂ] H)) :
    ‖commutator (amplify ((firstCopiesProjection r).comp
      (Y.comp (firstCopiesProjection r))) n)
      (matrixOperator (fun i j => countableAmplify (X i j)))‖ =
    ‖commutator (amplify ((firstCopiesInclusion r).adjoint.comp
      (Y.comp (firstCopiesInclusion r))) n)
      (matrixOperator (fun i j => amplify (X i j) r))‖ := by
…

Mentions: OAI.KadisonSimilarity.CountableCopies, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.firstCopiesProjection, OAI.KadisonSimilarity.matrixOperator, OAI.KadisonSimilarity.countableAmplify, OAI.KadisonSimilarity.firstCopiesInclusion

def OAI.KadisonSimilarity.countableRepresentation line 201
Source documentation
The countable standard amplification of a represented algebra.
```
def countableRepresentation (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) :
    A →⋆ₐ[ℂ] (CountableCopies H →L[ℂ] CountableCopies H) where
…
```
Mentions: OAI.KadisonSimilarity.CountableCopies
theorem OAI.KadisonSimilarity.countableRepresentation_apply line 213

theorem OAI.KadisonSimilarity.countable_amplification_bound_of_finite line 219

Source documentation

The first-finite-copy estimates imply the same estimate on the countable standard representation. The finite-copy premise is a downstream estimate, not an additional published input.

theorem countable_amplification_bound_of_finite
    (σ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) {C : ℝ} (hC : 0 ≤ C)
    (hfinite : ∀ (r : ℕ) (T : HilbertCopies H r →L[ℂ] HilbertCopies H r)
      (d : ℝ), 0 ≤ d →
      (∀ a, ‖commutator T (amplify (σ a) r)‖ ≤ d * ‖a‖) →
      ∀ (n : ℕ) (X : CStarMatrix (Fin n) (Fin n) A),
        ‖commutator (amplify T n)
          (representedMatrix (amplifiedScalarRepresentation σ r) X)‖ ≤ C * d * ‖X‖)
    (Y : CountableCopies H →L[ℂ] CountableCopies H) {d : ℝ} (hd : 0 ≤ d)
    (hscalar : ∀ a, ‖commutator Y (countableRepresentation σ a)‖ ≤ d * ‖a‖)
    (n : ℕ) (X : CStarMatrix (Fin n) (Fin n) A) :
    ‖commutator (amplify Y n) (representedMatrix (countableRepresentation σ) X)‖ ≤
…

Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify, OAI.KadisonSimilarity.representedMatrix, OAI.KadisonSimilarity.amplifiedScalarRepresentation, OAI.KadisonSimilarity.CountableCopies, OAI.KadisonSimilarity.countableRepresentation

theorem OAI.KadisonSimilarity.gns_countable_amplification_bound line 248

Source documentation

The actual GNS representation is a direct instance of the countable amplification transfer, with its original finite-copy constant.

theorem gns_countable_amplification_bound (τ : A →ₚ[ℂ] ℂ)
    {C : ℝ} (hC : 0 ≤ C)
    (hfinite : ∀ (r : ℕ) (T : HilbertCopies τ.GNS r →L[ℂ] HilbertCopies τ.GNS r)
      (d : ℝ), 0 ≤ d →
      (∀ a, ‖commutator T (amplify (τ.gnsStarAlgHom a) r)‖ ≤ d * ‖a‖) →
      ∀ (n : ℕ) (X : CStarMatrix (Fin n) (Fin n) A),
        ‖commutator (amplify T n)
          (representedMatrix (amplifiedScalarRepresentation τ.gnsStarAlgHom r) X)‖ ≤
        C * d * ‖X‖)
    (Y : CountableCopies τ.GNS →L[ℂ] CountableCopies τ.GNS)
    {d : ℝ} (hd : 0 ≤ d)
    (hscalar : ∀ a, ‖commutator Y (countableRepresentation τ.gnsStarAlgHom a)‖ ≤ d * ‖a‖)
…