SourceCornerQuantization.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Local quantization inside every nonzero corner of the prescribed source.

def OAI.KadisonSimilarity.sourceCornerHom line 20

Source documentation

The original inclusion restricted to matching corners.

def sourceCornerHom (φ : A →⋆ₐ[ℂ] B) (p : A) (hp : IsStarProjection p) :
    Corner p hp →⋆ₐ[ℂ] Corner (φ p) (hp.map φ) where
…

theorem OAI.KadisonSimilarity.sourceCornerHom_coe line 35

theorem OAI.KadisonSimilarity.source_corner_irreducible line 53

Source documentation

Corner irreducibility retains the given source inclusion.

theorem source_corner_irreducible
    (hirr : ∀ c : M.toStarSubalgebra,
      (∀ a : N.toStarSubalgebra, coordinateInclusion hNM a * c =
        c * coordinateInclusion hNM a) → ∃ z : ℂ, c = z • 1)
    (p : N.toStarSubalgebra) (hp : IsStarProjection p) :
    ∀ c : Corner (coordinateInclusion hNM p) (hp.map (coordinateInclusion hNM)),
      (∀ a : Corner p hp, sourceCornerHom (coordinateInclusion hNM) p hp a * c =
        c * sourceCornerHom (coordinateInclusion hNM) p hp a) → ∃ z : ℂ, c = z • 1 := by
…

Mentions: OAI.KadisonSimilarity.sourceCornerHom

theorem OAI.KadisonSimilarity.exists_source_corner_model line 85

Source documentation

The normalized source-corner inclusion has a simultaneous normal model.

theorem exists_source_corner_model (p : N.toStarSubalgebra) (hp : IsStarProjection p)
    (hp0 : p ≠ 0) :
    Nonempty (TracialInclusionModel (sourceCornerHom (coordinateInclusion hNM) p hp)
      (cornerTrace (coordinateInclusion hNM p) (hp.map (coordinateInclusion hNM))
        (vectorPositiveFunctional M υ.vector))) := by
…

Mentions: OAI.KadisonSimilarity.TracialInclusionModel, OAI.KadisonSimilarity.sourceCornerHom, OAI.KadisonSimilarity.vectorPositiveFunctional

theorem OAI.KadisonSimilarity.source_corner_factor line 120

Source documentation

Scalar center of a nonzero source corner.

theorem source_corner_factor
    (hfactor : ∀ c : N.toStarSubalgebra, (∀ a, a * c = c * a) → ∃ z : ℂ, c = z • 1)
    (hdiff : ∀ p : N.toStarSubalgebra, IsStarProjection p → p ≠ 0 →
      ∃ q, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q)
    (p : N.toStarSubalgebra) (hp : IsStarProjection p) (hp0 : p ≠ 0) :
    ∀ c : Corner p hp, (∀ a, a * c = c * a) → ∃ z : ℂ, c = z • 1 := by
…

theorem OAI.KadisonSimilarity.source_corner_diffuse line 142

Source documentation

A nonzero projection in the source corner can be split there.

theorem source_corner_diffuse
    (hdiff : ∀ p : N.toStarSubalgebra, IsStarProjection p → p ≠ 0 →
      ∃ q, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q)
    (p : N.toStarSubalgebra) (hp : IsStarProjection p) :
    ∀ q : Corner p hp, IsStarProjection q → q ≠ 0 →
      ∃ r, IsStarProjection r ∧ r ≠ 0 ∧ r ≠ q ∧ q * r = r ∧ r * q = r := by
…

theorem OAI.KadisonSimilarity.exists_source_corner_compression line 158

Source documentation

Centered coefficients in the normalized corner admit small source projections.

theorem exists_source_corner_compression
    (hfactor : ∀ c : N.toStarSubalgebra, (∀ a, a * c = c * a) → ∃ z : ℂ, c = z • 1)
    (hdiff : ∀ p : N.toStarSubalgebra, IsStarProjection p → p ≠ 0 →
      ∃ q, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q)
    (hirr : ∀ c : M.toStarSubalgebra,
      (∀ a : N.toStarSubalgebra, coordinateInclusion hNM a * c =
        c * coordinateInclusion hNM a) → ∃ z : ℂ, c = z • 1)
    (p : N.toStarSubalgebra) (hp : IsStarProjection p) (hp0 : p ≠ 0)
    {I : Type*} [Fintype I]
    (x : I → Corner (coordinateInclusion hNM p) (hp.map (coordinateInclusion hNM)))
    (hx : ∀ i, cornerTrace (coordinateInclusion hNM p)
      (hp.map (coordinateInclusion hNM)) (vectorPositiveFunctional M υ.vector) (x i) = 0)
…

Mentions: OAI.KadisonSimilarity.vectorPositiveFunctional

theorem OAI.KadisonSimilarity.sourceCorner_compressed_eq line 213

Source documentation

Compression of a centered corner element in the original coordinates.

theorem sourceCorner_compressed_eq (p : N.toStarSubalgebra) (hp : IsStarProjection p)
    (q : Corner p hp) (hq : IsStarProjection q) (x : M.toStarSubalgebra) (c : ℂ) :
    let φ := coordinateInclusion hNM
…

theorem OAI.KadisonSimilarity.exists_source_relative_small_corner line 235

Source documentation

Every nonzero source corner admits relative compression, with the normalization expressed using the original ambient trace.

theorem exists_source_relative_small_corner
    (hfactor : ∀ c : N.toStarSubalgebra, (∀ a, a * c = c * a) → ∃ z : ℂ, c = z • 1)
    (hdiff : ∀ p : N.toStarSubalgebra, IsStarProjection p → p ≠ 0 →
      ∃ q, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q)
    (hirr : ∀ c : M.toStarSubalgebra,
      (∀ a : N.toStarSubalgebra, coordinateInclusion hNM a * c =
        c * coordinateInclusion hNM a) → ∃ z : ℂ, c = z • 1)
    (p : N.toStarSubalgebra) (hp : IsStarProjection p) (hp0 : p ≠ 0)
    {I : Type*} [Fintype I] (x : I → M.toStarSubalgebra)
    {δ η : ℝ} (hδ : 0 < δ) (hη : 0 < η) :
    ∃ q : N.toStarSubalgebra, IsStarProjection q ∧ q ≤ p ∧ q ≠ 0 ∧
      (υ.trace (coordinateInclusion hNM q)).re < η ∧
…