OAI/Analysis/KadisonKastler/PositiveCornerSquare.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A strictly positive off-diagonal matrix corner

A positive lower bound on the off-diagonal entry gives the two quadratic corner bounds used by the strict diagonal-contraction estimate.

  1. theorem OAI.KadisonKastler.scalar_sq_le_star_mul_of_scalar_le line 18