OAI/Analysis/KadisonKastler/ModularFrequencyBridge.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

From separated modular cuts to actual Fourier defects

The character moves the Fourier cut by one. Conjugating by the two modular gauges then turns its off-diagonal block into multiplication by the product of separated logarithmic spectral projections.

  1. theorem OAI.KadisonKastler.field_norm_bound line 24
  2. theorem OAI.KadisonKastler.field_one_sub line 36
  3. theorem OAI.KadisonKastler.norm_modular_gauge_cut_product_le line 46
  4. theorem OAI.KadisonKastler.frequency_block_factorization line 78
  5. theorem OAI.KadisonKastler.modular_comparison_multiplier line 98
  6. theorem OAI.KadisonKastler.frequencyDefectBound_of_modular_cuts line 130