OAI/Analysis/KadisonKastler/ComplexRowExtraction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Scalar recovery for a complex scalar

Only the real part of the recovered scalar needs to be bounded below. The quadratic forms of a selfadjoint operator are real, so the modulus of the scalar gives the same universal estimate.

  1. theorem OAI.KadisonKastler.WeakOperatorConverges.row_pairing_sub_complex line 23
  2. theorem OAI.KadisonKastler.row_complex_scalar_quadratic_bound line 35