OAI/Analysis/KadisonKastler/JointProjectionEnergy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Vector energy in two commuting finite spectral partitions

  1. theorem OAI.KadisonKastler.jointProjection_total line 18
  2. theorem OAI.KadisonKastler.jointProjection_orthogonal line 26
  3. theorem OAI.KadisonKastler.jointProjection_weighted_sum line 44
  4. theorem OAI.KadisonKastler.norm_jointProjection_weighted_sum_sq line 63
  5. theorem OAI.KadisonKastler.jointProjection_gap_energy line 83