OAI/Analysis/KadisonKastler/OutwardCutEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Norm-free energy bounds for outward spectral cuts

The upper estimate uses only the two vector norms and their displacement. The lower estimate recovers half of the original displacement energy.

  1. theorem OAI.KadisonKastler.weighted_signedSquare_energy line 18
  2. theorem OAI.KadisonKastler.finiteOutwardProjection_gap_integrable line 58
  3. theorem OAI.KadisonKastler.finiteOutwardProjection_integral_lower line 65
  4. theorem OAI.KadisonKastler.finiteOutwardProjection_integral_upper_sq line 75