ConstructedFiniteAmplification.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The constructed finite-factor estimate in the stability notation

The finite-factor commutator estimate is uniform over separable representations. Square matrix estimates imply the rectangular complete bound used in strong stability.

theorem OAI.KadisonKastler.constructed_finiteFactor_estimate line 32
Source documentation
A commutator estimate uniform over separably represented finite factors.
```
theorem constructed_finiteFactor_estimate (M : VonNeumannAlgebra H)
    (hM : Generator.IsII1Factor M.toStarSubalgebra) :
    KadisonSimilarity.CommutatorEstimate M (3 * KadisonSimilarity.cornerConstant + 2) := by
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonSimilarity.CommutatorEstimate, OAI.KadisonSimilarity.cornerConstant
theorem OAI.KadisonKastler.constructed_finiteFactor_constant_le line 45
Source documentation
A numerical upper bound for the finite-factor commutator constant.
```
theorem constructed_finiteFactor_constant_le :
    3 * KadisonSimilarity.cornerConstant + 2 ≤ (1000000 : ℝ) := by
…
```
Mentions: OAI.KadisonSimilarity.cornerConstant
theorem OAI.KadisonKastler.similarity_matrixOperator_eq line 66
Source documentation
The two concrete definitions of an operator matrix have the same action.
```
theorem similarity_matrixOperator_eq {n : ℕ}
    (X : CStarMatrix (Fin n) (Fin n) (H →L[ℂ] H)) :
    KadisonSimilarity.matrixOperator (fun i j => X i j) = hilbertMatrix X := rfl
```
Mentions: OAI.KadisonSimilarity.matrixOperator, OAI.KadisonKastler.hilbertMatrix

theorem OAI.KadisonKastler.constructed_finiteFactor_completelyBounded line 71

Source documentation

Convert the proved finite square estimates to all rectangular levels.

theorem constructed_finiteFactor_completelyBounded
    (M : VonNeumannAlgebra H) (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (T : H →L[ℂ] H) {δ : ℝ} (hδ : 0 ≤ δ)
    (hb : ∀ a ∈ M, ‖T * a - a * T‖ ≤ δ * ‖a‖) :
    CompletelyBoundedBy ((innerDerivation T).comp M.toStarSubalgebra.subtype.toLinearMap)
      (1000000 * δ) := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.CompletelyBoundedBy, OAI.KadisonKastler.innerDerivation