OAI/Analysis/KadisonKastler/ModularStrongLimit.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The strong limit of the regularized modular groups

The weighted estimates make the approximants Cauchy on a dense range. Their contraction bounds extend convergence to every vector. Group laws and inverse operators then pass to the strong limit.

  1. def OAI.KadisonKastler.modularRegularizationScale line 23
  2. theorem OAI.KadisonKastler.modularRegularizationScale_pos line 25
  3. theorem OAI.KadisonKastler.modularRegularizationScale_tendsto line 29
  4. def OAI.KadisonKastler.modularApproximation line 33
  5. theorem OAI.KadisonKastler.modularApproximation_contracts line 37
  6. theorem OAI.KadisonKastler.modularApproximation_cutoff_cauchy line 43
  7. theorem OAI.KadisonKastler.exists_modularStrongLimit line 72
  8. def OAI.KadisonKastler.modularStrongLimit line 85
  9. theorem OAI.KadisonKastler.modularStrongLimit_contracts line 90
  10. theorem OAI.KadisonKastler.modularApproximation_tendsto line 96
  11. theorem OAI.KadisonKastler.modularStrongLimit_zero line 103
  12. theorem OAI.KadisonKastler.modularStrongLimit_add line 116
  13. theorem OAI.KadisonKastler.modularStrongLimit_norm_map line 135
  14. def OAI.KadisonKastler.modularStrongUnitary line 146

    Source documentation

    The limiting group consists of actual unitaries, with inverse at negative time.

    def modularStrongUnitary (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H)
    (hsep : Function.Injective (algebraVectorMap M Ω))
    (hcyc : DenseRange (algebraVectorMap M Ω)) (t : ℝ) : unitary (H →L[ℂ] H) :=
…

    Mentions: OAI.KadisonKastler.algebraVectorMap

  15. theorem OAI.KadisonKastler.modularStrongUnitary_coe line 164
  16. def OAI.KadisonKastler.modularStrongGroup line 170