FiniteProjectionAveraging.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Constructed finite-factor projection averages

theorem OAI.KadisonKastler.ambient_projection_le line 21
Source documentation
The ambient operator order agrees with the algebraic projection order.
```
theorem ambient_projection_le {p q : AlgebraProjection M} (hpq : p ≤ q) :
    p.val.val ≤ q.val.val := by
…
```

theorem OAI.KadisonKastler.exists_average_of_consecutive_matrix_cuts line 28

Source documentation

Consecutive equal-trace matrix cuts give an average within one matrix slot.

theorem exists_average_of_consecutive_matrix_cuts (τ : TracialRepresentation M)
    {n m : ℕ} (hn : 0 < n) (hm : m < n)
    (E : MatrixUnitSystem (Fin n) (Algebra M))
    (ht : ∀ i, τ.trace (E.entry i i) = (((n : ℝ)⁻¹ : ℝ) : ℂ))
    (p : AlgebraProjection M)
    (hlo : matrixDiagonalCut E (Finset.univ.filter (fun i => i.val < m)) ≤ p)
    (hhi : p ≤ matrixDiagonalCut E
      (insert ⟨m, hm⟩ (Finset.univ.filter (fun i => i.val < m)))) :
    ∃ A : FiniteInnerAverage M,
      ‖A.apply p.val.val - (((m : ℝ) / n : ℝ) : ℂ) • (1 : H →L[ℂ] H)‖ ≤ (n : ℝ)⁻¹ := by
…

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

theorem OAI.KadisonKastler.exists_projection_scalar_average_of_trace_lt_one line 70

Source documentation

Every projection of trace below one has scalar finite averages with arbitrarily small error, obtained by rational cuts and inner transport.

theorem exists_projection_scalar_average_of_trace_lt_one (τ : 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) (hp : (τ.trace p.val).re < 1)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ (A : FiniteInnerAverage M) (z : ℂ),
      ‖A.apply p.val.val - z • (1 : H →L[ℂ] H)‖ < ε := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteInnerAverage