OAI/Analysis/ModularTheory/ScalarCompression.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Compression of the concrete modular representation to scalar functions times the distinguished vector. This constructs the compression and its generator formulas. A trace on the core is not assumed here.

  1. def OAI.WeakPureInfiniteness.modularScalarInclusion line 20
  2. def OAI.WeakPureInfiniteness.modularScalarExtraction line 23
  3. lemma OAI.WeakPureInfiniteness.modularScalarInclusion_ae line 26
  4. lemma OAI.WeakPureInfiniteness.modularScalarExtraction_ae line 30
  5. lemma OAI.WeakPureInfiniteness.modularScalarInclusion_norm line 34
  6. def OAI.WeakPureInfiniteness.modularScalarIsometry line 43
  7. lemma OAI.WeakPureInfiniteness.modularScalarExtraction_adjoint line 47
  8. lemma OAI.WeakPureInfiniteness.modularScalarExtraction_inclusion line 58
  9. def OAI.WeakPureInfiniteness.modularScalarCompression line 66
  10. lemma OAI.WeakPureInfiniteness.modularScalarCompression_one line 70
  11. def OAI.WeakPureInfiniteness.modularScalarCompressionMap line 75
  12. lemma OAI.WeakPureInfiniteness.modularScalarCompressionMap_apply line 80
  13. theorem OAI.WeakPureInfiniteness.modularScalarCompressionMap_cp line 86
  14. theorem OAI.WeakPureInfiniteness.modularScalarCompressionMap_contractive line 89
  15. lemma OAI.WeakPureInfiniteness.modularScalarCompression_coefficient line 96
  16. lemma OAI.WeakPureInfiniteness.modularScalarInclusion_translate line 117
  17. lemma OAI.WeakPureInfiniteness.modularScalarInclusion_right line 128
  18. lemma OAI.WeakPureInfiniteness.modularScalarCompression_translate line 139
  19. lemma OAI.WeakPureInfiniteness.scalarExtraction_right line 150
  20. theorem OAI.WeakPureInfiniteness.modularScalarCompression_commutes line 174

    Source documentation

    Compression of every core operator commutes with the scalar regular representation. This is a statement about the whole von Neumann closure.

    theorem modularScalarCompression_commutes (T : Lp H 2 μ →L[ℂ] Lp H 2 μ)
    (hT : T ∈ modularCrossedProduct μ S) (s : ℝ) :
    Commute (modularScalarCompression μ S T)
      (modularLpTranslateEquiv (H := ℂ) μ s : Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ) := by
…

    Mentions: OAI.WeakPureInfiniteness.modularCrossedProduct, OAI.WeakPureInfiniteness.modularScalarCompression, OAI.WeakPureInfiniteness.modularLpTranslateEquiv