TracialInclusionQuantization.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Relative local quantization in two abstract von Neumann algebras, through one faithful normal representation of their given inclusion.

theorem OAI.KadisonSimilarity.TracialInclusionModel.source_factor line 24
theorem OAI.KadisonSimilarity.TracialInclusionModel.source_diffuse line 40
theorem OAI.KadisonSimilarity.TracialInclusionModel.source_irreducible line 60

theorem OAI.KadisonSimilarity.TracialInclusionModel.exists_small_source_compression line 81

Source documentation

A centered ambient family has an arbitrarily small compression by a nonzero projection in the original source algebra.

theorem exists_small_source_compression [Nontrivial A]
    (hfactor : ∀ c : A, (∀ a, a * c = c * a) → ∃ z : ℂ, c = z • 1)
    (hdiff : ∀ p : A, IsStarProjection p → p ≠ 0 →
      ∃ q, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q)
    (hirr : ∀ c : B, (∀ a : A, φ a * c = c * φ a) → ∃ z : ℂ, c = z • 1)
    {I : Type*} [Fintype I] (x : I → B) (hx : ∀ i, τ (x i) = 0)
    {δ η : ℝ} (hδ : 0 < δ) (hη : 0 < η) :
    ∃ q : A, IsStarProjection q ∧ q ≠ 0 ∧ (τ (φ q)).re < η ∧
      ∀ i, ‖τ.toPreGNS (φ q * x i * φ q)‖ ^ 2 < δ * (τ (φ q)).re := by
…

theorem OAI.KadisonSimilarity.exists_relative_compression_of_predual line 121

Source documentation

Apply relative quantization directly to the supplied normal traces.

theorem exists_relative_compression_of_predual
    [Nontrivial A]
    {X Y : Type u} [NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X]
    [NormedAddCommGroup Y] [NormedSpace ℂ Y] [CompleteSpace Y]
    (eA : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] A) (eB : StrongDual ℂ Y ≃ₗᵢ⋆[ℂ] B)
    (τA : A →ₚ[ℂ] ℂ) (τB : B →ₚ[ℂ] ℂ)
    (hnA : BoundedHochschild.TraceInPredual eA τA)
    (hnB : BoundedHochschild.TraceInPredual eB τB)
    (h1B : τB 1 = 1) (htrB : ∀ a b, τB (a * b) = τB (b * a))
    (hfB : ∀ a, τB (star a * a) = 0 → a = 0)
    (ψ : A →⋆ₐ[ℂ] B) (hi : Function.Injective ψ)
    (ht : ∀ a, τB (ψ a) = τA a)
…

Mentions: OAI.BoundedHochschild.TraceInPredual