LpTranslation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Translation and covariance for the concrete modular representation on L²(ℝ,H). No property of the von Neumann closure is postulated here.

def OAI.WeakPureInfiniteness.modularLpTranslate line 17
lemma OAI.WeakPureInfiniteness.modularLpTranslate_ae line 21
lemma OAI.WeakPureInfiniteness.modularLpTranslate_comp line 26
lemma OAI.WeakPureInfiniteness.modularLpTranslate_zero line 39
def OAI.WeakPureInfiniteness.modularLpTranslateEquiv line 45
lemma OAI.WeakPureInfiniteness.modularLp_covariance line 56
Source documentation
The regular translation and twisted coefficients obey the actual covariance equation for the spectral modular group.
```
lemma modularLp_covariance (D : BoundedRecovery.RealSpectralCalculus H)
    (t : ℝ) (T : H →L[ℂ] H) (f : Lp H 2 μ) :
    modularLpTranslate μ t
        (modularLpRepresentation μ D T (modularLpTranslate μ (-t) f)) =
      modularLpRepresentation μ D
        (D.unitary t * T * D.unitary (-t)) f := by
…
```
Mentions: OAI.BoundedRecovery.RealSpectralCalculus, OAI.WeakPureInfiniteness.modularLpTranslate, OAI.WeakPureInfiniteness.modularLpRepresentation