ConcreteHaarDischarge.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The precise diffuse-corner Haar input used by the free-corner argument is supplied by the constructed dyadic unitary.

theorem OAI.KadisonSimilarity.thielDiffuseCornerHaarInput line 20

theorem OAI.KadisonSimilarity.exists_concreteSmallFreeCornerData_of_diffuse line 29

Source documentation

A diffuse concrete source supplies the small corner, containing half projection and Haar unitary with no independent Haar existence premise.

theorem exists_concreteSmallFreeCornerData_of_diffuse
    (τ : TracialRepresentation N)
    (hdiff : ∀ p : N.toStarSubalgebra, IsStarProjection p → p ≠ 0 →
      ∃ q : N.toStarSubalgebra, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧
        p * q = q ∧ q * p = q)
    {I : ℕ → Type*} [∀ j, Fintype (I j)] [∀ j, DecidableEq (I j)]
    [∀ j, Nonempty (I j)]
    (V : N.toStarSubalgebra →ₗ[ℂ] H)
    (M : NestedTracialMatrices (A := I) (concreteTraceLinear τ) V)
…

Mentions: OAI.KadisonSimilarity.NestedTracialMatrices, OAI.KadisonSimilarity.concreteTraceLinear