ConcreteProjectionComparison.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The exact trace-comparison input used in the corner argument follows from projection comparison in a concrete finite factor.

theorem OAI.KadisonSimilarity.concrete_projection_trace_mono line 19
theorem OAI.KadisonSimilarity.finiteFactorProjectionComparison line 31
Source documentation
In a finite factor, a projection of smaller trace embeds into the larger projection. The partial isometry is constructed by the maximality argument, and faithfulness removes the possible residual.
```
theorem finiteFactorProjectionComparison (τ : TracialRepresentation M)
    (hfactor : ∀ c : M.toStarSubalgebra,
      (∀ a : M.toStarSubalgebra, a * c = c * a) →
        ∃ z : ℂ, c = z • (1 : M.toStarSubalgebra)) :
    FiniteFactorProjectionComparison (fun a : M.toStarSubalgebra => (τ.trace a).re) := by
…
```
Mentions: OAI.KadisonSimilarity.FiniteFactorProjectionComparison