UnitaryImageLinearMap.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The linear map determined by unitary trace vectors

Once every unitary vector has a unitary image, the four-unitary decomposition constructs a map on the whole algebra. A separating embedding proves linearity and the quantitative operator-norm bound.

theorem OAI.KadisonKastler.exists_linear_map_of_unitary_vectors line 25

Source documentation

A linear map on trace vectors extends to an actual algebra-valued linear map if it sends every unitary vector to a unitary vector.

theorem exists_linear_map_of_unitary_vectors
    (J : A →ₗ[ℂ] E) (K : B →ₗ[ℂ] E) (hK : Function.Injective K)
    (S : E →ₗ[ℂ] E)
    (hU : ∀ u : unitary A, ∃ v : unitary B, K v = S (J u)) :
    ∃ θ : A →ₗ[ℂ] B,
      (∀ a, K (θ a) = S (J a)) ∧ (∀ u : unitary A, θ u ∈ unitary B) := by
…

def OAI.KadisonKastler.continuousLinearMapOfUnitaryImages line 57
Source documentation
A linear map preserving unitaries is automatically bounded.
```
def continuousLinearMapOfUnitaryImages
    (θ : A →ₗ[ℂ] B) (hθ : ∀ u : unitary A, θ u ∈ unitary B) : A →L[ℂ] B :=
…
```

theorem OAI.KadisonKastler.linear_transfer_norm_sub_le line 69

Source documentation

The unitary approximation bound extends to all algebra elements, with the factor two from the four-unitary decomposition.

theorem linear_transfer_norm_sub_le
    (θ : Algebra M →ₗ[ℂ] Algebra N) {C : ℝ}
    (hθ : ∀ u : unitary (Algebra M),
      ‖(θ u : H →L[ℂ] H) - (u : Algebra M)‖ ≤ C) (a : Algebra M) :
    ‖(θ a : H →L[ℂ] H) - (a : H →L[ℂ] H)‖ ≤ 2 * C * ‖a‖ := by
…

Mentions: OAI.KadisonKastler.Algebra

def OAI.KadisonKastler.continuousLinearTransfer line 80

Source documentation

The transferred algebra map is bounded as soon as its unitary images are uniformly close to the original unitaries.

def continuousLinearTransfer
    (θ : Algebra M →ₗ[ℂ] Algebra N) {C : ℝ}
    (hθ : ∀ u : unitary (Algebra M),
      ‖(θ u : H →L[ℂ] H) - (u : Algebra M)‖ ≤ C) :
    Algebra M →L[ℂ] Algebra N :=
…

Mentions: OAI.KadisonKastler.Algebra