OAI/Analysis/KadisonKastler/CharacterContinuity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Continuous character fields in the scalar spectral variable

  1. theorem OAI.KadisonKastler.regularCharacter_apply_eq_fourier_translate line 18
  2. theorem OAI.KadisonKastler.continuous_regularCharacterUnitary line 29
  3. def OAI.KadisonKastler.resolventLogFrequency line 36
  4. theorem OAI.KadisonKastler.resolventLogFrequency_measurable line 38
  5. theorem OAI.KadisonKastler.modularSpectralPhase_eq_character line 41