OAI/Analysis/KadisonKastler/ModularPacketSelection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A short spectral interval retaining a strict state inequality

Strong invariance and the packet norm identity allow one Fourier fiber to retain any strict self-adjoint test. This is the local separation step toward the required approximate-eigenstate decomposition, without a disintegration hypothesis or an assumed measure on states.

  1. theorem OAI.KadisonKastler.exists_packet_fiber_gt line 23
  2. theorem OAI.KadisonKastler.ModularSpectralResolution.exists_packet_localized_vector_gt line 44
  3. theorem OAI.KadisonKastler.ModularSpectralResolution.exists_short_spectral_vector_gt line 70