OAI/Analysis/KadisonKastler/ScalarInvariantProjection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A natural positive projection onto shift-invariant scalar functions

The concrete Cesaro construction supplies the limit, its positivity and contractivity. Weak closure of pullback and bounded multiplication then proves naturality and the module identity needed by the boundary mean.

  1. structure OAI.KadisonKastler.ScalarInvariantProjection line 23
  2. theorem OAI.KadisonKastler.exists_scalarInvariantProjection line 34
  3. def OAI.KadisonKastler.scalarInvariantProjection line 50
  4. theorem OAI.KadisonKastler.ScalarInvariantProjection.map_const line 57
  5. theorem OAI.KadisonKastler.ScalarInvariantProjection.natural line 60
  6. theorem OAI.KadisonKastler.ScalarInvariantProjection.module_map line 75