OAI/Analysis/KadisonKastler/RegularCoreMonomials.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Algebraic generation by regular monomials

The core's algebraic generators reduce to finite linear combinations of one original-algebra coefficient followed by one translation. This is the dense algebra used to compute the frequency-window trace.

  1. def OAI.KadisonKastler.regularCoreMonomials line 21
  2. theorem OAI.KadisonKastler.regularCore_generator_mem_monomials line 33
  3. theorem OAI.KadisonKastler.regularCore_generator_star_mem_monomials line 42
  4. theorem OAI.KadisonKastler.regularCore_adjoin_eq_span_monomials line 55