CompleteLinearLimits.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Scalar and limit consequences of complete bounds

def OAI.KadisonKastler.scalarMatrixCopy line 21
Source documentation
The one-by-one matrix copy of the algebra.
```
def scalarMatrixCopy : A →⋆ₐ[ℂ] CStarMatrix (Fin 1) (Fin 1) A where
…
```
theorem OAI.KadisonKastler.scalarMatrixCopy_apply line 34
theorem OAI.KadisonKastler.scalarMatrixCopy_norm line 37
theorem OAI.KadisonKastler.CompletelyBoundedBy.apply_norm_le line 42
Source documentation
A complete bound includes the ordinary operator bound with no loss.
```
theorem CompletelyBoundedBy.apply_norm_le {D : A →ₗ[ℂ] B} {c : ℝ}
    (hD : CompletelyBoundedBy D c) (x : A) : ‖D x‖ ≤ c * ‖x‖ := by
…
```
Mentions: OAI.KadisonKastler.CompletelyBoundedBy
theorem OAI.KadisonKastler.HaagerupBound.apply_norm_le line 51
Source documentation
The row-column bound includes the scalar bilinear bound.
```
theorem HaagerupBound.apply_norm_le {f : A →ₗ[ℂ] A →ₗ[ℂ] A} {c : ℝ}
    (hf : HaagerupBound f c) (x y : A) : ‖f x y‖ ≤ c * ‖x‖ * ‖y‖ := by
…
```
Mentions: OAI.KadisonKastler.HaagerupBound
def OAI.KadisonKastler.CompletelyBoundedBy.toContinuousLinearMap line 61
Source documentation
Turn a completely bounded algebraic map into a continuous linear map.
```
def CompletelyBoundedBy.toContinuousLinearMap {D : A →ₗ[ℂ] B} {c : ℝ}
    (hD : CompletelyBoundedBy D c) : A →L[ℂ] B :=
…
```
Mentions: OAI.KadisonKastler.CompletelyBoundedBy
theorem OAI.KadisonKastler.CompletelyBoundedBy.toContinuousLinearMap_apply line 65
theorem OAI.KadisonKastler.CompletelyBoundedBy.exists_equiv_add_id line 71
Source documentation
A sufficiently small completely bounded perturbation of the identity is an algebraic linear equivalence, before any multiplicativity is considered.
```
theorem CompletelyBoundedBy.exists_equiv_add_id {D : A →ₗ[ℂ] A} {c : ℝ}
    (hc : 0 ≤ c) (hc1 : c < 1) (hD : CompletelyBoundedBy D c) :
    ∃ L : A ≃ₗ[ℂ] A, L.toLinearMap = LinearMap.id + D := by
…
```
Mentions: OAI.KadisonKastler.CompletelyBoundedBy

theorem OAI.KadisonKastler.completelyBoundedBy_of_pointwise_tendsto line 89

Source documentation

Complete bounds are closed under pointwise limits. This suffices to pass uniform rectangular estimates to the norm limit of correction maps.

theorem completelyBoundedBy_of_pointwise_tendsto {ι : Type*} {l : Filter ι}
    [l.NeBot] (F : ι → A →ₗ[ℂ] B) (G : A →ₗ[ℂ] B) {c : ℝ}
    (hF : ∀ i, CompletelyBoundedBy (F i) c)
    (hG : ∀ x, Tendsto (fun i => F i x) l (𝓝 (G x))) :
    CompletelyBoundedBy G c := by
…

Mentions: OAI.KadisonKastler.CompletelyBoundedBy