TracialConjugationBound.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Comparing tracial conjugations in common position

The two conjugations are supplied as actual conjugate-linear isometries. Common right-action commutation remains an explicit structural premise; the distance estimate itself follows from unit-ball approximation and the proved finite bimodular test.

def OAI.KadisonKastler.tracialConjugationDefect line 20
Source documentation
The complex-linear comparison operator of two conjugations.
```
def tracialConjugationDefect (J₁ J₂ : H ≃ₗᵢ⋆[ℂ] H) : H →L[ℂ] H :=
…
```
theorem OAI.KadisonKastler.tracialConjugationDefect_apply line 25

theorem OAI.KadisonKastler.norm_tracialConjugationDefect line 30

Source documentation

Composing by an involutive isometry identifies the two operator norms.

theorem norm_tracialConjugationDefect (J₁ J₂ : H ≃ₗᵢ⋆[ℂ] H)
    (hJ₁ : Function.Involutive J₁) :
    ‖tracialConjugationDefect J₁ J₂‖ =
      ‖(J₁ : H →L⋆[ℂ] H) - (J₂ : H →L⋆[ℂ] H)‖ := by
…

Mentions: OAI.KadisonKastler.tracialConjugationDefect

theorem OAI.KadisonKastler.tracialConjugationDefect_unitBall_bound line 55

Source documentation

Close unit balls bound the comparison operator on every bounded algebra vector by twice the Kadison--Kastler tolerance.

theorem tracialConjugationDefect_unitBall_bound
    {M N : VonNeumannAlgebra H} (J₁ J₂ : H ≃ₗᵢ⋆[ℂ] H)
    (Ω : H) (hΩ : ‖Ω‖ = 1)
    (hM : ∀ x : Algebra M, J₁ (x.val Ω) = (star x).val Ω)
    (hN : ∀ y : Algebra N, J₂ (y.val Ω) = (star y).val Ω)
    {b : ℝ} (hb : kkDistance M N < b) (x : Algebra M) (hx : ‖x‖ ≤ 1) :
    ‖tracialConjugationDefect J₁ J₂ (x.val Ω)‖ ≤ 2 * b := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.tracialConjugationDefect

theorem OAI.KadisonKastler.norm_tracialConjugations_sub_le line 84

Source documentation

The norm-768 tracial-conjugation estimate under common module actions commuting with the comparison operator.

theorem norm_tracialConjugations_sub_le
    {M N : VonNeumannAlgebra H} {R : Type*} [CStarAlgebra R]
    (τ : FaithfulTracialState (Algebra M)) (ι : Algebra M →ₗ[ℂ] H)
    (hι : ∀ x, ‖ι x‖ = traceTwoNorm τ x) (hιdense : DenseRange ι)
    (hτ : FiniteVectorTrace τ) (Ω : H) (hΩ : ‖Ω‖ = 1)
    (hιΩ : ∀ x : Algebra M, ι x = x.val Ω)
    (J₁ J₂ : H ≃ₗᵢ⋆[ℂ] H) (hJ₁ : Function.Involutive J₁)
    (hM : ∀ x : Algebra M, J₁ (x.val Ω) = (star x).val Ω)
    (hN : ∀ y : Algebra N, J₂ (y.val Ω) = (star y).val Ω)
    (φ : R →⋆ₐ[ℂ] Algebra M)
    (hirr : ∀ a : Algebra M, (∀ r : R, φ r * a = a * φ r) →
      ∃ c : ℂ, a = c • (1 : Algebra M))
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.FiniteVectorTrace