OAI/Analysis/KadisonKastler/OutwardSpectralCuts.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite outward spectral cuts

Negative thresholds take the lower spectral projection, positive thresholds take the upper one. Signed-square coordinates make their integrated vector mass equal to the squared norm of the original finite spectral sum.

  1. def OAI.KadisonKastler.finiteOutwardProjection line 23
  2. theorem OAI.KadisonKastler.finiteOutwardProjection_isProjection line 27
  3. theorem OAI.KadisonKastler.finiteOutwardProjection_sum line 37
  4. theorem OAI.KadisonKastler.finiteSpectralSum_norm_sq line 50
  5. theorem OAI.KadisonKastler.finiteOutwardProjection_mass line 62
  6. theorem OAI.KadisonKastler.finiteOutwardProjection_mass_integrable line 74
  7. theorem OAI.KadisonKastler.finiteOutwardProjection_integral_mass line 82
  8. theorem OAI.KadisonKastler.finiteOutwardProjection_gap_eq line 96
  9. theorem OAI.KadisonKastler.finiteOutwardProjection_integral_gap line 111