FiniteTraceMatrix.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform trace matrices and rational projection brackets

theorem OAI.KadisonKastler.exists_uniform_trace_matrix line 20

Source documentation

A diffuse finite factor contains a full matrix algebra of every positive size, with the prescribed normalized diagonal trace.

theorem exists_uniform_trace_matrix (τ : TracialRepresentation M)
    (hfactor : ∀ c : Algebra M, (∀ a : Algebra M, a * c = c * a) →
      ∃ z : ℂ, c = z • (1 : Algebra M))
    (hdiff : ∀ p : Algebra M, IsStarProjection p → p ≠ 0 →
      ∃ q : Algebra M, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q)
    (n : ℕ) (hn : 0 < n) :
    ∃ E : MatrixUnitSystem (Fin n) (Algebra M),
      ∀ i, τ.trace (E.entry i i) = (((n : ℝ)⁻¹ : ℝ) : ℂ) := by
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.initial_matrix_cut_trace line 38

Source documentation

The initial diagonal cut has exactly the expected rational trace.

theorem initial_matrix_cut_trace (τ : TracialRepresentation M)
    {n m : ℕ} (hm : m ≤ n) (E : MatrixUnitSystem (Fin n) (Algebra M))
    (ht : ∀ i, τ.trace (E.entry i i) = (((n : ℝ)⁻¹ : ℝ) : ℂ)) :
    τ.trace (matrixDiagonalCut E (Finset.univ.filter (fun i => i.val < m))).val =
      (((m : ℝ) / n : ℝ) : ℂ) := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixDiagonalCut

theorem OAI.KadisonKastler.exists_rational_trace_bracket line 47

Source documentation

A nonendpoint trace is bracketed by consecutive rational grid values.

theorem exists_rational_trace_bracket (t : ℝ) (ht : 0 ≤ t) (ht1 : t < 1)
    (n : ℕ) (hn : 0 < n) :
    ∃ m : ℕ, m < n ∧ (m : ℝ) / n ≤ t ∧ t ≤ ((m : ℝ) + 1) / n := by
…

theorem OAI.KadisonKastler.exists_rational_matrix_bracket line 61

Source documentation

After an inner conjugacy, every projection with trace below one lies between two consecutive cuts of an arbitrarily chosen matrix size.

theorem exists_rational_matrix_bracket (τ : TracialRepresentation M)
    (hfactor : ∀ c : Algebra M, (∀ a : Algebra M, a * c = c * a) →
      ∃ z : ℂ, c = z • (1 : Algebra M))
    (hdiff : ∀ p : Algebra M, IsStarProjection p → p ≠ 0 →
      ∃ q : Algebra M, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q)
    (p : AlgebraProjection M) (hp1 : (τ.trace p.val).re < 1)
    (n : ℕ) (hn : 0 < n) :
    ∃ (E : MatrixUnitSystem (Fin n) (Algebra M)) (m : ℕ) (hm : m < n)
      (r : AlgebraProjection M) (u : unitary (Algebra M)),
      (∀ i, τ.trace (E.entry i i) = (((n : ℝ)⁻¹ : ℝ) : ℂ)) ∧
      matrixDiagonalCut E (Finset.univ.filter (fun i => i.val < m)) ≤ r ∧
      r ≤ matrixDiagonalCut E (insert ⟨m, hm⟩ (Finset.univ.filter (fun i => i.val < m))) ∧
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixDiagonalCut