OAI/Analysis/KadisonKastler/RepresentationRowVariance.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exact loss of auxiliary Hilbert-space energy under a normalized row. The formula records the intertwining error of the averaged right operator.

  1. theorem OAI.KadisonKastler.representationRowAverage_variance line 18
  2. theorem OAI.KadisonKastler.representationRowAverage_inputEnergy_le line 45
  3. theorem OAI.KadisonKastler.representationRowAverage_energy_and_defect_le line 63