OAI/Probability/InvariantIsing/Spectral/SpectralGroupMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The changed coordinates in an eigenspace carry precisely their fraction of its Haar-averaged squared spin norm.

  1. lemma OAI.InvariantIsing.sum_changed_group_mass_le line 14
  2. lemma OAI.InvariantIsing.abs_weighted_spectral_change_le line 28