TracialProjectionLifting.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Projection lifting in a tracial ultrapower, using only the scalar spectral rounding estimate. The subsequent trace cutoff uses the strict gap between the desired trace and the coordinate trace bound.

def OAI.KadisonSimilarity.SpectralProjectionRoundingInput line 24
Source documentation
Blackadar, I.6.2.4 and I.9.2.1(iv): bounded Borel functional calculus with the cutoff at 1/2. The scalar estimate is |x - 1_[1/2,∞)(x)| ≤ 2 |x²-x|. This predicate is used only for the fixed finite von Neumann algebra, not for arbitrary C-star algebras.
```
def SpectralProjectionRoundingInput : Prop :=
…
```
theorem OAI.KadisonSimilarity.norm_le_one_of_star_projection line 29
theorem OAI.KadisonSimilarity.exists_projection_representative line 35
Source documentation
Every quotient projection has a representative consisting of actual projections. Rounding is the sole spectral-calculus prerequisite.
```
theorem exists_projection_representative (rounding : SpectralProjectionRoundingInput τ)
    (e : Ultrapower τ h1 ω htr) (he : IsStarProjection e) :
    ∃ p : ℕ →ᵇ A, (∀ i, IsStarProjection (p i)) ∧ quotientHom τ h1 ω htr p = e := by
…
```
Mentions: OAI.KadisonSimilarity.SpectralProjectionRoundingInput

theorem OAI.KadisonSimilarity.exists_projection_representative_trace_le line 72

Source documentation

A strict trace gap permits uniform coordinate bounds after changing a representative on a set outside the ultrafilter.

theorem exists_projection_representative_trace_le
    (rounding : SpectralProjectionRoundingInput τ)
    (e : Ultrapower τ h1 ω htr) (he : IsStarProjection e)
    {s : ℝ} (hs : (quotientTrace τ h1 ω htr e).re < s) :
    ∃ p : ℕ →ᵇ A, (∀ i, IsStarProjection (p i)) ∧
      (∀ i, (τ (p i)).re ≤ s) ∧ quotientHom τ h1 ω htr p = e := by
…

Mentions: OAI.KadisonSimilarity.SpectralProjectionRoundingInput