OAI/Analysis/OperatorAlgebra/TracialCanonicalCornerBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Specialize the finite-tracial corner estimate to canonical L² operator structures while all four operator families remain abstract.

  1. lemma OAI.WeakPureInfiniteness.tracial_canonical_lp_corner_sum_bound line 18